git.iko.soy/Idris-dev
on master help sign in
Merge branch 'ImprovedReflection' of https://github.com/JanBessai/Idris-dev into JanBessai-ImprovedReflection

Conflicts: effects/Effects.idr

commitea6bb9a9f67f2f04116ad56f95067a991f06a9f0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 1 Apr 2013, 19:17 (14 years ago) parentf1e61da9822081
12 files changed+794−75
compare with master
unifiedsplit
Setup.hs+25−14 config.mk+4−1 contribs/tool-support/vim/syntax/idris.vim+1−1 effects/Effects.idr+10−10 idris.cabal+4−1 lib/Language/Reflection.idr+166−9 samples/reflection.idr+151 src/Idris/AbsSyntaxTree.hs+6−1 src/Idris/Completion.hs+2 src/Idris/ElabTerm.hs+406−33 src/Idris/IBC.hs+12−4 src/Idris/Parser.hs+7−1
Setup.hs+25−14
@@ -44,7 +44,7 @@ cleanJavaLib verbosity
4444 execPomExists <- doesFileExist ("java" </> "executable_pom.xml")
4545 when pomExists $ removeFile ("java" </> "executable_pom.xml")
4646
47−installStdLib pkg local verbosity copy
47+installStdLib pkg local withoutEffects verbosity copy
4848 = do let dirs = L.absoluteInstallDirs pkg local copy
4949 let idir = datadir dirs
5050 let icmd = idrisCmd local
@@ -54,11 +54,12 @@ installStdLib pkg local verbosity copy
5454 , "TARGET=" ++ idir
5555 , "IDRIS=" ++ icmd
5656 ]
57− make verbosity
58− [ "-C", "effects", "install"
59− , "TARGET=" ++ idir
60− , "IDRIS=" ++ icmd
61− ]
57+ unless withoutEffects $
58+ make verbosity
59+ [ "-C", "effects", "install"
60+ , "TARGET=" ++ idir
61+ , "IDRIS=" ++ icmd
62+ ]
6263 let idirRts = idir </> "rts"
6364 putStrLn $ "Installing run time system in " ++ idirRts
6465 make verbosity
@@ -93,17 +94,18 @@ removeLibIdris local verbosity
9394 , "IDRIS=" ++ icmd
9495 ]
9596
96−checkStdLib local verbosity
97+checkStdLib local withoutEffects verbosity
9798 = do let icmd = idrisCmd local
9899 putStrLn $ "Building libraries..."
99100 make verbosity
100101 [ "-C", "lib", "check"
101102 , "IDRIS=" ++ icmd
102103 ]
103− make verbosity
104− [ "-C", "effects", "check"
105− , "IDRIS=" ++ icmd
106− ]
104+ unless withoutEffects $
105+ make verbosity
106+ [ "-C", "effects", "check"
107+ , "IDRIS=" ++ icmd
108+ ]
107109 make verbosity
108110 [ "-C", "rts", "check"
109111 , "IDRIS=" ++ icmd
@@ -117,6 +119,12 @@ javaFlag flags =
117119 Just False -> False
118120 Nothing -> False
119121
122+noEffectsFlag flags =
123+ case lookup (FlagName "noeffects") (S.configConfigurationsFlags flags) of
124+ Just True -> True
125+ Just False -> False
126+ Nothing -> False
127+
120128preparePoms version
121129 = do pomTemplate <- TIO.readFile ("java" </> "pom_template.xml")
122130 TIO.writeFile ("java" </> "pom.xml") (insertVersion pomTemplate)
@@ -132,11 +140,13 @@ main = do
132140 defaultMainWithHooks $ simpleUserHooks
133141 { postCopy = \ _ flags pkg lbi -> do
134142 let verb = S.fromFlag $ S.copyVerbosity flags
135− installStdLib pkg lbi verb
143+ let withoutEffects = noEffectsFlag $ configFlags lbi
144+ installStdLib pkg lbi withoutEffects verb
136145 (S.fromFlag $ S.copyDest flags)
137146 , postInst = \ _ flags pkg lbi -> do
138147 let verb = (S.fromFlag $ S.installVerbosity flags)
139− installStdLib pkg lbi verb
148+ let withoutEffects = noEffectsFlag $ configFlags lbi
149+ installStdLib pkg lbi withoutEffects verb
140150 NoCopyDest
141151 when (javaFlag $ configFlags lbi)
142152 (installJavaLib pkg
@@ -155,6 +165,7 @@ main = do
155165 cleanJavaLib verb
156166 , postBuild = \ _ flags _ lbi -> do
157167 let verb = S.fromFlag $ S.buildVerbosity flags
158− checkStdLib lbi verb
168+ let withoutEffects = noEffectsFlag $ configFlags lbi
169+ checkStdLib lbi withoutEffects verb
159170 when (javaFlag $ configFlags lbi) (checkJavaLib verb)
160171 }
config.mk+4−1
@@ -1,6 +1,9 @@
11GMP_INCLUDE_DIR :=
22CC :=gcc
33CABAL :=cabal
4−CABALFLAGS :=
4+#CABALFLAGS :=
55## Enable Java RTS:
66#CABALFLAGS :=-f Java
7+## Disable building of Effects
8+#CABALFLAGS :=-f NoEffects
9+
contribs/tool-support/vim/syntax/idris.vim+1−1
@@ -15,7 +15,7 @@ syn match idrisAnnotation "\<\(total\|partial\|auto\|impossible\|static\|implici
1515syn match idrisStatement "\<\(do\|case\|of\|rewrite\|let\|in\|with\)\>"
1616syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
1717syn match idrisConditional "\<\(if\|then\|else\)\>"
18−syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\)\>"
18+syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\|fill\|applyTactic\)\>"
1919syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
2020syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
2121syn match idrisDelimiter "(\|)\|\[\|\]\|,\|;\|_\|{\|}"
effects/Effects.idr+10−10
@@ -59,19 +59,19 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
5959---- The Effect EDSL itself ----
6060
6161-- some proof automation
62−findEffElem : Nat -> Tactic -- Nat is maximum search depth
63−findEffElem O = Refine "Here" `Seq` Solve
64−findEffElem (S n) = GoalType "EffElem"
62+findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
63+findEffElem O ctxt goal = Refine "Here" `Seq` Solve
64+findEffElem (S n) ctxt goal = GoalType "EffElem"
6565 (Try (Refine "Here" `Seq` Solve)
66− (Refine "There" `Seq` (Solve `Seq` findEffElem n)))
66+ (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))
6767
68−findSubList : Nat -> Tactic
69−findSubList O = Refine "SubNil" `Seq` Solve
70−findSubList (S n)
68+findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic
69+findSubList O ctxt goal = Refine "SubNil" `Seq` Solve
70+findSubList (S n) ctxt goal
7171 = GoalType "SubList"
7272 (Try (Refine "subListId" `Seq` Solve)
7373 ((Try (Refine "Keep" `Seq` Solve)
74− (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))
74+ (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt goal))
7575
7676updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
7777 List EFFECT
@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->
116116-- Eff : List (EFFECT m) -> Type -> Type
117117
118118implicit
119−lift' : {default tactics { reflect findSubList 100; solve; }
119+lift' : {default tactics { applyTactic findSubList 100; solve; }
120120 prf : SubList ys xs} ->
121121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
122122lift' {prf} e = lift prf e
123123
124124implicit
125125effect' : {a, b: _} -> {e : Effect} ->
126− {default tactics { reflect findEffElem 100; solve; }
126+ {default tactics { applyTactic findEffElem 100; solve; }
127127 prf : EffElem e a xs} ->
128128 (eff : e a b t) ->
129129 EffM m xs (updateResTy xs prf eff) t
idris.cabal+4−1
@@ -65,7 +65,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
6565 config.mk
6666 rts/*.c rts/*.h rts/Makefile
6767 js/*.js
68− java/org/idris/rts/*.java
68+ java/org/idris/rts/*.java
6969
7070source-repository head
7171 type: git
@@ -75,6 +75,9 @@ Flag Java
7575 Description: Build the Java RTS
7676 Default: False
7777
78+Flag NoEffects
79+ Description: Do not build the effects package
80+ Default: False
7881
7982Executable idris
8083 Main-is: Main.hs
lib/Language/Reflection.idr+166−9
@@ -1,19 +1,176 @@
11module Language.Reflection
22
3−TTName : Type
4−TTName = String -- needs to capture namespaces too...
3+%access public
54
6−data TT = Var TTName
7− | Lam TTName TT TT
8− | Pi TTName TT TT
9− | Let TTName TT TT TT
10− | App TTName TT TT
5+data TTName = UN String
6+ -- ^ User-provided name
7+ | NS TTName (List String)
8+ -- ^ Root, namespaces
9+ | MN Int String
10+ -- ^ Machine chosen names
11+ | NErased
12+ -- ^ Name of somethng which is never used in scope
13+
14+implicit
15+userSuppliedName : String -> TTName
16+userSuppliedName = UN
17+
18+data TTUExp = UVar Int
19+ -- ^ universe variable
20+ | UVal Int
21+ -- ^ explicit universe variable
22+
23+-- | Primitive constants
24+data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
25+ | IType | BIType | FlType | ChType | StrType
26+ | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
27+ | B8Type | B16Type | B32Type | B64Type
28+ | PtrType | VoidType | Forgot
29+
30+abstract class ReflConst (a : Type) where
31+ toConst : a -> Const
32+
33+instance ReflConst Int where
34+ toConst x = I x
35+
36+instance ReflConst Nat where
37+ toConst = BI
38+
39+instance ReflConst Float where
40+ toConst = Fl
41+
42+instance ReflConst Char where
43+ toConst = Ch
44+
45+instance ReflConst String where
46+ toConst = Str
47+
48+instance ReflConst Bits8 where
49+ toConst = B8
50+
51+instance ReflConst Bits16 where
52+ toConst = B16
53+
54+instance ReflConst Bits32 where
55+ toConst = B32
56+
57+instance ReflConst Bits64 where
58+ toConst = B64
59+
60+implicit
61+reflectConstant: (ReflConst a) => a -> Const
62+reflectConstant = toConst
63+
64+
65+-- | Types of named references
66+data NameType = Bound
67+ -- ^ reference which is just bound, e.g. by intro
68+ | Ref
69+ -- ^ reference to a variable
70+ | DCon Int Int
71+ -- ^ constructor with tag and number
72+ | TCon Int Int
73+ -- ^ type constructor with tag and number
74+
75+-- | Types annotations for bound variables in different
76+-- binding contexts
77+data Binder a = Lam a
78+ | Pi a
79+ | Let a a
80+ | NLet a a
81+ | Hole a
82+ | GHole a
83+ | Guess a a
84+ | PVar a
85+ | PVTy a
86+
87+
88+instance Functor Binder where
89+ fmap f (Lam x) = Lam (f x)
90+ fmap f (Pi x) = Pi (f x)
91+ fmap f (Let x y) = Let (f x) (f y)
92+ fmap f (NLet x y) = NLet (f x) (f y)
93+ fmap f (Hole x) = Hole (f x)
94+ fmap f (GHole x) = GHole (f x)
95+ fmap f (Guess x y) = Guess (f x) (f y)
96+ fmap f (PVar x) = PVar (f x)
97+ fmap f (PVTy x) = PVTy (f x)
98+
99+total
100+traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
101+traverse f (Lam x) = [| Lam (f x) |]
102+traverse f (Pi x) = [| Pi (f x) |]
103+traverse f (Let x y) = [| Let (f x) (f y) |]
104+traverse f (NLet x y) = [| NLet (f x) (f y) |]
105+traverse f (Hole x) = [| Hole (f x) |]
106+traverse f (GHole x) = [| GHole (f x) |]
107+traverse f (Guess x y) = [| Guess (f x) (f y) |]
108+traverse f (PVar x) = [| PVar (f x) |]
109+traverse f (PVTy x) = [| PVTy (f x) |]
110+
111+
112+-- | Reflection of the well typed core language
113+data TT = P NameType TTName TT
114+ -- ^ named binders
115+ | V Int
116+ -- ^ variables
117+ | Bind TTName (Binder TT) TT
118+ -- ^ type annotated named bindings
119+ | App TT TT
120+ -- ^ (named) application of a function to a value
121+ | TConst Const
122+ -- ^ constants
123+ | Proj TT Int
124+ -- ^ argument projection; runtime only
125+ | Erased
126+ -- ^ erased terms
127+ | Impossible
128+ -- ^ impossible terms
129+ | TType TTUExp
130+ -- ^ types
131+
132+-- | Raw terms without types
133+data Raw = Var TTName
134+ | RBind TTName (Binder Raw) Raw
135+ | RApp Raw Raw
136+ | RType
137+ | RForce Raw
138+ | RConstant Const
11139
12140data Tactic = Try Tactic Tactic
13− | GoalType TTName Tactic -- only run if the goal has the right type
141+ -- ^ try the first tactic and resort to the second one on failure
142+ | GoalType String Tactic
143+ -- ^ only run if the goal has the right type
14144 | Refine TTName
145+ -- ^ resolve function name, find matching arguments in the
146+ -- context and compute the proof target
15147 | Seq Tactic Tactic
148+ -- ^ apply both tactics in sequence
16149 | Trivial
150+ -- ^ intelligently construct the proof target from the context
17151 | Solve
18− | Exact TT -- not yet implemented
152+ -- ^ infer the proof target from the context
153+ | Intros
154+ -- ^ introduce all variables into the context
155+ | Intro TTName
156+ -- ^ introduce a named variable into the context, use the
157+ -- first one if the given name is not found
158+ | ApplyTactic TT
159+ -- ^ invoke the reflected rep. of another tactic
160+ | Reflect TT
161+ -- ^ turn a value into its reflected representation
162+ | Fill Raw
163+ -- ^ turn a raw value back into a term
164+ | Exact TT
165+ -- ^ use the given value to conclude the proof
166+ | Focus TTName
167+ -- ^ focus a named hole
168+ | Rewrite TT
169+ -- ^ rewrite using the reflected rep. of a equality proof
170+ | LetTac TTName TT
171+ -- ^ name a reflected term
172+ | LetTacTy TTName TT TT
173+ -- ^ name a reflected term and type it
174+ | Compute
175+ -- ^ normalise the context
19176
samples/reflection.idrnew file+151
@@ -0,0 +1,151 @@
1+module ReflectionExamples
2+
3+import Language.Reflection
4+
5+-- | The reflected term for (\ x => reverse "bba")
6+reflectVal : TT
7+reflectVal = ?valPrf
8+
9+-- | intEq for the integers 3 and 3
10+applyTac1 : Int
11+applyTac1 = ?tacPrf1
12+
13+-- | intEq for the integers 3 and 42
14+applyTac0 : Int
15+applyTac0 = ?tacPrf0
16+
17+-- | intEq for the two arguments
18+applyTacDyn : Int -> Int -> Int
19+applyTacDyn x y = ?tacPrfDyn
20+
21+-- | Restored version for RConstant (I 42)
22+fill : Int
23+fill = ?fillPrf
24+
25+-- | The type (TTName, TT) computed from its reflected raw rep.
26+envTuple : Type
27+envTuple = ?envTuplePrf
28+
29+-- | The type List (TTName, TT) computed from its reflected raw rep.
30+envList : List (TTName, TT)
31+envList = ?envListPrf
32+
33+-- | Reflected raw rep. for the type (TTName, TT)
34+tupleType : Raw
35+tupleType = RApp (RApp (Var (MN 0 "__Pair"))
36+ (Var (NS (UN "TTName") ["Reflection", "Language"])))
37+ (Var (NS (UN "TT") ["Reflection", "Language"]))
38+
39+-- | Reflected raw rep for the type List (TTName, TT)
40+mkTuple : Raw
41+mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
42+ (Var (NS (UN "TTName") ["Reflection", "Language"])))
43+ (Var (NS (UN "TT") ["Reflection", "Language"]))
44+
45+-- | Reflected raw rep for Prelude.List.Nil
46+nil : Raw
47+nil = (Var (NS (UN "Nil") ["List", "Prelude"]))
48+
49+-- | Reflected raw rep for Prelude.List.::
50+cons : Raw
51+cons = (Var (NS (UN "::") ["List", "Prelude"]))
52+
53+-- | 1 if the two arguments are equal, 0 otherwise
54+-- This function is chosen as simple as possible for
55+-- demo purposes.
56+intEq : Int -> Int -> Int
57+intEq x y = case x == y of
58+ True => 1
59+ False => 0
60+
61+-- | A tactic script to run intEq on two let-bound or introduced
62+-- arguments of the current (otherwise empty) proof context
63+firstEq : List (TTName, Binder TT) -> TT -> Tactic
64+firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)
65+firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66+firstEq xs _ = Exact (TConst (I 0))
67+
68+-- | Skip 1 argument of the proof context and return the second one which
69+-- has to be introduced. Used for the tactical dispatch example, which
70+-- will push dispatch, as first env agrument.
71+innerTac : List (TTName, Binder TT) -> TT -> Tactic
72+innerTac (_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
73+
74+-- | Returns the reflected representation of innerTac
75+innerTacTT : TT
76+innerTacTT = ?innerTacTTPrf
77+
78+-- | Dispatch to the reflected rep. of innerTac
79+dispatch : List (TTName, Binder TT) -> TT -> Tactic
80+dispatch xs _ = ApplyTactic (innerTacTT)
81+
82+-- | Call dispatch which will then dispatch to innerTac.
83+tacticalDispatch : Int -> Int
84+tacticalDispatch = ?tacticalDispatchPrf
85+
86+-- | A tactic to get the representation of its goal
87+studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic
88+studyGoalTac _ goal = Reflect goal
89+
90+-- | Returns the representation of its goal, TT
91+-- (so this is reflect on the type TT)
92+studyGoal : TT
93+studyGoal = ?studyGoalPrf
94+
95+---------- Proofs ----------
96+
97+ReflectionExamples.studyGoalPrf = proof {
98+ applyTactic studyGoalTac;
99+}
100+
101+ReflectionExamples.envTuplePrf = proof {
102+ let x = tupleType;
103+ fill x;
104+}
105+
106+ReflectionExamples.envListPrf = proof {
107+ let x : Raw = RApp nil tupleType;
108+ fill x;
109+}
110+
111+
112+ReflectionExamples.valPrf = proof {
113+ let x : (List String -> String) = (\ x => reverse "bba");
114+ reflect x;
115+}
116+
117+
118+ReflectionExamples.tacPrf1 = proof {
119+ let f : (Int -> Int -> Int) = intEq;
120+ let x : Int = 3;
121+ let y : Int = 3;
122+ applyTactic firstEq;
123+}
124+
125+ReflectionExamples.tacPrf0 = proof {
126+ let f : (Int -> Int -> Int) = intEq;
127+ let x : Int = 3;
128+ let y : Int = 42;
129+ applyTactic firstEq;
130+}
131+
132+ReflectionExamples.tacPrfDyn = proof {
133+ let f : (Int -> Int -> Int) = intEq;
134+ intros;
135+ applyTactic firstEq;
136+}
137+
138+ReflectionExamples.fillPrf = proof {
139+ let x : Raw = RConstant (I 42);
140+ fill x;
141+}
142+
143+ReflectionExamples.innerTacTTPrf = proof {
144+ reflect innerTac;
145+}
146+
147+ReflectionExamples.tacticalDispatchPrf = proof {
148+ intros;
149+ applyTactic dispatch;
150+}
151+
src/Idris/AbsSyntaxTree.hs+6−1
@@ -529,7 +529,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
529529 | ProofState | ProofTerm | Undo
530530 | Try (PTactic' t) (PTactic' t)
531531 | TSeq (PTactic' t) (PTactic' t)
532− | ReflectTac t -- see Language.Reflection module
532+ | ApplyTactic t -- see Language.Reflection module
533+ | Reflect t
534+ | Fill t
533535 | GoalType String (PTactic' t)
534536 | Qed | Abandon
535537 deriving (Show, Eq, Functor)
@@ -554,6 +556,9 @@ instance Sized a => Sized (PTactic' a) where
554556 size Undo = 1
555557 size (Try l r) = 1 + size l + size r
556558 size (TSeq l r) = 1 + size l + size r
559+ size (ApplyTactic t) = 1 + size t
560+ size (Reflect t) = 1 + size t
561+ size (Fill t) = 1 + size t
557562 size Qed = 1
558563 size Abandon = 1
559564
src/Idris/Completion.hs+2
@@ -35,7 +35,9 @@ tacticArgs = [ ("intro", Nothing)
3535 , ("let", Nothing) -- FIXME syntax for let
3636 , ("focus", Just ExprTArg)
3737 , ("exact", Just ExprTArg)
38+ , ("applyTactic", Just ExprTArg)
3839 , ("reflect", Just ExprTArg)
40+ , ("fill", Just ExprTArg)
3941 , ("try", Just AltsTArg)
4042 ] ++ map (\x -> (x, Nothing)) [
4143 "intro", "intros", "compute", "trivial", "solve", "attack",
src/Idris/ElabTerm.hs+406−33
@@ -13,6 +13,7 @@ import Core.Evaluate
1313import Control.Monad
1414import Control.Monad.State
1515import Data.List
16+
1617import Debug.Trace
1718
1819-- Data to pass to recursively called elaborators; e.g. for where blocks,
@@ -774,22 +775,67 @@ runTac autoSolve ist tac = do env <- get_env
774775 runT Solve = solve
775776 runT (Try l r) = do try' (runT l) (runT r) True
776777 runT (TSeq l r) = do runT l; runT r
777− runT (ReflectTac tm) = do attack -- let x : Tactic = tm in ...
778− valn <- unique_hole (MN 0 "tacval")
779− claim valn (Var tacticTy)
780− tacn <- unique_hole (MN 0 "tacn")
781− letbind tacn (Var tacticTy) (Var valn)
782− focus valn
783− elab ist toplevel False False (MN 0 "tac") tm
784− (tm', ty') <- get_type_val (Var tacn)
785− ctxt <- get_context
786− env <- get_env
787− let tactic = normalise ctxt env tm'
788− runReflected tactic
789−-- p <- get_term
790−-- trace (show p ++ "\n\n") $
791− return ()
792− where tacticTy = tacm "Tactic"
778+ runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
779+ tgoal <- goal -- store the goal
780+ attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
781+ script <- unique_hole (MN 0 "script")
782+ claim script scriptTy
783+ scriptvar <- unique_hole (MN 0 "scriptvar" )
784+ letbind scriptvar scriptTy (Var script)
785+ focus script
786+ elab ist toplevel False False (MN 0 "tac") tm
787+ (script', _) <- get_type_val (Var scriptvar)
788+ -- now that we have the script apply
789+ -- it to the reflected goal and context
790+ restac <- unique_hole (MN 0 "restac")
791+ claim restac tacticTy
792+ focus restac
793+ fill (raw_apply (forget script')
794+ [reflectEnv tenv, reflect tgoal])
795+ restac' <- get_guess
796+ solve
797+ -- normalise the result in order to
798+ -- reify it
799+ ctxt <- get_context
800+ env <- get_env
801+ let tactic = normalise ctxt env restac'
802+ runReflected tactic
803+ where tacticTy = Var (reflm "Tactic")
804+ listTy = Var (NS (UN "List") ["List", "Prelude"])
805+ scriptTy = (RBind (UN "__pi_arg")
806+ (Pi (RApp listTy envTupleType))
807+ (RBind (UN "__pi_arg1")
808+ (Pi (Var $ reflm "TT")) tacticTy))
809+
810+ runT (Reflect v) = do attack -- let x = reflect v in ...
811+ tyn <- unique_hole (MN 0 "letty")
812+ claim tyn RType
813+ valn <- unique_hole (MN 0 "letval")
814+ claim valn (Var tyn)
815+ letn <- unique_hole (MN 0 "letvar")
816+ letbind letn (Var tyn) (Var valn)
817+ focus valn
818+ elab ist toplevel False False (MN 0 "tac") v
819+ (value, _) <- get_type_val (Var letn)
820+ ctxt <- get_context
821+ env <- get_env
822+ let value' = hnf ctxt env value
823+ runTac autoSolve ist (Exact $ PQuote (reflect value'))
824+ runT (Fill v) = do attack -- let x = fill x in ...
825+ tyn <- unique_hole (MN 0 "letty")
826+ claim tyn RType
827+ valn <- unique_hole (MN 0 "letval")
828+ claim valn (Var tyn)
829+ letn <- unique_hole (MN 0 "letvar")
830+ letbind letn (Var tyn) (Var valn)
831+ focus valn
832+ elab ist toplevel False False (MN 0 "tac") v
833+ (value, _) <- get_type_val (Var letn)
834+ ctxt <- get_context
835+ env <- get_env
836+ let value' = normalise ctxt env value
837+ rawValue <- reifyRaw value'
838+ runTac autoSolve ist (Exact $ PQuote rawValue)
793839 runT (GoalType n tac) = do g <- goal
794840 case unApply g of
795841 (P _ n' _, _) ->
@@ -799,24 +845,351 @@ runTac autoSolve ist tac = do env <- get_env
799845 _ -> fail "Wrong goal type"
800846 runT x = fail $ "Not implemented " ++ show x
801847
802− runReflected t = do t' <- reify t
848+ runReflected t = do t' <- reify ist t
803849 runTac autoSolve ist t'
804− tacm n = NS (UN n) ["Reflection", "Language"]
805−
806− reify :: Term -> ElabD PTactic
807− reify (P _ n _) | n == tacm "Trivial" = return Trivial
808− reify (P _ n _) | n == tacm "Solve" = return Solve
809− reify f@(App _ _)
810− | (P _ f _, args) <- unApply f = reifyAp f args
811− reify t = fail ("Unknown tactic " ++ show t)
812−
813− reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)
814− reifyAp t [Constant (Str x)]
815− | t == tacm "Refine" = return $ Refine (UN x) []
816− reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)
817− reifyAp t [Constant (Str n), x]
818− | t == tacm "GoalType" = liftM (GoalType n) (reify x)
819− reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
850+
851+-- | Prefix a name with the "Reflection.Language" namespace
852+reflm :: String -> Name
853+reflm n = NS (UN n) ["Reflection", "Language"]
854+
855+
856+-- | Reify tactics from their reflected representation
857+reify :: IState -> Term -> ElabD PTactic
858+reify _ (P _ n _) | n == reflm "Intros" = return Intros
859+reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
860+reify _ (P _ n _) | n == reflm "Solve" = return Solve
861+reify _ (P _ n _) | n == reflm "Compute" = return Compute
862+reify ist t@(App _ _)
863+ | (P _ f _, args) <- unApply t = reifyApp ist f args
864+reify _ t = fail ("Unknown tactic " ++ show t)
865+
866+reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
867+reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
868+reifyApp _ t [x]
869+ | t == reflm "Refine" = do n <- reifyTTName x
870+ return $ Refine n []
871+reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
872+reifyApp ist t [Constant (Str n), x]
873+ | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
874+reifyApp _ t [Constant (Str n)]
875+ | t == reflm "Intro" = return $ Intro [UN n]
876+reifyApp ist t [t']
877+ | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
878+reifyApp ist t [t']
879+ | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
880+reifyApp _ t [t']
881+ | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
882+reifyApp ist t [t']
883+ | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
884+reifyApp ist t [x]
885+ | t == reflm "Focus" = liftM Focus (reifyTTName x)
886+reifyApp ist t [t']
887+ | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
888+reifyApp ist t [n, t']
889+ | t == reflm "LetTac" = do n' <- reifyTTName n
890+ t'' <- reifyTT t'
891+ return $ LetTac n' (delab ist t')
892+reifyApp ist t [n, tt', t']
893+ | t == reflm "LetTacTy" = do n' <- reifyTTName n
894+ tt'' <- reifyTT tt'
895+ t'' <- reifyTT t'
896+ return $ LetTacTy n' (delab ist tt'') (delab ist t'')
897+reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
898+
899+-- | Reify terms from their reflected representation
900+reifyTT :: Term -> ElabD Term
901+reifyTT t@(App _ _)
902+ | (P _ f _, args) <- unApply t = reifyTTApp f args
903+reifyTT t@(P _ n _)
904+ | n == reflm "Erased" = return $ Erased
905+reifyTT t@(P _ n _)
906+ | n == reflm "Impossible" = return $ Impossible
907+reifyTT t = fail ("Unknown reflection term: " ++ show t)
908+
909+reifyTTApp :: Name -> [Term] -> ElabD Term
910+reifyTTApp t [nt, n, x]
911+ | t == reflm "P" = do nt' <- reifyTTNameType nt
912+ n' <- reifyTTName n
913+ x' <- reifyTT x
914+ return $ P nt' n' x'
915+reifyTTApp t [Constant (I i)]
916+ | t == reflm "V" = return $ V i
917+reifyTTApp t [n, b, x]
918+ | t == reflm "Bind" = do n' <- reifyTTName n
919+ b' <- reifyTTBinder reifyTT (reflm "TT") b
920+ x' <- reifyTT x
921+ return $ Bind n' b' x'
922+reifyTTApp t [f, x]
923+ | t == reflm "App" = do f' <- reifyTT f
924+ x' <- reifyTT x
925+ return $ App f' x'
926+reifyTTApp t [c]
927+ | t == reflm "TConst" = liftM Constant (reifyTTConst c)
928+reifyTTApp t [t', Constant (I i)]
929+ | t == reflm "Proj" = do t'' <- reifyTT t'
930+ return $ Proj t'' i
931+reifyTTApp t [tt]
932+ | t == reflm "TType" = liftM TType (reifyTTUExp tt)
933+reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
934+
935+-- | Reify raw terms from their reflected representation
936+reifyRaw :: Term -> ElabD Raw
937+reifyRaw t@(App _ _)
938+ | (P _ f _, args) <- unApply t = reifyRawApp f args
939+reifyRaw t@(P _ n _)
940+ | n == reflm "RType" = return $ RType
941+reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)
942+
943+reifyRawApp :: Name -> [Term] -> ElabD Raw
944+reifyRawApp t [n]
945+ | t == reflm "Var" = liftM Var (reifyTTName n)
946+reifyRawApp t [n, b, x]
947+ | t == reflm "RBind" = do n' <- reifyTTName n
948+ b' <- reifyTTBinder reifyRaw (reflm "Raw") b
949+ x' <- reifyRaw x
950+ return $ RBind n' b' x'
951+reifyRawApp t [f, x]
952+ | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
953+reifyRawApp t [t']
954+ | t == reflm "RForce" = liftM RForce (reifyRaw t')
955+reifyRawApp t [c]
956+ | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
957+reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))
958+
959+reifyTTName :: Term -> ElabD Name
960+reifyTTName t@(App _ _)
961+ | (P _ f _, args) <- unApply t = reifyTTNameApp f args
962+reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
963+
964+reifyTTNameApp :: Name -> [Term] -> ElabD Name
965+reifyTTNameApp t [Constant (Str n)]
966+ | t == reflm "UN" = return $ UN n
967+reifyTTNameApp t [n, ns]
968+ | t == reflm "NS" = do n' <- reifyTTName n
969+ ns' <- reifyTTNamespace ns
970+ return $ NS n' ns'
971+reifyTTNameApp t [Constant (I i), Constant (Str n)]
972+ | t == reflm "MN" = return $ MN i n
973+reifyTTNameApp t []
974+ | t == reflm "NErased" = return NErased
975+reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
976+
977+reifyTTNamespace :: Term -> ElabD [String]
978+reifyTTNamespace t@(App _ _)
979+ = case unApply t of
980+ (P _ f _, [Constant StrType])
981+ | f == NS (UN "Nil") ["List", "Prelude"] -> return []
982+ (P _ f _, [Constant StrType, Constant (Str n), ns])
983+ | f == NS (UN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
984+ _ -> fail ("Unknown reflection namespace arg: " ++ show t)
985+reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
986+
987+reifyTTNameType :: Term -> ElabD NameType
988+reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
989+reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
990+reifyTTNameType t@(App _ _)
991+ = case unApply t of
992+ (P _ f _, [Constant (I tag), Constant (I num)])
993+ | f == reflm "DCon" -> return $ DCon tag num
994+ | f == reflm "TCon" -> return $ TCon tag num
995+ _ -> fail ("Unknown reflection name type: " ++ show t)
996+reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
997+
998+reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
999+reifyTTBinder reificator binderType t@(App _ _)
1000+ = case unApply t of
1001+ (P _ f _, bt:args) | forget bt == Var binderType
1002+ -> reifyTTBinderApp reificator f args
1003+ _ -> fail ("Mismatching binder reflection: " ++ show t)
1004+reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
1005+
1006+reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
1007+reifyTTBinderApp reif f [t]
1008+ | f == reflm "Lam" = liftM Lam (reif t)
1009+reifyTTBinderApp reif f [t]
1010+ | f == reflm "Pi" = liftM Pi (reif t)
1011+reifyTTBinderApp reif f [x, y]
1012+ | f == reflm "Let" = liftM2 Let (reif x) (reif y)
1013+reifyTTBinderApp reif f [x, y]
1014+ | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
1015+reifyTTBinderApp reif f [t]
1016+ | f == reflm "Hole" = liftM Hole (reif t)
1017+reifyTTBinderApp reif f [t]
1018+ | f == reflm "GHole" = liftM GHole (reif t)
1019+reifyTTBinderApp reif f [x, y]
1020+ | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
1021+reifyTTBinderApp reif f [t]
1022+ | f == reflm "PVar" = liftM PVar (reif t)
1023+reifyTTBinderApp reif f [t]
1024+ | f == reflm "PVTy" = liftM PVTy (reif t)
1025+reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
1026+
1027+reifyTTConst :: Term -> ElabD Const
1028+reifyTTConst (P _ n _) | n == reflm "IType" = return $ IType
1029+reifyTTConst (P _ n _) | n == reflm "BIType" = return $ BIType
1030+reifyTTConst (P _ n _) | n == reflm "FlType" = return $ FlType
1031+reifyTTConst (P _ n _) | n == reflm "ChType" = return $ ChType
1032+reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
1033+reifyTTConst (P _ n _) | n == reflm "B8Type" = return $ B8Type
1034+reifyTTConst (P _ n _) | n == reflm "B16Type" = return $ B16Type
1035+reifyTTConst (P _ n _) | n == reflm "B32Type" = return $ B32Type
1036+reifyTTConst (P _ n _) | n == reflm "B64Type" = return $ B64Type
1037+reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
1038+reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
1039+reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
1040+reifyTTConst t@(App _ _)
1041+ | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
1042+reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
1043+
1044+reifyTTConstApp :: Name -> Term -> ElabD Const
1045+reifyTTConstApp f (Constant c@(I _))
1046+ | f == reflm "I" = return $ c
1047+reifyTTConstApp f (Constant c@(BI _))
1048+ | f == reflm "BI" = return $ c
1049+reifyTTConstApp f (Constant c@(Fl _))
1050+ | f == reflm "Fl" = return $ c
1051+reifyTTConstApp f (Constant c@(I _))
1052+ | f == reflm "Ch" = return $ c
1053+reifyTTConstApp f (Constant c@(Str _))
1054+ | f == reflm "Str" = return $ c
1055+reifyTTConstApp f (Constant c@(B8 _))
1056+ | f == reflm "B8" = return $ c
1057+reifyTTConstApp f (Constant c@(B16 _))
1058+ | f == reflm "B16" = return $ c
1059+reifyTTConstApp f (Constant c@(B32 _))
1060+ | f == reflm "B32" = return $ c
1061+reifyTTConstApp f (Constant c@(B64 _))
1062+ | f == reflm "B64" = return $ c
1063+reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
1064+
1065+reifyTTUExp :: Term -> ElabD UExp
1066+reifyTTUExp t@(App _ _)
1067+ = case unApply t of
1068+ (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
1069+ (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
1070+ _ -> fail ("Unknown reflection type universe expression: " ++ show t)
1071+reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
1072+
1073+-- | Create a reflected call to a named function/constructor
1074+reflCall :: String -> [Raw] -> Raw
1075+reflCall funName args
1076+ = raw_apply (Var (reflm funName)) args
1077+
1078+-- | Lift a term into its Language.Reflection.TT representation
1079+reflect :: Term -> Raw
1080+reflect (P nt n t)
1081+ = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
1082+reflect (V n)
1083+ = reflCall "V" [RConstant (I n)]
1084+reflect (Bind n b x)
1085+ = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
1086+reflect (App f x)
1087+ = reflCall "App" [reflect f, reflect x]
1088+reflect (Constant c)
1089+ = reflCall "TConst" [reflectConstant c]
1090+reflect (Proj t i)
1091+ = reflCall "Proj" [reflect t, RConstant (I i)]
1092+reflect (Erased) = Var (reflm "Erased")
1093+reflect (Impossible) = Var (reflm "Impossible")
1094+reflect (TType exp) = reflCall "TType" [reflectUExp exp]
1095+
1096+reflectNameType :: NameType -> Raw
1097+reflectNameType (Bound) = Var (reflm "Bound")
1098+reflectNameType (Ref) = Var (reflm "Ref")
1099+reflectNameType (DCon x y)
1100+ = reflCall "DCon" [RConstant (I x), RConstant (I y)]
1101+reflectNameType (TCon x y)
1102+ = reflCall "TCon" [RConstant (I x), RConstant (I y)]
1103+
1104+reflectName :: Name -> Raw
1105+reflectName (UN str)
1106+ = reflCall "UN" [RConstant (Str str)]
1107+reflectName (NS n ns)
1108+ = reflCall "NS" [ reflectName n
1109+ , foldr (\ n s ->
1110+ raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )
1111+ [ RConstant StrType, RConstant (Str n), s ])
1112+ ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )
1113+ [ RConstant StrType ])
1114+ ns
1115+ ]
1116+reflectName (MN i n)
1117+ = reflCall "MN" [RConstant (I i), RConstant (Str n)]
1118+reflectName (NErased) = Var (reflm "NErased")
1119+
1120+reflectBinder :: Binder Term -> Raw
1121+reflectBinder (Lam t)
1122+ = reflCall "Lam" [Var (reflm "TT"), reflect t]
1123+reflectBinder (Pi t)
1124+ = reflCall "Pi" [Var (reflm "TT"), reflect t]
1125+reflectBinder (Let x y)
1126+ = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
1127+reflectBinder (NLet x y)
1128+ = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
1129+reflectBinder (Hole t)
1130+ = reflCall "Hole" [Var (reflm "TT"), reflect t]
1131+reflectBinder (GHole t)
1132+ = reflCall "GHole" [Var (reflm "TT"), reflect t]
1133+reflectBinder (Guess x y)
1134+ = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
1135+reflectBinder (PVar t)
1136+ = reflCall "PVar" [Var (reflm "TT"), reflect t]
1137+reflectBinder (PVTy t)
1138+ = reflCall "PVTy" [Var (reflm "TT"), reflect t]
1139+
1140+reflectConstant :: Const -> Raw
1141+reflectConstant c@(I _) = reflCall "I" [RConstant c]
1142+reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
1143+reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
1144+reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
1145+reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
1146+reflectConstant (IType) = Var (reflm "IType")
1147+reflectConstant (BIType) = Var (reflm "BIType")
1148+reflectConstant (FlType) = Var (reflm "FlType")
1149+reflectConstant (ChType) = Var (reflm "ChType")
1150+reflectConstant (StrType) = Var (reflm "StrType")
1151+reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
1152+reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
1153+reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
1154+reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
1155+reflectConstant (B8Type) = Var (reflm "B8Type")
1156+reflectConstant (B16Type) = Var (reflm "B16Type")
1157+reflectConstant (B32Type) = Var (reflm "B32Type")
1158+reflectConstant (B64Type) = Var (reflm "B64Type")
1159+reflectConstant (PtrType) = Var (reflm "PtrType")
1160+reflectConstant (VoidType) = Var (reflm "VoidType")
1161+reflectConstant (Forgot) = Var (reflm "Forgot")
1162+
1163+reflectUExp :: UExp -> Raw
1164+reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
1165+reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
1166+
1167+-- | Reflect the environment of a proof into a List (TTName, Binder TT)
1168+reflectEnv :: Env -> Raw
1169+reflectEnv = foldr consToEnvList emptyEnvList
1170+ where
1171+ consToEnvList :: (Name, Binder Term) -> Raw -> Raw
1172+ consToEnvList (n, b) l
1173+ = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))
1174+ [ envTupleType
1175+ , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
1176+ , (RApp (Var $ reflm "Binder")
1177+ (Var $ reflm "TT"))
1178+ , reflectName n
1179+ , reflectBinder b
1180+ ]
1181+ , l
1182+ ]
1183+
1184+ emptyEnvList :: Raw
1185+ emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))
1186+ [envTupleType]
1187+
1188+envTupleType :: Raw
1189+envTupleType
1190+ = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
1191+ , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
1192+ ]
8201193
8211194solveAll = try (do solve; solveAll) (return ())
8221195
src/Idris/IBC.hs+12−4
@@ -21,7 +21,7 @@ import System.Directory
2121import Paths_idris
2222
2323ibcVersion :: Word8
24−ibcVersion = 28
24+ibcVersion = 29
2525
2626data IBCFile = IBCFile { ver :: Word8,
2727 sourcefile :: FilePath,
@@ -1390,8 +1390,12 @@ instance (Binary t) => Binary (PTactic' t) where
13901390 put x1
13911391 put x2
13921392 Qed -> putWord8 15
1393− ReflectTac x1 -> do putWord8 16
1394− put x1
1393+ ApplyTactic x1 -> do putWord8 16
1394+ put x1
1395+ Reflect x1 -> do putWord8 17
1396+ put x1
1397+ Fill x1 -> do putWord8 18
1398+ put x1
13951399 get
13961400 = do i <- getWord8
13971401 case i of
@@ -1424,7 +1428,11 @@ instance (Binary t) => Binary (PTactic' t) where
14241428 return (TSeq x1 x2)
14251429 15 -> return Qed
14261430 16 -> do x1 <- get
1427− return (ReflectTac x1)
1431+ return (ApplyTactic x1)
1432+ 17 -> do x1 <- get
1433+ return (Reflect x1)
1434+ 18 -> do x1 <- get
1435+ return (Fill x1)
14281436 _ -> error "Corrupted binary data for PTactic'"
14291437
14301438
src/Idris/Parser.hs+7−1
@@ -1537,9 +1537,15 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
15371537 <|> do reserved "exact"; t <- pExpr syn;
15381538 i <- getState
15391539 return $ Exact (desugar syn i t)
1540+ <|> do reserved "applyTactic"; t <- pExpr syn;
1541+ i <- getState
1542+ return $ ApplyTactic (desugar syn i t)
15401543 <|> do reserved "reflect"; t <- pExpr syn;
15411544 i <- getState
1542− return $ ReflectTac (desugar syn i t)
1545+ return $ Reflect (desugar syn i t)
1546+ <|> do reserved "fill"; t <- pExpr syn;
1547+ i <- getState
1548+ return $ Fill (desugar syn i t)
15431549 <|> do reserved "try"; t <- pTactic syn;
15441550 lchar '|';
15451551 t1 <- pTactic syn