From 1f7d0c20ae30c11cdc64a2c2fc90f15cdf02c34b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 22 Feb 2009 17:17:01 -0500 Subject: demo/hello compiles with kind polymorphism --- src/core_util.sig | 36 ++++++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 14 deletions(-) (limited to 'src/core_util.sig') diff --git a/src/core_util.sig b/src/core_util.sig index fc5a2bea..fabb9878 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -30,20 +30,27 @@ signature CORE_UTIL = sig 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 @@ structure Con : sig 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 @@ structure Exp : sig 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 @@ structure Exp : sig 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 @@ structure Exp : sig 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 @@ structure Exp : sig 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 @@ structure Exp : sig 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 @@ end 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 @@ structure Decl : sig 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 @@ structure File : 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, @@ -190,7 +198,7 @@ structure File : sig 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', -- cgit v1.2.3