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

lib/builtins.idr+1−1

compare with master

unifiedsplit

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

10id : a -> a;

11id x = x;

12

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

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

14fst (x, y) = x;

15

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

src/Core/Evaluate.hs+11−6

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

33-- while building a proof.

34

35normalise :: 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))

37

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

39

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

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

42+

40bindEnv :: EnvTT n -> TT n -> TT n

43bindEnv :: EnvTT n -> TT n -> TT n

41bindEnv [] tm = tm

44bindEnv [] tm = tm

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

45bindEnv ((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

51

54

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

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

53eval ctxt genv tm = ev [] tm where

56eval ctxt genv tm = ev [] tm where

54− ev env (P Bound n ty)

57+ ev env (P _ n ty)

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

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

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

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

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

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

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

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

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

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

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

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

68 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

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

71 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

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

73 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)

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

76 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

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

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

74 ev env (Constant c) = VConstant c

79 ev env (Constant c) = VConstant c

75 ev env (Set i) = VSet i

80 ev env (Set i) = VSet i

src/Core/TT.hs+1−1

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

24 deriving Eq

25

26data Err = Msg String

27− | CantUnify Term Term

27+ | CantUnify Term Term Err

28 deriving Eq

29

30instance Show Err where

src/Core/Typecheck.hs+2−1

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

44 case fty' of

45 Bind x (Pi s) t ->

46 do converts ctxt env s aty

47− return (App fv av,

47+ return (App fv av,

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

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

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

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

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

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

51check 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)]

17unify ctxt env topx topy

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

19 OK v -> return v

20− _ -> tfail $ CantUnify topx topy

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

21 where

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

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

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

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

26 un' bnames tm (P Bound y _)

27 | 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 []

28

32

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

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

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

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

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

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

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

38 combine bnames h1 h2

42 combine bnames h1 h2

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

43 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

41

46

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

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

43 = do h1 <- un' bnames tx ty

48 = do h1 <- un' bnames tx ty

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

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

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

55

60

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

61 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

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

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

59 (okToUnify xnt && holeIn env y)

64 (okToUnify xnt && holeIn env y)

60 = do h <- un' bnames xp yp

65 = do h <- un' bnames xp yp

61 uArgs bnames h xargs yargs

66 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 []

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

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

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

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

64 uArgs bnames [] xargs yargs

72 uArgs bnames [] xargs yargs

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

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

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

78 next <- combine bnames h h'

86 next <- combine bnames h h'

79 uArgs bnames next xs ys

87 uArgs bnames next xs ys

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

80

89

81 combine bnames as [] = return as

90 combine bnames as [] = return as

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

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

src/Idris/AbsSyntax.hs+4−4

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

352falseTy = MN 0 "__False"

353falseDecl = PDatadecl falseTy PSet []

354

355−pairTy = MN 0 "__Pair"

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

356−pairCon = MN 0 "__MkPair"

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

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

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

359 PPi Imp (n "B") PSet (

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

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

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

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

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

364 where n a = MN 0 a

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

451 PExp tm : insertImpl ps given

452 insertImpl (PImp n ty : ps) given =

453 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'

455 Nothing -> PImp n Placeholder : insertImpl ps given

456 insertImpl expected [] = []

457 insertImpl [] given = given

src/Idris/ElabDecls.hs+3−2

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

57 ctxt <- getContext

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

59 ((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'

61 addDeferred defer

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

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

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

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

85elabVal info tm

86 = do ctxt <- getContext

87− logLvl 10 (show tm)

87+ logLvl 10 (showImp True tm)

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

89 (build info False (infTerm tm))

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

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

103 let lhs_ty = getInferType lhs'

104 logLvl 3 (show lhs_tm)

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

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

106 -- Elaborate where block

107 -- Elaborate where block

107 ist <- getIState

108 ist <- getIState

108 windex <- getName

109 windex <- getName

src/Idris/Error.hs+3−2

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

25

26pshow :: IState -> Err -> String

27pshow i (Msg s) = s

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

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

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

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

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

30

31

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

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

32tclift tc = case tc of

33tclift tc = case tc of