src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40999 69d0d445c46a
parent 40998 bcd23ddeecef
child 41000 4bbff1684465
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:30:38 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:30:57 2010 +0100
     1.3 @@ -364,8 +364,9 @@
     1.4    string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^
     1.5    subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2
     1.6  
     1.7 -fun string_for_assign_clause [] = "\<bot>"
     1.8 -  | string_for_assign_clause asgs =
     1.9 +fun string_for_assign_clause NONE = "\<top>"
    1.10 +  | string_for_assign_clause (SOME []) = "\<bot>"
    1.11 +  | string_for_assign_clause (SOME asgs) =
    1.12      space_implode " \<or> " (map string_for_assign_literal asgs)
    1.13  
    1.14  fun add_assign_literal (x, (sn, a)) clauses =
    1.15 @@ -380,7 +381,8 @@
    1.16  fun add_assign_disjunct _ NONE = NONE
    1.17    | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
    1.18  
    1.19 -val add_assign_clause = insert (op =)
    1.20 +fun add_assign_clause NONE = I
    1.21 +  | add_assign_clause (SOME clause) = insert (op =) clause
    1.22  
    1.23  fun annotation_comp Eq a1 a2 = (a1 = a2)
    1.24    | annotation_comp Neq a1 a2 = (a1 <> a2)
    1.25 @@ -506,22 +508,22 @@
    1.26  
    1.27  fun prop_for_bool b = if b then PL.True else PL.False
    1.28  fun prop_for_bool_var_equality (v1, v2) =
    1.29 -  PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)),
    1.30 -          PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2))
    1.31 +  PL.SAnd (PL.SOr (PL.BoolVar v1, PL.SNot (PL.BoolVar v2)),
    1.32 +           PL.SOr (PL.SNot (PL.BoolVar v1), PL.BoolVar v2))
    1.33  fun prop_for_assign (x, a) =
    1.34    let val (b1, b2) = bools_from_annotation a in
    1.35 -    PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not,
    1.36 -            PL.BoolVar (snd_var x) |> not b2 ? PL.Not)
    1.37 +    PL.SAnd (PL.BoolVar (fst_var x) |> not b1 ? PL.SNot,
    1.38 +             PL.BoolVar (snd_var x) |> not b2 ? PL.SNot)
    1.39    end
    1.40  fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
    1.41 -  | prop_for_assign_literal (x, (Minus, a)) = PL.Not (prop_for_assign (x, a))
    1.42 +  | prop_for_assign_literal (x, (Minus, a)) = PL.SNot (prop_for_assign (x, a))
    1.43  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
    1.44    | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
    1.45  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
    1.46    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
    1.47    | prop_for_atom_equality (V x1, V x2) =
    1.48 -    PL.And (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
    1.49 -            prop_for_bool_var_equality (pairself snd_var (x1, x2)))
    1.50 +    PL.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
    1.51 +             prop_for_bool_var_equality (pairself snd_var (x1, x2)))
    1.52  val prop_for_assign_clause = PL.exists o map prop_for_assign_literal
    1.53  fun prop_for_exists_var_assign_literal xs a =
    1.54    PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
    1.55 @@ -529,7 +531,7 @@
    1.56      PL.SAnd (prop_for_comp (aa1, aa2, Leq, []),
    1.57               prop_for_comp (aa2, aa1, Leq, []))
    1.58    | prop_for_comp (aa1, aa2, Neq, []) =
    1.59 -    PL.Not (prop_for_comp (aa1, aa2, Eq, []))
    1.60 +    PL.SNot (prop_for_comp (aa1, aa2, Eq, []))
    1.61    | prop_for_comp (aa1, aa2, Leq, []) =
    1.62      PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
    1.63    | prop_for_comp (aa1, aa2, cmp, xs) =
    1.64 @@ -560,7 +562,7 @@
    1.65    trace_msg (fn () =>
    1.66                  "*** Problem (calculus M" ^ string_of_int calculus ^ "):\n" ^
    1.67                  cat_lines (map string_for_comp comps @
    1.68 -                           map string_for_assign_clause clauses))
    1.69 +                           map (string_for_assign_clause o SOME) clauses))
    1.70  
    1.71  fun print_solution asgs =
    1.72    trace_msg (fn () => "*** Solution:\n" ^
    1.73 @@ -684,22 +686,24 @@
    1.74     [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
    1.75     [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
    1.76  
    1.77 -fun annotation_literal_from_quasi_literal (aa, (cmp, a)) =
    1.78 -  case aa of
    1.79 -    A a' => if annotation_comp cmp a' a then NONE
    1.80 -            else (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.81 -  | V x => SOME (x, (sign_for_comp_op cmp, a))
    1.82 +fun add_annotation_clause_from_quasi_clause _ NONE = NONE
    1.83 +  | add_annotation_clause_from_quasi_clause [] accum = accum
    1.84 +  | add_annotation_clause_from_quasi_clause ((aa, (cmp, a)) :: rest) accum =
    1.85 +    case aa of
    1.86 +      A a' => if annotation_comp cmp a' a then NONE
    1.87 +              else add_annotation_clause_from_quasi_clause rest accum
    1.88 +    | V x => add_annotation_clause_from_quasi_clause rest accum
    1.89 +             |> Option.map (cons (x, (sign_for_comp_op cmp, a)))
    1.90  
    1.91 -val assign_clause_from_quasi_clause =
    1.92 -  map_filter annotation_literal_from_quasi_literal
    1.93 -val add_quasi_clause = assign_clause_from_quasi_clause #> add_assign_clause
    1.94 +fun assign_clause_from_quasi_clause clause =
    1.95 +  add_annotation_clause_from_quasi_clause clause (SOME [])
    1.96  
    1.97  fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 =
    1.98    (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^
    1.99                         string_for_annotation_atom aa1 ^ " " ^ conn ^ " " ^
   1.100                         string_for_annotation_atom aa2);
   1.101 -   fold add_quasi_clause (mk_quasi_clauses res_aa aa1 aa2))
   1.102 -
   1.103 +   fold (add_assign_clause o assign_clause_from_quasi_clause)
   1.104 +        (mk_quasi_clauses res_aa aa1 aa2))
   1.105  fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 =
   1.106    fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
   1.107                     add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
   1.108 @@ -729,11 +733,17 @@
   1.109    | add_annotation_atom_comp_alt cmp (V x) aa1 aa2 =
   1.110      add_annotation_atom_comp cmp [x] aa1 aa2
   1.111  
   1.112 -fun add_arg_order1 ((_, aa), (_, prev_aa)) =
   1.113 +fun add_arg_order1 ((_, aa), (_, prev_aa)) = I
   1.114    add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa
   1.115 -fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) =
   1.116 -  add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa
   1.117 -  ##> add_quasi_clause [(arg_aa, (Neq, Gen)), (res_aa, (Eq, Gen))]
   1.118 +fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = I
   1.119 +  let
   1.120 +    val clause = [(arg_aa, (Eq, New)), (res_aa, (Eq, Gen))]
   1.121 +                 |> assign_clause_from_quasi_clause
   1.122 +  in
   1.123 +    trace_msg (fn () => "*** Add " ^ string_for_assign_clause clause);
   1.124 +    apsnd (add_assign_clause clause)
   1.125 +    #> add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa
   1.126 +  end
   1.127  fun add_app _ [] [] = I
   1.128    | add_app fun_aa res_frame arg_frame =
   1.129      add_comp_frame (A New) Leq arg_frame