Mercurial > urweb

comparison src/elab_util.sig @ 448:85819353a84f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
First Unnest tests working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 15:58:55 -0400
parents eec65c11d3e2
children 588b9d16b00a
comparison
equal deleted inserted replaced
447:b77863cd0be2 448:85819353a84f
55 val map : {kind : Elab.kind' -> Elab.kind', 55 val map : {kind : Elab.kind' -> Elab.kind',
56 con : Elab.con' -> Elab.con'} 56 con : Elab.con' -> Elab.con'}
57 -> Elab.con -> Elab.con 57 -> Elab.con -> Elab.con
58 val exists : {kind : Elab.kind' -> bool, 58 val exists : {kind : Elab.kind' -> bool,
59 con : Elab.con' -> bool} -> Elab.con -> bool 59 con : Elab.con' -> bool} -> Elab.con -> bool
60
61 val foldB : {kind : Elab.kind' * 'state -> 'state,
62 con : 'context * Elab.con' * 'state -> 'state,
63 bind : 'context * binder -> 'context}
64 -> 'context -> 'state -> Elab.con -> 'state
60 end 65 end
61 66
62 structure Exp : sig 67 structure Exp : sig
63 datatype binder = 68 datatype binder =
64 RelC of string * Elab.kind 69 RelC of string * Elab.kind
81 bind : 'context * binder -> 'context} 86 bind : 'context * binder -> 'context}
82 -> 'context -> (Elab.exp -> Elab.exp) 87 -> 'context -> (Elab.exp -> Elab.exp)
83 val exists : {kind : Elab.kind' -> bool, 88 val exists : {kind : Elab.kind' -> bool,
84 con : Elab.con' -> bool, 89 con : Elab.con' -> bool,
85 exp : Elab.exp' -> bool} -> Elab.exp -> bool 90 exp : Elab.exp' -> bool} -> Elab.exp -> bool
91
92 val foldB : {kind : Elab.kind' * 'state -> 'state,
93 con : 'context * Elab.con' * 'state -> 'state,
94 exp : 'context * Elab.exp' * 'state -> 'state,
95 bind : 'context * binder -> 'context}
96 -> 'context -> 'state -> Elab.exp -> 'state
86 end 97 end
87 98
88 structure Sgn : sig 99 structure Sgn : sig
89 datatype binder = 100 datatype binder =
90 RelC of string * Elab.kind 101 RelC of string * Elab.kind
154 sgn_item : Elab.sgn_item' -> 'a option, 165 sgn_item : Elab.sgn_item' -> 'a option,
155 sgn : Elab.sgn' -> 'a option, 166 sgn : Elab.sgn' -> 'a option,
156 str : Elab.str' -> 'a option, 167 str : Elab.str' -> 'a option,
157 decl : Elab.decl' -> 'a option} 168 decl : Elab.decl' -> 'a option}
158 -> Elab.decl -> 'a option 169 -> Elab.decl -> 'a option
170
171 val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state,
172 con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
173 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
174 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
175 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
176 str : 'context * Elab.str' * 'state -> Elab.str' * 'state,
177 decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
178 bind : 'context * binder -> 'context}
179 -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
180 end
181
182 structure File : sig
183 val maxName : Elab.file -> int
159 end 184 end
160 185
161 end 186 end