> module QuicQuid.Logic (
>              unify1,substitute,Binding
> ) where

> import Data.Maybe
> import qualified Data.Map as M
> import QuicQuid.Term 

A logic layer built on top of the 'Term' syntax.

Logic predicates are expressed as Term's "applications": <pred> <obj>.

For example: friend(john,mike). 

Two terms have special meaning: "and [..]" "or[..]". 

TODO:
* Support variables parameter to specificy timeouts/max number of answers...
For example: ? {name:varname,maxAnswer:10,timeoutMs:1000}

* Support unification with "not care" variables (that match but do no return bindings).
Note, in F-Logic:
Anonymous and don’t care variables: Variables of the form ?_ or ? are called anonymous
variable. They are used whenever a unique new variable is needed. In particular, two different
occurrences of ?_ or ? in the same clause are treated as different variables. Named variables
that start with an underscore, e.g., ?_foo, are called don’t care variables. Unlike anonymous
variables, two different occurrences of such a variable in the same clause refer to the same
variable.

> -- |The type of the unification's result.
> type Binding = M.Map String Term 

> -- |Unify a pattern with a term, if successful returns a binding otherwise return Nothing.
> unify1 :: Term -- ^The pattern 
>        -> Term -- ^The term to unify to
>        -> Maybe Binding
> unify1 = unify M.empty


For the purpose of unification,some terms are assumed to have an internal/equivalent structure:
* [a,b..] is assumed to be equivalent to {1:a,2:b...} (BUG: unimplemented)
* v("n") == ?n
* values of simple types like numbers also match <type>(".."), e.g: 33 == number("33") (BUG: unimplemented)

> unify :: Binding -> Term -> Term -> Maybe Binding
> unify sub (App (Str "variable") t) (Var x)  = unify sub t (Str x)
> unify sub (App h1 t1)  (App h2 t2)   = unify sub h1 h2 >>= \s2 -> unify s2 t1 t2
> unify sub (Arr ts1) (Arr ts2)        = unifyN sub (ts1) (ts2)
> unify sub (Obj m1)  (Obj m2)         = unifyMaps m1 m2 sub
> unify sub (Var v)      t2            = maybe (Just $ M.insert v t2 sub) (\a -> unify sub a t2) (M.lookup v sub)
> unify sub t1 t2             | t1==t2 = Just sub
> unify _   t1 t2                      = Nothing

> unifyStr sub s1 s2 = if s1 == s2 then Just sub else Nothing

 unifyMaps :: M.Map Term Term -> M.Map Term Term -> Binding -> Maybe Binding

> unifyMaps m1 m2 sub = if M.size m1 /= M.size m2 then Nothing else unifyM (M.toList m1) (M.toList m2) sub

 unifyM :: [(Term, Term)] -> [(Term, Term)] -> Binding -> Maybe Binding

> unifyM []      ts sub = Just sub
> unifyM (p1:ps) ts sub = let r= unify1toN p1 ts sub;Just (sub2,rs) = r in if isNothing r then Nothing else unifyM ps rs sub2  

> -- |Unify a couple of terms with the first of a set of terms that matches it and returns the resulting binding and the unmatched terms. 

 unify1toN :: (Term, Term) -> [(Term, Term)] -> Binding -> Maybe (Binding,[(Term, Term)])

> unify1toN  e es sub = unify1toN0 e es [] sub

> unify1toN0    (k,v) []              rs sub = Nothing
> unify1toN0 e@(k,v)  (e2@(k2,v2):vs) rs sub = let r = unifyStr sub k k2 >>= \s2 -> unify s2 v v2 in if isJust r then Just (fromJust r,rs ++ vs) else unify1toN0 e vs (rs++[e2]) sub  

> -- |Unify the corresponding terms from two lists: 
> -- unifyN bindings [a1,a2..] [b1,b2..]  ==  { {bindings} a1 match b1} a2 match b2} a3 ... 
> unifyN sub ts1 ts2 = if length ts1 /= length ts2 then Nothing else foldl (\msub (t1,t2) -> maybe Nothing (\s->unify s t1 t2) msub) (Just sub) $ zip ts1 ts2 

> -- |Substitute a set of bindings in a term 
> substitute :: Binding -> Term -> Term
> substitute bindings   (App h t) = App (substitute bindings h) (substitute bindings t)
> -- TODO: check prob: {x=a,y=a} [?x:c ?y:d] -> ??
> substitute bindings   (Obj m)   = Obj (M.fromList (map (\(k,v) -> (k,substitute bindings v)) $ M.toList m)) 
> substitute bindings   (Arr ts)  = Arr (map (substitute bindings) ts)
> substitute bindings t@(Var v)   = let ma = M.lookup v bindings in maybe t id ma 
> substitute bindings t@(Str s)   = t

> -- |True if is a "don't care" variable.
> isDontCare (Var ('_':_)) = True
> isDontCare _ = False