Mercurial > urweb
comparison src/elab_util.sig @ 623:588b9d16b00a
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Feb 2009 16:10:25 -0500 |
parents | 85819353a84f |
children | 7292bcb7c02d |
comparison
equal
deleted
inserted
replaced
622:d64533157f40 | 623:588b9d16b00a |
---|---|
28 signature ELAB_UTIL = sig | 28 signature ELAB_UTIL = sig |
29 | 29 |
30 val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind | 30 val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind |
31 | 31 |
32 structure Kind : sig | 32 structure Kind : sig |
33 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, | |
34 bind : 'context * string -> 'context} | |
35 -> ('context, Elab.kind, 'state, 'abort) Search.mapfolderB | |
33 val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder | 36 val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder |
34 -> (Elab.kind, 'state, 'abort) Search.mapfolder | 37 -> (Elab.kind, 'state, 'abort) Search.mapfolder |
35 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool | 38 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool |
39 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', | |
40 bind : 'context * string -> 'context} | |
41 -> 'context -> (Elab.kind -> Elab.kind) | |
36 end | 42 end |
37 | 43 |
38 structure Con : sig | 44 structure Con : sig |
39 datatype binder = | 45 datatype binder = |
40 Rel of string * Elab.kind | 46 RelK of string |
41 | Named of string * int * Elab.kind | 47 | RelC of string * Elab.kind |
48 | NamedC of string * int * Elab.kind | |
42 | 49 |
43 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, | 50 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, |
44 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, | 51 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, |
45 bind : 'context * binder -> 'context} | 52 bind : 'context * binder -> 'context} |
46 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB | 53 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB |
47 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, | 54 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, |
48 con : (Elab.con', 'state, 'abort) Search.mapfolder} | 55 con : (Elab.con', 'state, 'abort) Search.mapfolder} |
49 -> (Elab.con, 'state, 'abort) Search.mapfolder | 56 -> (Elab.con, 'state, 'abort) Search.mapfolder |
50 | 57 |
51 val mapB : {kind : Elab.kind' -> Elab.kind', | 58 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', |
52 con : 'context -> Elab.con' -> Elab.con', | 59 con : 'context -> Elab.con' -> Elab.con', |
53 bind : 'context * binder -> 'context} | 60 bind : 'context * binder -> 'context} |
54 -> 'context -> (Elab.con -> Elab.con) | 61 -> 'context -> (Elab.con -> Elab.con) |
55 val map : {kind : Elab.kind' -> Elab.kind', | 62 val map : {kind : Elab.kind' -> Elab.kind', |
56 con : Elab.con' -> Elab.con'} | 63 con : Elab.con' -> Elab.con'} |
57 -> Elab.con -> Elab.con | 64 -> Elab.con -> Elab.con |
58 val exists : {kind : Elab.kind' -> bool, | 65 val exists : {kind : Elab.kind' -> bool, |
59 con : Elab.con' -> bool} -> Elab.con -> bool | 66 con : Elab.con' -> bool} -> Elab.con -> bool |
60 | 67 |
61 val foldB : {kind : Elab.kind' * 'state -> 'state, | 68 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, |
62 con : 'context * Elab.con' * 'state -> 'state, | 69 con : 'context * Elab.con' * 'state -> 'state, |
63 bind : 'context * binder -> 'context} | 70 bind : 'context * binder -> 'context} |
64 -> 'context -> 'state -> Elab.con -> 'state | 71 -> 'context -> 'state -> Elab.con -> 'state |
65 end | 72 end |
66 | 73 |
67 structure Exp : sig | 74 structure Exp : sig |
68 datatype binder = | 75 datatype binder = |
69 RelC of string * Elab.kind | 76 RelK of string |
77 | RelC of string * Elab.kind | |
70 | NamedC of string * int * Elab.kind | 78 | NamedC of string * int * Elab.kind |
71 | RelE of string * Elab.con | 79 | RelE of string * Elab.con |
72 | NamedE of string * Elab.con | 80 | NamedE of string * Elab.con |
73 | 81 |
74 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, | 82 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, |
75 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, | 83 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, |
76 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, | 84 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, |
77 bind : 'context * binder -> 'context} | 85 bind : 'context * binder -> 'context} |
78 -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB | 86 -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB |
79 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, | 87 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, |
80 con : (Elab.con', 'state, 'abort) Search.mapfolder, | 88 con : (Elab.con', 'state, 'abort) Search.mapfolder, |
81 exp : (Elab.exp', 'state, 'abort) Search.mapfolder} | 89 exp : (Elab.exp', 'state, 'abort) Search.mapfolder} |
82 -> (Elab.exp, 'state, 'abort) Search.mapfolder | 90 -> (Elab.exp, 'state, 'abort) Search.mapfolder |
83 val mapB : {kind : Elab.kind' -> Elab.kind', | 91 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', |
84 con : 'context -> Elab.con' -> Elab.con', | 92 con : 'context -> Elab.con' -> Elab.con', |
85 exp : 'context -> Elab.exp' -> Elab.exp', | 93 exp : 'context -> Elab.exp' -> Elab.exp', |
86 bind : 'context * binder -> 'context} | 94 bind : 'context * binder -> 'context} |
87 -> 'context -> (Elab.exp -> Elab.exp) | 95 -> 'context -> (Elab.exp -> Elab.exp) |
88 val exists : {kind : Elab.kind' -> bool, | 96 val exists : {kind : Elab.kind' -> bool, |
89 con : Elab.con' -> bool, | 97 con : Elab.con' -> bool, |
90 exp : Elab.exp' -> bool} -> Elab.exp -> bool | 98 exp : Elab.exp' -> bool} -> Elab.exp -> bool |
91 | 99 |
92 val foldB : {kind : Elab.kind' * 'state -> 'state, | 100 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, |
93 con : 'context * Elab.con' * 'state -> 'state, | 101 con : 'context * Elab.con' * 'state -> 'state, |
94 exp : 'context * Elab.exp' * 'state -> 'state, | 102 exp : 'context * Elab.exp' * 'state -> 'state, |
95 bind : 'context * binder -> 'context} | 103 bind : 'context * binder -> 'context} |
96 -> 'context -> 'state -> Elab.exp -> 'state | 104 -> 'context -> 'state -> Elab.exp -> 'state |
97 end | 105 end |
98 | 106 |
99 structure Sgn : sig | 107 structure Sgn : sig |
100 datatype binder = | 108 datatype binder = |
101 RelC of string * Elab.kind | 109 RelK of string |
110 | RelC of string * Elab.kind | |
102 | NamedC of string * int * Elab.kind | 111 | NamedC of string * int * Elab.kind |
103 | Str of string * Elab.sgn | 112 | Str of string * Elab.sgn |
104 | Sgn of string * Elab.sgn | 113 | Sgn of string * Elab.sgn |
105 | 114 |
106 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, | 115 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, |
107 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, | 116 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, |
108 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, | 117 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, |
109 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, | 118 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, |
110 bind : 'context * binder -> 'context} | 119 bind : 'context * binder -> 'context} |
111 -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB | 120 -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB |
125 | 134 |
126 end | 135 end |
127 | 136 |
128 structure Decl : sig | 137 structure Decl : sig |
129 datatype binder = | 138 datatype binder = |
130 RelC of string * Elab.kind | 139 RelK of string |
140 | RelC of string * Elab.kind | |
131 | NamedC of string * int * Elab.kind | 141 | NamedC of string * int * Elab.kind |
132 | RelE of string * Elab.con | 142 | RelE of string * Elab.con |
133 | NamedE of string * Elab.con | 143 | NamedE of string * Elab.con |
134 | Str of string * Elab.sgn | 144 | Str of string * Elab.sgn |
135 | Sgn of string * Elab.sgn | 145 | Sgn of string * Elab.sgn |
136 | 146 |
137 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, | 147 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, |
138 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, | 148 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, |
139 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, | 149 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, |
140 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, | 150 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, |
141 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, | 151 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, |
142 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB, | 152 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB, |
166 sgn : Elab.sgn' -> 'a option, | 176 sgn : Elab.sgn' -> 'a option, |
167 str : Elab.str' -> 'a option, | 177 str : Elab.str' -> 'a option, |
168 decl : Elab.decl' -> 'a option} | 178 decl : Elab.decl' -> 'a option} |
169 -> Elab.decl -> 'a option | 179 -> Elab.decl -> 'a option |
170 | 180 |
171 val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state, | 181 val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state, |
172 con : 'context * Elab.con' * 'state -> Elab.con' * 'state, | 182 con : 'context * Elab.con' * 'state -> Elab.con' * 'state, |
173 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, | 183 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, |
174 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, | 184 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, |
175 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state, | 185 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state, |
176 str : 'context * Elab.str' * 'state -> Elab.str' * 'state, | 186 str : 'context * Elab.str' * 'state -> Elab.str' * 'state, |