Mercurial > urweb
diff src/elab_util.sig @ 448:85819353a84f
First Unnest tests working
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 01 Nov 2008 15:58:55 -0400 |
parents | eec65c11d3e2 |
children | 588b9d16b00a |
line wrap: on
line diff
--- a/src/elab_util.sig Sat Nov 01 11:17:29 2008 -0400 +++ b/src/elab_util.sig Sat Nov 01 15:58:55 2008 -0400 @@ -57,6 +57,11 @@ -> Elab.con -> Elab.con val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool + + val foldB : {kind : Elab.kind' * 'state -> 'state, + con : 'context * Elab.con' * 'state -> 'state, + bind : 'context * binder -> 'context} + -> 'context -> 'state -> Elab.con -> 'state end structure Exp : sig @@ -83,6 +88,12 @@ val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool, exp : Elab.exp' -> bool} -> Elab.exp -> bool + + val foldB : {kind : Elab.kind' * 'state -> 'state, + con : 'context * Elab.con' * 'state -> 'state, + exp : 'context * Elab.exp' * 'state -> 'state, + bind : 'context * binder -> 'context} + -> 'context -> 'state -> Elab.exp -> 'state end structure Sgn : sig @@ -156,6 +167,20 @@ str : Elab.str' -> 'a option, decl : Elab.decl' -> 'a option} -> Elab.decl -> 'a option + + val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state, + con : 'context * Elab.con' * 'state -> Elab.con' * 'state, + exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, + sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, + sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state, + str : 'context * Elab.str' * 'state -> Elab.str' * 'state, + decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state, + bind : 'context * binder -> 'context} + -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state +end + +structure File : sig + val maxName : Elab.file -> int end end