# HG changeset patch # User wenzelm # Date 965237988 -7200 # Node ID 9cd32060bbc866cc66e4af7521a374533973082b # Parent e21a761422691093a77fbc109e791d184b1c2c7a derivations: maintain oracle flag; diff -r e21a76142269 -r 9cd32060bbc8 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Aug 02 19:38:33 2000 +0200 +++ b/src/Pure/thm.ML Wed Aug 02 19:39:48 2000 +0200 @@ -83,10 +83,10 @@ (*meta theorems*) type thm - val rep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int, + val rep_thm : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int, shyps: sort list, hyps: term list, prop: term} - val crep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int, + val crep_thm : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int, shyps: sort list, hyps: cterm list, prop: cterm} exception THM of string * int * thm list @@ -365,6 +365,7 @@ val keep_derivs = ref MinDeriv; +local (*Build a minimal derivation. Keep oracles; suppress atomic inferences; retain Theorems or their underlying links; keep anything else*) @@ -381,7 +382,6 @@ | Join (_, []) => squash_derivs ders | _ => der :: squash_derivs ders); - (*Ensure sharing of the most likely derivation, the empty one!*) val min_infer = Join (MinProof, []); @@ -390,10 +390,18 @@ | make_min_infer [der] = der | make_min_infer ders = Join (MinProof, ders); -fun infer_derivs (rl, []) = Join (rl, []) +fun is_oracle (Oracle _) = true + | is_oracle _ = false; + +in + +fun infer_derivs (rl, []: (bool * deriv) list) = (is_oracle rl, Join (rl, [])) | infer_derivs (rl, ders) = - if !keep_derivs=FullDeriv then Join (rl, ders) - else make_min_infer (squash_derivs ders); + (is_oracle rl orelse exists #1 ders, + if !keep_derivs=FullDeriv then Join (rl, map #2 ders) + else make_min_infer (squash_derivs (map #2 ders))); + +end; @@ -401,7 +409,7 @@ datatype thm = Thm of {sign_ref: Sign.sg_ref, (*mutable reference to signature*) - der: deriv, (*derivation*) + der: bool * deriv, (*derivation*) maxidx: int, (*maximum index of any Var or TVar*) shyps: sort list, (*sort hypotheses*) hyps: term list, (*hypotheses*) @@ -608,12 +616,12 @@ (* name and tags -- make proof objects more readable *) fun get_name_tags (Thm {der, ...}) = - (case der of + (case #2 der of Join (Theorem x, _) => x | Join (Axiom x, _) => x | _ => ("", [])); -fun put_name_tags x (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = +fun put_name_tags x (Thm {sign_ref, der = (ora, der), maxidx, shyps, hyps, prop}) = let val der' = (case der of @@ -621,7 +629,7 @@ | Join (Axiom _, ds) => Join (Axiom x, ds) | _ => Join (Theorem x, [der])); in - Thm {sign_ref = sign_ref, der = der', maxidx = maxidx, + Thm {sign_ref = sign_ref, der = (ora, der'), maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop} end; @@ -2168,7 +2176,7 @@ and subc skel (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) - (trec as (t0:term,etc:sort list*term list * rule mtree list)) = + (trec as (t0:term,etc:sort list*term list * (bool * deriv) list)) = (case t0 of Abs(a,T,t) => let val b = variant bounds a @@ -2353,7 +2361,7 @@ raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else fix_shyps [] [] (Thm {sign_ref = sign_ref', - der = Join (Oracle (name, sign, exn), []), + der = (true, Join (Oracle (name, sign, exn), [])), maxidx = maxidx, shyps = [], hyps = [],