Mercurial > urweb

comparison src/expl_util.sig @ 624:354800878b4d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Kind polymorphism through Explify
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:32:56 -0500
parents ab86aa858e6c
children
comparison
equal deleted inserted replaced
623:588b9d16b00a 624:354800878b4d
26 *) 26 *)
27 27
28 signature EXPL_UTIL = sig 28 signature EXPL_UTIL = sig
29 29
30 structure Kind : sig 30 structure Kind : sig
31 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
32 bind : 'context * string -> 'context}
33 -> ('context, Expl.kind, 'state, 'abort) Search.mapfolderB
31 val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder 34 val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
32 -> (Expl.kind, 'state, 'abort) Search.mapfolder 35 -> (Expl.kind, 'state, 'abort) Search.mapfolder
33 val exists : (Expl.kind' -> bool) -> Expl.kind -> bool 36 val exists : (Expl.kind' -> bool) -> Expl.kind -> bool
37 val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
38 bind : 'context * string -> 'context}
39 -> 'context -> (Expl.kind -> Expl.kind)
34 end 40 end
35 41
36 structure Con : sig 42 structure Con : sig
37 datatype binder = 43 datatype binder =
38 Rel of string * Expl.kind 44 RelK of string
39 | Named of string * Expl.kind 45 | RelC of string * Expl.kind
46 | NamedC of string * Expl.kind
40 47
41 val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, 48 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
42 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, 49 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
43 bind : 'context * binder -> 'context} 50 bind : 'context * binder -> 'context}
44 -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB 51 -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB
45 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, 52 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
46 con : (Expl.con', 'state, 'abort) Search.mapfolder} 53 con : (Expl.con', 'state, 'abort) Search.mapfolder}
47 -> (Expl.con, 'state, 'abort) Search.mapfolder 54 -> (Expl.con, 'state, 'abort) Search.mapfolder
48 55
49 val mapB : {kind : Expl.kind' -> Expl.kind', 56 val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
50 con : 'context -> Expl.con' -> Expl.con', 57 con : 'context -> Expl.con' -> Expl.con',
51 bind : 'context * binder -> 'context} 58 bind : 'context * binder -> 'context}
52 -> 'context -> (Expl.con -> Expl.con) 59 -> 'context -> (Expl.con -> Expl.con)
53 val map : {kind : Expl.kind' -> Expl.kind', 60 val map : {kind : Expl.kind' -> Expl.kind',
54 con : Expl.con' -> Expl.con'} 61 con : Expl.con' -> Expl.con'}
57 con : Expl.con' -> bool} -> Expl.con -> bool 64 con : Expl.con' -> bool} -> Expl.con -> bool
58 end 65 end
59 66
60 structure Exp : sig 67 structure Exp : sig
61 datatype binder = 68 datatype binder =
62 RelC of string * Expl.kind 69 RelK of string
70 | RelC of string * Expl.kind
63 | NamedC of string * Expl.kind 71 | NamedC of string * Expl.kind
64 | RelE of string * Expl.con 72 | RelE of string * Expl.con
65 | NamedE of string * Expl.con 73 | NamedE of string * Expl.con
66 74
67 val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, 75 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
68 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, 76 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
69 exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB, 77 exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB,
70 bind : 'context * binder -> 'context} 78 bind : 'context * binder -> 'context}
71 -> ('context, Expl.exp, 'state, 'abort) Search.mapfolderB 79 -> ('context, Expl.exp, 'state, 'abort) Search.mapfolderB
72 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, 80 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
78 exp : Expl.exp' -> bool} -> Expl.exp -> bool 86 exp : Expl.exp' -> bool} -> Expl.exp -> bool
79 end 87 end
80 88
81 structure Sgn : sig 89 structure Sgn : sig
82 datatype binder = 90 datatype binder =
83 RelC of string * Expl.kind 91 RelK of string
92 | RelC of string * Expl.kind
84 | NamedC of string * Expl.kind 93 | NamedC of string * Expl.kind
85 | Sgn of string * Expl.sgn 94 | Sgn of string * Expl.sgn
86 | Str of string * Expl.sgn 95 | Str of string * Expl.sgn
87 96
88 val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, 97 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
89 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, 98 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
90 sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB, 99 sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB,
91 sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB, 100 sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB,
92 bind : 'context * binder -> 'context} 101 bind : 'context * binder -> 'context}
93 -> ('context, Expl.sgn, 'state, 'abort) Search.mapfolderB 102 -> ('context, Expl.sgn, 'state, 'abort) Search.mapfolderB