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 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)
100traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
101traverse f (Lam x) = [| Lam (f x) |]
102traverse f (Pi x) = [| Pi (f x) |]
103traverse f (Let x y) = [| Let (f x) (f y) |]
104traverse f (NLet x y) = [| NLet (f x) (f y) |]
105traverse f (Hole x) = [| Hole (f x) |]
106traverse f (GHole x) = [| GHole (f x) |]
107traverse f (Guess x y) = [| Guess (f x) (f y) |]
108traverse f (PVar x) = [| PVar (f x) |]
109traverse f (PVTy x) = [| PVTy (f x) |]
112-- | Reflection of the well typed core language
113data TT = P NameType TTName TT
117 | Bind TTName (Binder TT) TT
118 -- ^ type annotated named bindings
120 -- ^ (named) application of a function to a value
124 -- ^ argument projection; runtime only
128 -- ^ impossible terms
132-- | Raw terms without types
134 | RBind TTName (Binder Raw) Raw
140data Tactic = Try Tactic Tactic
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
145 -- ^ resolve function name, find matching arguments in the
146 -- context and compute the proof target
148 -- ^ apply both tactics in sequence
150 -- ^ intelligently construct the proof target from the context
152 -- ^ infer the proof target from the context
154 -- ^ introduce all variables into the context
156 -- ^ introduce a named variable into the context, use the
157 -- first one if the given name is not found
159 -- ^ invoke the reflected rep. of another tactic
161 -- ^ turn a value into its reflected representation
163 -- ^ turn a raw value back into a term
165 -- ^ use the given value to conclude the proof
167 -- ^ focus a named hole
169 -- ^ rewrite using the reflected rep. of a equality proof
171 -- ^ name a reflected term
172 | LetTacTy TTName TT TT
173 -- ^ name a reflected term and type it
175 -- ^ 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