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

git.iko.soy/Idris-dev

Some tidying; compute; print

commit1921eac03bf0488730b3ec7e2c32b1fee5416458 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 24 Sep 2011, 22:30 (15 years ago) parent9c6ea4a

5 files changed+36−1

compare with master

unifiedsplit

src/Core.hs+15 src/Evaluate.hs+8−1 src/ProofShell.hs+4 src/ProofState.hs+7 src/ShellParser.hs+2

src/Core.hs+15

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

8080

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

8282

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+

8396bindEnv :: EnvTT n -> TT n -> TT n

8497bindEnv [] tm = tm

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

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

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

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

109122 | 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

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

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

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

src/Evaluate.hs+8−1

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

33module Evaluate(normalise,

44 Fun(..), Def(..), Context,

55 emptyContext, addToCtxt, addConstant,

6− lookupTy, lookupP, lookupVal, lookupTyEnv) where

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

88import Debug.Trace

99import Core

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

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

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

104104

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+

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

106113lookupVal n ctxt

107114 = do def <- lookup n ctxt

src/ProofShell.hs+4

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

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

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

3434 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")

3539processCommand (Tac t) state

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

3741 OK (ps', resp) ->

src/ProofState.hs+7

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

2727data Command = Theorem Name Raw

2828 | Eval Raw

2929 | Quit

30+ | Print Name

3031 | Tac Tactic

3132

3233data Tactic = Attack

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

3435 | Fill Raw

3536 | Regret

3637 | Solve

38+ | Compute

3739 | EvalIn Raw

3840 | CheckIn Raw

3941 | Intro Name

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

169171 _ -> fail "Nothing to introduce"

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

171173

174+compute :: RunTactic

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

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

177+

172178check_in :: Raw -> RunTactic

173179check_in t ctxt env tm =

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

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

213219 mktac (Fill r) = fill r

214220 mktac Regret = regret

215221 mktac Solve = solve

222+ mktac Compute = compute

216223 mktac (Intro n) = intro n

217224 mktac (CheckIn r) = check_in r

218225 mktac (EvalIn r) = eval_in r

src/ShellParser.hs+2

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

3939 return (Theorem n ty)

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

4141 return (Eval tm)

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

4243 <|> do reserved "quit";

4344 return Quit

4445

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

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

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

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

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

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

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

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