comparison src/core_util.sig @ 479:ffa18975e661

Broaden set of possible especializations
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 14:42:52 -0500
parents bd9ee9aeca2f
children 9117a7bf229c
comparison
equal deleted inserted replaced
478:6ee1c761818f 479:ffa18975e661
71 con : Core.con' * 'state -> Core.con' * 'state} 71 con : Core.con' * 'state -> Core.con' * 'state}
72 -> 'state -> Core.con -> Core.con * 'state 72 -> 'state -> Core.con -> Core.con * 'state
73 end 73 end
74 74
75 structure Exp : sig 75 structure Exp : sig
76 val compare : Core.exp * Core.exp -> order
77
76 datatype binder = 78 datatype binder =
77 RelC of string * Core.kind 79 RelC of string * Core.kind
78 | NamedC of string * int * Core.kind * Core.con option 80 | NamedC of string * int * Core.kind * Core.con option
79 | RelE of string * Core.con 81 | RelE of string * Core.con
80 | NamedE of string * int * Core.con * Core.exp option * string 82 | NamedE of string * int * Core.con * Core.exp option * string
105 -> 'state -> Core.exp -> 'state 107 -> 'state -> Core.exp -> 'state
106 108
107 val exists : {kind : Core.kind' -> bool, 109 val exists : {kind : Core.kind' -> bool,
108 con : Core.con' -> bool, 110 con : Core.con' -> bool,
109 exp : Core.exp' -> bool} -> Core.exp -> bool 111 exp : Core.exp' -> bool} -> Core.exp -> bool
112
113 val existsB : {kind : Core.kind' -> bool,
114 con : 'context * Core.con' -> bool,
115 exp : 'context * Core.exp' -> bool,
116 bind : 'context * binder -> 'context}
117 -> 'context -> Core.exp -> bool
110 118
111 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, 119 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
112 con : Core.con' * 'state -> Core.con' * 'state, 120 con : Core.con' * 'state -> Core.con' * 'state,
113 exp : Core.exp' * 'state -> Core.exp' * 'state} 121 exp : Core.exp' * 'state -> Core.exp' * 'state}
114 -> 'state -> Core.exp -> Core.exp * 'state 122 -> 'state -> Core.exp -> Core.exp * 'state