comparison src/core_util.sig @ 20:1ab48e37d0ef

Some con reducing
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 15:47:44 -0400
parents bc7b76ca57e0
children 067029c748e9
comparison
equal deleted inserted replaced
19:e634ae817a8e 20:1ab48e37d0ef
35 end 35 end
36 36
37 structure Con : sig 37 structure Con : sig
38 datatype binder = 38 datatype binder =
39 Rel of string * Core.kind 39 Rel of string * Core.kind
40 | Named of string * Core.kind 40 | Named of string * int * Core.kind * Core.con option
41 41
42 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 42 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
43 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, 43 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
44 bind : 'context * binder -> 'context} 44 bind : 'context * binder -> 'context}
45 -> ('context, Core.con, 'state, 'abort) Search.mapfolderB 45 -> ('context, Core.con, 'state, 'abort) Search.mapfolderB
60 end 60 end
61 61
62 structure Exp : sig 62 structure Exp : sig
63 datatype binder = 63 datatype binder =
64 RelC of string * Core.kind 64 RelC of string * Core.kind
65 | NamedC of string * Core.kind 65 | NamedC of string * int * Core.kind * Core.con option
66 | RelE of string * Core.con 66 | RelE of string * Core.con
67 | NamedE of string * Core.con 67 | NamedE of string * int * Core.con * Core.exp option
68 68
69 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 69 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
70 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, 70 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
71 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, 71 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
72 bind : 'context * binder -> 'context} 72 bind : 'context * binder -> 'context}
83 val exists : {kind : Core.kind' -> bool, 83 val exists : {kind : Core.kind' -> bool,
84 con : Core.con' -> bool, 84 con : Core.con' -> bool,
85 exp : Core.exp' -> bool} -> Core.exp -> bool 85 exp : Core.exp' -> bool} -> Core.exp -> bool
86 end 86 end
87 87
88 structure Decl : sig
89 datatype binder = datatype Exp.binder
90
91 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
92 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
93 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
94 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
95 bind : 'context * binder -> 'context}
96 -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB
88 end 97 end
98
99 structure File : sig
100 datatype binder = datatype Exp.binder
101
102 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
103 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
104 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
105 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
106 bind : 'context * binder -> 'context}
107 -> ('context, Core.file, 'state, 'abort) Search.mapfolderB
108
109 val mapB : {kind : Core.kind' -> Core.kind',
110 con : 'context -> Core.con' -> Core.con',
111 exp : 'context -> Core.exp' -> Core.exp',
112 decl : 'context -> Core.decl' -> Core.decl',
113 bind : 'context * binder -> 'context}
114 -> 'context -> Core.file -> Core.file
115 end
116
117 end