mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-21 10:49:33 -06:00
116 lines
3.8 KiB
Haskell
116 lines
3.8 KiB
Haskell
----------------------------------------------------------------------
|
|
-- |
|
|
-- Module : Unify
|
|
-- Maintainer : AR
|
|
-- Stability : (stable)
|
|
-- Portability : (portable)
|
|
--
|
|
-- > CVS $Date: 2005/04/21 16:22:31 $
|
|
-- > CVS $Author: bringert $
|
|
-- > CVS $Revision: 1.4 $
|
|
--
|
|
-- (c) Petri Mäenpää & Aarne Ranta, 1998--2001
|
|
--
|
|
-- brute-force adaptation of the old-GF program AR 21\/12\/2001 ---
|
|
-- the only use is in 'TypeCheck.splitConstraints'
|
|
-----------------------------------------------------------------------------
|
|
|
|
module GF.Grammar.Unify (unifyVal) where
|
|
|
|
import GF.Grammar
|
|
import GF.Data.Operations
|
|
|
|
import GF.Text.Pretty
|
|
import Data.List (partition)
|
|
|
|
unifyVal :: Constraints -> Err (Constraints,MetaSubst)
|
|
unifyVal cs0 = do
|
|
let (cs1,cs2) = partition notSolvable cs0
|
|
let (us,vs) = unzip cs2
|
|
let us' = map val2term us
|
|
let vs' = map val2term vs
|
|
let (ms,cs) = unifyAll (zip us' vs') []
|
|
return (cs1 ++ [(VClos [] t, VClos [] u) | (t,u) <- cs],
|
|
[(m, VClos [] t) | (m,t) <- ms])
|
|
where
|
|
notSolvable (v,w) = case (v,w) of -- don't consider nonempty closures
|
|
(VClos (_:_) _,_) -> True
|
|
(_,VClos (_:_) _) -> True
|
|
_ -> False
|
|
|
|
type Unifier = [(MetaId, Term)]
|
|
type Constrs = [(Term, Term)]
|
|
|
|
unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
|
|
unifyAll [] g = (g, [])
|
|
unifyAll ((a@(s, t)) : l) g =
|
|
let (g1, c) = unifyAll l g
|
|
in case unify s t g1 of
|
|
Ok g2 -> (g2, c)
|
|
_ -> (g1, a : c)
|
|
|
|
unify :: Term -> Term -> Unifier -> Err Unifier
|
|
unify e1 e2 g =
|
|
case (e1, e2) of
|
|
(Meta s, t) -> do
|
|
tg <- subst_all g t
|
|
let sg = maybe e1 id (lookup s g)
|
|
if (sg == Meta s) then extend g s tg else unify sg tg g
|
|
(t, Meta s) -> unify e2 e1 g
|
|
(Q (_,a), Q (_,b)) | (a == b) -> return g ---- qualif?
|
|
(QC (_,a), QC (_,b)) | (a == b)-> return g ----
|
|
(Vr x, Vr y) | (x == y) -> return g
|
|
(Abs _ x b, Abs _ y c) -> do let c' = substTerm [x] [(y,Vr x)] c
|
|
unify b c' g
|
|
(App c a, App d b) -> case unify c d g of
|
|
Ok g1 -> unify a b g1
|
|
_ -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1))
|
|
(RecType xs,RecType ys) | xs == ys -> return g
|
|
_ -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1))
|
|
|
|
extend :: Unifier -> MetaId -> Term -> Err Unifier
|
|
extend g s t | (t == Meta s) = return g
|
|
| occCheck s t = Bad (render ("occurs check" <+> ppTerm Unqualified 0 t))
|
|
| True = return ((s, t) : g)
|
|
|
|
subst_all :: Unifier -> Term -> Err Term
|
|
subst_all s u =
|
|
case (s,u) of
|
|
([], t) -> return t
|
|
(a : l, t) -> do
|
|
t' <- (subst_all l t) --- successive substs - why ?
|
|
return $ substMetas [a] t'
|
|
|
|
substMetas :: [(MetaId,Term)] -> Term -> Term
|
|
substMetas subst trm = case trm of
|
|
Meta x -> case lookup x subst of
|
|
Just t -> t
|
|
_ -> trm
|
|
_ -> composSafeOp (substMetas subst) trm
|
|
|
|
substTerm :: [Ident] -> Substitution -> Term -> Term
|
|
substTerm ss g c = case c of
|
|
Vr x -> maybe c id $ lookup x g
|
|
App f a -> App (substTerm ss g f) (substTerm ss g a)
|
|
Abs b x t -> let y = mkFreshVarX ss x in
|
|
Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
|
|
Prod b x a t -> let y = mkFreshVarX ss x in
|
|
Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
|
|
_ -> c
|
|
|
|
occCheck :: MetaId -> Term -> Bool
|
|
occCheck s u = case u of
|
|
Meta v -> s == v
|
|
App c a -> occCheck s c || occCheck s a
|
|
Abs _ x b -> occCheck s b
|
|
_ -> False
|
|
|
|
val2term :: Val -> Term
|
|
val2term v = case v of
|
|
VClos g e -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e
|
|
VApp f c -> App (val2term f) (val2term c)
|
|
VCn c -> Q c
|
|
VGen i x -> Vr x
|
|
VRecType xs -> RecType (map (\(l,v) -> (l,val2term v)) xs)
|
|
VType -> typeType
|