Mercurial > urweb

diff src/core_util.sig @ 20:1ab48e37d0ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some con reducing
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 15:47:44 -0400
parents bc7b76ca57e0
children 067029c748e9
line wrap: on
line diff
--- a/src/core_util.sig	Sun Jun 08 14:42:12 2008 -0400
+++ b/src/core_util.sig	Sun Jun 08 15:47:44 2008 -0400
@@ -37,7 +37,7 @@
 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 @@
 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 @@
                   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