Mercurial > urweb
comparison src/core_util.sig @ 193:8a70e2919e86
Specialization of single-parameter datatypes
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 08 Aug 2008 17:55:51 -0400 |
parents | 8e9f97508f0d |
children | ab86aa858e6c |
comparison
equal
deleted
inserted
replaced
192:9bbf4d383381 | 193:8a70e2919e86 |
---|---|
28 signature CORE_UTIL = sig | 28 signature CORE_UTIL = sig |
29 | 29 |
30 val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind | 30 val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind |
31 | 31 |
32 structure Kind : sig | 32 structure Kind : sig |
33 val compare : Core.kind * Core.kind -> order | |
34 | |
33 val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder | 35 val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder |
34 -> (Core.kind, 'state, 'abort) Search.mapfolder | 36 -> (Core.kind, 'state, 'abort) Search.mapfolder |
35 val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind | 37 val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind |
36 val exists : (Core.kind' -> bool) -> Core.kind -> bool | 38 val exists : (Core.kind' -> bool) -> Core.kind -> bool |
37 end | 39 end |
38 | 40 |
39 structure Con : sig | 41 structure Con : sig |
42 val compare : Core.con * Core.con -> order | |
43 | |
40 datatype binder = | 44 datatype binder = |
41 Rel of string * Core.kind | 45 Rel of string * Core.kind |
42 | Named of string * int * Core.kind * Core.con option | 46 | Named of string * int * Core.kind * Core.con option |
43 | 47 |
44 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, | 48 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, |
62 con : Core.con' * 'state -> 'state} | 66 con : Core.con' * 'state -> 'state} |
63 -> 'state -> Core.con -> 'state | 67 -> 'state -> Core.con -> 'state |
64 | 68 |
65 val exists : {kind : Core.kind' -> bool, | 69 val exists : {kind : Core.kind' -> bool, |
66 con : Core.con' -> bool} -> Core.con -> bool | 70 con : Core.con' -> bool} -> Core.con -> bool |
71 | |
72 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, | |
73 con : Core.con' * 'state -> Core.con' * 'state} | |
74 -> 'state -> Core.con -> Core.con * 'state | |
67 end | 75 end |
68 | 76 |
69 structure Exp : sig | 77 structure Exp : sig |
70 datatype binder = | 78 datatype binder = |
71 RelC of string * Core.kind | 79 RelC of string * Core.kind |