Mercurial > urweb

comparison src/elab_util.sig @ 11:e97c6d335869

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple elaboration working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 15:20:46 -0400
parents dde5c52e5e5e
children 6049e2193bf2
comparison
equal deleted inserted replaced
10:dde5c52e5e5e 11:e97c6d335869
32 -> (Elab.kind, 'state, 'abort) Search.mapfolder 32 -> (Elab.kind, 'state, 'abort) Search.mapfolder
33 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool 33 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
34 end 34 end
35 35
36 structure Con : sig 36 structure Con : sig
37 datatype binder =
38 Rel of string * Elab.kind
39 | Named of string * Elab.kind
40
41 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
42 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
43 bind : 'context * binder -> 'context}
44 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB
37 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 45 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
38 con : (Elab.con', 'state, 'abort) Search.mapfolder} 46 con : (Elab.con', 'state, 'abort) Search.mapfolder}
39 -> (Elab.con, 'state, 'abort) Search.mapfolder 47 -> (Elab.con, 'state, 'abort) Search.mapfolder
48
49 val mapB : {kind : Elab.kind' -> Elab.kind',
50 con : 'context -> Elab.con' -> Elab.con',
51 bind : 'context * binder -> 'context}
52 -> 'context -> (Elab.con -> Elab.con)
40 val exists : {kind : Elab.kind' -> bool, 53 val exists : {kind : Elab.kind' -> bool,
41 con : Elab.con' -> bool} -> Elab.con -> bool 54 con : Elab.con' -> bool} -> Elab.con -> bool
42 end 55 end
43 56
44 structure Exp : sig 57 structure Exp : sig
58 datatype binder =
59 RelC of string * Elab.kind
60 | NamedC of string * Elab.kind
61 | RelE of string * Elab.con
62 | NamedE of string * Elab.con
63
64 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
65 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
66 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
67 bind : 'context * binder -> 'context}
68 -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB
45 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 69 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
46 con : (Elab.con', 'state, 'abort) Search.mapfolder, 70 con : (Elab.con', 'state, 'abort) Search.mapfolder,
47 exp : (Elab.exp', 'state, 'abort) Search.mapfolder} 71 exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
48 -> (Elab.exp, 'state, 'abort) Search.mapfolder 72 -> (Elab.exp, 'state, 'abort) Search.mapfolder
49 val exists : {kind : Elab.kind' -> bool, 73 val exists : {kind : Elab.kind' -> bool,