e23c029 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow type annotations on let tactic

commite23c0299fd69ae89597e4a7523b90d54834f3511 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 Nov 2012, 16:06 (14 years ago) parent160eedd

6 files changed+38−7

compare with master

unifiedsplit

CHANGELOG+1 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/Delaborate.hs+2−2 src/Idris/ElabTerm.hs+15 src/Idris/IBC.hs+6 src/Idris/Parser.hs+11−4

CHANGELOG+1

@@ -13,6 +13,7 @@ User visible changes:

1313* Added documentation comments (Haddock style) and ':doc' REPL command

1414* Pattern matching on strings, big integers and characters

1515* Added System.Concurrency modules

16+* Added 'postulate' declarations

1617

1718Internal changes:

1819

src/Idris/AbsSyntaxTree.hs+3−1

@@ -398,6 +398,7 @@ updateNs ns t = mapPT updateRef t

398398

399399data PTerm = PQuote Raw

400400 | PRef FC Name

401+ | PInferRef FC Name -- a name to be defined later

401402 | PPatvar FC Name

402403 | PLam Name PTerm PTerm

403404 | PPi Plicity Name PTerm PTerm

@@ -450,7 +451,8 @@ mapPT f t = f (mpt t) where

450451

451452

452453data PTactic' t = Intro [Name] | Intros | Focus Name

453− | Refine Name [Bool] | Rewrite t | LetTac Name t

454+ | Refine Name [Bool] | Rewrite t

455+ | LetTac Name t | LetTacTy Name t t

454456 | Exact t | Compute | Trivial

455457 | Solve

456458 | Attack

src/Idris/Delaborate.hs+2−2

@@ -77,8 +77,8 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

7777 "\nThis is probably a bug, or a missing error message.\n" ++

7878 "Please consider reporting at " ++ bugaddr

7979pshow i (CantUnify _ x y e sc s)

80− = "Can't unify " ++ show (delab i x)

81− ++ " with " ++ show (delab i y) ++

80+ = "Can't unify " ++ showImp True (delab i x)

81+ ++ " with " ++ showImp True (delab i y) ++

8282-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

8383 case e of

8484 Msg "" -> ""

src/Idris/ElabTerm.hs+15

@@ -232,6 +232,8 @@ elab ist info pattern tcgen fn tm

232232 elabE (True, a) val

233233 elabE (True, a) sc

234234 solve

235+ elab' (ina, g) tm@(PApp fc (PInferRef _ f) args')

236+ = fail "Not implemented"

235237 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

236238 = do let args = {- case lookupCtxt f (inblock info) of

237239 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

@@ -564,6 +566,19 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

564566 focus valn

565567 elab ist toplevel False False (MN 0 "tac") tm

566568 when autoSolve solveAll

569+ runT (LetTacTy n ty tm)

570+ = do attack

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

572+ claim tyn RSet

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

574+ claim valn (Var tyn)

575+ letn <- unique_hole n

576+ letbind letn (Var tyn) (Var valn)

577+ focus tyn

578+ elab ist toplevel False False (MN 0 "tac") ty

579+ focus valn

580+ elab ist toplevel False False (MN 0 "tac") tm

581+ when autoSolve solveAll

567582 runT Compute = compute

568583 runT Trivial = do trivial ist; when autoSolve solveAll

569584 runT (Focus n) = focus n

src/Idris/IBC.hs+6

@@ -1224,6 +1224,9 @@ instance Binary PTerm where

12241224 PPatvar x1 x2 -> do putWord8 28

12251225 put x1

12261226 put x2

1227+ PInferRef x1 x2 -> do putWord8 29

1228+ put x1

1229+ put x2

12271230 get

12281231 = do i <- getWord8

12291232 case i of

@@ -1305,6 +1308,9 @@ instance Binary PTerm where

13051308 28 -> do x1 <- get

13061309 x2 <- get

13071310 return (PPatvar x1 x2)

1311+ 29 -> do x1 <- get

1312+ x2 <- get

1313+ return (PInferRef x1 x2)

13081314 _ -> error "Corrupted binary data for PTerm"

13091315

13101316instance (Binary t) => Binary (PTactic' t) where

src/Idris/Parser.hs+11−4

@@ -746,6 +746,9 @@ pSimpleExpr syn =

746746 <|> try (do x <- pfName

747747 fc <- pfc

748748 return (PRef fc x))

749+ <|> try (do lchar '!'; x <- pfName

750+ fc <- pfc

751+ return (PInferRef fc x))

749752 <|> try (pList syn)

750753 <|> try (pAlt syn)

751754 <|> try (pIdiom syn)

@@ -1469,10 +1472,14 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

14691472 <|> do reserved "rewrite"; t <- pExpr syn;

14701473 i <- getState

14711474 return $ Rewrite (desugar syn i t)

1472− <|> do reserved "let"; n <- pName; lchar '=';

1473− t <- pExpr syn;

1474− i <- getState

1475− return $ LetTac n (desugar syn i t)

1475+ <|> try (do reserved "let"; n <- pName; lchar ':';

1476+ ty <- pExpr' syn; lchar '='; t <- pExpr syn;

1477+ i <- getState

1478+ return $ LetTacTy n (desugar syn i ty) (desugar syn i t))

1479+ <|> try (do reserved "let"; n <- pName; lchar '=';

1480+ t <- pExpr syn;

1481+ i <- getState

1482+ return $ LetTac n (desugar syn i t))

14761483 <|> do reserved "focus"; n <- pName

14771484 return $ Focus n

14781485 <|> do reserved "exact"; t <- pExpr syn;