344 | aux (MPair Mp) = MPair (pairself aux Mp) |
345 | aux (MPair Mp) = MPair (pairself aux Mp) |
345 | aux (MType (s, Ms)) = MType (s, map aux Ms) |
346 | aux (MType (s, Ms)) = MType (s, map aux Ms) |
346 | aux (MRec z) = MRec z |
347 | aux (MRec z) = MRec z |
347 in aux end |
348 in aux end |
348 |
349 |
349 datatype comp_op = Eq | Leq |
350 datatype comp_op = Eq | Neq | Leq |
350 |
351 |
351 type comp = annotation_atom * annotation_atom * comp_op * var list |
352 type comp = annotation_atom * annotation_atom * comp_op * var list |
352 type assign_clause = assign_literal list |
353 type assign_clause = assign_literal list |
353 |
354 |
354 type constraint_set = comp list * assign_clause list |
355 type constraint_set = comp list * assign_clause list |
355 |
356 |
356 fun string_for_comp_op Eq = "=" |
357 fun string_for_comp_op Eq = "=" |
|
358 | string_for_comp_op Neq = "\<noteq>" |
357 | string_for_comp_op Leq = "\<le>" |
359 | string_for_comp_op Leq = "\<le>" |
358 |
360 |
359 fun string_for_comp (aa1, aa2, cmp, xs) = |
361 fun string_for_comp (aa1, aa2, cmp, xs) = |
360 string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^ |
362 string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^ |
361 subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2 |
363 subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2 |
362 |
364 |
363 fun string_for_assign_clause [] = "\<bot>" |
365 fun string_for_assign_clause [] = "\<bot>" |
364 | string_for_assign_clause asgs = |
366 | string_for_assign_clause asgs = |
365 space_implode " \<or> " (map string_for_assign_literal asgs) |
367 space_implode " \<or> " (map string_for_assign_literal asgs) |
366 |
368 |
367 fun add_assign_literal (x, a) clauses = |
369 fun add_assign_literal (x, (sn, a)) clauses = |
368 if exists (fn [(x', a')] => x = x' andalso a <> a' | _ => false) clauses then |
370 if exists (fn [(x', (sn', a'))] => |
|
371 x = x' andalso ((sn = sn' andalso a <> a') orelse |
|
372 (sn <> sn' andalso a = a')) |
|
373 | _ => false) clauses then |
369 NONE |
374 NONE |
370 else |
375 else |
371 SOME ([(x, a)] :: clauses)fun add_assign_conjunct _ NONE = NONE |
376 SOME ([(x, a)] :: clauses) |
372 |
377 |
373 fun add_assign_disjunct _ NONE = NONE |
378 fun add_assign_disjunct _ NONE = NONE |
374 | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs) |
379 | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs) |
375 |
380 |
376 fun do_annotation_atom_comp Eq [] aa1 aa2 (cset as (comps, clauses)) = |
381 fun annotation_comp Eq a1 a2 = (a1 = a2) |
|
382 | annotation_comp Neq a1 a2 = (a1 <> a2) |
|
383 | annotation_comp Leq a1 a2 = (a1 = a2 orelse a2 = Gen) |
|
384 |
|
385 fun comp_op_sign Eq = Plus |
|
386 | comp_op_sign Neq = Minus |
|
387 | comp_op_sign Leq = |
|
388 raise BAD ("Nitpick_Mono.comp_op_sign", "unexpected \"Leq\"") |
|
389 |
|
390 fun do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) = |
377 (case (aa1, aa2) of |
391 (case (aa1, aa2) of |
378 (A a1, A a2) => if a1 = a2 then SOME cset else NONE |
392 (A a1, A a2) => if annotation_comp Leq a1 a2 then SOME cset else NONE |
|
393 | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses)) |
|
394 | do_annotation_atom_comp cmp [] aa1 aa2 (cset as (comps, clauses)) = |
|
395 (case (aa1, aa2) of |
|
396 (A a1, A a2) => if annotation_comp cmp a1 a2 then SOME cset else NONE |
379 | (V x1, A a2) => |
397 | (V x1, A a2) => |
380 clauses |> add_assign_literal (x1, a2) |> Option.map (pair comps) |
398 clauses |> add_assign_literal (x1, (comp_op_sign cmp, a2)) |
381 | (V _, V _) => SOME (insert (op =) (aa1, aa2, Eq, []) comps, clauses) |
399 |> Option.map (pair comps) |
382 | _ => do_annotation_atom_comp Eq [] aa2 aa1 cset) |
400 | (A _, V _) => do_annotation_atom_comp cmp [] aa2 aa1 cset |
383 | do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) = |
401 | (V _, V _) => SOME (insert (op =) (aa1, aa2, cmp, []) comps, clauses)) |
384 (case (aa1, aa2) of |
|
385 (_, A Gen) => SOME cset |
|
386 | (A Gen, A _) => NONE |
|
387 | (A a1, A a2) => if a1 = a2 then SOME cset else NONE |
|
388 | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses)) |
|
389 | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) = |
402 | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) = |
390 SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses) |
403 SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses) |
391 |
404 |
392 fun add_annotation_atom_comp cmp xs aa1 aa2 |
405 fun add_annotation_atom_comp cmp xs aa1 aa2 |
393 ((comps, clauses) : constraint_set) = |
406 ((comps, clauses) : constraint_set) = |
438 val add_is_sub_mtype = add_mtype_comp Leq |
451 val add_is_sub_mtype = add_mtype_comp Leq |
439 |
452 |
440 fun do_notin_mtype_fv _ _ _ NONE = NONE |
453 fun do_notin_mtype_fv _ _ _ NONE = NONE |
441 | do_notin_mtype_fv Minus _ MAlpha cset = cset |
454 | do_notin_mtype_fv Minus _ MAlpha cset = cset |
442 | do_notin_mtype_fv Plus [] MAlpha _ = NONE |
455 | do_notin_mtype_fv Plus [] MAlpha _ = NONE |
443 | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME clauses) = |
456 | do_notin_mtype_fv Plus [asg] MAlpha (SOME clauses) = |
444 clauses |> add_assign_literal (x, a) |
457 clauses |> add_assign_literal asg |
445 | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) = |
458 | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) = |
446 SOME (insert (op =) clause clauses) |
459 SOME (insert (op =) clause clauses) |
447 | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset = |
460 | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset = |
448 cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus clause M1 |
461 cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus clause M1 |
449 else I) |
462 else I) |
450 |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus clause M1 |
463 |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus clause M1 |
451 else I) |
464 else I) |
452 |> do_notin_mtype_fv sn clause M2 |
465 |> do_notin_mtype_fv sn clause M2 |
453 | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset = |
466 | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset = |
454 cset |> (case add_assign_disjunct (x, Gen) (SOME clause) of |
467 cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME clause) of |
455 NONE => I |
468 NONE => I |
456 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
469 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
457 |> do_notin_mtype_fv Minus clause M1 |
470 |> do_notin_mtype_fv Minus clause M1 |
458 |> do_notin_mtype_fv Plus clause M2 |
471 |> do_notin_mtype_fv Plus clause M2 |
459 | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) cset = |
472 | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) cset = |
460 cset |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru] |
473 cset |> (case fold (fn a => add_assign_disjunct (x, (Plus, a))) [Fls, Tru] |
461 (SOME clause) of |
474 (SOME clause) of |
462 NONE => I |
475 NONE => I |
463 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
476 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
464 |> do_notin_mtype_fv Minus clause M2 |
477 |> do_notin_mtype_fv Minus clause M2 |
465 | do_notin_mtype_fv sn clause (MPair (M1, M2)) cset = |
478 | do_notin_mtype_fv sn clause (MPair (M1, M2)) cset = |
493 |
506 |
494 fun prop_for_bool b = if b then PL.True else PL.False |
507 fun prop_for_bool b = if b then PL.True else PL.False |
495 fun prop_for_bool_var_equality (v1, v2) = |
508 fun prop_for_bool_var_equality (v1, v2) = |
496 PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)), |
509 PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)), |
497 PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2)) |
510 PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2)) |
498 fun prop_for_assign_literal (x, a) = |
511 fun prop_for_assign (x, a) = |
499 let val (b1, b2) = bools_from_annotation a in |
512 let val (b1, b2) = bools_from_annotation a in |
500 PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not, |
513 PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not, |
501 PL.BoolVar (snd_var x) |> not b2 ? PL.Not) |
514 PL.BoolVar (snd_var x) |> not b2 ? PL.Not) |
502 end |
515 end |
|
516 fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a) |
|
517 | prop_for_assign_literal (x, (Minus, a)) = PL.Not (prop_for_assign (x, a)) |
503 fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a') |
518 fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a') |
504 | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, a) |
519 | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a)) |
505 fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) |
520 fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) |
506 | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) |
521 | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) |
507 | prop_for_atom_equality (V x1, V x2) = |
522 | prop_for_atom_equality (V x1, V x2) = |
508 PL.And (prop_for_bool_var_equality (pairself fst_var (x1, x2)), |
523 PL.And (prop_for_bool_var_equality (pairself fst_var (x1, x2)), |
509 prop_for_bool_var_equality (pairself snd_var (x1, x2))) |
524 prop_for_bool_var_equality (pairself snd_var (x1, x2))) |
510 val prop_for_assign_clause = PL.exists o map prop_for_assign_literal |
525 val prop_for_assign_clause = PL.exists o map prop_for_assign_literal |
511 fun prop_for_exists_var_assign_literal xs a = |
526 fun prop_for_exists_var_assign_literal xs a = |
512 PL.exists (map (fn x => prop_for_assign_literal (x, a)) xs) |
527 PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs) |
513 fun prop_for_comp (aa1, aa2, Eq, []) = |
528 fun prop_for_comp (aa1, aa2, Eq, []) = |
514 PL.SAnd (prop_for_comp (aa1, aa2, Leq, []), |
529 PL.SAnd (prop_for_comp (aa1, aa2, Leq, []), |
515 prop_for_comp (aa2, aa1, Leq, [])) |
530 prop_for_comp (aa2, aa1, Leq, [])) |
|
531 | prop_for_comp (aa1, aa2, Neq, []) = |
|
532 PL.Not (prop_for_comp (aa1, aa2, Eq, [])) |
516 | prop_for_comp (aa1, aa2, Leq, []) = |
533 | prop_for_comp (aa1, aa2, Leq, []) = |
517 PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) |
534 PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) |
518 | prop_for_comp (aa1, aa2, cmp, xs) = |
535 | prop_for_comp (aa1, aa2, cmp, xs) = |
519 PL.SOr (prop_for_exists_var_assign_literal xs Gen, |
536 PL.SOr (prop_for_exists_var_assign_literal xs Gen, |
520 prop_for_comp (aa1, aa2, cmp, [])) |
537 prop_for_comp (aa1, aa2, cmp, [])) |