Mercurial > urweb
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 |