Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Unification/evaluation fixes

Ignore-this: 3dda0d38e235f3c514d85ee67bf42c98

darcs-hash:20091201195351-228f4-253f99d07686fc7c3537b6860b287325de9b63d9.gz
  • Loading branch information...
commit 279ddc19977392b3a35162d16800603a958d4822 1 parent 19089d0
eb authored
41 Ivor/Evaluator.lhs
View
@@ -6,11 +6,11 @@
> import Ivor.Gadgets
> import Ivor.Constant
> import Ivor.Nobby
-> import Ivor.Typecheck
> import Debug.Trace
> import Data.Typeable
> import Control.Monad.State
+> import List
data Machine = Machine { term :: (TT Name),
mstack :: [TT Name],
@@ -56,39 +56,44 @@ Code Stack Env Result
> Maybe [Name] -> -- Names not to reduce
> Maybe [(Name, Int)] -> -- Names to reduce a maximum number
> TT Name
-> evaluate open gam tm jns maxns = evalState (eval tm [] [] []) maxns
+> evaluate open gam tm jns maxns = {- trace ("EVALUATING: " ++ show tm) $ -} evalState (eval tm [] [] []) maxns
> where
> eval :: TT Name -> Stack -> SEnv ->
> [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name)
-> eval (P x) xs env pats
+> eval tm stk env pats = {- trace (show (tm, stk, env, pats)) $ -} eval' tm stk env pats
+
+> eval' (P x) xs env pats
> = do mns <- get
> let (use, mns') = usename x jns mns
> put mns'
> case lookup x pats of
> Nothing -> if use then evalP x (lookupval x gam) xs env pats
> else evalP x Nothing xs env pats
-> Just val -> eval val xs env pats
-> eval (V i) xs env pats
+> Just val -> eval val xs env (removep x pats)
+> where removep n [] = []
+> removep n ((x,t):xs) | n==x = removep n xs
+> | otherwise = (x,t):(removep n xs)
+> eval' (V i) xs env pats
> = if (length env>i)
> then eval (getEnv i env) xs env pats
> else unload (V i) xs pats env -- blocked, so unload
-> eval (App f a) xs env pats
+> eval' (App f a) xs env pats
> = do a' <- eval a [] env pats
> eval f (a':xs) env pats
-> eval (Bind n (B Lambda ty) (Sc sc)) xs env pats
+> eval' (Bind n (B Lambda ty) (Sc sc)) xs env pats
> = do ty' <- eval ty [] env pats
> evalScope Lambda n ty' sc xs env pats
-> eval (Bind n (B Pi ty) (Sc sc)) xs env pats
+> eval' (Bind n (B Pi ty) (Sc sc)) xs env pats
> = do ty' <- eval ty [] env pats
> evalScope Pi n ty' sc xs env pats
> -- unload (Bind n (B Pi ty') (Sc sc)) [] pats env
-> eval (Bind n (B (Let val) ty) (Sc sc)) xs env pats
+> eval' (Bind n (B (Let val) ty) (Sc sc)) xs env pats
> = do val' <- eval val [] env pats
> eval sc xs ((n,ty,val'):env) pats
-> eval (Bind n (B bt ty) (Sc sc)) xs env pats
+> eval' (Bind n (B bt ty) (Sc sc)) xs env pats
> = do ty' <- eval ty [] env pats
> unload (Bind n (B bt ty') (Sc sc)) [] pats env
-> eval x stk env pats = unload x stk pats env
+> eval' x stk env pats = unload x stk pats env
> evalP n (Just v) xs env pats
> = case v of
@@ -135,11 +140,23 @@ Code Stack Env Result
> = buildenv xs (subst tm (Sc t))
> -- = buildenv xs (Bind n (B (Let tm) ty) (Sc t))
+> renameRHS pbinds rhs env = rrhs [] [] (nub pbinds) rhs where
+> rrhs namemap pbinds' [] rhs = {-trace ("BEFORE " ++ show (rhs, pbinds, pbinds')) $ -}
+> (pbinds', substNames namemap rhs)
+> rrhs namemap pbinds ((n,t):ns) rhs
+> = let n' = uniqify' (UN (show n)) (map sfst env ++ map fst pbinds ++ map fst ns) in
+> rrhs ((n,P n'):namemap) ((n',t):pbinds) ns rhs
+
+> substNames [] rhs = {-trace ("AFTER " ++ show rhs) $ -} rhs
+> substNames ((n,t):ns) rhs = substNames ns (substName n t (Sc rhs))
+
> pmatch n (PMFun i clauses) xs env pats =
> do cm <- matches clauses xs env pats
> case cm of
> Nothing -> unload (P n) xs pats env
-> Just (rhs, pbinds, stk) -> eval rhs stk env pbinds
+> Just (rhs, pbinds, stk) ->
+> let (pbinds', rhs') = renameRHS pbinds rhs env in
+> eval rhs' stk env pbinds'
> matches [] xs env pats = return Nothing
> matches (c:cs) xs env pats
29 Ivor/TTCore.lhs
View
@@ -941,3 +941,32 @@ Some handy gadgets for Raw terms
> forgetTT (Stage (Escape t _)) = RStage (REscape (forgetTT t))
> forgetTT (Const x) = RConst x
> forgetTT Star = RStar
+
+> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))
+> pToV = pToV2 0
+
+> pToV2 v p (P n) | p==n = Sc (V v)
+> | otherwise = Sc (P n)
+> pToV2 v p (V w) = Sc (V w)
+> pToV2 v p (Con t n i) = Sc (Con t n i)
+> pToV2 v p (TyCon n i) = Sc (TyCon n i)
+> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))
+> where getSc (Sc a) = a
+> pToV2 v p (Elim n) = Sc (Elim n)
+> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)
+> (pToV2 (v+1) p sc))
+> where getSc (Sc a) = a
+> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))
+> (getSc (pToV2 v p a))
+> where getSc (Sc a) = a
+> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))
+> (Comp n (map (getSc.(pToV2 v p)) ts))
+> pToV2 v p (Call (Comp n ts) t) = Sc $ Call
+> (Comp n (map (getSc.(pToV2 v p)) ts))
+> (getSc (pToV2 v p t))
+> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))
+> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))
+> where getSc (Sc a) = a
+> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
+> pToV2 v p (Const x) = Sc (Const x)
+> pToV2 v p Star = Sc Star
44 Ivor/Typecheck.lhs
View
@@ -12,6 +12,7 @@
> import Ivor.Unify
> import Ivor.Constant
> import Ivor.Errors
+> import Ivor.Evaluator
> import Control.Monad.State
> import Data.List
@@ -135,7 +136,7 @@ Handy to pass through all the variables, for tracing purposes when debugging.
> mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) all
> = do -- (s',nms) <- mkSubst xs
> let x' = papp s' x
-> let (Ind y') = normalise gam (Ind (papp s' y))
+> let (Ind y') = eval_nf gam (Ind (papp s' y))
> uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of
> Right uns -> {- trace (show (y', x', uns)) $ -} return uns
> Left err -> {- trace (showeqn all) $ -}
@@ -384,10 +385,10 @@ typechecker...
> case (fnfng,fnf) of
> ((Ind (Bind _ (B Pi s) (Sc t))),_) -> do
> (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
-> let sty = (normaliseEnv env emptyGam (Ind s))
+> let sty = (normaliseEnv env gamma (Ind s))
> let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
> let tmty = (normaliseEnv env emptyGam (Ind tt))
-> checkConvSt env gamma (Ind at) (Ind s)
+> checkConvSt env gamma (Ind at) sty
> return (Ind (App fv av), tmty)
> (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do
> (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
@@ -544,15 +545,17 @@ Insert inferred values into the term
> checkbinder gamma env lvl n (B Lambda t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
> let ttnf = normaliseEnv env gamma (Ind tt)
+> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
> case ttnf of
-> (Ind Star) -> return (B Lambda tv)
-> (Ind (P (MN ("INFER",_)))) -> return (B Lambda tv)
+> (Ind Star) -> return (B Lambda tvnf)
+> (Ind (P (MN ("INFER",_)))) -> return (B Lambda tvnf)
> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B Pi t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
+> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
> -- let ttnf = normaliseEnv env gamma (Ind tt)
> checkConvSt env gamma (Ind tt) (Ind Star)
-> return (B Pi tv)
+> return (B Pi tvnf)
case ttnf of
(Ind Star) -> return (B Pi tv)
@@ -733,35 +736,6 @@ extended environment.
> checkNotHoley i (Proj _ _ t) = checkNotHoley i t
> checkNotHoley _ _ = return ()
-> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))
-> pToV = pToV2 0
-
-> pToV2 v p (P n) | p==n = Sc (V v)
-> | otherwise = Sc (P n)
-> pToV2 v p (V w) = Sc (V w)
-> pToV2 v p (Con t n i) = Sc (Con t n i)
-> pToV2 v p (TyCon n i) = Sc (TyCon n i)
-> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))
-> where getSc (Sc a) = a
-> pToV2 v p (Elim n) = Sc (Elim n)
-> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)
-> (pToV2 (v+1) p sc))
-> where getSc (Sc a) = a
-> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))
-> (getSc (pToV2 v p a))
-> where getSc (Sc a) = a
-> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))
-> (Comp n (map (getSc.(pToV2 v p)) ts))
-> pToV2 v p (Call (Comp n ts) t) = Sc $ Call
-> (Comp n (map (getSc.(pToV2 v p)) ts))
-> (getSc (pToV2 v p t))
-> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))
-> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))
-> where getSc (Sc a) = a
-> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
-> pToV2 v p (Const x) = Sc (Const x)
-> pToV2 v p Star = Sc Star
-
checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name))
If we're paranoid - recheck a supposedly well-typed term. Might want to
18 Ivor/Unify.lhs
View
@@ -5,6 +5,7 @@
> import Ivor.Nobby
> import Ivor.TTCore
> import Ivor.Errors
+> import Ivor.Evaluator
> import Data.List
@@ -43,10 +44,17 @@ Unify on named terms, but normalise using de Bruijn indices.
> case unifynferr i env (p x)
> (p y) of
> (Right x) -> return x
-> _ -> unifynferr i env (p (normalise (gam' gam) x))
-> (p (normalise (gam' gam) y))
-> where p (Ind t) = Ind (makePs t)
+
+> _ -> {- trace (dbgtt x ++ ", " ++ dbgtt y ++"\n") $ -}
+> unifynferr i env (p (eval_nf (gam' gam) x))
+> (p (eval_nf (gam' gam) y))
+
+ _ -> unifynferr i env (p (normalise (gam' gam) x))
+ (p (normalise (gam' gam) y))
+
+> where p (Ind t) = Ind t --(makePs t)
> gam' g = concatGam g (envToGamHACK env)
+> dbgtt (Ind x) = show x -- debugTT x
Make the local environment something that Nobby knows about. Very hacky...
@@ -80,6 +88,10 @@ Collect names which do unify, and ignore errors
> | x == x' = un envl envr scl y acc
> un envl envr y (Bind x (B Lambda ty) (Sc (App scr (P x')))) acc
> | x == x' = un envl envr y scr acc
+> un envl envr (Bind x (B Lambda ty) (Sc (App scl (V 0)))) y acc
+> = un envl envr y scl acc
+> un envl envr y (Bind x (B Lambda ty) (Sc (App scr (V 0)))) acc
+> = un envl envr y scr acc
> un envl envr (P x) t acc | hole envl x = return ((x,t):acc)
> un envl envr t (P x) acc | hole envl x = return ((x,t):acc)
> un envl envr (Bind x b@(B Hole ty) (Sc sc)) t acc
Please sign in to comment.
Something went wrong with that request. Please try again.