a0346b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Begin implementation of reflected elab monad

a0346b6David Raymond Christiansen12 years ago

libs/prelude/Language/Reflection/Tactical.idrnew file+53

compare with master

unifiedsplit

@@ -0,0 +1,53 @@

1+module Language.Reflection.Tactical

3+import Builtins

4+import Prelude.Applicative

5+import Prelude.Functor

6+import Prelude.List

7+import Prelude.Maybe

8+import Prelude.Monad

9+import Language.Reflection

10+

11+data Tactical : Type -> Type where

12+ -- obligatory control stuff

13+ PureTactical : a -> Tactical a

14+ BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b

15+

16+ Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a

17+ Skip : Tactical ()

18+ Fail : {a : Type} -> List ErrorReportPart -> Tactical a

19+

20+ Env : Tactical (List (TTName, Binder TT))

21+ Goal : Tactical (TTName, TT)

22+ Holes : Tactical (List TTName)

23+ Guess : Tactical (Maybe TT)

24+

25+ Forget : TT -> Tactical Raw

26+

27+ Gensym : String -> Tactical TTName

28+

29+ Solve : Tactical ()

30+ Fill : Raw -> Tactical ()

31+ Focus : TTName -> Tactical ()

32+ Unfocus : TTName -> Tactical ()

33+ Attack : Tactical ()

34+

35+ Claim : TTName -> Raw -> Tactical ()

36+

37+

38+instance Functor Tactical where

39+ map f t = BindTactical t (\x => PureTactical (f x))

40+

41+instance Applicative Tactical where

42+ pure x = PureTactical x

43+ f <$> x = BindTactical f $ \g =>

44+ BindTactical x $ \y =>

45+ PureTactical $ g y

46+

47+instance Alternative Tactical where

48+ empty = Fail [TextPart "empty"]

49+ x <|> y = Try x y

50+

51+instance Monad Tactical where

52+ x >>= f = BindTactical x f

53+

libs/prelude/prelude.ipkg+1−1

@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11 Prelude.Uninhabited, Prelude.Pairs,

13− Language.Reflection, Language.Reflection.Errors,

13+ Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,

15 Decidable.Equality

src/Idris/AbsSyntax.hs+4

@@ -974,6 +974,7 @@ expandParams dec ps ns infs tm = en tm

974 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

975 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

976 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

977+ en (PRunTactics tm) = PRunTactics (en tm)

977 en t = t

978 en t = t

978

979

979 nselem x [] = False

980 nselem x [] = False

@@ -1444,6 +1445,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1444 imps top env (PHidden tm) = imps False env tm

1445 imps top env (PHidden tm) = imps False env tm

1445 imps top env (PUnifyLog tm) = imps False env tm

1446 imps top env (PUnifyLog tm) = imps False env tm

1446 imps top env (PNoImplicits tm) = imps False env tm

1447 imps top env (PNoImplicits tm) = imps False env tm

1448+ imps top env (PRunTactics tm) = imps False env tm

1447 imps top env _ = return ()

1449 imps top env _ = return ()

1448

1450

1449 pibind using [] sc = sc

1451 pibind using [] sc = sc

@@ -1565,6 +1567,7 @@ addImpl' inpat env infns ist ptm

1565 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1567 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1566 (fmap (ai True env ds) g)

1568 (fmap (ai True env ds) g)

1567 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1569 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1570+ ai qq env ds (PRunTactics tm) = PRunTactics (ai False env ds tm)

1568 ai qq env ds tm = tm

1571 ai qq env ds tm = tm

1569

1572

1570 handleErr (Left err) = PElabError err

1573 handleErr (Left err) = PElabError err

@@ -2089,4 +2092,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2089 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

2092 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

2090 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2093 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2091 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2094 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2095+ mkUniq (PRunTactics ts) = liftM PRunTactics (mkUniq ts)

2092 mkUniq t = return t

2096 mkUniq t = return t

src/Idris/AbsSyntaxTree.hs+2−1

@@ -790,7 +790,8 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

790 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

791 | PNoImplicits PTerm -- ^ never run implicit converions on the term

792 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

793− | PUnquote PTerm -- ^ ,Term

793+ | PUnquote PTerm -- ^ ~Term

794+ | PRunTactics PTerm -- ^ %run_tactics tm - New-style proof script

794 deriving (Eq, Data, Typeable)

795 deriving (Eq, Data, Typeable)

795

796

797

src/Idris/Core/Elaborate.hs+1−1

@@ -190,7 +190,7 @@ get_term :: Elab' aux Term

190get_term = do ES p _ _ <- get

191 return $! (getProofTerm (pterm (fst p)))

192

193−-- | get the proof term

193+-- | modify the proof term

194update_term :: (Term -> Term) -> Elab' aux ()

195update_term f = do ES (p,a) logs prev <- get

196 let p' = p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }

src/Idris/DeepSeq.hs+1

@@ -239,6 +239,7 @@ instance NFData PTerm where

239 rnf (PNoImplicits x1) = rnf x1 `seq` ()

240 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

241 rnf (PUnquote x1) = rnf x1 `seq` ()

242+ rnf (PRunTactics x1) = rnf x1 `seq` ()

242

243

243instance (NFData t) => NFData (PTactic' t) where

244instance (NFData t) => NFData (PTactic' t) where

244 rnf (Intro x1) = rnf x1 `seq` ()

245 rnf (Intro x1) = rnf x1 `seq` ()

src/Idris/ElabQuasiquote.hs+2

@@ -170,6 +170,8 @@ extractUnquotes n (PUnquote tm)

170 return (PRef (fileFC "(unquote)") n, [(n, tm)])

171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

172 extractUnquotes (n-1) tm

173+extractUnquotes n (PRunTactics tm)

174+ = fmap (\(tm', ex) -> (PRunTactics tm', ex)) $ extractUnquotes n tm

173extractUnquotes n x = return (x, []) -- no subterms!

175extractUnquotes n x = return (x, []) -- no subterms!

174

176

175

177

src/Idris/ElabTerm.hs+107−9

@@ -1,4 +1,4 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE PatternGuards, ViewPatterns #-}

3module Idris.ElabTerm where

@@ -1029,6 +1029,20 @@ elab ist info emode opts fn tm

1029 delayElab $ do focus h

1030 dotterm

1031 elab' ina fc t

1032+ elab' ina fc (PRunTactics tm) =

1033+ do attack

1034+ n <- getNameFrom (sMN 0 "tacticScript")

1035+ n' <- getNameFrom (sMN 0 "tacticExpr")

1036+ let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)

1037+ claim n scriptTy

1038+ movelast n

1039+ letbind n' scriptTy (Var n)

1040+ focus n

1041+ elab' ina fc tm

1042+ env <- get_env

1043+ ctxt <- get_context

1044+ runTactical ctxt env (P Bound n' Erased)

1045+ solve

1032 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1046 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1033

1047

1034 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

1048 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

@@ -1451,6 +1465,86 @@ case_ ind autoSolve ist fn tm = do

1451 else casetac (forget val)

1465 else casetac (forget val)

1452 when autoSolve solveAll

1466 when autoSolve solveAll

1453

1467

1468+runTactical :: Context -> Env -> Term -> ElabD ()

1469+runTactical ctxt env tm = runTacTm (eval tm) >> return ()

1470+ where

1471+ eval = normaliseAll ctxt env

1472+ tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1473+ returnUnit = fmap fst $ get_type_val (Var unitCon)

1474+

1475+ -- | Do a step in the reflected elaborator monad. The input is the

1476+ -- step, the output is the (reflected) term returned.

1477+ runTacTm :: Term -> ElabD Term

1478+ runTacTm (unApply -> tac@(P _ n _, args))

1479+ | n == tacN "Solve", [] <- args

1480+ = do solve

1481+ returnUnit

1482+ | n == tacN "Goal", [] <- args

1483+ = do (h:_) <- get_holes

1484+ t <- goal

1485+ fmap fst . get_type_val $

1486+ rawPair (Var (reflm "TTName"), Var (reflm "TT"))

1487+ (reflectName h, reflect t)

1488+ | n == tacN "Holes", [] <- args

1489+ = do hs <- get_holes

1490+ fmap fst . get_type_val $

1491+ mkList (Var $ reflm "TTName") (map reflectName hs)

1492+ | n == tacN "Guess", [] <- args

1493+ = do ok <- is_guess

1494+ if ok

1495+ then do guess <- fmap forget get_guess

1496+ fmap fst . get_type_val $

1497+ RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))

1498+ (Var (reflm "TT")))

1499+ guess

1500+ else fmap fst . get_type_val $

1501+ RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

1502+ (Var (reflm "TT"))

1503+ | n == tacN "Env", [] <- args

1504+ = do env <- get_env

1505+ fmap fst . get_type_val $ reflectEnv env

1506+ | n == tacN "Fail", [_a, errs] <- args

1507+ = do parts <- reifyReportParts (eval errs)

1508+ lift . tfail $ ReflectionError [parts] (Msg "")

1509+ | n == tacN "PureTactical", [_a, tm] <- args

1510+ = return tm

1511+ | n == tacN "BindTactical", [_a, _b, first, andThen] <- args

1512+ = do let first' = eval first

1513+ res <- runTacTm first'

1514+ let next = eval (App andThen res)

1515+ runTacTm next

1516+ | n == tacN "Try", [_a, first, alt] <- args

1517+ = do let first' = eval first

1518+ let alt' = eval alt

1519+ try' (runTacTm first') (runTacTm alt') True

1520+ | n == tacN "Fill", [raw] <- args

1521+ = do raw' <- reifyRaw raw

1522+ apply raw' []

1523+ returnUnit

1524+ | n == tacN "Gensym", [eval -> Constant (Str hint)] <- args

1525+ = do n <- getNameFrom (sMN 0 hint)

1526+ fmap fst $ get_type_val (reflectName n)

1527+ | n == tacN "Claim", [n, ty] <- args

1528+ = do n' <- reifyTTName n

1529+ ty' <- reifyRaw ty

1530+ claim n' ty'

1531+ returnUnit

1532+ | n == tacN "Forget", [tt] <- args

1533+ = do tt' <- reifyTT tt

1534+ fmap fst . get_type_val $ reflect tt'

1535+ | n == tacN "Attack", [] <- args

1536+ = do attack

1537+ returnUnit

1538+ | n == tacN "Focus", [what] <- args

1539+ = do n' <- reifyTTName what

1540+ focus n'

1541+ returnUnit

1542+ | n == tacN "Unfocus", [what] <- args

1543+ = do n' <- reifyTTName what

1544+ movelast n'

1545+ returnUnit

1546+ runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1547+

1454-- Running tactics directly

1548-- Running tactics directly

1455-- if a tactic adds unification problems, return an error

1549-- if a tactic adds unification problems, return an error

1456

1550

@@ -1776,16 +1870,20 @@ reifyApp ist t [n, tt', t']

1776 t'' <- reifyTT t'

1870 t'' <- reifyTT t'

1777 return $ LetTacTy n' (delab ist tt'') (delab ist t'')

1871 return $ LetTacTy n' (delab ist tt'') (delab ist t'')

1778reifyApp ist t [errs]

1872reifyApp ist t [errs]

1779− | t == reflm "Fail" = case unList errs of

1873+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)

1780− Nothing -> fail "Failed to reify errors"

1781− Just errs' ->

1782− let parts = mapM reifyReportPart errs' in

1783− case parts of

1784− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err

1785− Right errs'' ->

1786− return $ TFail errs''

1787reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

1874reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

1788

1875

1876+reifyReportParts :: Term -> ElabD [ErrorReportPart]

1877+reifyReportParts errs =

1878+ case unList errs of

1879+ Nothing -> fail "Failed to reify errors"

1880+ Just errs' ->

1881+ let parts = mapM reifyReportPart errs' in

1882+ case parts of

1883+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err

1884+ Right errs'' ->

1885+ return errs''

1886+

1789-- | Reify terms from their reflected representation

1887-- | Reify terms from their reflected representation

1790reifyTT :: Term -> ElabD Term

1888reifyTT :: Term -> ElabD Term

1791reifyTT t@(App _ _)

1889reifyTT t@(App _ _)

src/Idris/IBC.hs+5−1

@@ -36,7 +36,7 @@ import Codec.Compression.Zlib (compress)

36import Util.Zlib (decompressEither)

38ibcVersion :: Word8

39−ibcVersion = 96

39+ibcVersion = 97

41data IBCFile = IBCFile { ver :: Word8,

42 sourcefile :: FilePath,

@@ -1571,6 +1571,8 @@ instance Binary PTerm where

1571 put x2

1572 PUniverse x1 -> do putWord8 38

1573 put x1

1574+ PRunTactics x1 -> do putWord8 39

1575+ put x1

1574

1576

1575 get

1577 get

1576 = do i <- getWord8

1578 = do i <- getWord8

@@ -1689,6 +1691,8 @@ instance Binary PTerm where

1689 return (PDisamb x1 x2)

1691 return (PDisamb x1 x2)

1690 38 -> do x1 <- get

1692 38 -> do x1 <- get

1691 return (PUniverse x1)

1693 return (PUniverse x1)

1694+ 39 -> do x1 <- get

1695+ return (PRunTactics x1)

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

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

1693

1697

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

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

src/Idris/IdrisDoc.hs+1

@@ -318,6 +318,7 @@ extractPTermNames (PCoerced p) = extract p

318extractPTermNames (PDisamb _ p) = extract p

319extractPTermNames (PUnifyLog p) = extract p

320extractPTermNames (PNoImplicits p) = extract p

321+extractPTermNames (PRunTactics p) = extract p

321extractPTermNames _ = []

322extractPTermNames _ = []

322

323

323-- | Shorter name for extractPTermNames

324-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+12

@@ -221,6 +221,7 @@ InternalExpr ::=

221internalExpr :: SyntaxInfo -> IdrisParser PTerm

222internalExpr syn =

223 unifyLog syn

224+ <|> runTactics syn

224 <|> disamb syn

225 <|> disamb syn

225 <|> noImplicits syn

226 <|> noImplicits syn

226 <|> recordType syn

227 <|> recordType syn

@@ -487,6 +488,17 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")

487 return (PUnifyLog tm)

488 return (PUnifyLog tm)

488 <?> "unification log expression"

489 <?> "unification log expression"

489

490

491+{- | Parses a new-style tactics expression

492+RunTactics ::=

493+ '%' 'runTactics' SimpleExpr

494+ ;

495+-}

496+runTactics :: SyntaxInfo -> IdrisParser PTerm

497+runTactics syn = do try (lchar '%' *> reserved "runTactics")

498+ tm <- simpleExpr syn

499+ return (PRunTactics tm)

500+ <?> "new-style tactics expression"

501+

490{- | Parses a disambiguation expression

502{- | Parses a disambiguation expression

491Disamb ::=

503Disamb ::=

492 '%' 'disamb' NameList Expr

504 '%' 'disamb' NameList Expr