src/Pure/proofterm.ML
changeset 44333 cc53ce50f738
parent 44332 e10f6b873f88
child 44334 605381e7c7c5
equal deleted inserted replaced
44332:e10f6b873f88 44333:cc53ce50f738
    35 sig
    35 sig
    36   include BASIC_PROOFTERM
    36   include BASIC_PROOFTERM
    37 
    37 
    38   type oracle = string * term
    38   type oracle = string * term
    39   type pthm = serial * (string * term * proof_body future)
    39   type pthm = serial * (string * term * proof_body future)
    40   val check_body_thms: proof_body -> proof_body future
       
    41   val proof_of: proof_body -> proof
    40   val proof_of: proof_body -> proof
    42   val join_proof: proof_body future -> proof
    41   val join_proof: proof_body future -> proof
    43   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    42   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    44   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    43   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
       
    44   val join_bodies: proof_body list -> unit
    45   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    45   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    46 
    46 
    47   val oracle_ord: oracle * oracle -> order
    47   val oracle_ord: oracle * oracle -> order
    48   val thm_ord: pthm * pthm -> order
    48   val thm_ord: pthm * pthm -> order
    49   val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
    49   val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
   169    proof: proof};
   169    proof: proof};
   170 
   170 
   171 type oracle = string * term;
   171 type oracle = string * term;
   172 type pthm = serial * (string * term * proof_body future);
   172 type pthm = serial * (string * term * proof_body future);
   173 
   173 
   174 fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
       
   175 
       
   176 fun check_body_thms (body as PBody {thms, ...}) =
       
   177   (singleton o Future.cond_forks)
       
   178     {name = "Proofterm.check_body_thms", group = NONE,
       
   179       deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true}
       
   180     (fn () => (join_thms thms; body));
       
   181 
       
   182 fun proof_of (PBody {proof, ...}) = proof;
   174 fun proof_of (PBody {proof, ...}) = proof;
   183 val join_proof = Future.join #> proof_of;
   175 val join_proof = Future.join #> proof_of;
       
   176 
       
   177 fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
   184 
   178 
   185 
   179 
   186 (***** proof atoms *****)
   180 (***** proof atoms *****)
   187 
   181 
   188 fun fold_proof_atoms all f =
   182 fun fold_proof_atoms all f =
   209           let
   203           let
   210             val body' = Future.join body;
   204             val body' = Future.join body;
   211             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
   205             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
   212           in (f (name, prop, body') x', seen') end);
   206           in (f (name, prop, body') x', seen') end);
   213   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
   207   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
       
   208 
       
   209 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
   214 
   210 
   215 fun status_of bodies =
   211 fun status_of bodies =
   216   let
   212   let
   217     fun status (PBody {oracles, thms, ...}) x =
   213     fun status (PBody {oracles, thms, ...}) x =
   218       let
   214       let
  1465         (singleton o Future.cond_forks)
  1461         (singleton o Future.cond_forks)
  1466           {name = "Proofterm.prepare_thm_proof", group = NONE,
  1462           {name = "Proofterm.prepare_thm_proof", group = NONE,
  1467             deps = [], pri = 0, interrupts = true}
  1463             deps = [], pri = 0, interrupts = true}
  1468           (make_body0 o full_proof0);
  1464           (make_body0 o full_proof0);
  1469 
  1465 
  1470     fun new_prf () =
  1466     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
  1471       let
       
  1472         val body' = body0
       
  1473           |> fulfill_proof_future thy promises postproc
       
  1474           |> Future.map (fn body as PBody {thms, ...} => (join_thms thms; body));
       
  1475       in (serial (), body') end;
       
  1476 
       
  1477     val (i, body') =
  1467     val (i, body') =
  1478       (*non-deterministic, depends on unknown promises*)
  1468       (*non-deterministic, depends on unknown promises*)
  1479       (case strip_combt (fst (strip_combP prf)) of
  1469       (case strip_combt (fst (strip_combP prf)) of
  1480         (PThm (i, ((old_name, prop', NONE), body')), args') =>
  1470         (PThm (i, ((old_name, prop', NONE), body')), args') =>
  1481           if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'
  1471           if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'