consolidate nested thms with persistent result, for improved performance;
authorwenzelm
Fri Dec 16 19:07:16 2016 +0100 (2016-12-16)
changeset 645741134e4d5e5b7
parent 64573 e6aee01da22d
child 64575 d44f0b714e13
consolidate nested thms with persistent result, for improved performance;
always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/Pure/Thy/thy_info.ML
src/Pure/more_thm.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Dec 16 14:06:31 2016 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Dec 16 19:07:16 2016 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4        assms
     1.5        |> map (apsnd (rewrite ctxt eqs'))
     1.6        |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
     1.7 -      |> Old_Z3_Proof_Tools.thm_net_of snd 
     1.8 +      |> Old_Z3_Proof_Tools.thm_net_of snd
     1.9  
    1.10      fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
    1.11  
    1.12 @@ -183,14 +183,14 @@
    1.13            if exact then (Thm.implies_elim thm1 th, ctxt)
    1.14            else assume thm1 ctxt
    1.15          val thms' = if exact then thms else th :: thms
    1.16 -      in 
    1.17 +      in
    1.18          ((insert (op =) i is, thms'),
    1.19            (ctxt', Inttab.update (idx, Thm thm) ptab))
    1.20        end
    1.21  
    1.22      fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
    1.23        let
    1.24 -        val thm1 = 
    1.25 +        val thm1 =
    1.26            Thm.trivial ct
    1.27            |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
    1.28          val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
    1.29 @@ -218,7 +218,7 @@
    1.30    val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
    1.31  in
    1.32  fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
    1.33 -  | mp p_q p = 
    1.34 +  | mp p_q p =
    1.35        let
    1.36          val pq = thm_of p_q
    1.37          val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
    1.38 @@ -509,7 +509,7 @@
    1.39      (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of
    1.40        SOME eq => eq
    1.41      | NONE => if exn then raise MONO else prove_refl cp)
    1.42 -  
    1.43 +
    1.44    val prove_exn = prove_eq true
    1.45    and prove_safe = prove_eq false
    1.46  
    1.47 @@ -752,7 +752,9 @@
    1.48  fun check_after idx r ps ct (p, (ctxt, _)) =
    1.49    if not (Config.get ctxt Old_SMT_Config.trace) then ()
    1.50    else
    1.51 -    let val thm = thm_of p |> tap (Thm.join_proofs o single)
    1.52 +    let
    1.53 +      val thm = thm_of p
    1.54 +      val _ = Thm.consolidate thm
    1.55      in
    1.56        if (Thm.cprop_of thm) aconvc ct then ()
    1.57        else
    1.58 @@ -852,7 +854,7 @@
    1.59  
    1.60    fun discharge_assms_tac ctxt rules =
    1.61      REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt)))
    1.62 -    
    1.63 +
    1.64    fun discharge_assms ctxt rules thm =
    1.65      if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
    1.66      else
    1.67 @@ -881,7 +883,7 @@
    1.68      if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})
    1.69      else
    1.70        (Thm @{thm TrueI}, cxp)
    1.71 -      |> fold (prove simpset vars) steps 
    1.72 +      |> fold (prove simpset vars) steps
    1.73        |> discharge rules outer_ctxt
    1.74        |> pair []
    1.75    end
     2.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 16 14:06:31 2016 +0100
     2.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 16 19:07:16 2016 +0100
     2.3 @@ -293,7 +293,7 @@
     2.4    | SOME _ => error ("Cannot associate a type with " ^ s ^
     2.5        "\nsince it is no record or enumeration type");
     2.6  
     2.7 -fun check_enum [] [] = NONE 
     2.8 +fun check_enum [] [] = NONE
     2.9    | check_enum els [] = SOME ("has no element(s) " ^ commas els)
    2.10    | check_enum [] cs = SOME ("has extra element(s) " ^
    2.11        commas (map (Long_Name.base_name o fst) cs))
    2.12 @@ -305,7 +305,7 @@
    2.13  fun invert_map [] = I
    2.14    | invert_map cmap =
    2.15        map (apfst (the o AList.lookup (op =) (map swap cmap)));
    2.16 - 
    2.17 +
    2.18  fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
    2.19        (check_no_assoc thy prfx s;
    2.20         (ids,
    2.21 @@ -677,7 +677,7 @@
    2.22     "+", "-", "*", "/", "div", "mod", "**"]);
    2.23  
    2.24  fun complex_expr (Number _) = false
    2.25 -  | complex_expr (Ident _) = false 
    2.26 +  | complex_expr (Ident _) = false
    2.27    | complex_expr (Funct (s, es)) =
    2.28        not (Symtab.defined builtin s) orelse exists complex_expr es
    2.29    | complex_expr (Quantifier (_, _, _, e)) = complex_expr e
    2.30 @@ -959,7 +959,7 @@
    2.31      | SOME {vcs, path, ...} =>
    2.32          let
    2.33            val (proved, unproved) = partition_vcs vcs;
    2.34 -          val _ = Thm.join_proofs (maps (#2 o snd) proved);
    2.35 +          val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
    2.36            val (proved', proved'') =
    2.37              List.partition (fn (_, (_, thms, _, _)) =>
    2.38                exists (#oracle o Thm.peek_status) thms) proved;
    2.39 @@ -1117,7 +1117,7 @@
    2.40            [(term_of_rule thy' prfx types pfuns ids rl, [])]))
    2.41             other_rules),
    2.42         Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
    2.43 -          
    2.44 +
    2.45    in
    2.46      set_env ctxt defs' types funs ids vcs' path prfx thy'
    2.47    end;
     3.1 --- a/src/Pure/Thy/thy_info.ML	Fri Dec 16 14:06:31 2016 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 16 19:07:16 2016 +0100
     3.3 @@ -159,7 +159,7 @@
     3.4      (*toplevel proofs and diags*)
     3.5      val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
     3.6      (*fully nested proofs*)
     3.7 -    val res = Exn.capture Thm.join_theory_proofs theory;
     3.8 +    val res = Exn.capture Thm.consolidate_theory theory;
     3.9    in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
    3.10  
    3.11  datatype task =
     4.1 --- a/src/Pure/more_thm.ML	Fri Dec 16 14:06:31 2016 +0100
     4.2 +++ b/src/Pure/more_thm.ML	Fri Dec 16 19:07:16 2016 +0100
     4.3 @@ -111,7 +111,7 @@
     4.4    val untag: string -> attribute
     4.5    val kind: string -> attribute
     4.6    val register_proofs: thm list -> theory -> theory
     4.7 -  val join_theory_proofs: theory -> unit
     4.8 +  val consolidate_theory: theory -> unit
     4.9    val show_consts_raw: Config.raw
    4.10    val show_consts: bool Config.T
    4.11    val show_hyps_raw: Config.raw
    4.12 @@ -644,8 +644,8 @@
    4.13  fun register_proofs more_thms =
    4.14    Proofs.map (fold (cons o Thm.trim_context) more_thms);
    4.15  
    4.16 -fun join_theory_proofs thy =
    4.17 -  Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
    4.18 +fun consolidate_theory thy =
    4.19 +  List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
    4.20  
    4.21  
    4.22  
     5.1 --- a/src/Pure/proofterm.ML	Fri Dec 16 14:06:31 2016 +0100
     5.2 +++ b/src/Pure/proofterm.ML	Fri Dec 16 19:07:16 2016 +0100
     5.3 @@ -46,7 +46,7 @@
     5.4    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
     5.5    val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     5.6      proof_body list -> 'a -> 'a
     5.7 -  val join_bodies: proof_body list -> unit
     5.8 +  val consolidate: proof_body -> unit
     5.9    val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    5.10  
    5.11    val oracle_ord: oracle * oracle -> order
    5.12 @@ -182,7 +182,8 @@
    5.13    {oracles: (string * term) Ord_List.T,
    5.14     thms: (serial * thm_node) Ord_List.T,
    5.15     proof: proof}
    5.16 -and thm_node = Thm_Node of string * term * proof_body future;
    5.17 +and thm_node =
    5.18 +  Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
    5.19  
    5.20  type oracle = string * term;
    5.21  type pthm = serial * thm_node;
    5.22 @@ -190,12 +191,24 @@
    5.23  fun proof_of (PBody {proof, ...}) = proof;
    5.24  val join_proof = Future.join #> proof_of;
    5.25  
    5.26 -fun thm_node_name (Thm_Node (name, _, _)) = name;
    5.27 -fun thm_node_prop (Thm_Node (_, prop, _)) = prop;
    5.28 -fun thm_node_body (Thm_Node (_, _, body)) = body;
    5.29 +fun rep_thm_node (Thm_Node args) = args;
    5.30 +val thm_node_name = #name o rep_thm_node;
    5.31 +val thm_node_prop = #prop o rep_thm_node;
    5.32 +val thm_node_body = #body o rep_thm_node;
    5.33 +val thm_node_consolidate = #consolidate o rep_thm_node;
    5.34  
    5.35  fun join_thms (thms: pthm list) =
    5.36 -  ignore (Future.joins (map (fn (_, Thm_Node (_, _, body)) => body) thms));
    5.37 +  Future.joins (map (thm_node_body o #2) thms);
    5.38 +
    5.39 +fun consolidate (PBody {thms, ...}) =
    5.40 +  List.app (Lazy.force o thm_node_consolidate o #2) thms;
    5.41 +
    5.42 +fun make_thm_node name prop body =
    5.43 +  Thm_Node {name = name, prop = prop, body = body,
    5.44 +    consolidate =
    5.45 +      Lazy.lazy (fn () =>
    5.46 +        let val PBody {thms, ...} = Future.join body
    5.47 +        in List.app consolidate (join_thms thms) end)};
    5.48  
    5.49  
    5.50  (***** proof atoms *****)
    5.51 @@ -218,27 +231,27 @@
    5.52  fun fold_body_thms f =
    5.53    let
    5.54      fun app (PBody {thms, ...}) =
    5.55 -      tap join_thms thms |> fold (fn (i, Thm_Node (name, prop, body)) => fn (x, seen) =>
    5.56 +      tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
    5.57          if Inttab.defined seen i then (x, seen)
    5.58          else
    5.59            let
    5.60 -            val body' = Future.join body;
    5.61 -            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    5.62 -          in (f {serial = i, name = name, prop = prop, body = body'} x', seen') end);
    5.63 +            val name = thm_node_name thm_node;
    5.64 +            val prop = thm_node_prop thm_node;
    5.65 +            val body = Future.join (thm_node_body thm_node);
    5.66 +            val (x', seen') = app body (x, Inttab.update (i, ()) seen);
    5.67 +          in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
    5.68    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    5.69  
    5.70 -fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    5.71 -
    5.72  fun peek_status bodies =
    5.73    let
    5.74      fun status (PBody {oracles, thms, ...}) x =
    5.75        let
    5.76          val ((oracle, unfinished, failed), seen) =
    5.77 -          (thms, x) |-> fold (fn (i, Thm_Node (_, _, body)) => fn (st, seen) =>
    5.78 +          (thms, x) |-> fold (fn (i, thm_node) => fn (st, seen) =>
    5.79              if Inttab.defined seen i then (st, seen)
    5.80              else
    5.81                let val seen' = Inttab.update (i, ()) seen in
    5.82 -                (case Future.peek body of
    5.83 +                (case Future.peek (thm_node_body thm_node) of
    5.84                    SOME (Exn.Res body') => status body' (st, seen')
    5.85                  | SOME (Exn.Exn _) =>
    5.86                      let val (oracle, unfinished, _) = st
    5.87 @@ -264,12 +277,12 @@
    5.88  val all_oracles_of =
    5.89    let
    5.90      fun collect (PBody {oracles, thms, ...}) =
    5.91 -      tap join_thms thms |> fold (fn (i, Thm_Node (_, _, body)) => fn (x, seen) =>
    5.92 +      tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
    5.93          if Inttab.defined seen i then (x, seen)
    5.94          else
    5.95            let
    5.96 -            val body' = Future.join body;
    5.97 -            val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
    5.98 +            val body = Future.join (thm_node_body thm_node);
    5.99 +            val (x', seen') = collect body (x, Inttab.update (i, ()) seen);
   5.100            in (if null oracles then x' else oracles :: x', seen') end);
   5.101    in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
   5.102  
   5.103 @@ -277,7 +290,7 @@
   5.104    let
   5.105      val (oracles, thms) = fold_proof_atoms false
   5.106        (fn Oracle (s, prop, _) => apfst (cons (s, prop))
   5.107 -        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, Thm_Node (name, prop, body)))
   5.108 +        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, make_thm_node name prop body))
   5.109          | _ => I) [prf] ([], []);
   5.110    in
   5.111      PBody
   5.112 @@ -321,8 +334,9 @@
   5.113      ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
   5.114  and proof_body (PBody {oracles, thms, proof = prf}) =
   5.115    triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
   5.116 -and pthm (a, Thm_Node (b, c, body)) =
   5.117 -  pair int (triple string term proof_body) (a, (b, c, Future.join body));
   5.118 +and pthm (a, thm_node) =
   5.119 +  pair int (triple string term proof_body)
   5.120 +    (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
   5.121  
   5.122  in
   5.123  
   5.124 @@ -358,7 +372,7 @@
   5.125    in PBody {oracles = a, thms = b, proof = c} end
   5.126  and pthm x =
   5.127    let val (a, (b, c, d)) = pair int (triple string term proof_body) x
   5.128 -  in (a, Thm_Node (b, c, Future.value d)) end;
   5.129 +  in (a, make_thm_node b c (Future.value d)) end;
   5.130  
   5.131  in
   5.132  
   5.133 @@ -1519,6 +1533,8 @@
   5.134  
   5.135  fun fulfill_norm_proof thy ps body0 =
   5.136    let
   5.137 +    val _ = List.app (consolidate o #2) ps;
   5.138 +    val _ = consolidate body0;
   5.139      val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
   5.140      val oracles =
   5.141        unions_oracles
   5.142 @@ -1616,7 +1632,7 @@
   5.143            else new_prf ()
   5.144        | _ => new_prf ());
   5.145      val head = PThm (i, ((name, prop1, NONE), body'));
   5.146 -  in ((i, Thm_Node (name, prop1, body')), head, args, argsP, args1) end;
   5.147 +  in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
   5.148  
   5.149  fun thm_proof thy name shyps hyps concl promises body =
   5.150    let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
     6.1 --- a/src/Pure/thm.ML	Fri Dec 16 14:06:31 2016 +0100
     6.2 +++ b/src/Pure/thm.ML	Fri Dec 16 19:07:16 2016 +0100
     6.3 @@ -86,7 +86,7 @@
     6.4    val proof_bodies_of: thm list -> proof_body list
     6.5    val proof_body_of: thm -> proof_body
     6.6    val proof_of: thm -> proof
     6.7 -  val join_proofs: thm list -> unit
     6.8 +  val consolidate: thm -> unit
     6.9    val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
    6.10    val future: thm future -> cterm -> thm
    6.11    val derivation_closed: thm -> bool
    6.12 @@ -588,17 +588,11 @@
    6.13    let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises))
    6.14    in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end;
    6.15  
    6.16 -fun proof_bodies_of thms =
    6.17 -  let
    6.18 -    val _ = join_promises_of thms;
    6.19 -    val bodies = map fulfill_body thms;
    6.20 -    val _ = Proofterm.join_bodies bodies;
    6.21 -  in bodies end;
    6.22 -
    6.23 +fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms);
    6.24  val proof_body_of = singleton proof_bodies_of;
    6.25  val proof_of = Proofterm.proof_of o proof_body_of;
    6.26  
    6.27 -val join_proofs = Proofterm.join_bodies o proof_bodies_of;
    6.28 +val consolidate = ignore o proof_bodies_of o single;
    6.29  
    6.30  
    6.31  (* derivation status *)