cc4eb28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

let bindings; fixed bug with simple lambda app

commitcc4eb28e436d226881978009a1983723799dd6a4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 24 Oct 2011, 00:24 (15 years ago) parent796fa25

8 files changed+55−12

compare with master

unifiedsplit

lib/vect.idr+5−1 src/Core/Elaborate.hs+4−1 src/Core/ProofState.hs+10 src/Idris/AbsSyntax.hs+7 src/Idris/Delaborate.hs+2−1 src/Idris/ElabDecls.hs+19−7 src/Idris/Parser.hs+5 src/Main.hs+3−2

lib/vect.idr+5−1

@@ -13,4 +13,8 @@ data Vect : Set -> Nat -> Set where

1313vlookup : (i : Fin n) -> Vect a n -> a;

1414vlookup fO (x :: xs) = x;

1515vlookup (fS k) (x :: xs) = vlookup k xs;

16−

16+

17+vapp : Vect a n -> Vect a m -> Vect a (plus n m);

18+vapp VNil ys = ys;

19+vapp (x :: xs) ys = x :: vapp xs ys;

20+

src/Core/Elaborate.hs+4−1

@@ -163,6 +163,9 @@ intro n = processTactic' (Intro n)

163163forall :: Name -> Raw -> Elab ()

164164forall n t = processTactic' (Forall n t)

165165

166+letbind :: Name -> Raw -> Raw -> Elab ()

167+letbind n t v = processTactic' (LetBind n t v)

168+

166169patvar :: Name -> Elab ()

167170patvar n = processTactic' (PatVar n)

168171

@@ -272,8 +275,8 @@ simple_app fun arg =

272275 start_unify s

273276 claim s (Var a)

274277 prep_fill f [s]

278+ focus s; arg -- need to work out the type of the arg, so do it first

275279 focus f; fun

276− focus s; arg

277280 complete_fill

278281 end_unify

279282

src/Core/ProofState.hs+10

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

4949 | CheckIn Raw

5050 | Intro Name

5151 | Forall Name Raw

52+ | LetBind Name Raw Raw

5253 | PatVar Name

5354 | PatBind Name

5455 | Focus Name

@@ -270,6 +271,14 @@ patvar n ctxt env (Bind x (Hole t) sc) =

270271 do action (\ps -> ps { holes = holes ps \\ [x] })

271272 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

272273

274+letbind :: Name -> Raw -> Raw -> RunTactic

275+letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

276+ do (tyv, tyt) <- lift $ check ctxt env ty

277+ (valv, valt) <- lift $ check ctxt env val

278+ lift $ isSet ctxt env tyt

279+ return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

280+letbind n ty val ctxt env _ = fail "Can't let bind here"

281+

273282patbind :: Name -> RunTactic

274283patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

275284 do let t' = normalise ctxt env t

@@ -379,6 +388,7 @@ process t h = tactic (Just h) (mktac t)

379388 mktac Compute = compute

380389 mktac (Intro n) = intro n

381390 mktac (Forall n t) = forall n t

391+ mktac (LetBind n t v) = letbind n t v

382392 mktac (PatVar n) = patvar n

383393 mktac (PatBind n) = patbind n

384394 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntax.hs+7

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

263263 se p (PQuote r) = "![" ++ show r ++ "]"

264264 se p (PRef _ n) = show n

265265 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

266+ se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

267+ " in " ++ se 10 sc

266268 se p (PPi Exp n ty sc)

267269 | n `elem` allNamesIn sc = bracket p 2 $

268270 "(" ++ show n ++ " : " ++ se 10 ty ++

@@ -433,6 +435,11 @@ addImpl ist ptm = ai [] ptm

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

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

435437 PLam n ty' sc'

438+ ai env (PLet n ty val sc)

439+ = let ty' = ai env ty

440+ val' = ai env val

441+ sc' = ai (n:env) sc in

442+ PLet n ty' val' sc'

436443 ai env (PPi p n ty sc) = let ty' = ai env ty

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

438445 PPi p n ty' sc'

src/Idris/Delaborate.hs+2−1

@@ -16,7 +16,8 @@ delab ist tm = de [] tm

1616 un = FC "(val)" 0

1717

1818 de env (App f a) = deFn env f [a]

19− de env (V i) = PRef un (env!!i)

19+ de env (V i) | i < length env = PRef un (env!!i)

20+ | otherwise = PRef un (UN ["v" ++ show i ++ ""])

2021 de env (P _ n _) | n == unitTy = PTrue un

2122 | n == unitCon = PTrue un

2223 | n == falseTy = PFalse un

src/Idris/ElabDecls.hs+19−7

@@ -90,7 +90,7 @@ elabVal info tm

9090 = do ctxt <- getContext

9191 logLvl 10 (showImp True tm)

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

93− (build info False (infTerm tm))

93+ (build info True (infTerm tm))

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

9595 let vtm = getInferTerm tm'

9696 logLvl 2 (show vtm)

@@ -241,18 +241,30 @@ elab info pattern tm = do elab' tm

241241 elab' ty

242242 elab' sc

243243 solve

244+ elab' (PLet n Placeholder val sc)

245+ = do attack; -- (h:_) <- get_holes

246+ tyn <- unique_hole (MN 0 "letty")

247+ -- start_unify h

248+ claim tyn (RSet 0)

249+ valn <- unique_hole (MN 0 "letval")

250+ claim valn (Var tyn)

251+ letbind n (Var tyn) (Var valn)

252+ focus valn

253+ elab' val

254+ elab' sc

255+ -- end_unify

256+ solve

244257 elab' (PApp fc (PRef _ f) args)

245258 | Just ps <- lookupCtxt f (inblock info)

246259 = erun fc $

247260 elabApp (liftname info f) (map (PExp . (PRef fc)) ps ++ args)

248261 | otherwise = erun fc $ elabApp f args

249262 where elabApp f args

250− = -- erun (FC "FOO" 42) $

251− try (do ns <- apply (Var f) (map isph args)

252− solve

253− elabArgs ns (map getTm args))

254− (do apply_elab f (map toElab args)

255− solve)

263+ = try (do ns <- apply (Var f) (map isph args)

264+ solve

265+ elabArgs ns (map getTm args))

266+ (do apply_elab f (map toElab args)

267+ solve)

256268 elab' (PApp fc f [arg])

257269 = erun fc $

258270 do simple_app (elab' f) (elab' (getTm arg))

src/Idris/Parser.hs+5

@@ -258,6 +258,7 @@ pNoExtExpr syn =

258258 try (pApp syn)

259259 <|> pSimpleExpr syn

260260 <|> try (pLambda syn)

261+ <|> try (pLet syn)

261262 <|> try (pPi syn)

262263 <|> try (pDoBlock syn)

263264

@@ -354,6 +355,10 @@ pLambda syn = do lchar '\\';

354355 sc <- pExpr syn

355356 return (bindList PLam xt sc)

356357

358+pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn

359+ reserved "in"; sc <- pExpr syn

360+ return (PLet n Placeholder v sc)

361+

357362pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'

358363 symbol "->"

359364 sc <- pExpr syn

src/Main.hs+3−2

@@ -41,13 +41,14 @@ main = do xs <- getArgs

4141runIdris :: [Opt] -> Idris ()

4242runIdris opts =

4343 do let inputs = opt getFile opts

44+ let runrepl = not (NoREPL `elem` opts)

4445 mapM_ makeOption opts

4546 elabPrims

4647 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

4748 return ()

49+ when runrepl $ iputStrLn banner

4850 mods <- mapM loadModule inputs

49− when (not (NoREPL `elem` opts)) $ do iputStrLn banner

50− repl (mkPrompt mods)

51+ when runrepl $ repl (mkPrompt mods)

5152 where

5253 makeOption (OLogging i) = setLogLevel i

5354 makeOption _ = return ()