{-# LANGUAGE PatternGuards #-}
-- | A model of the evaluation of logic programs (i.e., resolving Horn clauses)
--
-- The point is not to re-implement Prolog with all the conveniences
-- but to formalize evaluation strategies such as SLD, SLD-interleaving, 
-- and others.
-- The formalization is aimed at reasoning about termination and
-- solution sequences. See App A and B of the full FLOPS 2008 paper 
-- (the file arithm.pdf in this directory).
--
module Language.DefinitionTree where

import Data.Map
import Prelude hiding (lookup)

-- | A logic var is represented by a pair of an integer
-- and a list of `predicate marks' (which are themselves
-- integers). Such an odd representation is needed to
-- ensure the standardization apart: different instances
-- of a clause must have distinctly renamed variables.
-- Unlike Claessen, we get by without the state monad
-- to generate unique variable names (labels). See the
-- discussion and examples in the `tests' section below.
-- Our main advantage is that we separate the naming of
-- variables from the evaluation strategy. Evaluation
-- no longer cares about generating fresh names, which
-- notably simplifies the analysis of the strategies.
-- Logic vars are typed, albeit phantomly.
type VStack = [Int]
type LogicVar term = (Int,VStack)

-- | A finite map from vars to terms (parameterized over the domain of terms)
type Subst term = Map (LogicVar term) term


-- | Formulas 
--
-- A formula describes a finite or _infinite_ AND-OR tree
-- that encodes the logic-program clauses that may be needed to
-- evaluate a particular goal.
-- We represent a goal g(t1,...,tn) by a combination of the goal
-- g(X1,...,Xn), whose arguments are distinct fresh logic
-- variables, and a substitution {Xi=ti}. For a goal
-- g(X1,...,Xn), a |Formula| encodes all the clauses of the
-- logic program that could possibly prove g, in their order. Each
-- clause 
--
-- > g(t1,...,tn) :- b1(t11,...,t1m), ...
--
-- is represented by the (guarding) substitution {Xi=ti, Ykj=tkj}
-- and the sequence of the goals bk(Yk1,...,Ykm) in the body. 
-- Each of these goals is again encoded as a |Formula|. 
-- All variables in the clauses are renamed to ensure the standardization apart.
--
-- Our trees are similar to Antoy's definitional trees, used to encode
-- rewriting rules and represent control strategies in
-- term-rewriting systems and _functional logic_ programming.
-- However, in definitional trees, function calls can be nested, 
-- and patterns are linear.
--
-- The translation from Prolog is straightforward; the first step
-- is to re-write clauses so that the arguments of each goal are 
-- logic variables:
-- A fact 
--
-- >    g(term).
--
-- is converted to
--
-- >    g(X) :- X = term.
--
-- A clause
--
-- >    g(term) :- g1(term1), g2(term2).
--
-- is converted to
--
-- >    g(X) :- X = term, _V1 = term1, g1(_V1), _V2=term2, g2(_V2).
--
-- See the real examples at the end
--
-- A formula (parameterized by the domain of terms) is an OR-sequence
-- of clauses
data Formula term = Fail | (Clause term) :+: (Formula term)

-- | A clause is a guarded body; the latter is an AND-sequence of formulas
data Clause term = G (Subst term) (Body term)

data Body term   = Fact  | (Formula term) :*: (Body term)

infixr 6 :+:
infix  7 `G`
infixr 8 :*:

--             Evaluation of formulas

-- | The evaluation process starts with a formula and the initial
-- substitution, which together represent a goal.  The
-- guarding substitution of the clause conjoins with the current
-- substitution to yield the substitution for the evaluation of the body. 
-- The conjunction of substitutions may lead to a contradiction, 
-- in which case the clause is skipped (`pruned').
--
-- Evaluation as pruning: we traverse a tree and prune away failed branches
prune :: Unifiable term => Formula term -> Subst term -> Formula term
prune Fail _ = Fail
prune (cl :+: f2) s = case prunec cl s of
                       Nothing -> prune f2 s
                       Just cl -> cl :+: prune f2 s

prunec :: Unifiable term => Clause term -> Subst term -> Maybe (Clause term)
prunec (G s' b) s  = case unify s s' of
                      Nothing -> Nothing
                      Just s  -> case pruneb b s of
                                  Nothing -> Nothing
                                  Just b -> Just $ G s b
pruneb Fact s = Just Fact
pruneb (f :*: b) s  = case prune f s of
                       Fail -> Nothing
                       f    -> case pruneb b s of
                               Nothing -> Nothing
                               Just b  -> Just $ f :*: b

-- one may also try to push disjunctions up using distributivity...


-- | A different evaluator: Evaluate a tree to a stream (lazy list)
-- given the initial substitution s.
-- Here we use the SLD strategy.
eval :: Unifiable term => Formula term -> Subst term -> [Subst term]
eval Fail _ = []
eval  (cl :+: f2) s = evalc cl s ++ eval f2 s
evalc (G s' b) s    = maybe [] (evalb b) $ unify s s'
evalb Fact s        = [s]
evalb (f :*: b) s   = concatMap (evalb b) (eval f s) 

-- | Same as above, using the SLD-interleaving strategy.
-- See Definition 3.1 of the LogicT paper (ICFP05)
evali :: Unifiable term => Formula term -> Subst term -> [Subst term]
evali Fail _        = []
evali (cl :+: f2) s = evalic cl s `interleave` evali f2 s
evalic (G s' b) s   = maybe [] (evalib b) $ unify s s'
evalib Fact s       = [s]
evalib (f :*: b) s  = fairConcatMap (evalib b) (evali f s)
  where fairConcatMap k [] = []
        fairConcatMap k (a:m) = interleave (k a) (fairConcatMap k m)

interleave [] m = m
interleave (a:m1) m2 = a : (interleave m2 m1)

--              Terms and substitutions

-- | Evaluation, substitutions and unification are parametric over terms
-- (term algebra), provided the following two operations are defined.
-- We should be able to examine a term and determine if it is a variable
-- or a constructor (represented by an integer) applied to a sequence of
-- zero or more terms. Conversely, given a constructor (represented by an
-- integer) and a list of terms-children we should be able to build a term.
-- The two operations must satisfy the laws:
--
-- > either id build . classify === id
-- > classify . build === Right
--
class Unifiable term where
    classify :: term -> Either (LogicVar term) (Int,[term])
    build    :: (Int,[term]) -> term

-- | building substitutions
bv :: LogicVar term -> term -> Subst term
bv x = singleton x

ins :: Subst term -> (LogicVar term, term) -> Subst term
ins m (v,t) = insert v t m

-- | Apply a substitution to a term
sapp :: Unifiable term => Subst term -> term -> term
sapp s t = either dov donv $ classify t
 where dov v          = maybe t id $ lookup v s -- term is a variable
       donv (ctr, ts) = build (ctr, Prelude.map (sapp s) ts) -- non-var term


-- | Conjoin two substitutions (see Defn 1 of the FLOPS 2008 paper).
-- We merge two substitutions and solve the resulting set of equations, 
-- returning Nothing if the two original substitutions are contradictory.
unify :: Unifiable term => Subst term -> Subst term -> Maybe (Subst term)
unify s1 s2 = solve empty $ foldWithKey fld (foldWithKey fld [] s1) s2 
  where
  fld v t l = (Left v,t) : l

-- | Solve the equations using the naive realization of the 
-- Martelli and Montanari process
solve :: Unifiable term => Subst term -> 
         [(Either (LogicVar term) term,term)] -> 
         Maybe (Subst term)
solve s [] = Just s
solve s ((Left v,t):r) = either dov donv $ classify t
  where dov v' = if v == v' then solve s r else add'cont
        donv _ = add'cont -- skip the occurs check
        s' = insert v t s
        add'cont = solve s' (Prelude.map (sapp'eq s') r)
        sapp'eq s (Left v,t) = (maybe (Left v) Right $ lookup v s, sapp s t)
        sapp'eq s (Right t1,t2) = (Right $ sapp s t1, sapp s t2)
solve s ((Right t1,t2):r) = 
  case (classify t1, classify t2) of
    (Left v,_) -> solve s $ (Left v,t2):r
    (_,Left v) -> solve s $ (Left v,t1):r
    (Right (ctr1,ts1),Right (ctr2,ts2)) 
        | ctr1 == ctr2, length ts1 == length ts2 ->
            solve s $ (zipWith (\x y -> (Right x,y)) ts1 ts2) ++ r
    _ -> Nothing



--              Tests and examples

-- | Unary numerals
--
data UN = UNv (LogicVar UN)
        | UZ
        | US UN 
          deriving (Eq, Show)

-- | Constructor UZ is represented by 0, and US is represented by 1
instance Unifiable UN where
    classify (UNv v) = Left v
    classify UZ      = Right (0,[])
    classify (US n)  = Right (1,[n])

    build (0,[])  = UZ
    build (1,[n]) = US n


-- | Encoding of variable names to ensure standardization apart.
-- A clause such as genu(X) or add(X,Y,Z) may appear in the tree
-- (infinitely) many times. We must ensure that each instance uses distinct
-- logic variables. To this end, we name variables by a pair (Int, VStack)
-- whose first component is the local label of a variable within a clause.
-- VStack is a path from the root of the tree to the current occurrence
-- of the clause in the tree. Each predicate along the path is represented
-- by an integer label (0 for genu, 1 for add, 2 for mul, etc). 
-- To `pass' arguments to a clause, we add to the current substitution
-- the bindings for the variables of that clause. See the genu' example
-- below: whereas (0,h) is the label of the variable X in the current
-- instance of genu, (0,genu_mark:h) is X in the callee.
--
-- A logic program
--
-- > genu([]).
-- > genu([u|X]) :- genu(X).
--
-- and the goal genu(X) are encoded as follows. The argument of genu' is
-- the path of the current instance of genu' from the top of the AND-OR
-- tree.
--
genu :: Formula UN
genu = genu' []
 where
 genu' h = (bv x UZ) `G` Fact :+: 
           (bv x (US (UNv x'))) `G` (genu' h') :*: Fact :+:
           Fail
   where x = (0,h)
         h' = genu_mark:h
         x' = (0,h')
         genu_mark = 0

test1 = take 5 (eval genu empty)
{-
*SLD> test1
  [fromList [((0,[]),UZ)],
   fromList [((0,[]),US UZ),((0,[0]),UZ)],
   fromList [((0,[]),US (US UZ)),((0,[0]),US UZ),((0,[0,0]),UZ)],
   fromList [((0,[]),US (US (US UZ))),((0,[0]),US (US UZ)),
             ((0,[0,0]),US UZ),((0,[0,0,0]),UZ)],
   fromList [((0,[]),US (US (US (US UZ)))),((0,[0]),US (US (US UZ))),
             ((0,[0,0]),US (US UZ)),((0,[0,0,0]),US UZ),((0,[0,0,0,0]),UZ)]]
-}


-- A logic program with the goal add(X,Y,Z)
--  add([],X,X).
--  add([u|X],Y,[u|Z]) :- add(X,Y,Z).
-- is encoded as follows. The labels of local variables are:
-- X is 0, Y is 1, Z is 2. 

add :: VStack -> Formula UN
add h = (bv x UZ) `ins` (y,(UNv z)) `G` Fact :+:
        (bv x (US (UNv x'))) `ins` (y,UNv y') `ins` (z,US (UNv z'))
            `G` add h' :*: Fact :+:
        Fail
  where
   [x,y,z]    = Prelude.map (\n->(n,h)) [0..2]  -- vars in the current call
   h' = add_mark:h
   [x',y',z'] = Prelude.map (\n->(n,h')) [0..2] -- vars in the recursive call
add_mark = 1

test2 = take 3 (eval (add []) empty)

{-
*SLD> test2
  [fromList [((0,[]),UZ),((1,[]),UNv (2,[]))],
   fromList [((0,[]),US UZ),((0,[1]),UZ),((1,[]),UNv (2,[1])),
             ((1,[1]),UNv (2,[1])),((2,[]),US (UNv (2,[1])))],
   fromList [((0,[]),US (US UZ)),((0,[1]),US UZ),((0,[1,1]),UZ),
             ((1,[]),UNv (2,[1,1])),((1,[1]),UNv (2,[1,1])),
             ((1,[1,1]),UNv (2,[1,1])),((2,[]),US (US (UNv (2,[1,1])))),
             ((2,[1]),US (UNv (2,[1,1])))]]

Note that (0,[]) is the top-level X, (1,[]) is teh top-level Y,
(2,[]) is the top-level Z. In the more concise notation, the above
list of substitution reads:
  [(X,0), (Y,Z)]
  [(X,1), (Y,Z'), (Z, succ(Z'))]
  [(X,2), (Y,Z''), (Z,succ (succ (Z'')))]
-}

test3 = take 3 (evali (add []) empty)
-- the same as test2

-- A logic program with the goal mul(X,Y,Z) (Sec 2.3 of the FLOPS paper)
--  mul([],_,[]).
--  mul([u|_],[],[]).
--  mul([u|X],[u|Y],Z) :- add([u|Y],Z1,Z), mul(X,[u|Y],Z1).
-- is converted into
--  mul(X,Y,Z) :- X=[], Z=[].
--  mul(X,Y,Z) :- X=[u|X1], Y=[], Z=[].
--  mul(X,Y,Z) :- X=[u|X1], Y=[u|Y1], 
--                AddX=Y,  AddY=Z1, AddZ=Z,
--                MulX=X1, MulY=Y,  MulZ=Z1, 
--                add(AddX,AddY,AddZ), mul(MulX,MulY,MulZ).

-- is encoded as follows. The labels of local variables are:
-- X is 0, Y is 1, Z is 2.

mul :: VStack -> Formula UN
mul h = (bv x UZ) `ins` (z,UZ) `G` Fact :+:

        (bv x (US (UNv x1))) `ins` (y,UZ) `ins` (z,UZ) `G` Fact :+:

        (bv x (US (UNv x1))) `ins` (y,US (UNv y1)) `ins`
        (addx,(UNv y)) `ins` (addy,(UNv z1)) `ins` (addz,(UNv z)) `ins`
        (mulx,(UNv x1)) `ins` (muly,(UNv y)) `ins` (mulz,(UNv z1))
        `G` add h'add :*: mul h'mul :*: Fact :+:
      Fail
  where
   [x,y,z,x1,y1,z1] = Prelude.map (\n->(n,h)) [0..5]
   h'add = add_mark:h -- frame for the call to add
   h'mul = mul_mark:h -- frame for the recursive call to mul
   [addx,addy,addz] = Prelude.map (\n->(n,h'add)) [0..2]
   [mulx,muly,mulz] = Prelude.map (\n->(n,h'mul)) [0..2]
mul_mark = 2

test4 = take 6 . Prelude.map proj_xyz $ (eval (mul []) empty)
test5 = take 8 . Prelude.map proj_xyz $ (evali (mul []) empty)

proj_xyz s = (pv 0, pv 1, pv 2)
 where
 pv n = maybe (UNv (n,[])) chase $ lookup (n,[]) s
 chase t = let t' = sapp s t in if t == t' then t else chase t'

{-
*SLD> test4
  [(UZ,UNv (1,[]),UZ),
   (US (UNv (3,[])),UZ,UZ),
   (US UZ,US UZ,US UZ),
   (US (US UZ),US UZ,US (US UZ)),
   (US (US (US UZ)),US UZ,US (US (US UZ))),
   (US (US (US (US UZ))),US UZ,US (US (US (US UZ))))]

This result matches the one mentioned on p10 of the paper (mul for SLD
without interleaving). In each solution except the first two, Y is 1.

For interleaving, the picture is different:

*SLD> test5
  [(UZ,UNv (1,[]),UZ),
   (US (UNv (3,[])),UZ,UZ),
   (US UZ,US UZ,US UZ),                     -- (1,1,1)
   (US UZ,US (US UZ),US (US UZ)),           -- (1,2,2)
   (US (US UZ),US UZ,US (US UZ)),           -- (2,1,1)
   (US UZ,US (US (US UZ)),US (US (US UZ))), -- (1,3,3)
   (US (US (US UZ)),US UZ,US (US (US UZ))), -- (3,1,3)
   (US (US UZ),US (US UZ),US (US (US (US UZ))))] -- (2,2,4)
-}