Mercurial > urweb

comparison src/elab_util.sig @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 85819353a84f
children 7292bcb7c02d
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
28 signature ELAB_UTIL = sig 28 signature ELAB_UTIL = sig
29 29
30 val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind 30 val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind
31 31
32 structure Kind : sig 32 structure Kind : sig
33 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
34 bind : 'context * string -> 'context}
35 -> ('context, Elab.kind, 'state, 'abort) Search.mapfolderB
33 val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder 36 val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
34 -> (Elab.kind, 'state, 'abort) Search.mapfolder 37 -> (Elab.kind, 'state, 'abort) Search.mapfolder
35 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool 38 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
39 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
40 bind : 'context * string -> 'context}
41 -> 'context -> (Elab.kind -> Elab.kind)
36 end 42 end
37 43
38 structure Con : sig 44 structure Con : sig
39 datatype binder = 45 datatype binder =
40 Rel of string * Elab.kind 46 RelK of string
41 | Named of string * int * Elab.kind 47 | RelC of string * Elab.kind
48 | NamedC of string * int * Elab.kind
42 49
43 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 50 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
44 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 51 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
45 bind : 'context * binder -> 'context} 52 bind : 'context * binder -> 'context}
46 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB 53 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB
47 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 54 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
48 con : (Elab.con', 'state, 'abort) Search.mapfolder} 55 con : (Elab.con', 'state, 'abort) Search.mapfolder}
49 -> (Elab.con, 'state, 'abort) Search.mapfolder 56 -> (Elab.con, 'state, 'abort) Search.mapfolder
50 57
51 val mapB : {kind : Elab.kind' -> Elab.kind', 58 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
52 con : 'context -> Elab.con' -> Elab.con', 59 con : 'context -> Elab.con' -> Elab.con',
53 bind : 'context * binder -> 'context} 60 bind : 'context * binder -> 'context}
54 -> 'context -> (Elab.con -> Elab.con) 61 -> 'context -> (Elab.con -> Elab.con)
55 val map : {kind : Elab.kind' -> Elab.kind', 62 val map : {kind : Elab.kind' -> Elab.kind',
56 con : Elab.con' -> Elab.con'} 63 con : Elab.con' -> Elab.con'}
57 -> Elab.con -> Elab.con 64 -> Elab.con -> Elab.con
58 val exists : {kind : Elab.kind' -> bool, 65 val exists : {kind : Elab.kind' -> bool,
59 con : Elab.con' -> bool} -> Elab.con -> bool 66 con : Elab.con' -> bool} -> Elab.con -> bool
60 67
61 val foldB : {kind : Elab.kind' * 'state -> 'state, 68 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
62 con : 'context * Elab.con' * 'state -> 'state, 69 con : 'context * Elab.con' * 'state -> 'state,
63 bind : 'context * binder -> 'context} 70 bind : 'context * binder -> 'context}
64 -> 'context -> 'state -> Elab.con -> 'state 71 -> 'context -> 'state -> Elab.con -> 'state
65 end 72 end
66 73
67 structure Exp : sig 74 structure Exp : sig
68 datatype binder = 75 datatype binder =
69 RelC of string * Elab.kind 76 RelK of string
77 | RelC of string * Elab.kind
70 | NamedC of string * int * Elab.kind 78 | NamedC of string * int * Elab.kind
71 | RelE of string * Elab.con 79 | RelE of string * Elab.con
72 | NamedE of string * Elab.con 80 | NamedE of string * Elab.con
73 81
74 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 82 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
75 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 83 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
76 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, 84 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
77 bind : 'context * binder -> 'context} 85 bind : 'context * binder -> 'context}
78 -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB 86 -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB
79 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 87 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
80 con : (Elab.con', 'state, 'abort) Search.mapfolder, 88 con : (Elab.con', 'state, 'abort) Search.mapfolder,
81 exp : (Elab.exp', 'state, 'abort) Search.mapfolder} 89 exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
82 -> (Elab.exp, 'state, 'abort) Search.mapfolder 90 -> (Elab.exp, 'state, 'abort) Search.mapfolder
83 val mapB : {kind : Elab.kind' -> Elab.kind', 91 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
84 con : 'context -> Elab.con' -> Elab.con', 92 con : 'context -> Elab.con' -> Elab.con',
85 exp : 'context -> Elab.exp' -> Elab.exp', 93 exp : 'context -> Elab.exp' -> Elab.exp',
86 bind : 'context * binder -> 'context} 94 bind : 'context * binder -> 'context}
87 -> 'context -> (Elab.exp -> Elab.exp) 95 -> 'context -> (Elab.exp -> Elab.exp)
88 val exists : {kind : Elab.kind' -> bool, 96 val exists : {kind : Elab.kind' -> bool,
89 con : Elab.con' -> bool, 97 con : Elab.con' -> bool,
90 exp : Elab.exp' -> bool} -> Elab.exp -> bool 98 exp : Elab.exp' -> bool} -> Elab.exp -> bool
91 99
92 val foldB : {kind : Elab.kind' * 'state -> 'state, 100 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
93 con : 'context * Elab.con' * 'state -> 'state, 101 con : 'context * Elab.con' * 'state -> 'state,
94 exp : 'context * Elab.exp' * 'state -> 'state, 102 exp : 'context * Elab.exp' * 'state -> 'state,
95 bind : 'context * binder -> 'context} 103 bind : 'context * binder -> 'context}
96 -> 'context -> 'state -> Elab.exp -> 'state 104 -> 'context -> 'state -> Elab.exp -> 'state
97 end 105 end
98 106
99 structure Sgn : sig 107 structure Sgn : sig
100 datatype binder = 108 datatype binder =
101 RelC of string * Elab.kind 109 RelK of string
110 | RelC of string * Elab.kind
102 | NamedC of string * int * Elab.kind 111 | NamedC of string * int * Elab.kind
103 | Str of string * Elab.sgn 112 | Str of string * Elab.sgn
104 | Sgn of string * Elab.sgn 113 | Sgn of string * Elab.sgn
105 114
106 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 115 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
107 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 116 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
108 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, 117 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
109 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, 118 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
110 bind : 'context * binder -> 'context} 119 bind : 'context * binder -> 'context}
111 -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB 120 -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB
125 134
126 end 135 end
127 136
128 structure Decl : sig 137 structure Decl : sig
129 datatype binder = 138 datatype binder =
130 RelC of string * Elab.kind 139 RelK of string
140 | RelC of string * Elab.kind
131 | NamedC of string * int * Elab.kind 141 | NamedC of string * int * Elab.kind
132 | RelE of string * Elab.con 142 | RelE of string * Elab.con
133 | NamedE of string * Elab.con 143 | NamedE of string * Elab.con
134 | Str of string * Elab.sgn 144 | Str of string * Elab.sgn
135 | Sgn of string * Elab.sgn 145 | Sgn of string * Elab.sgn
136 146
137 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 147 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
138 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 148 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
139 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, 149 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
140 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, 150 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
141 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, 151 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
142 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB, 152 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB,
166 sgn : Elab.sgn' -> 'a option, 176 sgn : Elab.sgn' -> 'a option,
167 str : Elab.str' -> 'a option, 177 str : Elab.str' -> 'a option,
168 decl : Elab.decl' -> 'a option} 178 decl : Elab.decl' -> 'a option}
169 -> Elab.decl -> 'a option 179 -> Elab.decl -> 'a option
170 180
171 val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state, 181 val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state,
172 con : 'context * Elab.con' * 'state -> Elab.con' * 'state, 182 con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
173 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, 183 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
174 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, 184 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
175 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state, 185 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
176 str : 'context * Elab.str' * 'state -> Elab.str' * 'state, 186 str : 'context * Elab.str' * 'state -> Elab.str' * 'state,