From 56fa65fe24da94c3a0d2ce1fcdd0bd7325e5d7ba Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sun, 22 Feb 2009 16:32:56 -0500
Subject: Kind polymorphism through Explify

---
 src/expl_util.sig | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

(limited to 'src/expl_util.sig')

diff --git a/src/expl_util.sig b/src/expl_util.sig
index 2a6c7abe..3e5c333f 100644
--- a/src/expl_util.sig
+++ b/src/expl_util.sig
@@ -28,17 +28,24 @@
 signature EXPL_UTIL = sig
 
 structure Kind : sig
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * string -> 'context}
+                   -> ('context, Expl.kind, 'state, 'abort) Search.mapfolderB
     val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
                   -> (Expl.kind, 'state, 'abort) Search.mapfolder
     val exists : (Expl.kind' -> bool) -> Expl.kind -> bool
+    val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
+                bind : 'context * string -> 'context}
+               -> 'context -> (Expl.kind -> Expl.kind)
 end
 
 structure Con : sig
     datatype binder =
-             Rel of string * Expl.kind
-           | Named of string * Expl.kind
+             RelK of string
+           | RelC of string * Expl.kind
+           | NamedC of string * Expl.kind
 
-    val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
                    -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB
@@ -46,7 +53,7 @@ structure Con : sig
                    con : (Expl.con', 'state, 'abort) Search.mapfolder}
                   -> (Expl.con, 'state, 'abort) Search.mapfolder
 
-    val mapB : {kind : Expl.kind' -> Expl.kind',
+    val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
                 con : 'context -> Expl.con' -> Expl.con',
                 bind : 'context * binder -> 'context}
                -> 'context -> (Expl.con -> Expl.con)
@@ -59,12 +66,13 @@ end
 
 structure Exp : sig
     datatype binder =
-             RelC of string * Expl.kind
+             RelK of string
+           | RelC of string * Expl.kind
            | NamedC of string * Expl.kind
            | RelE of string * Expl.con
            | NamedE of string * Expl.con
 
-    val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
@@ -80,12 +88,13 @@ end
 
 structure Sgn : sig
     datatype binder =
-             RelC of string * Expl.kind
+             RelK of string
+           | RelC of string * Expl.kind
            | NamedC of string * Expl.kind
            | Sgn of string * Expl.sgn
            | Str of string * Expl.sgn
 
-    val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
                     sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB,
                     sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB,
-- 
cgit v1.2.3