1921eac · Idris-dev · git.iko.soy

src/Core.hs+15

compare with master

unifiedsplit

@@ -80,6 +80,19 @@ data TT n = P NameType n (TT n) -- embed type

80

81type EnvTT n = [(n, Binder (TT n))]

82

83+-- Returns true if V 0 does not occur in the term

84+

85+noOccurrence :: TT n -> Bool

86+noOccurrence t = no' 0 t

87+ where

88+ no' i (V x) = not (i == x)

89+ no' i (Bind n b sc) = noB' i b && no' (i+1) sc

90+ where noB' i (Let t v) = no' i t && no' i v

91+ noB' i (Guess t v) = no' i t && no' i v

92+ noB' i b = no' i (binderTy b)

93+ no' i (App f a) = no' i f && no' i a

94+ no' i _ = True

95+

83bindEnv :: EnvTT n -> TT n -> TT n

96bindEnv :: EnvTT n -> TT n -> TT n

84bindEnv [] tm = tm

97bindEnv [] tm = tm

85bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)

98bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)

@@ -107,6 +120,8 @@ showEnv' env t dbg = se 10 env t where

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

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

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

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

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

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

123+ se p env (Bind n b@(Pi t) sc)

124+ | noOccurrence sc = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc

110 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

125 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

111 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

126 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

112 se p env (Set i) = "Set" ++ show i

127 se p env (Set i) = "Set" ++ show i

src/Evaluate.hs+8−1

@@ -3,7 +3,7 @@

3module Evaluate(normalise,

4 Fun(..), Def(..), Context,

5 emptyContext, addToCtxt, addConstant,

6− lookupTy, lookupP, lookupVal, lookupTyEnv) where

6+ lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where

7

8import Debug.Trace

9import Core

@@ -102,6 +102,13 @@ lookupP n ctxt

102 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

103 (Constant nt ty hty) -> return (P nt n ty)

104

105+lookupDef :: Name -> Context -> Maybe Term

106+lookupDef n ctxt

107+ = do def <- lookup n ctxt

108+ case def of

109+ (Function (Fun ty _ tm _)) -> return tm

110+ (Constant nt ty hty) -> return (P nt n ty)

111+

105lookupVal :: Name -> Context -> Maybe Value

112lookupVal :: Name -> Context -> Maybe Value

106lookupVal n ctxt

113lookupVal n ctxt

107 = do def <- lookup n ctxt

114 = do def <- lookup n ctxt

src/ProofShell.hs+4

@@ -32,6 +32,10 @@ processCommand (Eval t) state =

32 tnf = normalise (ctxt state) [] ty in

33 (state, show nf ++ " : " ++ show ty)

34 err -> (state, show err)

35+processCommand (Print n) state =

36+ case lookupDef n (ctxt state) of

37+ Just tm -> (state, show tm)

38+ Nothing -> (state, "No such name")

35processCommand (Tac t) state

39processCommand (Tac t) state

36 | Just ps <- prf state = case processTactic t ps of

40 | Just ps <- prf state = case processTactic t ps of

37 OK (ps', resp) ->

41 OK (ps', resp) ->

src/ProofState.hs+7

@@ -27,6 +27,7 @@ data Goal = GD { premises :: Env,

27data Command = Theorem Name Raw

28 | Eval Raw

29 | Quit

30+ | Print Name

30 | Tac Tactic

31 | Tac Tactic

31

32

32data Tactic = Attack

33data Tactic = Attack

@@ -34,6 +35,7 @@ data Tactic = Attack

34 | Fill Raw

35 | Fill Raw

35 | Regret

36 | Regret

36 | Solve

37 | Solve

38+ | Compute

37 | EvalIn Raw

39 | EvalIn Raw

38 | CheckIn Raw

40 | CheckIn Raw

39 | Intro Name

41 | Intro Name

@@ -169,6 +171,10 @@ intro n ctxt env (Bind x (Hole t) (V 0)) =

169 _ -> fail "Nothing to introduce"

171 _ -> fail "Nothing to introduce"

170intro ctxt env _ _ = fail "Can't introduce here."

172intro ctxt env _ _ = fail "Can't introduce here."

171

173

174+compute :: RunTactic

175+compute ctxt env (Bind x (Hole ty) sc) =

176+ do return $ Bind x (Hole (normalise ctxt env ty)) sc

177+

172check_in :: Raw -> RunTactic

178check_in :: Raw -> RunTactic

173check_in t ctxt env tm =

179check_in t ctxt env tm =

174 do (val, valty) <- lift $ check ctxt env t

180 do (val, valty) <- lift $ check ctxt env t

@@ -213,6 +219,7 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)

213 mktac (Fill r) = fill r

219 mktac (Fill r) = fill r

214 mktac Regret = regret

220 mktac Regret = regret

215 mktac Solve = solve

221 mktac Solve = solve

222+ mktac Compute = compute

216 mktac (Intro n) = intro n

223 mktac (Intro n) = intro n

217 mktac (CheckIn r) = check_in r

224 mktac (CheckIn r) = check_in r

218 mktac (EvalIn r) = eval_in r

225 mktac (EvalIn r) = eval_in r

src/ShellParser.hs+2

@@ -39,6 +39,7 @@ pCommand = do reserved "theorem"; n <- iName; lchar ':'; ty <- pTerm

39 return (Theorem n ty)

40 <|> do reserved "eval"; tm <- pTerm

41 return (Eval tm)

42+ <|> do reserved "print"; n <- iName; return (Print n)

42 <|> do reserved "quit";

43 <|> do reserved "quit";

43 return Quit

44 return Quit

44

45

@@ -49,6 +50,7 @@ pTactic = do reserved "attack"; return Attack

49 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)

50 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)

50 <|> do reserved "regret"; return Regret

51 <|> do reserved "regret"; return Regret

51 <|> do reserved "solve"; return Solve

52 <|> do reserved "solve"; return Solve

53+ <|> do reserved "compute"; return Compute

52 <|> do reserved "intro"; n <- iName; return (Intro n)

54 <|> do reserved "intro"; n <- iName; return (Intro n)

53 <|> do reserved "eval"; t <- pTerm; return (EvalIn t)

55 <|> do reserved "eval"; t <- pTerm; return (EvalIn t)

54 <|> do reserved "check"; t <- pTerm; return (CheckIn t)

56 <|> do reserved "check"; t <- pTerm; return (CheckIn t)