30fe374 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1932 from david-christiansen/wip/tactical

30fe374David Christiansen12 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -5,6 +5,9 @@ New in 0.9.17:

5* A new tactic "claim N TY" that introduces a new hole named N with type TY

6* A new tactic "unfocus" that moves the current hole to the bottom of the

7 hole stack

8+* Quasiquotation supports the generation of Language.Reflection.Raw terms

9+ in addition to Language.Reflection.TT. Types are used for disambiguation,

10+ defaulting to TT at the REPL.

9New in 0.9.16:

12New in 0.9.16:

10--------------

13--------------

idris.cabal+3

@@ -513,6 +513,9 @@ Extra-source-files:

513 test/quasiquote004/run

514 test/quasiquote004/*.idr

515 test/quasiquote004/expected

516+ test/quasiquote005/run

517+ test/quasiquote005/*.idr

518+ test/quasiquote005/expected

516

519

517

520

518 test/records001/run

521 test/records001/run

libs/prelude/Language/Reflection.idr+16−3

@@ -49,7 +49,7 @@ data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

49 | B32V Bits32x4 | B64V Bits64x2

50 | AType ArithTy | StrType

52−

52+ | WorldType | TheWorld

53%name Const c, c'

55abstract class ReflConst (a : Type) where

@@ -146,6 +146,8 @@ instance Traversable Binder where

146 traverse f (PVar x) = [| PVar (f x) |]

147 traverse f (PVTy x) = [| PVTy (f x) |]

148

149+||| Universes

150+data Universe = NullType | UniqueType | AllTypes

149

151

150||| Reflection of the well typed core language

152||| Reflection of the well typed core language

151data TT =

153data TT =

@@ -166,7 +168,8 @@ data TT =

166 ||| Impossible terms

168 ||| Impossible terms

167 Impossible |

169 Impossible |

168 ||| The type of types along (with universe constraints)

170 ||| The type of types along (with universe constraints)

169− TType TTUExp

171+ TType TTUExp |

172+ UType Universe

170%name TT tm, tm'

173%name TT tm, tm'

171

174

172||| Raw terms without types

175||| Raw terms without types

@@ -179,6 +182,7 @@ data Raw =

179 RApp Raw Raw |

182 RApp Raw Raw |

180 ||| The type of types

183 ||| The type of types

181 RType |

184 RType |

185+ RUType Universe |

182 RForce Raw |

186 RForce Raw |

183 ||| Embed a constant

187 ||| Embed a constant

184 RConstant Const

188 RConstant Const

@@ -399,13 +403,20 @@ instance Quotable Const where

399 quote BufferType = `(BufferType)

403 quote BufferType = `(BufferType)

400 quote VoidType = `(VoidType)

404 quote VoidType = `(VoidType)

401 quote Forgot = `(Forgot)

405 quote Forgot = `(Forgot)

402−

406+ quote WorldType = `(WorldType)

407+ quote TheWorld = `(TheWorld)

403

408

404instance Quotable TTUExp where

409instance Quotable TTUExp where

405 quotedTy = `(TTUExp)

410 quotedTy = `(TTUExp)

406 quote (UVar x) = `(UVar ~(quote x))

411 quote (UVar x) = `(UVar ~(quote x))

407 quote (UVal x) = `(UVal ~(quote x))

412 quote (UVal x) = `(UVal ~(quote x))

408

413

414+instance Quotable Universe where

415+ quotedTy = `(Universe)

416+ quote Reflection.NullType = `(NullType)

417+ quote Reflection.UniqueType = `(UniqueType)

418+ quote Reflection.AllTypes = `(AllTypes)

419+

409mutual

420mutual

410 instance Quotable TT where

421 instance Quotable TT where

411 quotedTy = `(TT)

422 quotedTy = `(TT)

@@ -418,6 +429,7 @@ mutual

418 quote Erased = `(Erased)

429 quote Erased = `(Erased)

419 quote Impossible = `(Impossible)

430 quote Impossible = `(Impossible)

420 quote (TType uexp) = `(TType ~(quote uexp))

431 quote (TType uexp) = `(TType ~(quote uexp))

432+ quote (UType u) = `(UType ~(quote u))

421

433

422 instance Quotable (Binder TT) where

434 instance Quotable (Binder TT) where

423 quotedTy = `(Binder TT)

435 quotedTy = `(Binder TT)

@@ -449,6 +461,7 @@ mutual

449 quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))

461 quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))

450 quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))

462 quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))

451 quoteRaw RType = `(RType)

463 quoteRaw RType = `(RType)

464+ quoteRaw (RUType u) = `(RUType ~(quote u))

452 quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))

465 quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))

453 quoteRaw (RConstant c) = `(RConstant ~(quote c))

466 quoteRaw (RConstant c) = `(RConstant ~(quote c))

454

467

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

@@ -0,0 +1,95 @@

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+abstract

12+data Tactical : Type -> Type where

13+ -- obligatory control stuff

14+ prim__PureTactical : a -> Tactical a

15+ prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b

16+

17+ prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a

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

19+

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

21+ prim__Goal : Tactical (TTName, TT)

22+ prim__Holes : Tactical (List TTName)

23+ prim__Guess : Tactical (Maybe TT)

24+

25+ prim__Forget : TT -> Tactical Raw

26+

27+ prim__Gensym : String -> Tactical TTName

28+

29+ prim__Solve : Tactical ()

30+ prim__Fill : Raw -> Tactical ()

31+ prim__Focus : TTName -> Tactical ()

32+ prim__Unfocus : TTName -> Tactical ()

33+ prim__Attack : Tactical ()

34+

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

36+

37+-------------

38+-- Public API

39+-------------

40+%access public

41+

42+instance Functor Tactical where

43+ map f t = prim__BindTactical t (\x => prim__PureTactical (f x))

44+

45+instance Applicative Tactical where

46+ pure x = prim__PureTactical x

47+ f <$> x = prim__BindTactical f $ \g =>

48+ prim__BindTactical x $ \y =>

49+ prim__PureTactical $ g y

50+

51+instance Alternative Tactical where

52+ empty = prim__Fail [TextPart "empty"]

53+ x <|> y = prim__Try x y

54+

55+instance Monad Tactical where

56+ x >>= f = prim__BindTactical x f

57+

58+fail : List ErrorReportPart -> Tactical a

59+fail err = prim__Fail err

60+

61+getEnv : Tactical (List (TTName, Binder TT))

62+getEnv = prim__Env

63+

64+getGoal : Tactical (TTName, TT)

65+getGoal = prim__Goal

66+

67+getHoles : Tactical (List TTName)

68+getHoles = prim__Holes

69+

70+getGuess : Tactical (Maybe TT)

71+getGuess = prim__Guess

72+

73+forgetTypes : TT -> Tactical Raw

74+forgetTypes tt = prim__Forget tt

75+

76+gensym : (hint : String) -> Tactical TTName

77+gensym hint = prim__Gensym hint

78+

79+solve : Tactical ()

80+solve = prim__Solve

81+

82+fill : Raw -> Tactical ()

83+fill tm = prim__Fill tm

84+

85+focus : (hole : TTName) -> Tactical ()

86+focus hole = prim__Focus hole

87+

88+unfocus : TTName -> Tactical ()

89+unfocus hole = prim__Unfocus hole

90+

91+attack : Tactical ()

92+attack = prim__Attack

93+

94+claim : TTName -> Raw -> Tactical ()

95+claim n ty = prim__Claim n ty

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 fc tm) = PRunTactics fc (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 fc 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 fc tm) = PRunTactics fc (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 fc ts) = liftM (PRunTactics fc ) (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 FC PTerm -- ^ %runTactics 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 x2) = rnf x1 `seq` rnf x2 `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 fc tm)

174+ = fmap (\(tm', ex) -> (PRunTactics fc 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+232−81

@@ -1,5 +1,5 @@

1−{-# LANGUAGE PatternGuards #-}

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

2−

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3module Idris.ElabTerm where

5import Idris.AbsSyntax

@@ -420,6 +420,7 @@ elab ist info emode opts fn tm

420 where -- if none work, take the error from the first

421 trySeq (x : xs) = let e1 = elab' ina fc x in

422 try' e1 (trySeq' e1 xs) True

423+ trySeq [] = fail "Nothing to try in sequence"

423 trySeq' deferr [] = proofFail deferr

424 trySeq' deferr [] = proofFail deferr

424 trySeq' deferr (x : xs)

425 trySeq' deferr (x : xs)

425 = try' (do elab' ina fc x

426 = try' (do elab' ina fc x

@@ -546,7 +547,8 @@ elab ist info emode opts fn tm

546 -- HACK: If the name leaks into its type, it may leak out of

547 -- HACK: If the name leaks into its type, it may leak out of

547 -- scope outside, so substitute in the outer scope.

548 -- scope outside, so substitute in the outer scope.

548 expandLet n (case lookup n env of

549 expandLet n (case lookup n env of

549− Just (Let t v) -> v)

550+ Just (Let t v) -> v

551+ other -> error ("Value not a let binding: " ++ show other))

550 solve

552 solve

551 elab' ina _ (PGoal fc r n sc) = do

553 elab' ina _ (PGoal fc r n sc) = do

552 rty <- goal

554 rty <- goal

@@ -955,13 +957,16 @@ elab ist info emode opts fn tm

955 elab' ina fc (PUnifyLog t) = do unifyLog True

957 elab' ina fc (PUnifyLog t) = do unifyLog True

956 elab' ina fc t

958 elab' ina fc t

957 unifyLog False

959 unifyLog False

958− elab' ina fc (PQuasiquote t goal) -- TODO: goal type

960+ elab' ina fc (PQuasiquote t goal)

959 = do -- First extract the unquoted subterms, replacing them with fresh

961 = do -- First extract the unquoted subterms, replacing them with fresh

960 -- names in the quasiquoted term. Claim their reflections to be

962 -- names in the quasiquoted term. Claim their reflections to be

961− -- of type TT.

963+ -- an inferred type (to support polytypic quasiquotes).

962 (t, unq) <- extractUnquotes 0 t

964 (t, unq) <- extractUnquotes 0 t

963 let unquoteNames = map fst unq

965 let unquoteNames = map fst unq

966+ mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")

967+ claim uqh RType

968+ movelast uqh

964− mapM_ (flip claim (Var tt)) unquoteNames

969+ claim uqn (Var uqh)) unquoteNames

965

970

966

971

967 -- Save the old state - we need a fresh proof state to avoid

972 -- Save the old state - we need a fresh proof state to avoid

@@ -1017,9 +1022,14 @@ elab ist info emode opts fn tm

1017 Just q -> do ctxt <- get_context

1022 Just q -> do ctxt <- get_context

1018 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1023 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1019 if pattern

1024 if pattern

1020− then reflectQuotePattern unquoteNames q'

1025+ then reflectTTQuotePattern unquoteNames q'

1026+ -- TODO: support quasiquote patterns of Raw terms

1027+ else do try' (fill $ reflectTTQuote unquoteNames q')

1028+ -- we forget q' instead of using q to ensure rechecking

1021− else do fill $ reflectQuote unquoteNames q'

1029+ (fill $ reflectRawQuote unquoteNames (forget q'))

1030+ True -- ignore errors like proof search does

1022 solve

1031 solve

1032+

1023 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

1033 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

1024

1034

1025 -- Finally fill in the terms or patterns from the unquotes. This

1035 -- Finally fill in the terms or patterns from the unquotes. This

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

1049 delayElab $ do focus h

1059 delayElab $ do focus h

1050 dotterm

1060 dotterm

1051 elab' ina fc t

1061 elab' ina fc t

1062+ elab' ina _ (PRunTactics fc tm) =

1063+ do attack

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

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

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

1067+ claim n scriptTy

1068+ movelast n

1069+ letbind n' scriptTy (Var n)

1070+ focus n

1071+ elab' ina (Just fc) tm

1072+ env <- get_env

1073+ ctxt <- get_context

1074+ runTactical fc ctxt env (P Bound n' Erased)

1075+ solve

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

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

1053

1077

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

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

@@ -1072,6 +1096,7 @@ elab ist info emode opts fn tm

1072 findScr [(n, (_, t))] = [(n, (True, t))]

1096 findScr [(n, (_, t))] = [(n, (True, t))]

1073 findScr (x : xs) = x : findScr xs

1097 findScr (x : xs) = x : findScr xs

1074 -- [] can't happen since scrutinee is in the environment!

1098 -- [] can't happen since scrutinee is in the environment!

1099+ findScr [] = error "The impossible happened - the scrutinee was not in the environment"

1075

1100

1076 -- To make sure top level pattern name remains in scope, put

1101 -- To make sure top level pattern name remains in scope, put

1077 -- it at the end of the environment

1102 -- it at the end of the environment

@@ -1233,7 +1258,8 @@ elab ist info emode opts fn tm

1233 lift (tfail (elaboratingArgErr while' e))

1258 lift (tfail (elaboratingArgErr while' e))

1234 put newState

1259 put newState

1235 return result

1260 return result

1236−

1261+ elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =

1262+ fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole

1237

1263

1238-- For every alternative, look at the function at the head. Automatically resolve

1264-- For every alternative, look at the function at the head. Automatically resolve

1239-- any nested alternatives where that function is also at the head

1265-- any nested alternatives where that function is also at the head

@@ -1411,6 +1437,7 @@ resTC' tcs defaultOn depth topg fn ist

1411 let imps = case lookupCtxtName n (idris_implicits ist) of

1437 let imps = case lookupCtxtName n (idris_implicits ist) of

1412 [] -> []

1438 [] -> []

1413 [args] -> map isImp (snd args) -- won't be overloaded!

1439 [args] -> map isImp (snd args) -- won't be overloaded!

1440+ xs -> error "The impossible happened - overloading is not expected here!"

1414 ps <- get_probs

1441 ps <- get_probs

1415 tm <- get_term

1442 tm <- get_term

1416 args <- map snd <$> try' (apply (Var n) imps)

1443 args <- map snd <$> try' (apply (Var n) imps)

@@ -1471,6 +1498,86 @@ case_ ind autoSolve ist fn tm = do

1471 else casetac (forget val)

1498 else casetac (forget val)

1472 when autoSolve solveAll

1499 when autoSolve solveAll

1473

1500

1501+runTactical :: FC -> Context -> Env -> Term -> ElabD ()

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

1503+ where

1504+ eval = normaliseAll ctxt env

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

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

1507+

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

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

1510+ runTacTm :: Term -> ElabD Term

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

1512+ | n == tacN "prim__Solve", [] <- args

1513+ = do solve

1514+ returnUnit

1515+ | n == tacN "prim__Goal", [] <- args

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

1517+ t <- goal

1518+ fmap fst . get_type_val $

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

1520+ (reflectName h, reflect t)

1521+ | n == tacN "prim__Holes", [] <- args

1522+ = do hs <- get_holes

1523+ fmap fst . get_type_val $

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

1525+ | n == tacN "prim__Guess", [] <- args

1526+ = do ok <- is_guess

1527+ if ok

1528+ then do guess <- fmap forget get_guess

1529+ fmap fst . get_type_val $

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

1531+ (Var (reflm "TT")))

1532+ guess

1533+ else fmap fst . get_type_val $

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

1535+ (Var (reflm "TT"))

1536+ | n == tacN "prim__Env", [] <- args

1537+ = do env <- get_env

1538+ fmap fst . get_type_val $ reflectEnv env

1539+ | n == tacN "prim__Fail", [_a, errs] <- args

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

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

1542+ | n == tacN "prim__PureTactical", [_a, tm] <- args

1543+ = return tm

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

1545+ = do let first' = eval first

1546+ res <- runTacTm first'

1547+ let next = eval (App andThen res)

1548+ runTacTm next

1549+ | n == tacN "prim__Try", [_a, first, alt] <- args

1550+ = do let first' = eval first

1551+ let alt' = eval alt

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

1553+ | n == tacN "prim__Fill", [raw] <- args

1554+ = do raw' <- reifyRaw raw

1555+ apply raw' []

1556+ returnUnit

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

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

1559+ fmap fst $ get_type_val (reflectName n)

1560+ | n == tacN "prim__Claim", [n, ty] <- args

1561+ = do n' <- reifyTTName n

1562+ ty' <- reifyRaw ty

1563+ claim n' ty'

1564+ returnUnit

1565+ | n == tacN "prim__Forget", [tt] <- args

1566+ = do tt' <- reifyTT tt

1567+ fmap fst . get_type_val $ reflect tt'

1568+ | n == tacN "prim__Attack", [] <- args

1569+ = do attack

1570+ returnUnit

1571+ | n == tacN "prim__Focus", [what] <- args

1572+ = do n' <- reifyTTName what

1573+ focus n'

1574+ returnUnit

1575+ | n == tacN "prim__Unfocus", [what] <- args

1576+ = do n' <- reifyTTName what

1577+ movelast n'

1578+ returnUnit

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

1580+

1474-- Running tactics directly

1581-- Running tactics directly

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

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

1476

1583

@@ -1796,16 +1903,20 @@ reifyApp ist t [n, tt', t']

1796 t'' <- reifyTT t'

1903 t'' <- reifyTT t'

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

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

1798reifyApp ist t [errs]

1905reifyApp ist t [errs]

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

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

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

1801− Just errs' ->

1802− let parts = mapM reifyReportPart errs' in

1803− case parts of

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

1805− Right errs'' ->

1806− return $ TFail errs''

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

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

1808

1908

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

1910+reifyReportParts errs =

1911+ case unList errs of

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

1913+ Just errs' ->

1914+ let parts = mapM reifyReportPart errs' in

1915+ case parts of

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

1917+ Right errs'' ->

1918+ return errs''

1919+

1809-- | Reify terms from their reflected representation

1920-- | Reify terms from their reflected representation

1810reifyTT :: Term -> ElabD Term

1921reifyTT :: Term -> ElabD Term

1811reifyTT t@(App _ _)

1922reifyTT t@(App _ _)

@@ -1985,6 +2096,7 @@ reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

1985reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

2096reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

1986reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)

2097reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)

1987 (reifyNativeTy nt)

2098 (reifyNativeTy nt)

2099+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

1988

2100

1989reifyTTUExp :: Term -> ElabD UExp

2101reifyTTUExp :: Term -> ElabD UExp

1990reifyTTUExp t@(App _ _)

2102reifyTTUExp t@(App _ _)

@@ -2001,7 +2113,11 @@ reflCall funName args

2001

2113

2002-- | Lift a term into its Language.Reflection.TT representation

2114-- | Lift a term into its Language.Reflection.TT representation

2003reflect :: Term -> Raw

2115reflect :: Term -> Raw

2004−reflect = reflectQuote []

2116+reflect = reflectTTQuote []

2117+

2118+-- | Lift a term into its Language.Reflection.Raw representation

2119+reflectRaw :: Raw -> Raw

2120+reflectRaw = reflectRawQuote []

2005

2121

2006claimTT :: Name -> ElabD Name

2122claimTT :: Name -> ElabD Name

2007claimTT n = do n' <- getNameFrom n

2123claimTT n = do n' <- getNameFrom n

@@ -2012,8 +2128,8 @@ claimTT n = do n' <- getNameFrom n

2012-- In particular, the less-interesting bits are elaborated to _ patterns. This

2128-- In particular, the less-interesting bits are elaborated to _ patterns. This

2013-- happens to NameTypes, universe levels, names that are bound but not used,

2129-- happens to NameTypes, universe levels, names that are bound but not used,

2014-- and the type annotation field of the P constructor.

2130-- and the type annotation field of the P constructor.

2015−reflectQuotePattern :: [Name] -> Term -> ElabD ()

2131+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()

2016−reflectQuotePattern unq (P _ n _)

2132+reflectTTQuotePattern unq (P _ n _)

2017 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

2133 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

2018 do fill (Var n) ; solve

2134 do fill (Var n) ; solve

2019 | otherwise =

2135 | otherwise =

@@ -2027,10 +2143,10 @@ reflectQuotePattern unq (P _ n _)

2027 fill $ reflCall "P" [Var nt, Var n', Var tyannot]

2143 fill $ reflCall "P" [Var nt, Var n', Var tyannot]

2028 solve

2144 solve

2029 focus n'; reflectNameQuotePattern n

2145 focus n'; reflectNameQuotePattern n

2030−reflectQuotePattern unq (V n)

2146+reflectTTQuotePattern unq (V n)

2031 = do fill $ reflCall "V" [RConstant (I n)]

2147 = do fill $ reflCall "V" [RConstant (I n)]

2032 solve

2148 solve

2033−reflectQuotePattern unq (Bind n b x)

2149+reflectTTQuotePattern unq (Bind n b x)

2034 = do x' <- claimTT (sMN 0 "sc")

2150 = do x' <- claimTT (sMN 0 "sc")

2035 movelast x'

2151 movelast x'

2036 b' <- getNameFrom (sMN 0 "binder")

2152 b' <- getNameFrom (sMN 0 "binder")

@@ -2050,7 +2166,7 @@ reflectQuotePattern unq (Bind n b x)

2050 Var b',

2166 Var b',

2051 Var x']

2167 Var x']

2052 solve

2168 solve

2053− focus x'; reflectQuotePattern unq x

2169+ focus x'; reflectTTQuotePattern unq x

2054 focus b'; reflectBinderQuotePattern unq b

2170 focus b'; reflectBinderQuotePattern unq b

2055

2171

2056 where

2172 where

@@ -2059,102 +2175,136 @@ reflectQuotePattern unq (Bind n b x)

2059 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2175 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2060 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

2176 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

2061 solve

2177 solve

2062− focus t'; reflectQuotePattern unq t

2178+ focus t'; reflectTTQuotePattern unq t

2063 reflectBinderQuotePattern unq (Pi _ t k)

2179 reflectBinderQuotePattern unq (Pi _ t k)

2064 = do t' <- claimTT (sMN 0 "ty") ; movelast t'

2180 = do t' <- claimTT (sMN 0 "ty") ; movelast t'

2065 k' <- claimTT (sMN 0 "k"); movelast k';

2181 k' <- claimTT (sMN 0 "k"); movelast k';

2066 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

2182 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

2067 solve

2183 solve

2068− focus t'; reflectQuotePattern unq t

2184+ focus t'; reflectTTQuotePattern unq t

2069 reflectBinderQuotePattern unq (Let x y)

2185 reflectBinderQuotePattern unq (Let x y)

2070 = do x' <- claimTT (sMN 0 "ty"); movelast x';

2186 = do x' <- claimTT (sMN 0 "ty"); movelast x';

2071 y' <- claimTT (sMN 0 "v"); movelast y';

2187 y' <- claimTT (sMN 0 "v"); movelast y';

2072 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

2188 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

2073 solve

2189 solve

2074− focus x'; reflectQuotePattern unq x

2190+ focus x'; reflectTTQuotePattern unq x

2075− focus y'; reflectQuotePattern unq y

2191+ focus y'; reflectTTQuotePattern unq y

2076 reflectBinderQuotePattern unq (NLet x y)

2192 reflectBinderQuotePattern unq (NLet x y)

2077 = do x' <- claimTT (sMN 0 "ty"); movelast x'

2193 = do x' <- claimTT (sMN 0 "ty"); movelast x'

2078 y' <- claimTT (sMN 0 "v"); movelast y'

2194 y' <- claimTT (sMN 0 "v"); movelast y'

2079 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

2195 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

2080 solve

2196 solve

2081− focus x'; reflectQuotePattern unq x

2197+ focus x'; reflectTTQuotePattern unq x

2082− focus y'; reflectQuotePattern unq y

2198+ focus y'; reflectTTQuotePattern unq y

2083 reflectBinderQuotePattern unq (Hole t)

2199 reflectBinderQuotePattern unq (Hole t)

2084 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2200 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2085 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

2201 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

2086 solve

2202 solve

2087− focus t'; reflectQuotePattern unq t

2203+ focus t'; reflectTTQuotePattern unq t

2088 reflectBinderQuotePattern unq (GHole _ t)

2204 reflectBinderQuotePattern unq (GHole _ t)

2089 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2205 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2090 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

2206 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

2091 solve

2207 solve

2092− focus t'; reflectQuotePattern unq t

2208+ focus t'; reflectTTQuotePattern unq t

2093 reflectBinderQuotePattern unq (Guess x y)

2209 reflectBinderQuotePattern unq (Guess x y)

2094 = do x' <- claimTT (sMN 0 "ty"); movelast x'

2210 = do x' <- claimTT (sMN 0 "ty"); movelast x'

2095 y' <- claimTT (sMN 0 "v"); movelast y'

2211 y' <- claimTT (sMN 0 "v"); movelast y'

2096 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

2212 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

2097 solve

2213 solve

2098− focus x'; reflectQuotePattern unq x

2214+ focus x'; reflectTTQuotePattern unq x

2099− focus y'; reflectQuotePattern unq y

2215+ focus y'; reflectTTQuotePattern unq y

2100 reflectBinderQuotePattern unq (PVar t)

2216 reflectBinderQuotePattern unq (PVar t)

2101 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2217 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2102 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

2218 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

2103 solve

2219 solve

2104− focus t'; reflectQuotePattern unq t

2220+ focus t'; reflectTTQuotePattern unq t

2105 reflectBinderQuotePattern unq (PVTy t)

2221 reflectBinderQuotePattern unq (PVTy t)

2106 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2222 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2107 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

2223 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

2108 solve

2224 solve

2109− focus t'; reflectQuotePattern unq t

2225+ focus t'; reflectTTQuotePattern unq t

2110−reflectQuotePattern unq (App f x)

2226+reflectTTQuotePattern unq (App f x)

2111 = do f' <- claimTT (sMN 0 "f"); movelast f'

2227 = do f' <- claimTT (sMN 0 "f"); movelast f'

2112 x' <- claimTT (sMN 0 "x"); movelast x'

2228 x' <- claimTT (sMN 0 "x"); movelast x'

2113 fill $ reflCall "App" [Var f', Var x']

2229 fill $ reflCall "App" [Var f', Var x']

2114 solve

2230 solve

2115− focus f'; reflectQuotePattern unq f

2231+ focus f'; reflectTTQuotePattern unq f

2116− focus x'; reflectQuotePattern unq x

2232+ focus x'; reflectTTQuotePattern unq x

2117−reflectQuotePattern unq (Constant c)

2233+reflectTTQuotePattern unq (Constant c)

2118 = do fill $ reflCall "TConst" [reflectConstant c]

2234 = do fill $ reflCall "TConst" [reflectConstant c]

2119 solve

2235 solve

2120−reflectQuotePattern unq (Proj t i)

2236+reflectTTQuotePattern unq (Proj t i)

2121 = do t' <- claimTT (sMN 0 "t"); movelast t'

2237 = do t' <- claimTT (sMN 0 "t"); movelast t'

2122 fill $ reflCall "Proj" [Var t', RConstant (I i)]

2238 fill $ reflCall "Proj" [Var t', RConstant (I i)]

2123 solve

2239 solve

2124− focus t'; reflectQuotePattern unq t

2240+ focus t'; reflectTTQuotePattern unq t

2125−reflectQuotePattern unq (Erased)

2241+reflectTTQuotePattern unq (Erased)

2126 = do erased <- claimTT (sMN 0 "erased")

2242 = do erased <- claimTT (sMN 0 "erased")

2127 movelast erased

2243 movelast erased

2128 fill $ (Var erased)

2244 fill $ (Var erased)

2129 solve

2245 solve

2130−reflectQuotePattern unq (Impossible)

2246+reflectTTQuotePattern unq (Impossible)

2131 = do fill $ Var (reflm "Impossible")

2247 = do fill $ Var (reflm "Impossible")

2132 solve

2248 solve

2133−reflectQuotePattern unq (TType exp)

2249+reflectTTQuotePattern unq (TType exp)

2134 = do ue <- getNameFrom (sMN 0 "uexp")

2250 = do ue <- getNameFrom (sMN 0 "uexp")

2135 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

2251 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

2136 movelast ue

2252 movelast ue

2137 fill $ reflCall "TType" [Var ue]

2253 fill $ reflCall "TType" [Var ue]

2138 solve

2254 solve

2255+reflectTTQuotePattern unq (UType u)

2256+ = do uH <- getNameFrom (sMN 0 "someUniv")

2257+ claim uH (Var (reflm "Universe"))

2258+ movelast uH

2259+ fill $ reflCall "UType" [Var uH]

2260+ solve

2261+ focus uH

2262+ fill (Var (reflm (case u of

2263+ NullType -> "NullType"

2264+ UniqueType -> "UniqueType"

2265+ AllTypes -> "AllTypes")))

2266+ solve

2139

2267

2268+reflectUniverse :: Universe -> Raw

2269+reflectUniverse u =

2270+ (Var (reflm (case u of

2271+ NullType -> "NullType"

2272+ UniqueType -> "UniqueType"

2273+ AllTypes -> "AllTypes")))

2274+

2140−-- | Create a reflected term, but leave refs to the provided name intact

2275+-- | Create a reflected TT term, but leave refs to the provided name intact

2141−reflectQuote :: [Name] -> Term -> Raw

2276+reflectTTQuote :: [Name] -> Term -> Raw

2142−reflectQuote unq (P nt n t)

2277+reflectTTQuote unq (P nt n t)

2143 | n `elem` unq = Var n

2278 | n `elem` unq = Var n

2144− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]

2279+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]

2145−reflectQuote unq (V n)

2280+reflectTTQuote unq (V n)

2146 = reflCall "V" [RConstant (I n)]

2281 = reflCall "V" [RConstant (I n)]

2147−reflectQuote unq (Bind n b x)

2282+reflectTTQuote unq (Bind n b x)

2148− = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]

2283+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]

2149−reflectQuote unq (App f x)

2284+reflectTTQuote unq (App f x)

2150− = reflCall "App" [reflectQuote unq f, reflectQuote unq x]

2285+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2151−reflectQuote unq (Constant c)

2286+reflectTTQuote unq (Constant c)

2152 = reflCall "TConst" [reflectConstant c]

2287 = reflCall "TConst" [reflectConstant c]

2153−reflectQuote unq (Proj t i)

2288+reflectTTQuote unq (Proj t i)

2154− = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]

2289+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]

2155−reflectQuote unq (Erased) = Var (reflm "Erased")

2290+reflectTTQuote unq (Erased) = Var (reflm "Erased")

2156−reflectQuote unq (Impossible) = Var (reflm "Impossible")

2291+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")

2157−reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

2292+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

2293+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]

2294+

2295+reflectRawQuote :: [Name] -> Raw -> Raw

2296+reflectRawQuote unq (Var n)

2297+ | n `elem` unq = Var n

2298+ | otherwise = reflCall "Var" [reflectName n]

2299+reflectRawQuote unq (RBind n b r) =

2300+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]

2301+reflectRawQuote unq (RApp f x) =

2302+ reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2303+reflectRawQuote unq RType = Var (reflm "RType")

2304+reflectRawQuote unq (RUType u) =

2305+ reflCall "RUType" [reflectUniverse u]

2306+reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]

2307+reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]

2158

2308

2159reflectNameType :: NameType -> Raw

2309reflectNameType :: NameType -> Raw

2160reflectNameType (Bound) = Var (reflm "Bound")

2310reflectNameType (Bound) = Var (reflm "Bound")

@@ -2205,27 +2355,27 @@ reflectNameQuotePattern _ -- for all other names, match any

2205 solve

2355 solve

2206

2356

2207reflectBinder :: Binder Term -> Raw

2357reflectBinder :: Binder Term -> Raw

2208−reflectBinder = reflectBinderQuote []

2358+reflectBinder = reflectBinderQuote reflectTTQuote []

2209−

2359+

2210−reflectBinderQuote :: [Name] -> Binder Term -> Raw

2360+reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2211−reflectBinderQuote unq (Lam t)

2361+reflectBinderQuote q unq (Lam t)

2212− = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]

2362+ = reflCall "Lam" [Var (reflm "TT"), q unq t]

2213−reflectBinderQuote unq (Pi _ t k)

2363+reflectBinderQuote q unq (Pi _ t k)

2214− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]

2364+ = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2215−reflectBinderQuote unq (Let x y)

2365+reflectBinderQuote q unq (Let x y)

2216− = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

2366+ = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2217−reflectBinderQuote unq (NLet x y)

2367+reflectBinderQuote q unq (NLet x y)

2218− = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

2368+ = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2219−reflectBinderQuote unq (Hole t)

2369+reflectBinderQuote q unq (Hole t)

2220− = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]

2370+ = reflCall "Hole" [Var (reflm "TT"), q unq t]

2221−reflectBinderQuote unq (GHole _ t)

2371+reflectBinderQuote q unq (GHole _ t)

2222− = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]

2372+ = reflCall "GHole" [Var (reflm "TT"), q unq t]

2223−reflectBinderQuote unq (Guess x y)

2373+reflectBinderQuote q unq (Guess x y)

2224− = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

2374+ = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2225−reflectBinderQuote unq (PVar t)

2375+reflectBinderQuote q unq (PVar t)

2226− = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]

2376+ = reflCall "PVar" [Var (reflm "TT"), q unq t]

2227−reflectBinderQuote unq (PVTy t)

2377+reflectBinderQuote q unq (PVTy t)

2228− = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]

2378+ = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2229

2379

2230mkList :: Raw -> [Raw] -> Raw

2380mkList :: Raw -> [Raw] -> Raw

2231mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2381mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2265,7 +2415,8 @@ reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")

2265reflectConstant BufferType = Var (reflm "BufferType")

2415reflectConstant BufferType = Var (reflm "BufferType")

2266reflectConstant VoidType = Var (reflm "VoidType")

2416reflectConstant VoidType = Var (reflm "VoidType")

2267reflectConstant Forgot = Var (reflm "Forgot")

2417reflectConstant Forgot = Var (reflm "Forgot")

2268−

2418+reflectConstant WorldType = Var (reflm "WorldType")

2419+reflectConstant TheWorld = Var (reflm "TheWorld")

2269

2420

2270reflectUExp :: UExp -> Raw

2421reflectUExp :: UExp -> Raw

2271reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

2422reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

src/Idris/IBC.hs+150−1

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

1{-# LANGUAGE TypeSynonymInstances #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3module Idris.IBC where

4module Idris.IBC where

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

36import Util.Zlib (decompressEither)

37import Util.Zlib (decompressEither)

38ibcVersion :: Word8

39ibcVersion :: Word8

39−ibcVersion = 96

40+ibcVersion = 98

41data IBCFile = IBCFile { ver :: Word8,

42data IBCFile = IBCFile { ver :: Word8,

42 sourcefile :: FilePath,

43 sourcefile :: FilePath,

@@ -610,6 +611,7 @@ instance Binary a => Binary (D.Block a) where

610 4 -> liftM3 D.CodeBlock get get get

611 4 -> liftM3 D.CodeBlock get get get

611 5 -> liftM D.HtmlBlock get

612 5 -> liftM D.HtmlBlock get

612 6 -> return D.HRule

613 6 -> return D.HRule

614+ _ -> error "Corrupted binary data for Block"

613

615

614instance Binary a => Binary (D.Inline a) where

616instance Binary a => Binary (D.Inline a) where

615 put (D.Str txt) = do putWord8 0 ; put txt

617 put (D.Str txt) = do putWord8 0 ; put txt

@@ -636,6 +638,7 @@ instance Binary a => Binary (D.Inline a) where

636 8 -> liftM3 D.Image get get get

638 8 -> liftM3 D.Image get get get

637 9 -> liftM D.Entity get

639 9 -> liftM D.Entity get

638 10 -> liftM D.RawHtml get

640 10 -> liftM D.RawHtml get

641+ _ -> error "Corrupted binary data for Inline"

639

642

640instance Binary CT.ListType where

643instance Binary CT.ListType where

641 put (CT.Bullet c) = putWord8 0 >> put c

644 put (CT.Bullet c) = putWord8 0 >> put c

@@ -644,6 +647,7 @@ instance Binary CT.ListType where

644 case i of

647 case i of

645 0 -> liftM CT.Bullet get

648 0 -> liftM CT.Bullet get

646 1 -> liftM2 CT.Numbered get get

649 1 -> liftM2 CT.Numbered get get

650+ _ -> error "Corrupted binary data for ListType"

647

651

648instance Binary CT.CodeAttr where

652instance Binary CT.CodeAttr where

649 put (CT.CodeAttr a b) = put a >> put b

653 put (CT.CodeAttr a b) = put a >> put b

@@ -656,6 +660,7 @@ instance Binary CT.NumWrapper where

656 case i of

660 case i of

657 0 -> return CT.PeriodFollowing

661 0 -> return CT.PeriodFollowing

658 1 -> return CT.ParenFollowing

662 1 -> return CT.ParenFollowing

663+ _ -> error "Corrupted binary data for NumWrapper"

659

664

660----- Generated by 'derive'

665----- Generated by 'derive'

661

666

@@ -868,6 +873,9 @@ instance Binary PReason where

868 put x1

873 put x1

869 NotProductive -> putWord8 5

874 NotProductive -> putWord8 5

870 BelieveMe -> putWord8 6

875 BelieveMe -> putWord8 6

876+ UseUndef x1 -> do putWord8 7

877+ put x1

878+ ExternalIO -> putWord8 8

871 get

879 get

872 = do i <- getWord8

880 = do i <- getWord8

873 case i of

881 case i of

@@ -880,6 +888,9 @@ instance Binary PReason where

880 return (Mutual x1)

888 return (Mutual x1)

881 5 -> return NotProductive

889 5 -> return NotProductive

882 6 -> return BelieveMe

890 6 -> return BelieveMe

891+ 7 -> do x1 <- get

892+ return (UseUndef x1)

893+ 8 -> return ExternalIO

883 _ -> error "Corrupted binary data for PReason"

894 _ -> error "Corrupted binary data for PReason"

884

895

885instance Binary Totality where

896instance Binary Totality where

@@ -913,6 +924,7 @@ instance Binary MetaInformation where

913 0 -> return EmptyMI

924 0 -> return EmptyMI

914 1 -> do x1 <- get

925 1 -> do x1 <- get

915 return (DataMI x1)

926 return (DataMI x1)

927+ _ -> error "Corrupted binary data for MetaInformation"

916

928

917instance Binary IBCFile where

929instance Binary IBCFile where

918 put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

930 put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

@@ -1019,6 +1031,7 @@ instance Binary DataOpt where

1019 1 -> return DefaultEliminator

1031 1 -> return DefaultEliminator

1020 2 -> return DataErrRev

1032 2 -> return DataErrRev

1021 3 -> return DefaultCaseFun

1033 3 -> return DefaultCaseFun

1034+ _ -> error "Corrupted binary data for DataOpt"

1022

1035

1023instance Binary FnOpt where

1036instance Binary FnOpt where

1024 put x

1037 put x

@@ -1038,6 +1051,8 @@ instance Binary FnOpt where

1038 CoveringFn -> putWord8 11

1051 CoveringFn -> putWord8 11

1039 NoImplicit -> putWord8 12

1052 NoImplicit -> putWord8 12

1040 Constructor -> putWord8 13

1053 Constructor -> putWord8 13

1054+ CExport x1 -> do putWord8 14

1055+ put x1

1041 get

1056 get

1042 = do i <- getWord8

1057 = do i <- getWord8

1043 case i of

1058 case i of

@@ -1056,6 +1071,8 @@ instance Binary FnOpt where

1056 11 -> return CoveringFn

1071 11 -> return CoveringFn

1057 12 -> return NoImplicit

1072 12 -> return NoImplicit

1058 13 -> return Constructor

1073 13 -> return Constructor

1074+ 14 -> do x1 <- get

1075+ return $ CExport x1

1059 _ -> error "Corrupted binary data for FnOpt"

1076 _ -> error "Corrupted binary data for FnOpt"

1060

1077

1061instance Binary Fixity where

1078instance Binary Fixity where

@@ -1249,6 +1266,20 @@ instance (Binary t) => Binary (PDecl' t) where

1249 put x4

1266 put x4

1250 put x5

1267 put x5

1251 put x6

1268 put x6

1269+ PSyntax x1 x2 -> do putWord8 13

1270+ put x1

1271+ put x2

1272+ PDirective x1 -> error "Cannot serialize PDirective"

1273+ PProvider x1 x2 x3 x4 -> do putWord8 15

1274+ put x1

1275+ put x2

1276+ put x3

1277+ put x4

1278+ PTransform x1 x2 x3 x4 -> do putWord8 16

1279+ put x1

1280+ put x2

1281+ put x3

1282+ put x4

1252 get

1283 get

1253 = do i <- getWord8

1284 = do i <- getWord8

1254 case i of

1285 case i of

@@ -1328,8 +1359,37 @@ instance (Binary t) => Binary (PDecl' t) where

1328 x5 <- get

1359 x5 <- get

1329 x6 <- get

1360 x6 <- get

1330 return (PPostulate x1 x2 x3 x4 x5 x6)

1361 return (PPostulate x1 x2 x3 x4 x5 x6)

1362+ 13 -> do x1 <- get

1363+ x2 <- get

1364+ return (PSyntax x1 x2)

1365+ 14 -> do error "Cannot deserialize PDirective"

1366+ 15 -> do x1 <- get

1367+ x2 <- get

1368+ x3 <- get

1369+ x4 <- get

1370+ return (PProvider x1 x2 x3 x4)

1371+ 16 -> do x1 <- get

1372+ x2 <- get

1373+ x3 <- get

1374+ x4 <- get

1375+ return (PTransform x1 x2 x3 x4)

1331 _ -> error "Corrupted binary data for PDecl'"

1376 _ -> error "Corrupted binary data for PDecl'"

1332

1377

1378+instance Binary t => Binary (ProvideWhat' t) where

1379+ put (ProvTerm x1 x2) = do putWord8 0

1380+ put x1

1381+ put x2

1382+ put (ProvPostulate x1) = do putWord8 1

1383+ put x1

1384+ get = do y <- getWord8

1385+ case y of

1386+ 0 -> do x1 <- get

1387+ x2 <- get

1388+ return (ProvTerm x1 x2)

1389+ 1 -> do x1 <- get

1390+ return (ProvPostulate x1)

1391+ _ -> error "Corrupted binary data for ProvideWhat"

1392+

1333instance Binary Using where

1393instance Binary Using where

1334 put (UImplicit x1 x2) = do putWord8 0; put x1; put x2

1394 put (UImplicit x1 x2) = do putWord8 0; put x1; put x2

1335 put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

1395 put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

@@ -1338,6 +1398,7 @@ instance Binary Using where

1338 case i of

1398 case i of

1339 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)

1399 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)

1340 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1400 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1401+ _ -> error "Corrupted binary data for Using"

1341

1402

1342instance Binary SyntaxInfo where

1403instance Binary SyntaxInfo where

1343 put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1404 put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

@@ -1452,6 +1513,7 @@ instance Binary PunInfo where

1452 0 -> return TypeOrTerm

1513 0 -> return TypeOrTerm

1453 1 -> return IsType

1514 1 -> return IsType

1454 2 -> return IsTerm

1515 2 -> return IsTerm

1516+ _ -> error "Corrupted binary data for PunInfo"

1455

1517

1456instance Binary PTerm where

1518instance Binary PTerm where

1457 put x

1519 put x

@@ -1571,6 +1633,21 @@ instance Binary PTerm where

1571 put x2

1633 put x2

1572 PUniverse x1 -> do putWord8 38

1634 PUniverse x1 -> do putWord8 38

1573 put x1

1635 put x1

1636+ PRunTactics x1 x2 -> do putWord8 39

1637+ put x1

1638+ put x2

1639+ PAs x1 x2 x3 -> do putWord8 40

1640+ put x1

1641+ put x2

1642+ put x3

1643+ PElabError x1 -> do putWord8 41

1644+ put x1

1645+ PQuasiquote x1 x2 -> do putWord8 42

1646+ put x1

1647+ put x2

1648+ PUnquote x1 -> do putWord8 43

1649+ put x1

1650+

1574

1651

1575 get

1652 get

1576 = do i <- getWord8

1653 = do i <- getWord8

@@ -1689,6 +1766,20 @@ instance Binary PTerm where

1689 return (PDisamb x1 x2)

1766 return (PDisamb x1 x2)

1690 38 -> do x1 <- get

1767 38 -> do x1 <- get

1691 return (PUniverse x1)

1768 return (PUniverse x1)

1769+ 39 -> do x1 <- get

1770+ x2 <- get

1771+ return (PRunTactics x1 x2)

1772+ 40 -> do x1 <- get

1773+ x2 <- get

1774+ x3 <- get

1775+ return (PAs x1 x2 x3)

1776+ 41 -> do x1 <- get

1777+ return (PElabError x1)

1778+ 42 -> do x1 <- get

1779+ x2 <- get

1780+ return (PQuasiquote x1 x2)

1781+ 43 -> do x1 <- get

1782+ return (PUnquote x1)

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

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

1693

1784

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

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

@@ -1742,6 +1833,35 @@ instance (Binary t) => Binary (PTactic' t) where

1742 CaseTac x1 -> do putWord8 23

1833 CaseTac x1 -> do putWord8 23

1743 put x1

1834 put x1

1744 SourceFC -> putWord8 24

1835 SourceFC -> putWord8 24

1836+ Intros -> putWord8 25

1837+ Equiv x1 -> do putWord8 26

1838+ put x1

1839+ Claim x1 x2 -> do putWord8 27

1840+ put x1

1841+ put x2

1842+ Unfocus -> putWord8 28

1843+ MatchRefine x1 -> do putWord8 29

1844+ put x1

1845+ LetTacTy x1 x2 x3 -> do putWord8 30

1846+ put x1

1847+ put x2

1848+ put x3

1849+ TCInstance -> putWord8 31

1850+ GoalType x1 x2 -> do putWord8 32

1851+ put x1

1852+ put x2

1853+ TCheck x1 -> do putWord8 33

1854+ put x1

1855+ TEval x1 -> do putWord8 34

1856+ put x1

1857+ TDocStr x1 -> do putWord8 35

1858+ put x1

1859+ TSearch x1 -> do putWord8 36

1860+ put x1

1861+ Skip -> putWord8 37

1862+ TFail x1 -> do putWord8 38

1863+ put x1

1864+ Abandon -> putWord8 39

1745 get

1865 get

1746 = do i <- getWord8

1866 = do i <- getWord8

1747 case i of

1867 case i of

@@ -1793,6 +1913,35 @@ instance (Binary t) => Binary (PTactic' t) where

1793 23 -> do x1 <- get

1913 23 -> do x1 <- get

1794 return (CaseTac x1)

1914 return (CaseTac x1)

1795 24 -> return SourceFC

1915 24 -> return SourceFC

1916+ 25 -> return Intros

1917+ 26 -> do x1 <- get

1918+ return (Equiv x1)

1919+ 27 -> do x1 <- get

1920+ x2 <- get

1921+ return (Claim x1 x2)

1922+ 28 -> return Unfocus

1923+ 29 -> do x1 <- get

1924+ return (MatchRefine x1)

1925+ 30 -> do x1 <- get

1926+ x2 <- get

1927+ x3 <- get

1928+ return (LetTacTy x1 x2 x3)

1929+ 31 -> return TCInstance

1930+ 32 -> do x1 <- get

1931+ x2 <- get

1932+ return (GoalType x1 x2)

1933+ 33 -> do x1 <- get

1934+ return (TCheck x1)

1935+ 34 -> do x1 <- get

1936+ return (TEval x1)

1937+ 35 -> do x1 <- get

1938+ return (TDocStr x1)

1939+ 36 -> do x1 <- get

1940+ return (TSearch x1)

1941+ 37 -> return Skip

1942+ 38 -> do x1 <- get

1943+ return (TFail x1)

1944+ 39 -> return Abandon

1796 _ -> error "Corrupted binary data for PTactic'"

1945 _ -> error "Corrupted binary data for PTactic'"

1797

1946

1798

1947

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+14

@@ -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,19 @@ 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+ fc <- getFC

499+ tm <- simpleExpr syn

500+ i <- get

501+ return $ debindApp syn (desugar syn i (PRunTactics fc tm))

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

503+

490{- | Parses a disambiguation expression

504{- | Parses a disambiguation expression

491Disamb ::=

505Disamb ::=

492 '%' 'disamb' NameList Expr

506 '%' 'disamb' NameList Expr

test/quasiquote005/Quasiquote005.idrnew file+9

@@ -0,0 +1,9 @@

1+module Quasiquote005

3+test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =

4+ RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))

5+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

6+ (Var (NS (UN "Z") ["Nat", "Prelude"]))))

7+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

8+ (Var (NS (UN "Z") ["Nat", "Prelude"])))

9+test = Refl

test/quasiquote005/expectednew file

No changes to the content.

test/quasiquote005/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --check --nocolour Quasiquote005.idr

3+rm -f *.ibc