1module Language.Reflection
6 -- ^ User-provided name
7 | NS TTName (List String)
10 -- ^ Machine chosen names
12 -- ^ Name of somethng which is never used in scope
15userSuppliedName : String -> TTName
19 -- ^ universe variable
21 -- ^ explicit universe variable
23-- | Primitive constants
24data 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
30abstract class ReflConst (a : Type) where
33instance ReflConst Int where
36instance ReflConst Nat where
39instance ReflConst Float where
42instance ReflConst Char where
45instance ReflConst String where
48instance ReflConst Bits8 where
51instance ReflConst Bits16 where
54instance ReflConst Bits32 where
57instance ReflConst Bits64 where
61reflectConstant: (ReflConst a) => a -> Const
62reflectConstant = toConst
65-- | Types of named references
67 -- ^ reference which is just bound, e.g. by intro
69 -- ^ reference to a variable
71 -- ^ constructor with tag and number
73 -- ^ type constructor with tag and number
75-- | Types annotations for bound variables in different
88instance Functor Binder where
89 map f (Lam x) = Lam (f x)
90 map f (Pi x) = Pi (f x)
91 map f (Let x y) = Let (f x) (f y)
92 map f (NLet x y) = NLet (f x) (f y)
93 map f (Hole x) = Hole (f x)
94 map f (GHole x) = GHole (f x)
95 map f (Guess x y) = Guess (f x) (f y)
96 map f (PVar x) = PVar (f x)
97 map f (PVTy x) = PVTy (f x)
99instance Foldable Binder where
100 foldr f z (Lam x) = f x z
101 foldr f z (Pi x) = f x z
102 foldr f z (Let x y) = f x (f y z)
103 foldr f z (NLet x y) = f x (f y z)
104 foldr f z (Hole x) = f x z
105 foldr f z (GHole x) = f x z
106 foldr f z (Guess x y) = f x (f y z)
107 foldr f z (PVar x) = f x z
108 foldr f z (PVTy x) = f x z
110instance Traversable Binder where
111 traverse f (Lam x) = [| Lam (f x) |]
112 traverse f (Pi x) = [| Pi (f x) |]
113 traverse f (Let x y) = [| Let (f x) (f y) |]
114 traverse f (NLet x y) = [| NLet (f x) (f y) |]
115 traverse f (Hole x) = [| Hole (f x) |]
116 traverse f (GHole x) = [| GHole (f x) |]
117 traverse f (Guess x y) = [| Guess (f x) (f y) |]
118 traverse f (PVar x) = [| PVar (f x) |]
119 traverse f (PVTy x) = [| PVTy (f x) |]
122-- | Reflection of the well typed core language
123data TT = P NameType TTName TT
127 | Bind TTName (Binder TT) TT
128 -- ^ type annotated named bindings
130 -- ^ (named) application of a function to a value
134 -- ^ argument projection; runtime only
138 -- ^ impossible terms
142-- | Raw terms without types
144 | RBind TTName (Binder Raw) Raw
150data Tactic = Try Tactic Tactic
151 -- ^ try the first tactic and resort to the second one on failure
152 | GoalType String Tactic
153 -- ^ only run if the goal has the right type
155 -- ^ resolve function name, find matching arguments in the
156 -- context and compute the proof target
158 -- ^ apply both tactics in sequence
160 -- ^ intelligently construct the proof target from the context
162 -- ^ infer the proof target from the context
164 -- ^ introduce all variables into the context
166 -- ^ introduce a named variable into the context, use the
167 -- first one if the given name is not found
169 -- ^ invoke the reflected rep. of another tactic
171 -- ^ turn a value into its reflected representation
173 -- ^ turn a raw value back into a term
175 -- ^ use the given value to conclude the proof
177 -- ^ focus a named hole
179 -- ^ rewrite using the reflected rep. of a equality proof
181 -- ^ name a reflected term
182 | LetTacTy TTName TT TT
183 -- ^ name a reflected term and type it
185 -- ^ normalise the context
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list