tuning
authorblanchet
Tue Sep 30 11:19:30 2014 +0200 (2014-09-30)
changeset 58490f6d99c69dae9
parent 58489 558459615a73
child 58491 5ddbc170e46c
tuning
src/HOL/Tools/SMT/verit_proof.ML
     1.1 --- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 30 11:06:26 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 30 11:19:30 2014 +0200
     1.3 @@ -91,49 +91,43 @@
     1.4       replace_bound_var_by_free_var v free_vars
     1.5    | replace_bound_var_by_free_var u _ = u
     1.6  
     1.7 -fun find_type_in_formula (Abs(v, ty, u)) var_name =
     1.8 -    if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name
     1.9 +fun find_type_in_formula (Abs (v, T, u)) var_name =
    1.10 +    if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
    1.11    | find_type_in_formula (u $ v) var_name =
    1.12      (case find_type_in_formula u var_name of
    1.13        NONE => find_type_in_formula v var_name
    1.14 -    | a => a)
    1.15 +    | some_T => some_T)
    1.16    | find_type_in_formula _ _ = NONE
    1.17  
    1.18 -fun add_bound_variables_to_ctxt cx bounds concl =
    1.19 -    fold (fn a => fn b => update_binding a b)
    1.20 -      (map (fn s => ((s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
    1.21 -       bounds) cx
    1.22 +fun add_bound_variables_to_ctxt concl =
    1.23 +  fold (update_binding o
    1.24 +    (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
    1.25  
    1.26 -fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx =
    1.27 +fun update_step_and_cx (node as VeriT_Node {id, rule, prems, concl, bounds}) cx =
    1.28    if rule = veriT_tmp_ite_elim_rule then
    1.29 -    (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl)
    1.30 +    (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt concl bounds cx)
    1.31    else if rule = veriT_tmp_skolemize_rule then
    1.32 -    let
    1.33 -      val concl' = replace_bound_var_by_free_var concl bounds
    1.34 -    in
    1.35 -      (mk_node id rule prems concl' [], add_bound_variables_to_ctxt cx bounds concl)
    1.36 +    let val concl' = replace_bound_var_by_free_var concl bounds in
    1.37 +      (mk_node id rule prems concl' [], add_bound_variables_to_ctxt concl bounds cx)
    1.38      end
    1.39    else
    1.40 -    (st, cx)
    1.41 +    (node, cx)
    1.42  
    1.43 -(*FIXME: using a reference would be better to know th numbers of the steps to add*)
    1.44 +(*FIXME: using a reference would be better to know the numbers of the steps to add*)
    1.45  fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
    1.46      cx)) =
    1.47    let
    1.48 -    fun mk_prop_of_term concl = (fastype_of concl = @{typ "bool"} ?
    1.49 -      curry (op $) @{term "Trueprop"}) concl
    1.50 -    fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl,
    1.51 -        bounds}) =
    1.52 +    fun mk_prop_of_term concl =
    1.53 +      concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
    1.54 +    fun inline_assumption assumption assumption_id
    1.55 +        (node as VeriT_Node {id, rule, prems, concl, bounds}) =
    1.56        if List.find (curry (op =) assumption_id) prems <> NONE then
    1.57 -        let
    1.58 -          val prems' = filter_out (curry (op =) assumption_id) prems
    1.59 -        in
    1.60 +        let val prems' = filter_out (curry (op =) assumption_id) prems in
    1.61            mk_node id rule (filter_out (curry (op =) assumption_id) prems')
    1.62 -            (Const (@{const_name "Pure.imp"}, @{typ "prop"} --> @{typ "prop"} --> @{typ "prop"})
    1.63 -            $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
    1.64 +            (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
    1.65          end
    1.66        else
    1.67 -        st
    1.68 +        node
    1.69      fun find_input_steps_and_inline [] last_step = ([], last_step)
    1.70        | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
    1.71            last_step =
    1.72 @@ -144,7 +138,8 @@
    1.73              (find_input_steps_and_inline steps (id_of_father_step ^ id'))
    1.74      val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
    1.75      val prems' =
    1.76 -      if last_step_id = "" then prems
    1.77 +      if last_step_id = "" then
    1.78 +        prems
    1.79        else
    1.80          (case prems of
    1.81            NONE => SOME [last_step_id]
    1.82 @@ -179,9 +174,9 @@
    1.83      fun make_or_from_clausification l =
    1.84        foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) =>
    1.85          (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
    1.86 -        perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
    1.87 -    fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule
    1.88 -      (the_default [] prems) concl bounds, cx)
    1.89 +         perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
    1.90 +    fun to_node (((((id, rule), prems), concl), bounds), cx) =
    1.91 +      (mk_node id rule (the_default [] prems) concl bounds, cx)
    1.92    in
    1.93      get_id
    1.94      ##> parse_rule
    1.95 @@ -206,23 +201,25 @@
    1.96  unbalanced on each line*)
    1.97  fun seperate_into_steps lines =
    1.98    let
    1.99 -    fun count ("(" :: l) n = count l (n+1)
   1.100 -      | count (")" :: l) n = count l (n-1)
   1.101 +    fun count ("(" :: l) n = count l (n + 1)
   1.102 +      | count (")" :: l) n = count l (n - 1)
   1.103        | count (_ :: l) n = count l n
   1.104        | count [] n = n
   1.105      fun seperate (line :: l) actual_lines m =
   1.106          let val n = count (raw_explode line) 0 in
   1.107            if m + n = 0 then
   1.108              [actual_lines ^ line] :: seperate l "" 0
   1.109 -          else seperate l (actual_lines ^ line) (m + n)
   1.110 +          else
   1.111 +            seperate l (actual_lines ^ line) (m + n)
   1.112          end
   1.113        | seperate [] _ 0 = []
   1.114    in
   1.115      seperate lines "" 0
   1.116    end
   1.117  
   1.118 - (* VeriT adds @ before every variable. *)
   1.119 -fun remove_all_at (SMTLIB.Sym v :: l) = SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
   1.120 +(* VeriT adds "@" before every variable. *)
   1.121 +fun remove_all_at (SMTLIB.Sym v :: l) =
   1.122 +    SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
   1.123    | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l'
   1.124    | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l
   1.125    | remove_all_at (v :: l) = v :: remove_all_at l
   1.126 @@ -235,9 +232,9 @@
   1.127    | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var)
   1.128  
   1.129  (*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
   1.130 -fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $
   1.131 -      (Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $
   1.132 -      (Const (@{const_name "HOL.eq"}, _) $ Free (var3, _) $ Free (var4, _) )) =
   1.133 +fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
   1.134 +      (Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $
   1.135 +      (Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) =
   1.136      let
   1.137        fun get_number_of_ite_transformed_var var =
   1.138          perhaps (try (unprefix "ite")) var
   1.139 @@ -261,13 +258,13 @@
   1.140        | (_, SOME _) => var2_introduced_var
   1.141        | (SOME _, _) => var1_introduced_var)
   1.142      end
   1.143 -  | find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $
   1.144 -      (Const (@{const_name "HOL.eq"}, _) $ Free (var, _) $ _ ) $
   1.145 -      (Const (@{const_name "HOL.eq"}, _) $ Free (var', _) $ _ )) =
   1.146 +  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
   1.147 +      (Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $
   1.148 +      (Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) =
   1.149      if var = var' then SOME var else NONE
   1.150 -  | find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $
   1.151 -      (Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var, _)) $
   1.152 -      (Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var', _))) =
   1.153 +  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
   1.154 +      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $
   1.155 +      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) =
   1.156      if var = var' then SOME var else NONE
   1.157    | find_ite_var_in_term (p $ q) =
   1.158      (case find_ite_var_in_term p of
   1.159 @@ -276,34 +273,31 @@
   1.160    | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
   1.161    | find_ite_var_in_term _ = NONE
   1.162  
   1.163 -fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) =
   1.164 +fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) =
   1.165    if rule = veriT_tmp_ite_elim_rule then
   1.166      if bounds = [] then
   1.167        (*if the introduced var has already been defined, adding the definition as a dependency*)
   1.168        let
   1.169 -        val new_prems =
   1.170 -          (case find_ite_var_in_term concl of
   1.171 -            NONE => prems
   1.172 -          | SOME var => find_in_which_step_defined var steps :: prems)
   1.173 +        val new_prems = prems
   1.174 +          |> (case find_ite_var_in_term concl of
   1.175 +               NONE => I
   1.176 +             | SOME var => cons (find_in_which_step_defined var steps))
   1.177        in
   1.178          VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
   1.179        end
   1.180      else
   1.181        (*some new variables are created*)
   1.182 -      let
   1.183 -        val concl' = replace_bound_var_by_free_var concl bounds
   1.184 -      in
   1.185 +      let val concl' = replace_bound_var_by_free_var concl bounds in
   1.186          mk_node id rule prems concl' []
   1.187        end
   1.188    else
   1.189 -    st
   1.190 +    node
   1.191  
   1.192  fun remove_alpha_conversion _ [] = []
   1.193    | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
   1.194      let
   1.195 -      fun correct_dependency prems =
   1.196 -        map (fn x => perhaps (Symtab.lookup replace_table) x) prems
   1.197 -      fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem
   1.198 +      val correct_dependency = map (perhaps (Symtab.lookup replace_table))
   1.199 +      val find_predecessor = perhaps (Symtab.lookup replace_table)
   1.200      in
   1.201        if rule = veriT_alpha_conv_rule then
   1.202          remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
   1.203 @@ -326,7 +320,7 @@
   1.204      val t = correct_veriT_steps u
   1.205      fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
   1.206        mk_step id rule prems concl bounds
   1.207 -   in
   1.208 +  in
   1.209      (map node_to_step t, ctxt_of env)
   1.210    end
   1.211