diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-06-08 15:47:44 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-06-08 15:47:44 -0400 |
| commit | e18863bcabc5d185b7fe1fc750bdf0bbdb5a4f78 (patch) | |
| tree | 180c8271605929d6c902c4dda9b8b756ff0e1fda /src/core_util.sig | |
| parent | b0bf85209e8ddd4937393908d953f451556e73e9 (diff) | |
Some con reducing
Diffstat (limited to 'src/core_util.sig')
| -rw-r--r-- | src/core_util.sig | 35 |
1 files changed, 32 insertions, 3 deletions
diff --git a/src/core_util.sig b/src/core_util.sig index a40e0664..07350798 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -37,7 +37,7 @@ end structure Con : sig datatype binder = Rel of string * Core.kind - | Named of string * Core.kind + | Named of string * int * Core.kind * Core.con option val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, @@ -62,9 +62,9 @@ end structure Exp : sig datatype binder = RelC of string * Core.kind - | NamedC of string * Core.kind + | NamedC of string * int * Core.kind * Core.con option | RelE of string * Core.con - | NamedE of string * Core.con + | NamedE of string * int * Core.con * Core.exp option val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, @@ -85,4 +85,33 @@ structure Exp : sig exp : Core.exp' -> bool} -> Core.exp -> bool end +structure Decl : sig + datatype binder = datatype Exp.binder + + val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, + exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, + decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB +end + +structure File : sig + datatype binder = datatype Exp.binder + + val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, + exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, + decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Core.file, 'state, 'abort) Search.mapfolderB + + val mapB : {kind : Core.kind' -> Core.kind', + con : 'context -> Core.con' -> Core.con', + exp : 'context -> Core.exp' -> Core.exp', + decl : 'context -> Core.decl' -> Core.decl', + bind : 'context * binder -> 'context} + -> 'context -> Core.file -> Core.file +end + end |