summaryrefslogtreecommitdiff
path: root/src/expl_util.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-22 16:32:56 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-22 16:32:56 -0500
commit85c5fc291ece27b13a28a3ec50b67ff437a18834 (patch)
tree9720fe837fa35bd4404d0013f77da0e0a51584ae /src/expl_util.sig
parent85cf99a95c910841f197ca911bb13d044456de7f (diff)
Kind polymorphism through Explify
Diffstat (limited to 'src/expl_util.sig')
-rw-r--r--src/expl_util.sig25
1 files changed, 17 insertions, 8 deletions
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,