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 fmap f (Lam x) = Lam (f x)
92 fmap f (Pi x) = Pi (f x)
93 fmap f (Let x y) = Let (f x) (f y)
94 fmap f (NLet x y) = NLet (f x) (f y)
95 fmap f (Hole x) = Hole (f x)
96 fmap f (GHole x) = GHole (f x)
97 fmap f (Guess x y) = Guess (f x) (f y)
98 fmap f (PVar x) = PVar (f x)
99 fmap f (PVTy x) = PVTy (f x)
102traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
103traverse f (Lam x) = [| Lam (f x) |]
104traverse f (Pi x) = [| Pi (f x) |]
105traverse f (Let x y) = [| Let (f x) (f y) |]
106traverse f (NLet x y) = [| NLet (f x) (f y) |]
107traverse f (Hole x) = [| Hole (f x) |]
108traverse f (GHole x) = [| GHole (f x) |]
109traverse f (Guess x y) = [| Guess (f x) (f y) |]
110traverse f (PVar x) = [| PVar (f x) |]
111traverse f (PVTy x) = [| PVTy (f x) |]
114-- | Reflection of the well typed core language
115data TT = P NameType TTName TT
119 | Bind TTName (Binder TT) TT
120 -- ^ type annotated named bindings
122 -- ^ (named) application of a function to a value
126 -- ^ argument projection; runtime only
130 -- ^ impossible terms
134-- | Raw terms without types
136 | RBind TTName (Binder Raw) Raw
142data Tactic = Try Tactic Tactic
143 -- ^ try the first tactic and resort to the second one on failure
144 | GoalType String Tactic
145 -- ^ only run if the goal has the right type
147 -- ^ resolve function name, find matching arguments in the
148 -- context and compute the proof target
150 -- ^ apply both tactics in sequence
152 -- ^ intelligently construct the proof target from the context
154 -- ^ infer the proof target from the context
156 -- ^ introduce all variables into the context
158 -- ^ introduce a named variable into the context, use the
159 -- first one if the given name is not found
161 -- ^ invoke the reflected rep. of another tactic
163 -- ^ turn a value into its reflected representation
165 -- ^ turn a raw value back into a term
167 -- ^ use the given value to conclude the proof
169 -- ^ focus a named hole
171 -- ^ rewrite using the reflected rep. of a equality proof
173 -- ^ name a reflected term
174 | LetTacTy TTName TT TT
175 -- ^ name a reflected term and type it
177 -- ^ 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