Permalink
Browse files

Tinker with unification

Ignore-this: 67d67602f23f4f98716b3a51b260bd1

darcs-hash:20100212113838-228f4-fb5a49ec9be06837a9ec1c4ab4a465b356031183.gz
  • Loading branch information...
eb
eb committed Feb 12, 2010
1 parent 30d8790 commit 79e8c5b059223281d79af5ee19ba39b2591ef5f0
Showing with 25 additions and 12 deletions.
  1. +10 −1 Ivor/Evaluator.lhs
  2. +2 −1 Ivor/Tactics.lhs
  3. +6 −5 Ivor/Typecheck.lhs
  4. +7 −5 Ivor/Unify.lhs
View
@@ -1,6 +1,7 @@
> {-# OPTIONS_GHC -fglasgow-exts #-}
-> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit,
+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_env,
+> eval_nf_without, eval_nf_limit,
> eval_nfEnv, tidyNames) where
> import Ivor.TTCore
@@ -26,6 +27,14 @@
> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing)
> in finalise (Ind res)
+> eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
+> eval_nf_env env g t
+> = eval_nf (addenv env g) t
+> where addenv [] g = g
+> addenv ((n,B (Let v) ty):xs) (Gam g)
+> = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))
+> addenv (_:xs) g = addenv xs g
+
> eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name
> eval_nf_without gam tm [] = eval_nf gam tm
> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing)
View
@@ -3,6 +3,7 @@
> import Ivor.TTCore
> import Ivor.Typecheck
> import Ivor.Nobby
+> import Ivor.Evaluator
> import Ivor.Gadgets
> import Ivor.Unify
> import Ivor.Errors
@@ -399,7 +400,7 @@ Normalise the goal
> evalGoal :: Tactic
> evalGoal gam env (Ind (Bind x (B Hole ty) sc)) =
-> do let (Ind nty) = normaliseEnv (ptovenv env) gam (finalise (Ind ty))
+> do let (Ind nty) = eval_nf_env (ptovenv env) gam (finalise (Ind ty))
> tacret $ Ind (Bind x (B Hole nty) sc)
> evalGoal _ _ (Ind (Bind x _ _)) = fail $ "evalGoal: " ++ show x ++ " Not a hole"
> evalGoal _ _ _ = fail "evalGoal: Can't happen"
View
@@ -119,7 +119,7 @@ constraints and applying it to the term and type.
> -- constraints in and they might depend on each other...
> do let cs = nub constraints
> (subst, nms) <- mkSubst $ (map (\x -> (True,x)) cs) ++
-> (map (\x -> (False,x)) (reverse cs))
+> (map (\x -> (False,x)) cs)
> let tm' = papp subst tm
> let ty' = papp subst ty
> return (Ind tm',Ind ty')
@@ -140,7 +140,7 @@ Handy to pass through all the variables, for tracing purposes when debugging.
> let x' = papp s' x
> 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
+> Right uns -> return uns
> Left err -> {- trace (showeqn all) $ -}
> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
@@ -403,11 +403,12 @@ typechecker...
> let tt' = (normaliseEnv env gamma (Ind tt))
> return (Ind (App fv av), (normaliseEnv env gamma (Ind tt)))
> _ -> fail $ "Cannot apply a non function type " ++ show ft ++ " to " ++ show a
-> return (rv,rt)
+> -- return (rv,rt)
> case exp of
> Nothing -> return (rv,rt)
-> Just expt -> do checkConvSt env gamma rt expt
-> return (rv,rt)
+> Just expt -> -- trace ("Checking " ++ show (rv, rt, expt)) $
+> do checkConvSt env gamma rt expt
+> return (rv,rt)
> tc env lvl (RConst x) _ = lift $ tcConst x
> tc env lvl RStar _ = return (Ind Star, Ind Star)
> tc env lvl (RFileLoc f l t) exp =
View
@@ -115,11 +115,13 @@ Collect names which do unify, and ignore errors
> else ifail $ ICantUnify (Ind x) (Ind y)
> where funify (P x) (P y)
> | x==y = True
-> | otherwise = hole envl x || hole envl y
-> funify (Con _ _ _) (P x) = hole envr x
-> funify (P x) (Con _ _ _) = hole envl x
-> funify (TyCon _ _) (P x) = hole envr x
-> funify (P x) (TyCon _ _) = hole envl x
+> | otherwise = False -- hole envl x || hole envl y
+> funify (Con _ _ _) (P x) = False -- hole envr x
+> funify (P x) (Con _ _ _) = False -- hole envl x
+> funify (TyCon _ _) (P x) = False -- hole envr x
+> funify (P x) (TyCon _ _) = False -- hole envl x
+> funify (P x) (App _ _) = False
+> funify (App _ _) (P x) = False
> funify _ _ = True -- unify normally
> un envl envr (Proj _ i t) (Proj _ i' t') acc
> | i == i' = un envl envr t t' acc

0 comments on commit 79e8c5b

Please sign in to comment.