From e18863bcabc5d185b7fe1fc750bdf0bbdb5a4f78 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sun, 8 Jun 2008 15:47:44 -0400
Subject: Some con reducing

---
 src/core_util.sig | 35 ++++++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

(limited to 'src/core_util.sig')

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
-- 
cgit v1.2.3