070b0fa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some unification/evaluation bug fixes

commit070b0fa6de4a644e1e3e3e1a8e1fd3cac136b447 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 17 Oct 2011, 15:32 (15 years ago) parent180e979

8 files changed+37−20

compare with master

unifiedsplit

lib/builtins.idr+1−1 src/Core/Evaluate.hs+11−6 src/Core/TT.hs+1−1 src/Core/Typecheck.hs+2−1 src/Core/Unify.hs+12−3 src/Idris/AbsSyntax.hs+4−4 src/Idris/ElabDecls.hs+3−2 src/Idris/Error.hs+3−2

lib/builtins.idr+1−1

@@ -10,7 +10,7 @@ getSigVal (Exists a v) = v;

1010id : a -> a;

1111id x = x;

1212

13−fst : (a, b) -> a;

13+fst : (s, t) -> s;

1414fst (x, y) = x;

1515

1616snd : (a, b) -> b;

src/Core/Evaluate.hs+11−6

@@ -33,10 +33,13 @@ instance Show Value where

3333-- while building a proof.

3434

3535normalise :: Context -> Env -> TT Name -> TT Name

36−normalise ctxt env t = quote 0 (eval ctxt env t)

36+normalise ctxt env t = quote 0 (eval ctxt (map finalEntry env) (finalise t))

3737

3838-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

3939

40+finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))

41+finalEntry (n, b) = (n, fmap finalise b)

42+

4043bindEnv :: EnvTT n -> TT n -> TT n

4144bindEnv [] tm = tm

4245bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)

@@ -51,7 +54,7 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

5154

5255eval :: Context -> Env -> TT Name -> Value

5356eval ctxt genv tm = ev [] tm where

54− ev env (P Bound n ty)

57+ ev env (P _ n ty)

5558 | Just (Let t v) <- lookup n genv = ev env v

5659 ev env (P Ref n ty) = case lookupDef n ctxt of

5760 Just (Function (Fun _ _ _ v)) -> v

@@ -63,13 +66,15 @@ eval ctxt genv tm = ev [] tm where

6366 _ -> VP Ref n (ev env ty)

6467 ev env (P nt n ty) = VP nt n (ev env ty)

6568 ev env (V i) | i < length env = env !! i

66− | otherwise = error $ "Internal error: V" ++ show i

69+ | otherwise = VV i --error $ "Internal error: V" ++ show i ++ " "

70+ -- ++ showEnv genv tm ++ "\n" ++ show genv

6771 ev env (Bind n (Let t v) sc)

68− = wknV (-1) $ ev (ev env v : env) sc

72+ = wknV (-1) $ ev (ev env (finalise v) : env) sc

6973 ev env (Bind n (NLet t v) sc)

70− = VBind n (Let (ev env t) (ev env v)) $ (\x -> ev (ev env v : env) sc)

74+ = VBind n (Let (ev env (finalise t)) (ev env (finalise v)))

75+ $ (\x -> ev (ev env v : env) sc)

7176 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

72− where vbind env t = fmap (ev env) t

77+ where vbind env t = fmap (\tm -> ev env (finalise tm)) t

7378 ev env (App f a) = evApply env [ev env a] (ev env f)

7479 ev env (Constant c) = VConstant c

7580 ev env (Set i) = VSet i

src/Core/TT.hs+1−1

@@ -24,7 +24,7 @@ data Option = SetInSet

2424 deriving Eq

2525

2626data Err = Msg String

27− | CantUnify Term Term

27+ | CantUnify Term Term Err

2828 deriving Eq

2929

3030instance Show Err where

src/Core/Typecheck.hs+2−1

@@ -44,7 +44,8 @@ check ctxt env (RApp f a)

4444 case fty' of

4545 Bind x (Pi s) t ->

4646 do converts ctxt env s aty

47− return (App fv av,

47+ return (App fv av,

48+-- normalise ctxt env (subst x av t))

4849 normalise ctxt env (Bind x (Let aty av) t))

4950 t -> fail "Can't apply a non-function type"

5051check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))

src/Core/Unify.hs+12−3

@@ -17,7 +17,7 @@ unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

1717unify ctxt env topx topy

1818 = case un' [] (normalise ctxt env topx) (normalise ctxt env topy) of

1919 OK v -> return v

20− _ -> tfail $ CantUnify topx topy

20+ Error e -> tfail $ CantUnify topx topy e

2121 where

2222 un' bnames (P Bound x _) (P Bound y _)

2323 | (x,y) `elem` bnames = return []

@@ -25,6 +25,10 @@ unify ctxt env topx topy

2525 | holeIn env x = return [(x, tm)]

2626 un' bnames tm (P Bound y _)

2727 | holeIn env y = return [(y, tm)]

28+ un' bnames (V i) (P Bound x _)

29+ | fst (bnames!!i) == x || snd (bnames!!i) == x = return []

30+ un' bnames (P Bound x _) (V i)

31+ | fst (bnames!!i) == x || snd (bnames!!i) == x = return []

2832

2933 un' bnames x@(App _ _) y@(App _ _)

3034 = uApp bnames (unApply x) (unApply y)

@@ -37,7 +41,8 @@ unify ctxt env topx topy

3741 h2 <- un' ((x,y):bnames) sx sy

3842 combine bnames h1 h2

3943 un' bnames x y | x == y = return []

40− | otherwise = fail "Can't unify"

44+ | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y

45+ ++ " " ++ show bnames ++ " " ++ show env

4146

4247 uB bnames (Let tx vx) (Let ty vy)

4348 = do h1 <- un' bnames tx ty

@@ -54,11 +59,14 @@ unify ctxt env topx topy

5459 uB bnames _ _ = fail "Can't unify"

5560

5661 uApp bnames (xp@(P xnt x xty), xargs) (yp@(P ynt y yty), yargs)

57− | (x == y && all okToUnify [xnt, ynt]) ||

62+ | (x == y && all okToUnify [xnt, ynt]) || -- functions x,y are injectice

5863 (holeIn env x && okToUnify ynt) ||

5964 (okToUnify xnt && holeIn env y)

6065 = do h <- un' bnames xp yp

6166 uArgs bnames h xargs yargs

67+ | x == y && xargs == yargs -- only ok if arguments are equal, if functions

68+ -- are not known to be injetive

69+ = return []

6270 uApp bnames (xf, xargs) (yf, yargs)

6371 = do un' bnames xf yf -- ignore result

6472 uArgs bnames [] xargs yargs

@@ -77,6 +85,7 @@ unify ctxt env topx topy

7785 h' <- un' bnames x' y'

7886 next <- combine bnames h h'

7987 uArgs bnames next xs ys

88+ uArgs bnames h _ _ = fail "Can't unify; argument lists different length"

8089

8190 combine bnames as [] = return as

8291 combine bnames as ((n, t) : bs)

src/Idris/AbsSyntax.hs+4−4

@@ -352,13 +352,13 @@ unitDecl = PDatadecl unitTy PSet

352352falseTy = MN 0 "__False"

353353falseDecl = PDatadecl falseTy PSet []

354354

355−pairTy = MN 0 "__Pair"

356−pairCon = MN 0 "__MkPair"

355+pairTy = UN ["Pair"] -- MN 0 "__Pair"

356+pairCon = UN ["MkPair"] -- MN 0 "__MkPair"

357357pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

358358 [(pairCon, PPi Imp (n "A") PSet (

359359 PPi Imp (n "B") PSet (

360360 PPi Exp (n "a") (PRef (n "A")) (

361− PPi Exp (n "b") (PRef (n "B"))

361+ PPi Exp (n "c") (PRef (n "B"))

362362 (PApp (PRef pairTy) [PExp (PRef (n "A")),

363363 PExp (PRef (n "B"))])))))]

364364 where n a = MN 0 a

@@ -451,7 +451,7 @@ addImpl ist ptm = ai [] ptm

451451 PExp tm : insertImpl ps given

452452 insertImpl (PImp n ty : ps) given =

453453 case find n given [] of

454− Just (tm, given') -> PImp n ty : insertImpl ps given'

454+ Just (tm, given') -> PImp n tm : insertImpl ps given'

455455 Nothing -> PImp n Placeholder : insertImpl ps given

456456 insertImpl expected [] = []

457457 insertImpl [] given = given

src/Idris/ElabDecls.hs+3−2

@@ -57,7 +57,7 @@ elabCon info (n, t)

5757 ctxt <- getContext

5858 logLvl 2 $ "Constructor " ++ show n ++ " : " ++ showImp True t

5959 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

60−-- logLvl 2 $ "Rechecking " ++ show t'

60+ logLvl 2 $ "Rechecking " ++ show t'

6161 addDeferred defer

6262 (cty, _) <- tclift $ recheck ctxt [] t'

6363 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

@@ -84,7 +84,7 @@ elabClauses info n_in cs = let n = liftname info n_in in

8484elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

8585elabVal info tm

8686 = do ctxt <- getContext

87− logLvl 10 (show tm)

87+ logLvl 10 (showImp True tm)

8888 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

8989 (build info False (infTerm tm))

9090 logLvl 3 ("Value: " ++ show tm')

@@ -103,6 +103,7 @@ elabClause info (PClause fname lhs rhs whereblock)

103103 let lhs_ty = getInferType lhs'

104104 logLvl 3 (show lhs_tm)

105105 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

106+ logLvl 5 ("Checked " ++ show clhs)

106107 -- Elaborate where block

107108 ist <- getIState

108109 windex <- getName

src/Idris/Error.hs+3−2

@@ -25,8 +25,9 @@ idrisCatch op handler = liftCatch catch op handler

2525

2626pshow :: IState -> Err -> String

2727pshow i (Msg s) = s

28−pshow i (CantUnify x y) = "Can't unify " ++ show (delab i x) ++

29− " with " ++ show (delab i y)

28+pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

29+ ++ " with " ++ show (delab i y)

30+ -- ++ "\n\t(" ++ pshow i e ++ ")"

3031

3132tclift :: Show a => TC a -> Idris a

3233tclift tc = case tc of