e23c029 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

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

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

14* Pattern matching on strings, big integers and characters

15* Added System.Concurrency modules

16+* Added 'postulate' declarations

16

17

17Internal changes:

18Internal changes:

18

19

src/Idris/AbsSyntaxTree.hs+3−1

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

398

399data PTerm = PQuote Raw

400 | PRef FC Name

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

401 | PPatvar FC Name

402 | PPatvar FC Name

402 | PLam Name PTerm PTerm

403 | PLam Name PTerm PTerm

403 | PPi Plicity Name PTerm PTerm

404 | PPi Plicity Name PTerm PTerm

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

450

451

452

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

453data 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

454 | Exact t | Compute | Trivial

456 | Exact t | Compute | Trivial

455 | Solve

457 | Solve

456 | Attack

458 | Attack

src/Idris/Delaborate.hs+2−2

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

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

78 "Please consider reporting at " ++ bugaddr

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

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

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

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

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

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

83 case e of

84 Msg "" -> ""

src/Idris/ElabTerm.hs+15

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

232 elabE (True, a) val

233 elabE (True, a) sc

234 solve

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

236+ = fail "Not implemented"

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

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

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

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

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

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

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

564 focus valn

566 focus valn

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

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

566 when autoSolve solveAll

568 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

567 runT Compute = compute

582 runT Compute = compute

568 runT Trivial = do trivial ist; when autoSolve solveAll

583 runT Trivial = do trivial ist; when autoSolve solveAll

569 runT (Focus n) = focus n

584 runT (Focus n) = focus n

src/Idris/IBC.hs+6

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

1224 PPatvar x1 x2 -> do putWord8 28

1225 put x1

1226 put x2

1227+ PInferRef x1 x2 -> do putWord8 29

1228+ put x1

1229+ put x2

1227 get

1230 get

1228 = do i <- getWord8

1231 = do i <- getWord8

1229 case i of

1232 case i of

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

1305 28 -> do x1 <- get

1308 28 -> do x1 <- get

1306 x2 <- get

1309 x2 <- get

1307 return (PPatvar x1 x2)

1310 return (PPatvar x1 x2)

1311+ 29 -> do x1 <- get

1312+ x2 <- get

1313+ return (PInferRef x1 x2)

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

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

1309

1315

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

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

src/Idris/Parser.hs+11−4

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

746 <|> try (do x <- pfName

747 fc <- pfc

748 return (PRef fc x))

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

750+ fc <- pfc

751+ return (PInferRef fc x))

749 <|> try (pList syn)

752 <|> try (pList syn)

750 <|> try (pAlt syn)

753 <|> try (pAlt syn)

751 <|> try (pIdiom syn)

754 <|> try (pIdiom syn)

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

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

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

1470 i <- getState

1473 i <- getState

1471 return $ Rewrite (desugar syn i t)

1474 return $ Rewrite (desugar syn i t)

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

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 '=';

1473− t <- pExpr syn;

1480+ t <- pExpr syn;

1474− i <- getState

1481+ i <- getState

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

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

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

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

1477 return $ Focus n

1484 return $ Focus n

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

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