33192

1 
(* Title: HOL/Nitpick/Tools/nitpick_mono.ML


2 
Author: Jasmin Blanchette, TU Muenchen


3 
Copyright 2009


4 


5 
Monotonicity predicate for higherorder logic.


6 
*)


7 


8 
signature NITPICK_MONO =


9 
sig


10 
type extended_context = NitpickHOL.extended_context


11 


12 
val formulas_monotonic :


13 
extended_context > typ > term list > term list > term > bool


14 
end;


15 


16 
structure NitpickMono : NITPICK_MONO =


17 
struct


18 


19 
open NitpickUtil


20 
open NitpickHOL


21 


22 
type var = int


23 


24 
datatype sign = Pos  Neg


25 
datatype sign_atom = S of sign  V of var


26 


27 
type literal = var * sign


28 


29 
datatype ctype =


30 
CAlpha 


31 
CFun of ctype * sign_atom * ctype 


32 
CPair of ctype * ctype 


33 
CType of string * ctype list 


34 
CRec of string * typ list


35 


36 
type cdata =


37 
{ext_ctxt: extended_context,


38 
alpha_T: typ,


39 
max_fresh: int Unsynchronized.ref,


40 
datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,


41 
constr_cache: (styp * ctype) list Unsynchronized.ref}


42 


43 
exception CTYPE of string * ctype list


44 


45 
(* string > unit *)


46 
fun print_g (s : string) = ()


47 


48 
(* var > string *)


49 
val string_for_var = signed_string_of_int


50 
(* string > var list > string *)


51 
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"


52 
 string_for_vars sep xs = space_implode sep (map string_for_var xs)


53 
fun subscript_string_for_vars sep xs =


54 
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"


55 


56 
(* sign > string *)


57 
fun string_for_sign Pos = "+"


58 
 string_for_sign Neg = ""


59 


60 
(* sign > sign > sign *)


61 
fun xor sn1 sn2 = if sn1 = sn2 then Pos else Neg


62 
(* sign > sign *)


63 
val negate = xor Neg


64 


65 
(* sign_atom > string *)


66 
fun string_for_sign_atom (S sn) = string_for_sign sn


67 
 string_for_sign_atom (V j) = string_for_var j


68 


69 
(* literal > string *)


70 
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn


71 


72 
val bool_C = CType (@{type_name bool}, [])


73 


74 
(* ctype > bool *)


75 
fun is_CRec (CRec _) = true


76 
 is_CRec _ = false


77 


78 
val no_prec = 100


79 
val prec_CFun = 1


80 
val prec_CPair = 2


81 


82 
(* tuple_set > int *)


83 
fun precedence_of_ctype (CFun _) = prec_CFun


84 
 precedence_of_ctype (CPair _) = prec_CPair


85 
 precedence_of_ctype _ = no_prec


86 


87 
(* ctype > string *)


88 
val string_for_ctype =


89 
let


90 
(* int > ctype > string *)


91 
fun aux outer_prec C =


92 
let


93 
val prec = precedence_of_ctype C


94 
val need_parens = (prec < outer_prec)


95 
in


96 
(if need_parens then "(" else "") ^


97 
(case C of


98 
CAlpha => "\<alpha>"


99 
 CFun (C1, a, C2) =>


100 
aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^


101 
string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2


102 
 CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2


103 
 CType (s, []) =>


104 
if s mem [@{type_name prop}, @{type_name bool}] then "o" else s


105 
 CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s


106 
 CRec (s, _) => "[" ^ s ^ "]") ^


107 
(if need_parens then ")" else "")


108 
end


109 
in aux 0 end


110 


111 
(* ctype > ctype list *)


112 
fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2]


113 
 flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs


114 
 flatten_ctype C = [C]


115 


116 
(* extended_context > typ > cdata *)


117 
fun initial_cdata ext_ctxt alpha_T =


118 
({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,


119 
datatype_cache = Unsynchronized.ref [],


120 
constr_cache = Unsynchronized.ref []} : cdata)


121 


122 
(* typ > typ > bool *)


123 
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =


124 
T = alpha_T orelse (not (is_fp_iterator_type T)


125 
andalso exists (could_exist_alpha_subtype alpha_T) Ts)


126 
 could_exist_alpha_subtype alpha_T T = (T = alpha_T)


127 
(* theory > typ > typ > bool *)


128 
fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) =


129 
could_exist_alpha_subtype alpha_T


130 
 could_exist_alpha_sub_ctype thy alpha_T = equal alpha_T orf is_datatype thy


131 


132 
(* ctype > bool *)


133 
fun exists_alpha_sub_ctype CAlpha = true


134 
 exists_alpha_sub_ctype (CFun (C1, _, C2)) =


135 
exists exists_alpha_sub_ctype [C1, C2]


136 
 exists_alpha_sub_ctype (CPair (C1, C2)) =


137 
exists exists_alpha_sub_ctype [C1, C2]


138 
 exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs


139 
 exists_alpha_sub_ctype (CRec _) = true


140 


141 
(* ctype > bool *)


142 
fun exists_alpha_sub_ctype_fresh CAlpha = true


143 
 exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true


144 
 exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) =


145 
exists_alpha_sub_ctype_fresh C2


146 
 exists_alpha_sub_ctype_fresh (CPair (C1, C2)) =


147 
exists exists_alpha_sub_ctype_fresh [C1, C2]


148 
 exists_alpha_sub_ctype_fresh (CType (_, Cs)) =


149 
exists exists_alpha_sub_ctype_fresh Cs


150 
 exists_alpha_sub_ctype_fresh (CRec _) = true


151 


152 
(* string * typ list > ctype list > ctype *)


153 
fun constr_ctype_for_binders z Cs =


154 
fold_rev (fn C => curry3 CFun C (S Neg)) Cs (CRec z)


155 


156 
(* ((string * typ list) * ctype) list > ctype list > ctype > ctype *)


157 
fun repair_ctype _ _ CAlpha = CAlpha


158 
 repair_ctype cache seen (CFun (C1, a, C2)) =


159 
CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2)


160 
 repair_ctype cache seen (CPair Cp) =


161 
CPair (pairself (repair_ctype cache seen) Cp)


162 
 repair_ctype cache seen (CType (s, Cs)) =


163 
CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs)


164 
 repair_ctype cache seen (CRec (z as (s, _))) =


165 
case AList.lookup (op =) cache z > the of


166 
CRec _ => CType (s, [])


167 
 C => if C mem seen then CType (s, [])


168 
else repair_ctype cache (C :: seen) C


169 


170 
(* ((string * typ list) * ctype) list Unsynchronized.ref > unit *)


171 
fun repair_datatype_cache cache =


172 
let


173 
(* (string * typ list) * ctype > unit *)


174 
fun repair_one (z, C) =


175 
Unsynchronized.change cache


176 
(AList.update (op =) (z, repair_ctype (!cache) [] C))


177 
in List.app repair_one (rev (!cache)) end


178 


179 
(* (typ * ctype) list > (styp * ctype) list Unsynchronized.ref > unit *)


180 
fun repair_constr_cache dtype_cache constr_cache =


181 
let


182 
(* styp * ctype > unit *)


183 
fun repair_one (x, C) =


184 
Unsynchronized.change constr_cache


185 
(AList.update (op =) (x, repair_ctype dtype_cache [] C))


186 
in List.app repair_one (!constr_cache) end


187 


188 
(* cdata > typ > ctype *)


189 
fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,


190 
datatype_cache, constr_cache, ...} : cdata) =


191 
let


192 
(* typ > typ > ctype *)


193 
fun do_fun T1 T2 =


194 
let


195 
val C1 = do_type T1


196 
val C2 = do_type T2


197 
val a = if is_boolean_type (body_type T2)


198 
andalso exists_alpha_sub_ctype_fresh C1 then


199 
V (Unsynchronized.inc max_fresh)


200 
else


201 
S Neg


202 
in CFun (C1, a, C2) end


203 
(* typ > ctype *)


204 
and do_type T =


205 
if T = alpha_T then


206 
CAlpha


207 
else case T of


208 
Type ("fun", [T1, T2]) => do_fun T1 T2


209 
 Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2


210 
 Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2))


211 
 Type (z as (s, _)) =>


212 
if could_exist_alpha_sub_ctype thy alpha_T T then


213 
case AList.lookup (op =) (!datatype_cache) z of


214 
SOME C => C


215 
 NONE =>


216 
let


217 
val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))


218 
val xs = datatype_constrs thy T


219 
val (all_Cs, constr_Cs) =


220 
fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>


221 
let


222 
val binder_Cs = map do_type (binder_types T')


223 
val new_Cs = filter exists_alpha_sub_ctype_fresh


224 
binder_Cs


225 
val constr_C = constr_ctype_for_binders z


226 
binder_Cs


227 
in


228 
(union (op =) new_Cs all_Cs,


229 
constr_C :: constr_Cs)


230 
end)


231 
xs ([], [])


232 
val C = CType (s, all_Cs)


233 
val _ = Unsynchronized.change datatype_cache


234 
(AList.update (op =) (z, C))


235 
val _ = Unsynchronized.change constr_cache


236 
(append (xs ~~ constr_Cs))


237 
in


238 
if forall (not o is_CRec o snd) (!datatype_cache) then


239 
(repair_datatype_cache datatype_cache;


240 
repair_constr_cache (!datatype_cache) constr_cache;


241 
AList.lookup (op =) (!datatype_cache) z > the)


242 
else


243 
C


244 
end


245 
else


246 
CType (s, [])


247 
 _ => CType (Refute.string_of_typ T, [])


248 
in do_type end


249 


250 
(* ctype > ctype list *)


251 
fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]


252 
 prodC_factors C = [C]


253 
(* ctype > ctype list * ctype *)


254 
fun curried_strip_ctype (CFun (C1, S Neg, C2)) =


255 
curried_strip_ctype C2 >> append (prodC_factors C1)


256 
 curried_strip_ctype C = ([], C)


257 
(* string > ctype > ctype *)


258 
fun sel_ctype_from_constr_ctype s C =


259 
let val (arg_Cs, dataC) = curried_strip_ctype C in


260 
CFun (dataC, S Neg,


261 
case sel_no_from_name s of ~1 => bool_C  n => nth arg_Cs n)


262 
end


263 


264 
(* cdata > styp > ctype *)


265 
fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,


266 
...}) (x as (_, T)) =


267 
if could_exist_alpha_sub_ctype thy alpha_T T then


268 
case AList.lookup (op =) (!constr_cache) x of


269 
SOME C => C


270 
 NONE => (fresh_ctype_for_type cdata (body_type T);


271 
AList.lookup (op =) (!constr_cache) x > the)


272 
else


273 
fresh_ctype_for_type cdata T


274 
fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =


275 
x > boxed_constr_for_sel ext_ctxt > ctype_for_constr cdata


276 
> sel_ctype_from_constr_ctype s


277 


278 
(* literal list > ctype > ctype *)


279 
fun instantiate_ctype lits =


280 
let


281 
(* ctype > ctype *)


282 
fun aux CAlpha = CAlpha


283 
 aux (CFun (C1, V x, C2)) =


284 
let


285 
val a = case AList.lookup (op =) lits x of


286 
SOME sn => S sn


287 
 NONE => V x


288 
in CFun (aux C1, a, aux C2) end


289 
 aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2)


290 
 aux (CPair Cp) = CPair (pairself aux Cp)


291 
 aux (CType (s, Cs)) = CType (s, map aux Cs)


292 
 aux (CRec z) = CRec z


293 
in aux end


294 


295 
datatype comp_op = Eq  Leq


296 


297 
type comp = sign_atom * sign_atom * comp_op * var list


298 
type sign_expr = literal list


299 


300 
datatype constraint_set =


301 
UnsolvableCSet 


302 
CSet of literal list * comp list * sign_expr list


303 


304 
(* comp_op > string *)


305 
fun string_for_comp_op Eq = "="


306 
 string_for_comp_op Leq = "\<le>"


307 


308 
(* sign_expr > string *)


309 
fun string_for_sign_expr [] = "\<bot>"


310 
 string_for_sign_expr lits =


311 
space_implode " \<or> " (map string_for_literal lits)


312 


313 
(* constraint_set *)


314 
val slack = CSet ([], [], [])


315 


316 
(* literal > literal list option > literal list option *)


317 
fun do_literal _ NONE = NONE


318 
 do_literal (x, sn) (SOME lits) =


319 
case AList.lookup (op =) lits x of


320 
SOME sn' => if sn = sn' then SOME lits else NONE


321 
 NONE => SOME ((x, sn) :: lits)


322 


323 
(* comp_op > var list > sign_atom > sign_atom > literal list * comp list


324 
> (literal list * comp list) option *)


325 
fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =


326 
(case (a1, a2) of


327 
(S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE


328 
 (V x1, S sn2) =>


329 
Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits))


330 
 (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps)


331 
 _ => do_sign_atom_comp Eq [] a2 a1 accum)


332 
 do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =


333 
(case (a1, a2) of


334 
(_, S Neg) => SOME accum


335 
 (S Pos, _) => SOME accum


336 
 (S Neg, S Pos) => NONE


337 
 (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)


338 
 _ => do_sign_atom_comp Eq [] a1 a2 accum)


339 
 do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =


340 
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)


341 


342 
(* comp > var list > ctype > ctype > (literal list * comp list) option


343 
> (literal list * comp list) option *)


344 
fun do_ctype_comp _ _ _ _ NONE = NONE


345 
 do_ctype_comp _ _ CAlpha CAlpha accum = accum


346 
 do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))


347 
(SOME accum) =


348 
accum > do_sign_atom_comp Eq xs a1 a2 > do_ctype_comp Eq xs C11 C21


349 
> do_ctype_comp Eq xs C12 C22


350 
 do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))


351 
(SOME accum) =


352 
(if exists_alpha_sub_ctype C11 then


353 
accum > do_sign_atom_comp Leq xs a1 a2


354 
> do_ctype_comp Leq xs C21 C11


355 
> (case a2 of


356 
S Neg => I


357 
 S Pos => do_ctype_comp Leq xs C11 C21


358 
 V x => do_ctype_comp Leq (x :: xs) C11 C21)


359 
else


360 
SOME accum)


361 
> do_ctype_comp Leq xs C12 C22


362 
 do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22))


363 
accum =


364 
(accum > fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]


365 
handle Library.UnequalLengths =>


366 
raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2]))


367 
 do_ctype_comp cmp xs (CType _) (CType _) accum =


368 
accum (* no need to compare them thanks to the cache *)


369 
 do_ctype_comp _ _ C1 C2 _ =


370 
raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2])


371 


372 
(* comp_op > ctype > ctype > constraint_set > constraint_set *)


373 
fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet


374 
 add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) =


375 
(print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^


376 
" " ^ string_for_ctype C2);


377 
case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of


378 
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)


379 
 SOME (lits, comps) => CSet (lits, comps, sexps))


380 


381 
(* ctype > ctype > constraint_set > constraint_set *)


382 
val add_ctypes_equal = add_ctype_comp Eq


383 
val add_is_sub_ctype = add_ctype_comp Leq


384 


385 
(* sign > sign_expr > ctype > (literal list * sign_expr list) option


386 
> (literal list * sign_expr list) option *)


387 
fun do_notin_ctype_fv _ _ _ NONE = NONE


388 
 do_notin_ctype_fv Neg _ CAlpha accum = accum


389 
 do_notin_ctype_fv Pos [] CAlpha _ = NONE


390 
 do_notin_ctype_fv Pos [(x, sn)] CAlpha (SOME (lits, sexps)) =


391 
SOME lits > do_literal (x, sn) > Option.map (rpair sexps)


392 
 do_notin_ctype_fv Pos sexp CAlpha (SOME (lits, sexps)) =


393 
SOME (lits, insert (op =) sexp sexps)


394 
 do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =


395 
accum > (if sn' = Pos andalso sn = Pos then do_notin_ctype_fv Pos sexp C1


396 
else I)


397 
> (if sn' = Neg orelse sn = Pos then do_notin_ctype_fv Neg sexp C1


398 
else I)


399 
> do_notin_ctype_fv sn sexp C2


400 
 do_notin_ctype_fv Pos sexp (CFun (C1, V x, C2)) accum =


401 
accum > (case do_literal (x, Neg) (SOME sexp) of


402 
NONE => I


403 
 SOME sexp' => do_notin_ctype_fv Pos sexp' C1)


404 
> do_notin_ctype_fv Neg sexp C1


405 
> do_notin_ctype_fv Pos sexp C2


406 
 do_notin_ctype_fv Neg sexp (CFun (C1, V x, C2)) accum =


407 
accum > (case do_literal (x, Pos) (SOME sexp) of


408 
NONE => I


409 
 SOME sexp' => do_notin_ctype_fv Pos sexp' C1)


410 
> do_notin_ctype_fv Neg sexp C2


411 
 do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =


412 
accum > fold (do_notin_ctype_fv sn sexp) [C1, C2]


413 
 do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =


414 
accum > fold (do_notin_ctype_fv sn sexp) Cs


415 
 do_notin_ctype_fv _ _ C _ =


416 
raise CTYPE ("NitpickMono.do_notin_ctype_fv", [C])


417 


418 
(* sign > ctype > constraint_set > constraint_set *)


419 
fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet


420 
 add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =


421 
(print_g ("*** Add " ^ string_for_ctype C ^ " is right" ^


422 
(case sn of Neg => "unique"  Pos => "total") ^ ".");


423 
case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of


424 
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)


425 
 SOME (lits, sexps) => CSet (lits, comps, sexps))


426 


427 
(* ctype > constraint_set > constraint_set *)


428 
val add_ctype_is_right_unique = add_notin_ctype_fv Neg


429 
val add_ctype_is_right_total = add_notin_ctype_fv Pos


430 


431 
(* constraint_set > constraint_set > constraint_set *)


432 
fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =


433 
(case SOME lits1 > fold do_literal lits2 of


434 
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)


435 
 SOME lits => CSet (lits, comps1 @ comps2, sexps1 @ sexps2))


436 
 unite _ _ = UnsolvableCSet


437 


438 
(* sign > bool *)


439 
fun bool_from_sign Pos = false


440 
 bool_from_sign Neg = true


441 
(* bool > sign *)


442 
fun sign_from_bool false = Pos


443 
 sign_from_bool true = Neg


444 


445 
(* literal > PropLogic.prop_formula *)


446 
fun prop_for_literal (x, sn) =


447 
(not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x)


448 
(* sign_atom > PropLogic.prop_formula *)


449 
fun prop_for_sign_atom_eq (S sn', sn) =


450 
if sn = sn' then PropLogic.True else PropLogic.False


451 
 prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn)


452 
(* sign_expr > PropLogic.prop_formula *)


453 
fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs)


454 
(* var list > sign > PropLogic.prop_formula *)


455 
fun prop_for_exists_eq xs sn =


456 
PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs)


457 
(* comp > PropLogic.prop_formula *)


458 
fun prop_for_comp (a1, a2, Eq, []) =


459 
PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),


460 
prop_for_comp (a2, a1, Leq, []))


461 
 prop_for_comp (a1, a2, Leq, []) =


462 
PropLogic.SOr (prop_for_sign_atom_eq (a1, Pos),


463 
prop_for_sign_atom_eq (a2, Neg))


464 
 prop_for_comp (a1, a2, cmp, xs) =


465 
PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))


466 


467 
(* var > (int > bool option) > literal list > literal list *)


468 
fun literals_from_assignments max_var asgns lits =


469 
fold (fn x => fn accum =>


470 
if AList.defined (op =) lits x then


471 
accum


472 
else case asgns x of


473 
SOME b => (x, sign_from_bool b) :: accum


474 
 NONE => accum) (max_var downto 1) lits


475 


476 
(* literal list > sign_atom > sign option *)


477 
fun lookup_sign_atom _ (S sn) = SOME sn


478 
 lookup_sign_atom lit (V x) = AList.lookup (op =) lit x


479 


480 
(* comp > string *)


481 
fun string_for_comp (a1, a2, cmp, xs) =


482 
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^


483 
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2


484 


485 
(* literal list > comp list > sign_expr list > unit *)


486 
fun print_problem lits comps sexps =


487 
print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @


488 
map string_for_comp comps @


489 
map string_for_sign_expr sexps))


490 


491 
(* literal list > unit *)


492 
fun print_solution lits =


493 
let val (pos, neg) = List.partition (equal Pos o snd) lits in


494 
print_g ("*** Solution:\n" ^


495 
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^


496 
": " ^ commas (map (string_for_var o fst) neg))


497 
end


498 


499 
(* var > constraint_set > literal list list option *)


500 
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)


501 
 solve max_var (CSet (lits, comps, sexps)) =


502 
let


503 
val _ = print_problem lits comps sexps


504 
val prop = PropLogic.all (map prop_for_literal lits @


505 
map prop_for_comp comps @


506 
map prop_for_sign_expr sexps)


507 
in


508 
case silence (SatSolver.invoke_solver "dpll") prop of


509 
SatSolver.SATISFIABLE asgns =>


510 
SOME (literals_from_assignments max_var asgns lits


511 
> tap print_solution)


512 
 _ => NONE


513 
end


514 


515 
(* var > constraint_set > bool *)


516 
val is_solvable = is_some oo solve


517 


518 
type ctype_schema = ctype * constraint_set


519 
type ctype_context =


520 
{bounds: ctype list,


521 
frees: (styp * ctype) list,


522 
consts: (styp * ctype_schema) list}


523 


524 
type accumulator = ctype_context * constraint_set


525 


526 
val initial_gamma = {bounds = [], frees = [], consts = []}


527 
val unsolvable_accum = (initial_gamma, UnsolvableCSet)


528 


529 
(* ctype > ctype_context > ctype_context *)


530 
fun push_bound C {bounds, frees, consts} =


531 
{bounds = C :: bounds, frees = frees, consts = consts}


532 
(* ctype_context > ctype_context *)


533 
fun pop_bound {bounds, frees, consts} =


534 
{bounds = tl bounds, frees = frees, consts = consts}


535 
handle List.Empty => initial_gamma


536 


537 
(* cdata > term > accumulator > ctype * accumulator *)


538 
fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,


539 
max_fresh, ...}) =


540 
let


541 
(* typ > ctype *)


542 
val ctype_for = fresh_ctype_for_type cdata


543 
(* ctype > ctype *)


544 
fun pos_set_ctype_for_dom C =


545 
CFun (C, S (if exists_alpha_sub_ctype C then Pos else Neg), bool_C)


546 
(* typ > accumulator > ctype * accumulator *)


547 
fun do_quantifier T (gamma, cset) =


548 
let


549 
val abs_C = ctype_for (domain_type (domain_type T))


550 
val body_C = ctype_for (range_type T)


551 
in


552 
(CFun (CFun (abs_C, S Neg, body_C), S Neg, body_C),


553 
(gamma, cset > add_ctype_is_right_total abs_C))


554 
end


555 
fun do_equals T (gamma, cset) =


556 
let val C = ctype_for (domain_type T) in


557 
(CFun (C, S Neg, CFun (C, S Neg, ctype_for (nth_range_type 2 T))),


558 
(gamma, cset > add_ctype_is_right_unique C))


559 
end


560 
fun do_robust_set_operation T (gamma, cset) =


561 
let


562 
val set_T = domain_type T


563 
val C1 = ctype_for set_T


564 
val C2 = ctype_for set_T


565 
val C3 = ctype_for set_T


566 
in


567 
(CFun (C1, S Neg, CFun (C2, S Neg, C3)),


568 
(gamma, cset > add_is_sub_ctype C1 C3 > add_is_sub_ctype C2 C3))


569 
end


570 
fun do_fragile_set_operation T (gamma, cset) =


571 
let


572 
val set_T = domain_type T


573 
val set_C = ctype_for set_T


574 
(* typ > ctype *)


575 
fun custom_ctype_for (T as Type ("fun", [T1, T2])) =


576 
if T = set_T then set_C


577 
else CFun (custom_ctype_for T1, S Neg, custom_ctype_for T2)


578 
 custom_ctype_for T = ctype_for T


579 
in


580 
(custom_ctype_for T, (gamma, cset > add_ctype_is_right_unique set_C))


581 
end


582 
(* typ > accumulator > ctype * accumulator *)


583 
fun do_pair_constr T accum =


584 
case ctype_for (nth_range_type 2 T) of


585 
C as CPair (a_C, b_C) =>


586 
(CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)


587 
 C => raise CTYPE ("NitpickMono.consider_term.do_pair_constr", [C])


588 
(* int > typ > accumulator > ctype * accumulator *)


589 
fun do_nth_pair_sel n T =


590 
case ctype_for (domain_type T) of


591 
C as CPair (a_C, b_C) =>


592 
pair (CFun (C, S Neg, if n = 0 then a_C else b_C))


593 
 C => raise CTYPE ("NitpickMono.consider_term.do_nth_pair_sel", [C])


594 
val unsolvable = (CType ("unsolvable", []), unsolvable_accum)


595 
(* typ > term > accumulator > ctype * accumulator *)


596 
fun do_bounded_quantifier abs_T bound_t body_t accum =


597 
let


598 
val abs_C = ctype_for abs_T


599 
val (bound_C, accum) = accum >> push_bound abs_C > do_term bound_t


600 
val expected_bound_C = pos_set_ctype_for_dom abs_C


601 
in


602 
accum > add_ctypes_equal expected_bound_C bound_C > do_term body_t


603 
> apfst pop_bound


604 
end


605 
(* term > accumulator > ctype * accumulator *)


606 
and do_term _ (_, UnsolvableCSet) = unsolvable


607 
 do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =


608 
(case t of


609 
Const (x as (s, T)) =>


610 
(case AList.lookup (op =) consts x of


611 
SOME (C, cset') => (C, (gamma, cset > unite cset'))


612 
 NONE =>


613 
if not (could_exist_alpha_subtype alpha_T T) then


614 
(ctype_for T, accum)


615 
else case s of


616 
@{const_name all} => do_quantifier T accum


617 
 @{const_name "=="} => do_equals T accum


618 
 @{const_name All} => do_quantifier T accum


619 
 @{const_name Ex} => do_quantifier T accum


620 
 @{const_name "op ="} => do_equals T accum


621 
 @{const_name The} => (print_g "*** The"; unsolvable)


622 
 @{const_name Eps} => (print_g "*** Eps"; unsolvable)


623 
 @{const_name If} =>


624 
do_robust_set_operation (range_type T) accum


625 
>> curry3 CFun bool_C (S Neg)


626 
 @{const_name Pair} => do_pair_constr T accum


627 
 @{const_name fst} => do_nth_pair_sel 0 T accum


628 
 @{const_name snd} => do_nth_pair_sel 1 T accum


629 
 @{const_name Id} =>


630 
(CFun (ctype_for (domain_type T), S Neg, bool_C), accum)


631 
 @{const_name insert} =>


632 
let


633 
val set_T = domain_type (range_type T)


634 
val C1 = ctype_for (domain_type set_T)


635 
val C1' = pos_set_ctype_for_dom C1


636 
val C2 = ctype_for set_T


637 
val C3 = ctype_for set_T


638 
in


639 
(CFun (C1, S Neg, CFun (C2, S Neg, C3)),


640 
(gamma, cset > add_ctype_is_right_unique C1


641 
> add_is_sub_ctype C1' C3


642 
> add_is_sub_ctype C2 C3))


643 
end


644 
 @{const_name converse} =>


645 
let


646 
val x = Unsynchronized.inc max_fresh


647 
(* typ > ctype *)


648 
fun ctype_for_set T =


649 
CFun (ctype_for (domain_type T), V x, bool_C)


650 
val ab_set_C = domain_type T > ctype_for_set


651 
val ba_set_C = range_type T > ctype_for_set


652 
in (CFun (ab_set_C, S Neg, ba_set_C), accum) end


653 
 @{const_name trancl} => do_fragile_set_operation T accum


654 
 @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)


655 
 @{const_name lower_semilattice_fun_inst.inf_fun} =>


656 
do_robust_set_operation T accum


657 
 @{const_name upper_semilattice_fun_inst.sup_fun} =>


658 
do_robust_set_operation T accum


659 
 @{const_name finite} =>


660 
let val C1 = ctype_for (domain_type (domain_type T)) in


661 
(CFun (pos_set_ctype_for_dom C1, S Neg, bool_C), accum)


662 
end


663 
 @{const_name rel_comp} =>


664 
let


665 
val x = Unsynchronized.inc max_fresh


666 
(* typ > ctype *)


667 
fun ctype_for_set T =


668 
CFun (ctype_for (domain_type T), V x, bool_C)


669 
val bc_set_C = domain_type T > ctype_for_set


670 
val ab_set_C = domain_type (range_type T) > ctype_for_set


671 
val ac_set_C = nth_range_type 2 T > ctype_for_set


672 
in


673 
(CFun (bc_set_C, S Neg, CFun (ab_set_C, S Neg, ac_set_C)),


674 
accum)


675 
end


676 
 @{const_name image} =>


677 
let


678 
val a_C = ctype_for (domain_type (domain_type T))


679 
val b_C = ctype_for (range_type (domain_type T))


680 
in


681 
(CFun (CFun (a_C, S Neg, b_C), S Neg,


682 
CFun (pos_set_ctype_for_dom a_C, S Neg,


683 
pos_set_ctype_for_dom b_C)), accum)


684 
end


685 
 @{const_name Sigma} =>


686 
let


687 
val x = Unsynchronized.inc max_fresh


688 
(* typ > ctype *)


689 
fun ctype_for_set T =


690 
CFun (ctype_for (domain_type T), V x, bool_C)


691 
val a_set_T = domain_type T


692 
val a_C = ctype_for (domain_type a_set_T)


693 
val b_set_C = ctype_for_set (range_type (domain_type


694 
(range_type T)))


695 
val a_set_C = ctype_for_set a_set_T


696 
val a_to_b_set_C = CFun (a_C, S Neg, b_set_C)


697 
val ab_set_C = ctype_for_set (nth_range_type 2 T)


698 
in


699 
(CFun (a_set_C, S Neg, CFun (a_to_b_set_C, S Neg, ab_set_C)),


700 
accum)


701 
end


702 
 @{const_name minus_fun_inst.minus_fun} =>


703 
let


704 
val set_T = domain_type T


705 
val left_set_C = ctype_for set_T


706 
val right_set_C = ctype_for set_T


707 
in


708 
(CFun (left_set_C, S Neg,


709 
CFun (right_set_C, S Neg, left_set_C)),


710 
(gamma, cset > add_ctype_is_right_unique right_set_C


711 
(* FIXME: > add_is_sub_ctype right_set_C left_set_C *)))


712 
end


713 
 @{const_name ord_fun_inst.less_eq_fun} =>


714 
do_fragile_set_operation T accum


715 
 @{const_name Tha} =>


716 
let


717 
val a_C = ctype_for (domain_type (domain_type T))


718 
val a_set_C = pos_set_ctype_for_dom a_C


719 
in (CFun (a_set_C, S Neg, a_C), accum) end


720 
 @{const_name FunBox} =>


721 
let val dom_C = ctype_for (domain_type T) in


722 
(CFun (dom_C, S Neg, dom_C), accum)


723 
end


724 
 _ => if is_sel s then


725 
if constr_name_for_sel_like s = @{const_name FunBox} then


726 
let val dom_C = ctype_for (domain_type T) in


727 
(CFun (dom_C, S Neg, dom_C), accum)


728 
end


729 
else


730 
(ctype_for_sel cdata x, accum)


731 
else if is_constr thy x then


732 
(ctype_for_constr cdata x, accum)


733 
else if is_built_in_const true x then


734 
case def_of_const thy def_table x of


735 
SOME t' => do_term t' accum


736 
 NONE => (print_g ("*** builtin " ^ s); unsolvable)


737 
else


738 
(ctype_for T, accum))


739 
 Free (x as (_, T)) =>


740 
(case AList.lookup (op =) frees x of


741 
SOME C => (C, accum)


742 
 NONE =>


743 
let val C = ctype_for T in


744 
(C, ({bounds = bounds, frees = (x, C) :: frees,


745 
consts = consts}, cset))


746 
end)


747 
 Var _ => (print_g "*** Var"; unsolvable)


748 
 Bound j => (nth bounds j, accum)


749 
 Abs (_, T, @{const False}) => (ctype_for (T > bool_T), accum)


750 
 Abs (s, T, t') =>


751 
let


752 
val C = ctype_for T


753 
val (C', accum) = do_term t' (accum >> push_bound C)


754 
in (CFun (C, S Neg, C'), accum >> pop_bound) end


755 
 Const (@{const_name All}, _)


756 
$ Abs (_, T', @{const "op >"} $ (t1 $ Bound 0) $ t2) =>


757 
do_bounded_quantifier T' t1 t2 accum


758 
 Const (@{const_name Ex}, _)


759 
$ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) =>


760 
do_bounded_quantifier T' t1 t2 accum


761 
 Const (@{const_name Let}, _) $ t1 $ t2 =>


762 
do_term (betapply (t2, t1)) accum


763 
 t1 $ t2 =>


764 
let


765 
val (C1, accum) = do_term t1 accum


766 
val (C2, accum) = do_term t2 accum


767 
in


768 
case accum of


769 
(_, UnsolvableCSet) => unsolvable


770 
 _ => case C1 of


771 
CFun (C11, _, C12) =>


772 
(C12, accum > add_is_sub_ctype C2 C11)


773 
 _ => raise CTYPE ("NitpickMono.consider_term.do_term \


774 
\(op $)", [C1])


775 
end)


776 
> tap (fn (C, _) =>


777 
print_g (" \<Gamma> \<turnstile> " ^


778 
Syntax.string_of_term ctxt t ^ " : " ^


779 
string_for_ctype C))


780 
in do_term end


781 


782 
(* cdata > sign > term > accumulator > accumulator *)


783 
fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =


784 
let


785 
(* typ > ctype *)


786 
val ctype_for = fresh_ctype_for_type cdata


787 
(* term > accumulator > ctype * accumulator *)


788 
val do_term = consider_term cdata


789 
(* term > accumulator > accumulator *)


790 
val do_boolean_term = snd oo do_term


791 
(* sign > term > accumulator > accumulator *)


792 
fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum


793 
 do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =


794 
let


795 
(* term > accumulator > accumulator *)


796 
val do_co_formula = do_formula sn


797 
val do_contra_formula = do_formula (negate sn)


798 
(* string > typ > term > accumulator *)


799 
fun do_quantifier quant_s abs_T body_t =


800 
let


801 
val abs_C = ctype_for abs_T


802 
val side_cond = ((sn = Neg) = (quant_s = @{const_name Ex}))


803 
val cset = cset > side_cond ? add_ctype_is_right_total abs_C


804 
in


805 
(gamma > push_bound abs_C, cset) > do_co_formula body_t


806 
>> pop_bound


807 
end


808 
(* typ > term > accumulator *)


809 
fun do_bounded_quantifier abs_T body_t =


810 
accum >> push_bound (ctype_for abs_T) > do_co_formula body_t


811 
>> pop_bound


812 
(* term > term > accumulator *)


813 
fun do_equals t1 t2 =


814 
case sn of


815 
Pos => do_boolean_term t accum


816 
 Neg => let


817 
val (C1, accum) = do_term t1 accum


818 
val (C2, accum) = do_term t2 accum


819 
in accum (* FIXME: > add_ctypes_equal C1 C2 *) end


820 
in


821 
case t of


822 
Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>


823 
do_quantifier s0 T1 t1


824 
 Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2


825 
 @{const "==>"} $ t1 $ t2 =>


826 
accum > do_contra_formula t1 > do_co_formula t2


827 
 @{const Trueprop} $ t1 => do_co_formula t1 accum


828 
 @{const Not} $ t1 => do_contra_formula t1 accum


829 
 Const (@{const_name All}, _)


830 
$ Abs (_, T1, t1 as @{const "op >"} $ (_ $ Bound 0) $ _) =>


831 
do_bounded_quantifier T1 t1


832 
 Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) =>


833 
do_quantifier s0 T1 t1


834 
 Const (@{const_name Ex}, _)


835 
$ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>


836 
do_bounded_quantifier T1 t1


837 
 Const (s0 as @{const_name Ex}, _) $ Abs (_, T1, t1) =>


838 
do_quantifier s0 T1 t1


839 
 Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2


840 
 @{const "op &"} $ t1 $ t2 =>


841 
accum > do_co_formula t1 > do_co_formula t2


842 
 @{const "op "} $ t1 $ t2 =>


843 
accum > do_co_formula t1 > do_co_formula t2


844 
 @{const "op >"} $ t1 $ t2 =>


845 
accum > do_contra_formula t1 > do_co_formula t2


846 
 Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>


847 
accum > do_boolean_term t1 > do_co_formula t2 > do_co_formula t3


848 
 Const (@{const_name Let}, _) $ t1 $ t2 =>


849 
do_co_formula (betapply (t2, t1)) accum


850 
 _ => do_boolean_term t accum


851 
end


852 
> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^


853 
Syntax.string_of_term ctxt t ^


854 
" : o\<^sup>" ^ string_for_sign sn))


855 
in do_formula end


856 


857 
(* The harmless axiom optimization below is somewhat too aggressive in the face


858 
of (rather peculiar) userdefined axioms. *)


859 
val harmless_consts =


860 
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}]


861 
val bounteous_consts = [@{const_name bisim}]


862 


863 
(* term > bool *)


864 
fun is_harmless_axiom t =


865 
Term.add_consts t [] > filter_out (is_built_in_const true)


866 
> (forall (member (op =) harmless_consts o original_name o fst)


867 
orf exists (member (op =) bounteous_consts o fst))


868 


869 
(* cdata > sign > term > accumulator > accumulator *)


870 
fun consider_nondefinitional_axiom cdata sn t =


871 
not (is_harmless_axiom t) ? consider_general_formula cdata sn t


872 


873 
(* cdata > term > accumulator > accumulator *)


874 
fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =


875 
if not (is_constr_pattern_formula thy t) then


876 
consider_nondefinitional_axiom cdata Pos t


877 
else if is_harmless_axiom t then


878 
I


879 
else


880 
let


881 
(* term > accumulator > accumulator *)


882 
val do_term = consider_term cdata


883 
(* typ > term > accumulator > accumulator *)


884 
fun do_all abs_T body_t accum =


885 
let val abs_C = fresh_ctype_for_type cdata abs_T in


886 
accum >> push_bound abs_C > do_formula body_t >> pop_bound


887 
end


888 
(* term > term > accumulator > accumulator *)


889 
and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2


890 
and do_equals t1 t2 accum =


891 
let


892 
val (C1, accum) = do_term t1 accum


893 
val (C2, accum) = do_term t2 accum


894 
in accum > add_ctypes_equal C1 C2 end


895 
(* term > accumulator > accumulator *)


896 
and do_formula _ (_, UnsolvableCSet) = unsolvable_accum


897 
 do_formula t accum =


898 
case t of


899 
Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum


900 
 @{const Trueprop} $ t1 => do_formula t1 accum


901 
 Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum


902 
 @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum


903 
 @{const Pure.conjunction} $ t1 $ t2 =>


904 
accum > do_formula t1 > do_formula t2


905 
 Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum


906 
 Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum


907 
 @{const "op &"} $ t1 $ t2 => accum > do_formula t1 > do_formula t2


908 
 @{const "op >"} $ t1 $ t2 => do_implies t1 t2 accum


909 
 _ => raise TERM ("NitpickMono.consider_definitional_axiom.\


910 
\do_formula", [t])


911 
in do_formula t end


912 


913 
(* Proof.context > literal list > term > ctype > string *)


914 
fun string_for_ctype_of_term ctxt lits t C =


915 
Syntax.string_of_term ctxt t ^ " : " ^


916 
string_for_ctype (instantiate_ctype lits C)


917 


918 
(* theory > literal list > ctype_context > unit *)


919 
fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =


920 
map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @


921 
map (fn (x, (C, _)) => string_for_ctype_of_term ctxt lits (Const x) C) consts


922 
> cat_lines > print_g


923 


924 
(* extended_context > typ > term list > term list > term > bool *)


925 
fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T def_ts nondef_ts


926 
core_t =


927 
let


928 
val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^


929 
Syntax.string_of_typ ctxt alpha_T)


930 
val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T


931 
val (gamma, cset) =


932 
(initial_gamma, slack)


933 
> fold (consider_definitional_axiom cdata) def_ts


934 
> fold (consider_nondefinitional_axiom cdata Pos) nondef_ts


935 
> consider_general_formula cdata Pos core_t


936 
in


937 
case solve (!max_fresh) cset of


938 
SOME lits => (print_ctype_context ctxt lits gamma; true)


939 
 _ => false


940 
end


941 
handle CTYPE (loc, Cs) => raise BAD (loc, commas (map string_for_ctype Cs))


942 


943 
end;
