Mercurial > urweb

diff src/core_util.sig @ 626:230654093b51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
demo/hello compiles with kind polymorphism
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 17:17:01 -0500
parents 3162bbf8e30f
children 54ec237a3028
line wrap: on
line diff
--- a/src/core_util.sig	Sun Feb 22 16:33:55 2009 -0500
+++ b/src/core_util.sig	Sun Feb 22 17:17:01 2009 -0500
@@ -30,20 +30,27 @@
 structure Kind : sig
     val compare : Core.kind * Core.kind -> order
 
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * string -> 'context}
+                   -> ('context, Core.kind, 'state, 'abort) Search.mapfolderB
     val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
                   -> (Core.kind, 'state, 'abort) Search.mapfolder
     val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind
     val exists : (Core.kind' -> bool) -> Core.kind -> bool
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
+                bind : 'context * string -> 'context}
+               -> 'context -> (Core.kind -> Core.kind)
 end
 
 structure Con : sig
     val compare : Core.con * Core.con -> order
 
     datatype binder =
-             Rel of string * Core.kind
-           | Named of string * int * Core.kind * Core.con option
+             RelK of string
+           | RelC of string * Core.kind
+           | NamedC of string * int * Core.kind * Core.con option
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
                    -> ('context, Core.con, 'state, 'abort) Search.mapfolderB
@@ -55,7 +62,7 @@
                con : Core.con' -> Core.con'}
               -> Core.con -> Core.con
 
-    val mapB : {kind : Core.kind' -> Core.kind',
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
                 con : 'context -> Core.con' -> Core.con',
                 bind : 'context * binder -> 'context}
                -> 'context -> (Core.con -> Core.con)
@@ -76,12 +83,13 @@
     val compare : Core.exp * Core.exp -> order
 
     datatype binder =
-             RelC of string * Core.kind
+             RelK of string
+           | RelC of string * Core.kind
            | NamedC of string * int * Core.kind * Core.con option
            | RelE of string * Core.con
            | NamedE of string * int * Core.con * Core.exp option * string
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
@@ -95,7 +103,7 @@
                con : Core.con' -> Core.con',
                exp : Core.exp' -> Core.exp'}
               -> Core.exp -> Core.exp
-    val mapB : {kind : Core.kind' -> Core.kind',
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
                 con : 'context -> Core.con' -> Core.con',
                 exp : 'context -> Core.exp' -> Core.exp',
                 bind : 'context * binder -> 'context}
@@ -106,7 +114,7 @@
                 exp : Core.exp' * 'state -> 'state}
                -> 'state -> Core.exp -> 'state
 
-    val foldB : {kind : Core.kind' * 'state -> 'state,
+    val foldB : {kind : 'context * Core.kind' * 'state -> 'state,
                  con : 'context * Core.con' * 'state -> 'state,
                  exp : 'context * Core.exp' * 'state -> 'state,
                  bind : 'context * binder -> 'context}
@@ -116,7 +124,7 @@
                   con : Core.con' -> bool,
                   exp : Core.exp' -> bool} -> Core.exp -> bool
 
-    val existsB : {kind : Core.kind' -> bool,
+    val existsB : {kind : 'context * Core.kind' -> bool,
                    con : 'context * Core.con' -> bool,
                    exp : 'context * Core.exp' -> bool,
                    bind : 'context * binder -> 'context}
@@ -126,7 +134,7 @@
                    con : Core.con' * 'state -> Core.con' * 'state,
                    exp : Core.exp' * 'state -> Core.exp' * 'state}
                   -> 'state -> Core.exp -> Core.exp * 'state
-    val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state,
+    val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
                     con : 'context * Core.con' * 'state -> Core.con' * 'state,
                     exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
                     bind : 'context * binder -> 'context}
@@ -136,7 +144,7 @@
 structure Decl : sig
     datatype binder = datatype Exp.binder
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
                     decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
@@ -159,7 +167,7 @@
                    exp : Core.exp' * 'state -> Core.exp' * 'state,
                    decl : Core.decl' * 'state -> Core.decl' * 'state}
                   -> 'state -> Core.decl -> Core.decl * 'state
-    val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state,
+    val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
                     con : 'context * Core.con' * 'state -> Core.con' * 'state,
                     exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
                     decl : 'context * Core.decl' * 'state -> Core.decl' * 'state,
@@ -177,7 +185,7 @@
 
     datatype binder = datatype Exp.binder
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
                     decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
@@ -190,7 +198,7 @@
                    decl : (Core.decl', 'state, 'abort) Search.mapfolder}
                   -> (Core.file, 'state, 'abort) Search.mapfolder
 
-    val mapB : {kind : Core.kind' -> Core.kind',
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
                 con : 'context -> Core.con' -> Core.con',
                 exp : 'context -> Core.exp' -> Core.exp',
                 decl : 'context -> Core.decl' -> Core.decl',