1module Language.Reflection
8 -- ^ User-provided name
9 | NS TTName (List String)
12 -- ^ Machine chosen names
14 -- ^ Name of somethng which is never used in scope
17userSuppliedName : String -> TTName
21 -- ^ universe variable
23 -- ^ explicit universe variable
25-- | Primitive constants
26data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
27 | IType | BIType | FlType | ChType | StrType
28 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
29 | B8Type | B16Type | B32Type | B64Type
30 | PtrType | VoidType | Forgot
32abstract class ReflConst (a : Type) where
35instance ReflConst Int where
38instance ReflConst Nat where
41instance ReflConst Float where
44instance ReflConst Char where
47instance ReflConst String where
50instance ReflConst Bits8 where
53instance ReflConst Bits16 where
56instance ReflConst Bits32 where
59instance ReflConst Bits64 where
63reflectConstant: (ReflConst a) => a -> Const
64reflectConstant = toConst
67-- | Types of named references
69 -- ^ reference which is just bound, e.g. by intro
71 -- ^ reference to a variable
73 -- ^ constructor with tag and number
75 -- ^ type constructor with tag and number
77-- | Types annotations for bound variables in different
90instance Functor Binder where
91 map f (Lam x) = Lam (f x)
92 map f (Pi x) = Pi (f x)
93 map f (Let x y) = Let (f x) (f y)
94 map f (NLet x y) = NLet (f x) (f y)
95 map f (Hole x) = Hole (f x)
96 map f (GHole x) = GHole (f x)
97 map f (Guess x y) = Guess (f x) (f y)
98 map f (PVar x) = PVar (f x)
99 map f (PVTy x) = PVTy (f x)
101instance Foldable Binder where
102 foldr f z (Lam x) = f x z
103 foldr f z (Pi x) = f x z
104 foldr f z (Let x y) = f x (f y z)
105 foldr f z (NLet x y) = f x (f y z)
106 foldr f z (Hole x) = f x z
107 foldr f z (GHole x) = f x z
108 foldr f z (Guess x y) = f x (f y z)
109 foldr f z (PVar x) = f x z
110 foldr f z (PVTy x) = f x z
112instance Traversable Binder where
113 traverse f (Lam x) = [| Lam (f x) |]
114 traverse f (Pi x) = [| Pi (f x) |]
115 traverse f (Let x y) = [| Let (f x) (f y) |]
116 traverse f (NLet x y) = [| NLet (f x) (f y) |]
117 traverse f (Hole x) = [| Hole (f x) |]
118 traverse f (GHole x) = [| GHole (f x) |]
119 traverse f (Guess x y) = [| Guess (f x) (f y) |]
120 traverse f (PVar x) = [| PVar (f x) |]
121 traverse f (PVTy x) = [| PVTy (f x) |]
124-- | Reflection of the well typed core language
125data TT = P NameType TTName TT
129 | Bind TTName (Binder TT) TT
130 -- ^ type annotated named bindings
132 -- ^ (named) application of a function to a value
136 -- ^ argument projection; runtime only
140 -- ^ impossible terms
144-- | Raw terms without types
146 | RBind TTName (Binder Raw) Raw
152data Tactic = Try Tactic Tactic
153 -- ^ try the first tactic and resort to the second one on failure
154 | GoalType String Tactic
155 -- ^ only run if the goal has the right type
157 -- ^ resolve function name, find matching arguments in the
158 -- context and compute the proof target
160 -- ^ apply both tactics in sequence
162 -- ^ intelligently construct the proof target from the context
164 -- ^ infer the proof target from the context
166 -- ^ introduce all variables into the context
168 -- ^ introduce a named variable into the context, use the
169 -- first one if the given name is not found
171 -- ^ invoke the reflected rep. of another tactic
173 -- ^ turn a value into its reflected representation
175 -- ^ turn a raw value back into a term
177 -- ^ use the given value to conclude the proof
179 -- ^ focus a named hole
181 -- ^ rewrite using the reflected rep. of a equality proof
183 -- ^ name a reflected term
184 | LetTacTy TTName TT TT
185 -- ^ name a reflected term and type it
187 -- ^ 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