@@ -1,149 +0,0 @@
1−module Language.Reflection.Tactical
2−
3−import Builtins
4−import Prelude.Applicative
5−import Prelude.Functor
6−import Prelude.List
7−import Prelude.Maybe
8−import Prelude.Monad
9−import Language.Reflection
10−
11−data Arg : Type where
12− Explicit : TTName -> Raw -> Arg
13− Implicit : TTName -> Raw -> Arg
14− Constraint : TTName -> Raw -> Arg
15−
16−data TyDecl : Type where
17− Declare : TTName -> List Arg -> Raw -> TyDecl
18−
19−data FunClause : Type where
20− MkFunClause : (lhs, rhs : Raw) -> FunClause
21− MkImpossibleClause : (lhs : Raw) -> FunClause
22−
23−data FunDefn : Type where
24− DefineFun : TTName -> List FunClause -> FunDefn
25−
26−abstract
27−data Tactical : Type -> Type where
28− -- obligatory control stuff
29− prim__PureTactical : a -> Tactical a
30− prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b
31−
32− prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a
33− prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a
34−
35− prim__Env : Tactical (List (TTName, Binder TT))
36− prim__Goal : Tactical (TTName, TT)
37− prim__Holes : Tactical (List TTName)
38− prim__Guess : Tactical (Maybe TT)
39−
40− prim__SourceLocation : Tactical SourceLocation
41−
42− prim__Forget : TT -> Tactical Raw
43−
44− prim__Gensym : String -> Tactical TTName
45−
46− prim__Solve : Tactical ()
47− prim__Fill : Raw -> Tactical ()
48− prim__Focus : TTName -> Tactical ()
49− prim__Unfocus : TTName -> Tactical ()
50− prim__Attack : Tactical ()
51−
52− prim__Rewrite : Raw -> Tactical ()
53−
54− prim__Claim : TTName -> Raw -> Tactical ()
55− prim__Intro : Maybe TTName -> Tactical ()
56−
57− prim__DeclareType : TyDecl -> Tactical ()
58− prim__DefineFunction : FunDefn -> Tactical ()
59−
60− prim__Debug : {a : Type} -> Maybe String -> Tactical a
61−
62−
63−-------------
64−-- Public API
65−-------------
66−%access public
67−
68−instance Functor Tactical where
69− map f t = prim__BindTactical t (\x => prim__PureTactical (f x))
70−
71−instance Applicative Tactical where
72− pure x = prim__PureTactical x
73− f <*> x = prim__BindTactical f $ \g =>
74− prim__BindTactical x $ \y =>
75− prim__PureTactical $ g y
76−
77−instance Alternative Tactical where
78− empty = prim__Fail [TextPart "empty"]
79− x <|> y = prim__Try x y
80−
81−instance Monad Tactical where
82− x >>= f = prim__BindTactical x f
83−
84−fail : List ErrorReportPart -> Tactical a
85−fail err = prim__Fail err
86−
87−getEnv : Tactical (List (TTName, Binder TT))
88−getEnv = prim__Env
89−
90−getGoal : Tactical (TTName, TT)
91−getGoal = prim__Goal
92−
93−getHoles : Tactical (List TTName)
94−getHoles = prim__Holes
95−
96−getGuess : Tactical (Maybe TT)
97−getGuess = prim__Guess
98−
99−forgetTypes : TT -> Tactical Raw
100−forgetTypes tt = prim__Forget tt
101−
102−gensym : (hint : String) -> Tactical TTName
103−gensym hint = prim__Gensym hint
104−
105−solve : Tactical ()
106−solve = prim__Solve
107−
108−fill : Raw -> Tactical ()
109−fill tm = prim__Fill tm
110−
111−focus : (hole : TTName) -> Tactical ()
112−focus hole = prim__Focus hole
113−
114−unfocus : TTName -> Tactical ()
115−unfocus hole = prim__Unfocus hole
116−
117−attack : Tactical ()
118−attack = prim__Attack
119−
120−claim : TTName -> Raw -> Tactical ()
121−claim n ty = prim__Claim n ty
122−
123−intro : Maybe TTName -> Tactical ()
124−intro n = prim__Intro n
125−
126−||| Find out the present source context for the tactic script
127−getSourceLocation : Tactical SourceLocation
128−getSourceLocation = prim__SourceLocation
129−
130−||| Attempt to solve the current goal with the source code location
131−sourceLocation : Tactical ()
132−sourceLocation = do loc <- getSourceLocation
133− fill (quote loc)
134− solve
135−
136−rewriteWith : Raw -> Tactical ()
137−rewriteWith rule = prim__Rewrite rule
138−
139−declareType : TyDecl -> Tactical ()
140−declareType decl = prim__DeclareType decl
141−
142−defineFunction : FunDefn -> Tactical ()
143−defineFunction defun = prim__DefineFunction defun
144−
145−debug : Tactical a
146−debug = prim__Debug Nothing
147−
148−debugMessage : String -> Tactical a
149−debugMessage msg = prim__Debug (Just msg)