git.iko.soy/Idris-dev
on master help sign in
Add name suggestions to reflection lib
e33cfb9David Raymond Christiansen
libs/base/Language/Reflection.idr+11−2
compare with master
unifiedsplit
@@ -10,6 +10,7 @@ data TTName = UN String
10 -- ^ Machine chosen names
10 -- ^ Machine chosen names
11 | NErased
11 | NErased
12 -- ^ Name of somethng which is never used in scope
12 -- ^ Name of somethng which is never used in scope
13+%name TTName n, n'
13
14
14implicit
15implicit
15userSuppliedName : String -> TTName
16userSuppliedName : String -> TTName
@@ -19,6 +20,7 @@ data TTUExp = UVar Int
19 -- ^ universe variable
20 -- ^ universe variable
20 | UVal Int
21 | UVal Int
21 -- ^ explicit universe variable
22 -- ^ explicit universe variable
23+%name TTUExp uexp
22
24
23-- | Primitive constants
25-- | Primitive constants
24data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
26data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
@@ -27,6 +29,8 @@ data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
27 | B8Type | B16Type | B32Type | B64Type
29 | B8Type | B16Type | B32Type | B64Type
28 | PtrType | VoidType | Forgot
30 | PtrType | VoidType | Forgot
29
31
32+%name Const c, c'
33+
30abstract class ReflConst (a : Type) where
34abstract class ReflConst (a : Type) where
31 toConst : a -> Const
35 toConst : a -> Const
32
36
@@ -71,6 +75,7 @@ data NameType = Bound
71 -- ^ constructor with tag and number
75 -- ^ constructor with tag and number
72 | TCon Int Int
76 | TCon Int Int
73 -- ^ type constructor with tag and number
77 -- ^ type constructor with tag and number
78+%name NameType nt, nt'
74
79
75-- | Types annotations for bound variables in different
80-- | Types annotations for bound variables in different
76-- binding contexts
81-- binding contexts
@@ -83,7 +88,7 @@ data Binder a = Lam a
83 | Guess a a
88 | Guess a a
84 | PVar a
89 | PVar a
85 | PVTy a
90 | PVTy a
86−
91+%name Binder b, b'
87
92
88instance Functor Binder where
93instance Functor Binder where
89 map f (Lam x) = Lam (f x)
94 map f (Lam x) = Lam (f x)
@@ -139,6 +144,8 @@ data TT = P NameType TTName TT
139 | TType TTUExp
144 | TType TTUExp
140 -- ^ types
145 -- ^ types
141
146
147+%name TT tm, tm'
148+
142-- | Raw terms without types
149-- | Raw terms without types
143data Raw = Var TTName
150data Raw = Var TTName
144 | RBind TTName (Binder Raw) Raw
151 | RBind TTName (Binder Raw) Raw
@@ -147,6 +154,8 @@ data Raw = Var TTName
147 | RForce Raw
154 | RForce Raw
148 | RConstant Const
155 | RConstant Const
149
156
157+%name Raw tm, tm'
158+
150data Tactic = Try Tactic Tactic
159data Tactic = Try Tactic Tactic
151 -- ^ try the first tactic and resort to the second one on failure
160 -- ^ try the first tactic and resort to the second one on failure
152 | GoalType String Tactic
161 | GoalType String Tactic
@@ -185,4 +194,4 @@ data Tactic = Try Tactic Tactic
185 -- ^ name a reflected term and type it
194 -- ^ name a reflected term and type it
186 | Compute
195 | Compute
187 -- ^ normalise the context
196 -- ^ normalise the context
188−
197+%name Tactic tac, tac'
libs/base/Language/Reflection/Errors.idr+8−3
@@ -2,7 +2,10 @@ module Language.Reflection.Errors
2
2
3import Language.Reflection
3import Language.Reflection
4
4
5+record SourceLocation : Type where
5−data SourceLocation = FileLoc String Int Int
6+ FileLoc : (filename : String) -> (line : Int) -> (col : Int) -> SourceLocation
7+
8+%name SourceLocation loc
6
9
7data Err = Msg String
10data Err = Msg String
8 | InternalMsg String
11 | InternalMsg String
@@ -36,13 +39,15 @@ data Err = Msg String
36 | ProviderError String
39 | ProviderError String
37 | LoadingFailed String Err
40 | LoadingFailed String Err
38
41
42+%name Err err, e
43+
39-- | Error reports are a list of report parts
44-- | Error reports are a list of report parts
40data ErrorReportPart = TextPart String
45data ErrorReportPart = TextPart String
41 | NamePart TTName
46 | NamePart TTName
42 | TermPart TT
47 | TermPart TT
43 | SubReport (List ErrorReportPart)
48 | SubReport (List ErrorReportPart)
44−
49+%name ErrorReportPart part, p
45
50
46-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
51-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
47ErrorHandler : Type
52ErrorHandler : Type
48−ErrorHandler = Err -> Maybe (List ErrorReportPart)
53+ErrorHandler = Err -> Maybe (List ErrorReportPart)