src/HOL/Tools/SMT/verit_proof.ML
author blanchet
Thu Aug 28 16:58:27 2014 +0200 (2014-08-28)
changeset 58078 d44c9dc4bf30
parent 58061 3d060f43accb
child 58490 f6d99c69dae9
permissions -rw-r--r--
took out one more occurrence of 'PolyML.makestring'
     1 (*  Title:      HOL/Tools/SMT/verit_proof.ML
     2     Author:     Mathias Fleury, ENS Rennes
     3     Author:     Sascha Boehme, TU Muenchen
     4 
     5 VeriT proofs: parsing and abstract syntax tree.
     6 *)
     7 
     8 signature VERIT_PROOF =
     9 sig
    10   (*proofs*)
    11   datatype veriT_step = VeriT_Step of {
    12     id: string,
    13     rule: string,
    14     prems: string list,
    15     concl: term,
    16     fixes: string list}
    17 
    18   (*proof parser*)
    19   val parse: typ Symtab.table -> term Symtab.table -> string list ->
    20     Proof.context -> veriT_step list * Proof.context
    21 
    22   val veriT_step_prefix : string
    23   val veriT_input_rule: string
    24   val veriT_la_generic_rule : string
    25   val veriT_rewrite_rule : string
    26   val veriT_simp_arith_rule : string
    27   val veriT_tmp_ite_elim_rule : string
    28   val veriT_tmp_skolemize_rule : string
    29 end;
    30 
    31 structure VeriT_Proof: VERIT_PROOF =
    32 struct
    33 
    34 open SMTLIB_Proof
    35 
    36 datatype veriT_node = VeriT_Node of {
    37   id: string,
    38   rule: string,
    39   prems: string list,
    40   concl: term,
    41   bounds: string list}
    42 
    43 fun mk_node id rule prems concl bounds =
    44   VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
    45 
    46 datatype veriT_step = VeriT_Step of {
    47   id: string,
    48   rule: string,
    49   prems: string list,
    50   concl: term,
    51   fixes: string list}
    52 
    53 fun mk_step id rule prems concl fixes =
    54   VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
    55 
    56 val veriT_step_prefix = ".c"
    57 val veriT_alpha_conv_rule = "tmp_alphaconv"
    58 val veriT_input_rule = "input"
    59 val veriT_la_generic_rule = "la_generic"
    60 val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
    61 val veriT_simp_arith_rule = "simp_arith"
    62 val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
    63 val veriT_tmp_skolemize_rule = "tmp_skolemize"
    64 
    65 (* proof parser *)
    66 
    67 fun node_of p cx =
    68   ([], cx)
    69   ||>> `(with_fresh_names (term_of p))
    70   |>> snd
    71 
    72 (*in order to get Z3-style quantification*)
    73 fun repair_quantification (SMTLIB.S (SMTLIB.Sym "forall" :: l)) =
    74     let val (quantified_vars, t) = split_last (map repair_quantification l)
    75     in
    76       SMTLIB.S (SMTLIB.Sym "forall" :: SMTLIB.S quantified_vars :: t :: [])
    77     end
    78   | repair_quantification (SMTLIB.S (SMTLIB.Sym "exists" :: l)) =
    79     let val (quantified_vars, t) = split_last (map repair_quantification l)
    80     in
    81       SMTLIB.S (SMTLIB.Sym "exists" :: SMTLIB.S quantified_vars :: t :: [])
    82     end
    83   | repair_quantification (SMTLIB.S l) = SMTLIB.S (map repair_quantification l)
    84   | repair_quantification x = x
    85 
    86 fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var =
    87     (case List.find (fn v => String.isPrefix v var) free_var of
    88       NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var)
    89     | SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var)
    90   | replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $
    91      replace_bound_var_by_free_var v free_vars
    92   | replace_bound_var_by_free_var u _ = u
    93 
    94 fun find_type_in_formula (Abs(v, ty, u)) var_name =
    95     if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name
    96   | find_type_in_formula (u $ v) var_name =
    97     (case find_type_in_formula u var_name of
    98       NONE => find_type_in_formula v var_name
    99     | a => a)
   100   | find_type_in_formula _ _ = NONE
   101 
   102 fun add_bound_variables_to_ctxt cx bounds concl =
   103     fold (fn a => fn b => update_binding a b)
   104       (map (fn s => ((s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
   105        bounds) cx
   106 
   107 fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx =
   108   if rule = veriT_tmp_ite_elim_rule then
   109     (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl)
   110   else if rule = veriT_tmp_skolemize_rule then
   111     let
   112       val concl' = replace_bound_var_by_free_var concl bounds
   113     in
   114       (mk_node id rule prems concl' [], add_bound_variables_to_ctxt cx bounds concl)
   115     end
   116   else
   117     (st, cx)
   118 
   119 (*FIXME: using a reference would be better to know th numbers of the steps to add*)
   120 fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
   121     cx)) =
   122   let
   123     fun mk_prop_of_term concl = (fastype_of concl = @{typ "bool"} ?
   124       curry (op $) @{term "Trueprop"}) concl
   125     fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl,
   126         bounds}) =
   127       if List.find (curry (op =) assumption_id) prems <> NONE then
   128         let
   129           val prems' = filter_out (curry (op =) assumption_id) prems
   130         in
   131           mk_node id rule (filter_out (curry (op =) assumption_id) prems')
   132             (Const (@{const_name "Pure.imp"}, @{typ "prop"} --> @{typ "prop"} --> @{typ "prop"})
   133             $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
   134         end
   135       else
   136         st
   137     fun find_input_steps_and_inline [] last_step = ([], last_step)
   138       | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
   139           last_step =
   140         if rule = veriT_input_rule then
   141           find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step
   142         else
   143           apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds))
   144             (find_input_steps_and_inline steps (id_of_father_step ^ id'))
   145     val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
   146     val prems' =
   147       if last_step_id = "" then prems
   148       else
   149         (case prems of
   150           NONE => SOME [last_step_id]
   151         | SOME l => SOME (last_step_id :: l))
   152   in
   153     (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx))
   154   end
   155 
   156 (*
   157 (set id rule :clauses(...) :args(..) :conclusion (...)).
   158 or
   159 (set id subproof (set ...) :conclusion (...)).
   160 *)
   161 
   162 fun parse_proof_step cx =
   163   let
   164     fun rotate_pair (a, (b, c)) = ((a, b), c)
   165     fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
   166       | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
   167     fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l)
   168     fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
   169         (SOME (map (fn (SMTLIB.Sym id) => id) source), l)
   170       | parse_source l = (NONE, l)
   171     fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
   172         let val (subproof_steps, cx') = parse_proof_step cx subproof_step in
   173           apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l)
   174         end
   175       | parse_subproof cx _ l = (([], cx), l)
   176     fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l
   177       | skip_args l = l
   178     fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl
   179     fun make_or_from_clausification l =
   180       foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) =>
   181         (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
   182         perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
   183     fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule
   184       (the_default [] prems) concl bounds, cx)
   185   in
   186     get_id
   187     ##> parse_rule
   188     #> rotate_pair
   189     ##> parse_source
   190     #> rotate_pair
   191     ##> skip_args
   192     #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub))
   193     #> rotate_pair
   194     ##> parse_conclusion
   195     ##> map repair_quantification
   196     #> (fn ((((id, rule), prems), (subproof, cx)), terms) =>
   197          (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx)))
   198     ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls)
   199     #> fix_subproof_steps
   200     ##> to_node
   201     #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
   202     #-> fold_map update_step_and_cx
   203   end
   204 
   205 (*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are
   206 unbalanced on each line*)
   207 fun seperate_into_steps lines =
   208   let
   209     fun count ("(" :: l) n = count l (n+1)
   210       | count (")" :: l) n = count l (n-1)
   211       | count (_ :: l) n = count l n
   212       | count [] n = n
   213     fun seperate (line :: l) actual_lines m =
   214         let val n = count (raw_explode line) 0 in
   215           if m + n = 0 then
   216             [actual_lines ^ line] :: seperate l "" 0
   217           else seperate l (actual_lines ^ line) (m + n)
   218         end
   219       | seperate [] _ 0 = []
   220   in
   221     seperate lines "" 0
   222   end
   223 
   224  (* VeriT adds @ before every variable. *)
   225 fun remove_all_at (SMTLIB.Sym v :: l) = SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
   226   | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l'
   227   | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l
   228   | remove_all_at (v :: l) = v :: remove_all_at l
   229   | remove_all_at [] = []
   230 
   231 fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) =
   232     (case List.find (fn v => String.isPrefix v var) bounds of
   233       NONE => find_in_which_step_defined var l
   234     | SOME _ => id)
   235   | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var)
   236 
   237 (*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
   238 fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $
   239       (Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $
   240       (Const (@{const_name "HOL.eq"}, _) $ Free (var3, _) $ Free (var4, _) )) =
   241     let
   242       fun get_number_of_ite_transformed_var var =
   243         perhaps (try (unprefix "ite")) var
   244         |> Int.fromString
   245       fun is_equal_and_has_correct_substring var var' var'' =
   246         if var = var' andalso String.isPrefix "ite" var then SOME var'
   247         else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE
   248       val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4
   249       val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2
   250     in
   251       (case (var1_introduced_var, var2_introduced_var) of
   252         (SOME a, SOME b) =>
   253           (*ill-generated case, might be possible when applying the rule to max a a. Only if the
   254           variable have been introduced before. Probably an impossible edge case*)
   255           (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of
   256             (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var
   257             (*Otherwise, it is a name clase between a parameter name and the introduced variable.
   258              Or the name convention has been changed.*)
   259           | (NONE, SOME _) => var2_introduced_var
   260           | (SOME _, NONE) => var2_introduced_var)
   261       | (_, SOME _) => var2_introduced_var
   262       | (SOME _, _) => var1_introduced_var)
   263     end
   264   | find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $
   265       (Const (@{const_name "HOL.eq"}, _) $ Free (var, _) $ _ ) $
   266       (Const (@{const_name "HOL.eq"}, _) $ Free (var', _) $ _ )) =
   267     if var = var' then SOME var else NONE
   268   | find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $
   269       (Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var, _)) $
   270       (Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var', _))) =
   271     if var = var' then SOME var else NONE
   272   | find_ite_var_in_term (p $ q) =
   273     (case find_ite_var_in_term p of
   274       NONE => find_ite_var_in_term q
   275     | x => x)
   276   | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
   277   | find_ite_var_in_term _ = NONE
   278 
   279 fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) =
   280   if rule = veriT_tmp_ite_elim_rule then
   281     if bounds = [] then
   282       (*if the introduced var has already been defined, adding the definition as a dependency*)
   283       let
   284         val new_prems =
   285           (case find_ite_var_in_term concl of
   286             NONE => prems
   287           | SOME var => find_in_which_step_defined var steps :: prems)
   288       in
   289         VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
   290       end
   291     else
   292       (*some new variables are created*)
   293       let
   294         val concl' = replace_bound_var_by_free_var concl bounds
   295       in
   296         mk_node id rule prems concl' []
   297       end
   298   else
   299     st
   300 
   301 fun remove_alpha_conversion _ [] = []
   302   | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
   303     let
   304       fun correct_dependency prems =
   305         map (fn x => perhaps (Symtab.lookup replace_table) x) prems
   306       fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem
   307     in
   308       if rule = veriT_alpha_conv_rule then
   309         remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
   310           replace_table) steps
   311       else
   312         VeriT_Node {id = id, rule = rule, prems = correct_dependency prems,
   313           concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps
   314     end
   315 
   316 fun correct_veriT_steps steps =
   317   steps
   318   |> map (correct_veriT_step steps)
   319   |> remove_alpha_conversion Symtab.empty
   320 
   321 fun parse typs funs lines ctxt =
   322   let
   323     val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines))
   324     val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
   325       smtlib_lines_without_at (empty_context ctxt typs funs))
   326     val t = correct_veriT_steps u
   327     fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
   328       mk_step id rule prems concl bounds
   329    in
   330     (map node_to_step t, ctxt_of env)
   331   end
   332 
   333 end;