7b1336b · Idris-dev · git.iko.soy

lib/builtins.idr+3

compare with master

unifiedsplit

@@ -11,6 +11,9 @@ getSigVal (Exists a v) = v;

11replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;

12replace refl prf = prf;

13

14+sym : {x:a} -> {y:a} -> x = y -> y = x;

15+sym refl = refl;

16+

14lazy : a -> a;

17lazy : a -> a;

15lazy x = x; -- compiled specially

18lazy x = x; -- compiled specially

16

19

src/Core/Evaluate.hs+7−2

@@ -1,7 +1,7 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2 PatternGuards #-}

3

4−module Core.Evaluate(normalise, specialise, hnf,

4+module Core.Evaluate(normalise, normaliseC, specialise, hnf,

5 Fun(..), Def(..), Context,

6 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

7 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

@@ -51,6 +51,11 @@ instance Show (a -> b) where

51-- i.e. it's an intermediate environment that we have while type checking or

52-- while building a proof.

53

54+normaliseC :: Context -> Env -> TT Name -> TT Name

55+normaliseC ctxt env t

56+ = evalState (do val <- eval ctxt emptyContext env t []

57+ quote 0 val) ()

58+

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

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

55normalise ctxt env t

60normalise ctxt env t

56 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []

61 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []

@@ -103,7 +108,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

103 ev top env (V i) | i < length env = return $ env !! i

108 ev top env (V i) | i < length env = return $ env !! i

104 | otherwise = return $ VV i

109 | otherwise = return $ VV i

105 ev top env (Bind n (Let t v) sc)

110 ev top env (Bind n (Let t v) sc)

106− = do v' <- ev top env (finalise v)

111+ = do v' <- ev top env v --(finalise v)

107 sc' <- ev top (v' : env) sc

112 sc' <- ev top (v' : env) sc

108 wknV (-1) sc'

113 wknV (-1) sc'

109 ev top env (Bind n (NLet t v) sc)

114 ev top env (Bind n (NLet t v) sc)

src/Core/ProofState.hs+5−5

@@ -288,11 +288,11 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

288 (P _ (UN ["="]) _, [lt,rt,l,r]) ->

289 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

290 let newt = mkP l r l t

291− return (Bind x (Hole newt)

291+ let sc = forget $ (Bind x (Hole newt)

292− (mkApp (P Ref (UN ["replace"]) (Set 0))

292+ (mkApp (P Ref (UN ["replace"]) (Set 0))

293− [lt, l, r, p, tmv, xp]))

293+ [lt, l, r, p, tmv, xp]))

294− -- fail $ "Rewrite " ++ show l ++ " to " ++ show r ++ " in " ++

294+ (scv, sct) <- lift $ check ctxt env sc

295− -- show t ++ " with " ++ show (p, newt) ++ " not done yet"

295+ return scv

296 _ -> fail "Not an equality type"

297 where

298 -- to make the P for rewrite, replace syntactic occurrences of l in ty with

src/Core/TT.hs+1−1

@@ -329,7 +329,7 @@ showEnvDbg env t = showEnv' env t True

329

330showEnv' env t dbg = se 10 env t where

331 se p env (P nt n t) = show n

332− ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

332+ -- ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

333 se p env (V i) | i < length env = (show $ fst $ env!!i) ++

334 if dbg then "{" ++ show i ++ "}" else ""

335 | otherwise = "!!V " ++ show i ++ "!!"

src/Core/Typecheck.hs+10−5

@@ -39,15 +39,20 @@ check ctxt env (Var n)

39check ctxt env (RApp f a)

40 = do (fv, fty) <- check ctxt env f

41 (av, aty) <- check ctxt env a

42− let fty' = normalise ctxt env fty

42+ let fty' = renameBinders 0 $ normalise ctxt env fty

43−-- trace (showEnv env fty ++ " ===> " ++ showEnv env fty') $

44 case fty' of

43 case fty' of

45 Bind x (Pi s) t ->

44 Bind x (Pi s) t ->

46 do converts ctxt env s aty

45 do converts ctxt env s aty

46+ let apty = {- normalise ctxt env -} (Bind x (Let aty av) t)

47− return (App fv av,

47+ return (App fv av, apty)

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

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

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

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

49+ -- This rather unpleasant hack is needed because during incomplete

50+ -- proofs, variables are locally bound with an explicit name. If we just

51+ -- make sure bound names in function types are locally unique, machine

52+ -- generated names, we'll be fine.

53+ where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)

54+ (renameBinders (i+1) t)

55+ renameBinders i sc = sc

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

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

52check ctxt env (RConstant c) = return (Constant c, constType c)

57check ctxt env (RConstant c) = return (Constant c, constType c)

53 where constType (I _) = Constant IType

58 where constType (I _) = Constant IType

src/Idris/REPL.hs+3−3

@@ -46,9 +46,9 @@ process Help

46process (Eval t) = do (tm, ty) <- elabVal toplevel t

47 ctxt <- getContext

48 ist <- get

49− let tm' = normalise ctxt [] tm

49+ let tm' = normaliseC ctxt [] tm

50− let ty' = normalise ctxt [] ty

50+ let ty' = normaliseC ctxt [] ty

51− logLvl 3 $ "Raw: " ++ show tm'

51+ logLvl 3 $ "Raw: " ++ show (tm', ty')

52 iputStrLn (show (delab ist tm') ++ " : " ++

53 show (delab ist ty'))

54process (Spec t) = do (tm, ty) <- elabVal toplevel t