Mercurial > urweb

comparison src/elab_util.sig @ 792:d20d6afc1206

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improvements while working on Graftid
author Adam Chlipala <adamc@hcoop.net>
date Tue, 12 May 2009 18:02:25 -0400
parents 7292bcb7c02d
children b2413e4dd109
comparison
equal deleted inserted replaced
791:5368deb3764b 792:d20d6afc1206
43 43
44 structure Con : sig 44 structure Con : sig
45 datatype binder = 45 datatype binder =
46 RelK of string 46 RelK of string
47 | RelC of string * Elab.kind 47 | RelC of string * Elab.kind
48 | NamedC of string * int * Elab.kind 48 | NamedC of string * int * Elab.kind * Elab.con option
49 49
50 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, 50 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
51 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 51 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
52 bind : 'context * binder -> 'context} 52 bind : 'context * binder -> 'context}
53 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB 53 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB
77 77
78 structure Exp : sig 78 structure Exp : sig
79 datatype binder = 79 datatype binder =
80 RelK of string 80 RelK of string
81 | RelC of string * Elab.kind 81 | RelC of string * Elab.kind
82 | NamedC of string * int * Elab.kind 82 | NamedC of string * int * Elab.kind * Elab.con option
83 | RelE of string * Elab.con 83 | RelE of string * Elab.con
84 | NamedE of string * Elab.con 84 | NamedE of string * Elab.con
85 85
86 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, 86 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
87 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 87 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
110 110
111 structure Sgn : sig 111 structure Sgn : sig
112 datatype binder = 112 datatype binder =
113 RelK of string 113 RelK of string
114 | RelC of string * Elab.kind 114 | RelC of string * Elab.kind
115 | NamedC of string * int * Elab.kind 115 | NamedC of string * int * Elab.kind * Elab.con option
116 | Str of string * Elab.sgn 116 | Str of string * int * Elab.sgn
117 | Sgn of string * Elab.sgn 117 | Sgn of string * int * Elab.sgn
118 118
119 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, 119 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
120 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 120 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
121 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, 121 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
122 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, 122 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
134 con : Elab.con' -> Elab.con', 134 con : Elab.con' -> Elab.con',
135 sgn_item : Elab.sgn_item' -> Elab.sgn_item', 135 sgn_item : Elab.sgn_item' -> Elab.sgn_item',
136 sgn : Elab.sgn' -> Elab.sgn'} 136 sgn : Elab.sgn' -> Elab.sgn'}
137 -> Elab.sgn -> Elab.sgn 137 -> Elab.sgn -> Elab.sgn
138 138
139 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
140 con : 'context -> Elab.con' -> Elab.con',
141 sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
142 sgn : 'context -> Elab.sgn' -> Elab.sgn',
143 bind : 'context * binder -> 'context}
144 -> 'context -> Elab.sgn -> Elab.sgn
145
139 end 146 end
140 147
141 structure Decl : sig 148 structure Decl : sig
142 datatype binder = 149 datatype binder =
143 RelK of string 150 RelK of string
144 | RelC of string * Elab.kind 151 | RelC of string * Elab.kind
145 | NamedC of string * int * Elab.kind 152 | NamedC of string * int * Elab.kind * Elab.con option
146 | RelE of string * Elab.con 153 | RelE of string * Elab.con
147 | NamedE of string * Elab.con 154 | NamedE of string * Elab.con
148 | Str of string * Elab.sgn 155 | Str of string * Elab.sgn
149 | Sgn of string * Elab.sgn 156 | Sgn of string * Elab.sgn
150 157