06a81c9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Elaborating types and data declarations

commit06a81c9d11afd6388170378d6cbe7c2768518c79 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 7 Oct 2011, 16:49 (15 years ago) parentefd11bb

8 files changed+60−14

compare with master

unifiedsplit

decls.mi+4 miniidris.cabal+2−1 src/Core/Elaborate.hs+17−3 src/Core/ProofShell.hs+1−1 src/Core/ProofState.hs+2−1 src/Core/ShellParser.hs+2−2 src/Idris/AbsSyntax.hs+29−5 src/Main.hs+3−1

decls.mi+4

@@ -10,6 +10,10 @@ data Vect : Set -> Nat -> Set where

1010 VNil : Vect a O

1111 | (::) : a -> Vect a k -> Vect a (S k);

1212

13+data Env : Vect Set n -> Set where

14+ Empty : Env VNil

15+ | Extend : {xs : Vect Set n} -> a -> Env xs -> Env (a :: xs);

16+

1317plus : Nat -> Nat -> Nat;

1418plus O y = y;

1519plus (S k) y = S (plus k y);

miniidris.cabal+2−1

@@ -21,7 +21,8 @@ Executable miniidris

2121 Core.ProofShell, Core.ProofState, Core.CoreParser,

2222 Core.ShellParser, Core.Unify, Core.Elaborate,

2323

24− Idris.AbsSyntax, Idris.Parser, Idris.REPL

24+ Idris.AbsSyntax, Idris.Parser, Idris.REPL,

25+ Idris.REPLParser, Idris.ElabDecls

2526

2627 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

2728 containers, process

src/Core/Elaborate.hs+17−3

@@ -29,12 +29,20 @@ data Command = Theorem Name Raw

2929

3030type Elab a = StateT (ProofState, String) TC a

3131

32−runElab :: Elab a -> ProofState -> TC (ProofState, String)

33−runElab e ps = execStateT e (ps, "")

32+runElab :: Elab a -> ProofState -> TC (a, (ProofState, String))

33+runElab e ps = runStateT e (ps, "")

34+

35+execElab :: Elab a -> ProofState -> TC (ProofState, String)

36+execElab e ps = execStateT e (ps, "")

3437

3538initElaborator :: Name -> Context -> Type -> ProofState

3639initElaborator = newProof

3740

41+elaborate :: Context -> Name -> Type -> Elab a -> TC (a, String)

42+elaborate ctxt n ty elab = do let ps = initElaborator n ctxt ty

43+ (a, (ps', str)) <- runElab elab ps

44+ return (a, str)

45+

3846processTactic' t = do (p, logs) <- get

3947 (p', log) <- lift $ processTactic t p

4048 put (p', logs ++ log)

@@ -47,6 +55,11 @@ get_context :: Elab Context

4755get_context = do (p, _) <- get

4856 return (context p)

4957

58+-- get the proof term

59+get_term :: Elab Term

60+get_term = do (p, _) <- get

61+ return (pterm p)

62+

5063-- get the local context at the currently in focus hole

5164get_env :: Elab Env

5265get_env = do (p, _) <- get

@@ -174,7 +187,7 @@ prepare_apply fn imps =

174187 doClaims t [] claims = return (reverse claims)

175188 doClaims _ _ _ = fail "Wrong number of arguments"

176189

177−apply :: Raw -> [Bool] -> Elab ()

190+apply :: Raw -> [Bool] -> Elab [Name]

178191apply fn imps =

179192 do args <- prepare_apply fn imps

180193 fill (raw_apply fn (map Var args))

@@ -186,6 +199,7 @@ apply fn imps =

186199 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

187200 put (p { unified = unify }, s)

188201 end_unify

202+ return args

189203

190204-- Abstract over an argument of unknown type, giving a name for the hole

191205-- which we'll fill with the argument type too.

src/Core/ProofShell.hs+1−1

@@ -41,7 +41,7 @@ processCommand (Print n) state =

4141 Just tm -> (state, show tm)

4242 Nothing -> (state, "No such name")

4343processCommand (Tac e) state

44− | Just ps <- prf state = case runElab e ps of

44+ | Just ps <- prf state = case execElab e ps of

4545 OK (ps', resp) ->

4646 if (not (done ps'))

4747 then (state { prf = Just ps' }, resp)

src/Core/ProofState.hs+2−1

@@ -53,6 +53,7 @@ data Tactic = Attack

5353 | ProofState

5454 | Undo

5555 | QED

56+ deriving Show

5657

5758-- Some utilites on proof and tactic states

5859

@@ -213,7 +214,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

213214 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })

214215 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

215216 | otherwise = fail "I see a hole in your solution."

216−solve _ _ _ = fail "Not a guess."

217+solve _ _ h = fail $ "Not a guess " ++ show h

217218

218219intro :: Name -> RunTactic

219220intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

src/Core/ShellParser.hs+2−2

@@ -51,13 +51,13 @@ pTactic = do reserved "attack"; return attack

5151 <|> do reserved "exact"; tm <- pTerm; return (exact tm)

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

5353 <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;

54− return (apply tm args)

54+ return (discard (apply tm args))

5555 <|> do reserved "solve"; return solve

5656 <|> do reserved "compute"; return compute

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

5858 <|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm

5959 return (forall n ty)

60−-- <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

60+ <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

6161 <|> do reserved "patvar"; n <- iName; return (patvar n)

6262-- <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)

6363 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

src/Idris/AbsSyntax.hs+29−5

@@ -31,9 +31,23 @@ idrisInit = IState emptyContext [] emptyContext "" []

3131-- global state (hence the IO inner monad).

3232type Idris a = StateT IState IO a

3333

34+getContext :: Idris Context

35+getContext = do i <- get; return (tt_ctxt i)

36+

37+setContext :: Context -> Idris ()

38+setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

39+

40+updateContext :: (Context -> Context) -> Idris ()

41+updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

42+

3443iputStrLn :: String -> Idris ()

3544iputStrLn = lift.putStrLn

3645

46+tclift :: Show a => TC a -> Idris a

47+tclift tc = case tc of

48+ OK v -> return v

49+ err -> fail (show err)

50+

3751setOpt :: IOption -> Bool -> Idris ()

3852setOpt o True = do i <- get

3953 put (i { idris_options = nub (o : idris_options i) })

@@ -143,6 +157,8 @@ showImp impl tm = se 10 tm where

143157 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++

144158 "} -> " ++ se 10 sc

145159 | otherwise = se 10 sc

160+ se p (PApp (PRef f) _ [])

161+ | not impl = show f

146162 se p (PApp (PRef op@(UN [f:_])) _ [l, r])

147163 | not impl && not (isAlpha f)

148164 = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r

@@ -221,10 +237,15 @@ implicitise ist tm

221237addImpl :: IState -> PTerm -> PTerm

222238addImpl ist ptm = ai [] ptm

223239 where

240+ ai env (PRef f) = aiFn env (PRef f) [] []

241+ ai env (PApp (PRef f) is es)

242+ = let is' = map (\ (n, tm) -> (n, ai env tm)) is

243+ es' = map (ai env) es in

244+ aiFn env (PRef f) is' es'

224245 ai env (PApp f is es) = let f' = ai env f

225− is' = map (\ (n, tm) -> (n, ai env tm)) is

246+ is' = map (\ (n, tm) -> (n, ai env tm)) is

226247 es' = map (ai env) es in

227− aiFn env f is' es'

248+ aiFn env f' is' es'

228249 ai env (PLam n ty sc) = let ty' = ai env ty

229250 sc' = ai (n:env) sc in

230251 PLam n ty' sc'

@@ -236,9 +257,12 @@ addImpl ist ptm = ai [] ptm

236257

237258 aiFn env (PRef f) is es | not (f `elem` env)

238259 = case lookupCtxt f (idris_implicits ist) of

239− Just ns -> PApp (PRef f) (insertImpl ns is) es

240− Nothing -> PApp (PRef f) is es

241− aiFn env f is es = PApp f is es

260+ Just ns -> pApp (PRef f) (insertImpl ns is) es

261+ Nothing -> pApp (PRef f) is es

262+ aiFn env f is es = pApp f is es

263+

264+ pApp f [] [] = f

265+ pApp f is es = PApp f is es

242266

243267 insertImpl [] given = []

244268 insertImpl (n:ns) given

src/Main.hs+3−1

@@ -18,7 +18,7 @@ import Core.Evaluate

1818import Idris.AbsSyntax

1919import Idris.Parser

2020import Idris.REPL

21−

21+import Idris.ElabDecls

2222

2323-- Main program reads command line options, parses the main program, and gets

2424-- on with the REPL.

@@ -45,6 +45,8 @@ loadModule f = do iLOG ("Reading " ++ show f)

4545 iLOG (dumpDecls ds)

4646 i <- get

4747 iLOG (show (idris_infixes i))

48+ -- Now add all the declarations to the context

49+ mapM_ elabDecl ds

4850 return ()

4951

5052dumpDecls :: [PDecl] -> String