--- a/src/Pure/General/cache.scala Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/General/cache.scala Thu Aug 15 21:46:43 2019 +0200
@@ -37,9 +37,6 @@
x
}
- protected def cache_int(x: Int): Int =
- lookup(x) getOrElse store(x)
-
protected def cache_string(x: String): String =
{
if (x == "") ""
@@ -58,6 +55,5 @@
}
// main methods
- def int(x: Int): Int = synchronized { cache_int(x) }
def string(x: String): String = synchronized { cache_string(x) }
}
--- a/src/Pure/PIDE/document.scala Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/PIDE/document.scala Thu Aug 15 21:46:43 2019 +0200
@@ -390,6 +390,9 @@
def iterator: Iterator[(Node.Name, Node)] =
graph.iterator.map({ case (name, (node, _)) => (name, node) })
+ def theory_name(theory: String): Option[Node.Name] =
+ graph.keys_iterator.find(name => name.theory == theory)
+
def commands_loading(file_name: Node.Name): List[Command] =
(for {
(_, node) <- iterator
--- a/src/Pure/Proof/extraction.ML Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Aug 15 21:46:43 2019 +0200
@@ -597,7 +597,7 @@
| corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
let
- val {pos, name, prop, ...} = thm_header;
+ val {pos, theory_name, name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -622,8 +622,9 @@
val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
- Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs')
- corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
+ Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
+ (corr_name name vs') corr_prop
+ (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
val corr_prf' =
Proofterm.proof_combP
@@ -698,7 +699,7 @@
| extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
let
- val {pos, name = s, prop, ...} = thm_header;
+ val {pos, theory_name, name = s, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -742,8 +743,9 @@
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
- Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs')
- corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
+ Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
+ (corr_name s vs') corr_prop
+ (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
--- a/src/Pure/Thy/export.scala Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/Thy/export.scala Thu Aug 15 21:46:43 2019 +0200
@@ -226,6 +226,10 @@
def apply(export_name: String): Option[Entry] =
read_entry(db, session_name, theory_name, export_name)
+ def focus(other_theory: String): Provider =
+ if (other_theory == theory_name) this
+ else Provider.database(db, session_name, other_theory)
+
override def toString: String = db.toString
}
@@ -234,6 +238,15 @@
def apply(export_name: String): Option[Entry] =
snapshot.exports_map.get(export_name)
+ def focus(other_theory: String): Provider =
+ if (other_theory == snapshot.node_name.theory) this
+ else {
+ val node_name =
+ snapshot.version.nodes.theory_name(other_theory) getOrElse
+ error("Bad theory " + quote(other_theory))
+ Provider.snapshot(snapshot.state.snapshot(node_name))
+ }
+
override def toString: String = snapshot.toString
}
@@ -242,6 +255,10 @@
def apply(export_name: String): Option[Entry] =
read_entry(dir, session_name, theory_name, export_name)
+ def focus(other_theory: String): Provider =
+ if (other_theory == theory_name) this
+ else Provider.directory(dir, session_name, other_theory)
+
override def toString: String = dir.toString
}
}
@@ -255,6 +272,8 @@
case Some(entry) => entry.uncompressed_yxml(cache = cache)
case None => Nil
}
+
+ def focus(other_theory: String): Provider
}
--- a/src/Pure/Thy/export_theory.ML Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML Thu Aug 15 21:46:43 2019 +0200
@@ -220,40 +220,40 @@
(* axioms and facts *)
- fun prop_of raw_thm =
+ fun standard_prop used extra_shyps raw_prop raw_proof =
let
- val thm = raw_thm
- |> Thm.transfer thy
- |> Thm.check_hyps (Context.Theory thy)
- |> Thm.strip_shyps;
- val prop = thm
- |> Thm.full_prop_of;
- in (Thm.extra_shyps thm, prop) end;
-
- fun encode_prop used (Ss, raw_prop) =
- let
- val prop = Proofterm.standard_vars_term used raw_prop;
+ val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
val args = rev (add_frees used prop []);
val typargs = rev (add_tfrees used prop []);
- val used' = fold (Name.declare o #1) typargs used;
- val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
- in
- (sorts @ typargs, args, prop) |>
- let open XML.Encode Term_XML.Encode
- in triple (list (pair string sort)) (list (pair string typ)) term end
- end;
+ val used_typargs = fold (Name.declare o #1) typargs used;
+ val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
+ in ((sorts @ typargs, args, prop), proof) end;
+
+ val encode_prop =
+ let open XML.Encode Term_XML.Encode
+ in triple (list (pair string sort)) (list (pair string typ)) term end;
+
+ fun encode_axiom used prop =
+ encode_prop (#1 (standard_prop used [] prop NONE));
- fun encode_axiom used t = encode_prop used ([], t);
+ val clean_thm =
+ Thm.transfer thy
+ #> Thm.check_hyps (Context.Theory thy)
+ #> Thm.strip_shyps;
- val encode_fact = encode_prop Name.context;
- val encode_fact_single = encode_fact o prop_of;
- val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
+ val encode_fact = clean_thm #> (fn thm =>
+ standard_prop Name.context
+ (Thm.extra_shyps thm)
+ (Thm.full_prop_of thm)
+ (try Thm.reconstruct_proof_of thm) |>
+ let open XML.Encode Term_XML.Encode
+ in pair encode_prop (option Proofterm.encode_full) end);
val _ =
export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
Theory.axiom_space (Theory.axioms_of thy);
val _ =
- export_entities "facts" (K (SOME o encode_fact_multi))
+ export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
(Facts.space_of o Global_Theory.facts_of)
(Facts.dest_static true [] (Global_Theory.facts_of thy));
@@ -262,12 +262,12 @@
val encode_class =
let open XML.Encode Term_XML.Encode
- in pair (list (pair string typ)) (list encode_fact_single) end;
+ in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
fun export_class name =
(case try (Axclass.get_info thy) name of
NONE => ([], [])
- | SOME {params, axioms, ...} => (params, axioms))
+ | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
|> encode_class |> SOME;
val _ =
--- a/src/Pure/Thy/export_theory.scala Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala Thu Aug 15 21:46:43 2019 +0200
@@ -65,6 +65,7 @@
/** theory content **/
val export_prefix: String = "theory/"
+ val export_prefix_proofs: String = "proofs/"
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
@@ -284,7 +285,7 @@
})
- /* facts */
+ /* axioms and facts */
sealed case class Prop(
typargs: List[(String, Term.Sort)],
@@ -309,23 +310,45 @@
Prop(typargs, args, t)
}
- sealed case class Fact_Single(entity: Entity, prop: Prop)
+
+ sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
+ {
+ def cache(cache: Term.Cache): Fact =
+ Fact(prop.cache(cache), proof.map(cache.proof _))
+ }
+
+ def decode_fact(body: XML.Body): Fact =
+ {
+ val (prop, proof) =
+ {
+ import XML.Decode._
+ pair(decode_prop _, option(Term_XML.Decode.proof))(body)
+ }
+ Fact(prop, proof)
+ }
+
+ sealed case class Fact_Single(entity: Entity, fact: Fact)
{
def cache(cache: Term.Cache): Fact_Single =
- Fact_Single(entity.cache(cache), prop.cache(cache))
+ Fact_Single(entity.cache(cache), fact.cache(cache))
+
+ def prop: Prop = fact.prop
+ def proof: Option[Term.Proof] = fact.proof
}
- sealed case class Fact_Multi(entity: Entity, props: List[Prop])
+ sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
{
def cache(cache: Term.Cache): Fact_Multi =
- Fact_Multi(entity.cache(cache), props.map(_.cache(cache)))
+ Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
+
+ def props: List[Prop] = facts.map(_.prop)
def split: List[Fact_Single] =
- props match {
- case List(prop) => List(Fact_Single(entity, prop))
+ facts match {
+ case List(fact) => List(Fact_Single(entity, fact))
case _ =>
- for ((prop, i) <- props.zipWithIndex)
- yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
+ for ((fact, i) <- facts.zipWithIndex)
+ yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
}
}
@@ -334,17 +357,32 @@
{
val (entity, body) = decode_entity(Kind.AXIOM, tree)
val prop = decode_prop(body)
- Fact_Single(entity, prop)
+ Fact_Single(entity, Fact(prop, None))
})
def read_facts(provider: Export.Provider): List[Fact_Multi] =
provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.FACT, tree)
- val props = XML.Decode.list(decode_prop)(body)
- Fact_Multi(entity, props)
+ val facts = XML.Decode.list(decode_fact)(body)
+ Fact_Multi(entity, facts)
})
+ def read_proof(
+ provider: Export.Provider,
+ theory_name: String,
+ serial: Long,
+ cache: Option[Term.Cache] = None): (Term.Term, Term.Proof) =
+ {
+ val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
+ if (body.isEmpty) error("Bad proof export " + serial)
+ val (prop, proof) = XML.Decode.pair(Term_XML.Decode.term, Term_XML.Decode.proof)(body)
+ cache match {
+ case None => (prop, proof)
+ case Some(cache) => (cache.term(prop), cache.proof(proof))
+ }
+ }
+
/* type classes */
--- a/src/Pure/proofterm.ML Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/proofterm.ML Thu Aug 15 21:46:43 2019 +0200
@@ -11,7 +11,8 @@
type thm_node
type proof_serial = int
type thm_header =
- {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option}
+ {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+ prop: term, types: typ list option}
type thm_body
datatype proof =
MinProof
@@ -40,7 +41,8 @@
type oracle = string * term
val proof_of: proof_body -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
- val thm_header: proof_serial -> Position.T list -> string -> term -> typ list option -> thm_header
+ val thm_header: proof_serial -> Position.T list -> string -> string -> term -> typ list option ->
+ thm_header
val thm_body: proof_body -> thm_body
val thm_body_proof_raw: thm_body -> proof
val thm_body_proof_open: thm_body -> proof
@@ -67,6 +69,7 @@
val encode: proof XML.Encode.T
val encode_body: proof_body XML.Encode.T
+ val encode_full: proof XML.Encode.T
val decode: proof XML.Decode.T
val decode_body: proof_body XML.Decode.T
@@ -162,9 +165,8 @@
val prop_of: proof -> term
val expand_proof: theory -> (string * term option) list -> proof -> proof
- val standard_vars: Name.context -> term list * proof list -> term list * proof list
+ val standard_vars: Name.context -> term * proof option -> term * proof option
val standard_vars_term: Name.context -> term -> term
- val standard_vars_proof: Name.context -> proof -> proof
val proof_serial: unit -> proof_serial
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -185,7 +187,8 @@
type proof_serial = int;
type thm_header =
- {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option};
+ {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+ prop: term, types: typ list option};
datatype proof =
MinProof
@@ -217,8 +220,8 @@
fun map_proof_of f (PBody {oracles, thms, proof}) =
PBody {oracles = oracles, thms = thms, proof = f proof};
-fun thm_header serial pos name prop types : thm_header =
- {serial = serial, pos = pos, name = name, prop = prop, types = types};
+fun thm_header serial pos theory_name name prop types : thm_header =
+ {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
val no_export_proof = Lazy.value ();
@@ -379,8 +382,8 @@
fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
fn OfClass (a, b) => ([b], typ a),
fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
- fn PThm ({serial, pos, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
- ([int_atom serial, name],
+ fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+ ([int_atom serial, theory_name, name],
pair (list properties) (pair term (pair (option (list typ)) proof_body))
(map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
and proof_body (PBody {oracles, thms, proof = prf}) =
@@ -389,10 +392,25 @@
pair int (triple string term proof_body)
(a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
+fun full_proof prf = prf |> variant
+ [fn MinProof => ([], []),
+ fn PBound a => ([int_atom a], []),
+ fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)),
+ fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)),
+ fn a % SOME b => ([], pair full_proof term (a, b)),
+ fn a %% b => ([], pair full_proof full_proof (a, b)),
+ fn Hyp a => ([], term a),
+ fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
+ fn OfClass (T, c) => ([c], typ T),
+ fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
+ fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
+ ([int_atom serial, theory_name, name], list typ Ts)];
+
in
val encode = proof;
val encode_body = proof_body;
+val encode_full = full_proof;
end;
@@ -414,12 +432,12 @@
fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
fn ([b], a) => OfClass (typ a, b),
fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
- fn ([a, b], c) =>
+ fn ([a, b, c], d) =>
let
- val ((d, (e, (f, g)))) =
- pair (list properties) (pair term (pair (option (list typ)) proof_body)) c;
- val header = thm_header (int_atom a) (map Position.of_properties d) b e f;
- in PThm (header, thm_body g) end]
+ val ((e, (f, (g, h)))) =
+ pair (list properties) (pair term (pair (option (list typ)) proof_body)) d;
+ val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
+ in PThm (header, thm_body h) end]
and proof_body x =
let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
in PBody {oracles = a, thms = b, proof = c} end
@@ -493,8 +511,8 @@
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
| proof (OfClass T_c) = ofclass T_c
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
- | proof (PThm ({serial, pos, name, prop, types = SOME Ts}, thm_body)) =
- PThm (thm_header serial pos name prop (SOME (typs Ts)), thm_body)
+ | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
+ PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
| proof _ = raise Same.SAME;
in proof end;
@@ -533,8 +551,8 @@
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
- | change_types types (PThm ({serial, pos, name, prop, types = _}, thm_body)) =
- PThm (thm_header serial pos name prop types, thm_body)
+ | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
+ PThm (thm_header serial pos theory_name name prop types, thm_body)
| change_types _ prf = prf;
@@ -681,8 +699,9 @@
OfClass (htypeT Envir.norm_type_same T, c)
| norm (Oracle (s, prop, Ts)) =
Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
- | norm (PThm ({serial = i, pos = p, name = a, prop = t, types = Ts}, thm_body)) =
- PThm (thm_header i p a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
+ | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
+ PThm (thm_header i p theory_name a t
+ (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
| norm _ = raise Same.SAME;
in Same.commit norm end;
@@ -998,9 +1017,9 @@
OfClass (Logic.incr_tvar_same inc T, c)
| lift' _ _ (Oracle (s, prop, Ts)) =
Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
- | lift' _ _ (PThm ({serial = i, pos = p, name = s, prop, types = Ts}, thm_body)) =
- PThm (thm_header i p s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
- thm_body)
+ | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
+ PThm (thm_header i p theory_name s prop
+ ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
| lift' _ _ _ = raise Same.SAME
and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
@@ -1429,8 +1448,8 @@
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
- | subst _ _ (PThm ({serial = i, pos = p, name = id, prop, types}, thm_body)) =
- PThm (thm_header i p id prop (Same.map_option substTs types), thm_body)
+ | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
+ PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
| subst _ _ _ = raise Same.SAME;
in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -2023,31 +2042,43 @@
| variant_proof bs (Hyp t) = Hyp (variant_term bs t)
| variant_proof _ prf = prf;
+val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
+fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
+val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
+
+val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
+val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
+val unvarify_proof = map_proof_terms unvarify unvarifyT;
+
+fun hidden_types prop proof =
+ let
+ val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
+ val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
+ in rev (fold_proof_terms (fold_types add_hiddenT) add_hiddenT proof []) end;
+
+fun standard_hidden_types term proof =
+ let
+ val hidden = hidden_types term proof;
+ val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1;
+ fun smash T = if member (op =) hidden T then TVar (("'", idx), Type.sort_of_atyp T) else T;
+ val smashT = map_atyps smash;
+ in map_proof_terms (map_types smashT) smashT proof end;
+
in
-fun standard_vars used (terms, proofs) =
+fun standard_vars used (term, opt_proof) =
let
- val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
- val inst = Term_Subst.zero_var_indexes_inst used (terms @ proof_terms);
+ val proofs = the_list (Option.map (standard_hidden_types term) opt_proof);
+ val proof_terms = rev (fold (fold_proof_terms cons (cons o Logic.mk_type)) proofs []);
+ val used_frees = used
+ |> used_frees_term term
+ |> fold used_frees_proof proofs;
+ val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
+ val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
+ val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
+ in (term', try hd proofs') end;
- val is_used = Name.is_declared used o Name.clean;
- fun unvarifyT ty = ty |> Term.map_atyps
- (fn TVar ((a, _), S) => TFree (a, S)
- | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
- | T => T);
- fun unvarify tm = tm |> Term.map_aterms
- (fn Var ((x, _), T) => Free (x, T)
- | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
- | t => t);
-
- val terms' = terms
- |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> variant_term []);
- val proofs' = proofs
- |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
- in (terms', proofs') end;
-
-fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
-fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
+fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
end;
@@ -2076,37 +2107,14 @@
fun clean_proof thy = rew_proof thy #> shrink_proof;
-
-local open XML.Encode Term_XML.Encode in
-
-fun proof prf = prf |> variant
- [fn MinProof => ([], []),
- fn PBound a => ([int_atom a], []),
- fn Abst (a, SOME b, c) => ([a], pair typ proof (b, c)),
- fn AbsP (a, SOME b, c) => ([a], pair term proof (b, c)),
- fn a % SOME b => ([], pair proof term (a, b)),
- fn a %% b => ([], pair proof proof (a, b)),
- fn Hyp a => ([], term a),
- fn PAxm (name, b, SOME Ts) => ([name], list typ Ts),
- fn OfClass (T, c) => ([c], typ T),
- fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
- fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
-
-fun encode_export prop prf = pair term proof (prop, prf);
-
-
-val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
-fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
-val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
-
-end;
+fun encode_export prop prf =
+ let open XML.Encode Term_XML.Encode
+ in pair term encode_full (prop, prf) end;
fun export_proof thy i prop prf =
let
- val free_names = Name.context
- |> used_frees_term prop
- |> used_frees_proof prf;
- val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
+ val (prop', SOME prf') =
+ standard_vars Name.context (prop, SOME (reconstruct_proof thy prop prf));
val xml = encode_export prop' prf';
val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
in
@@ -2188,7 +2196,8 @@
val pthm = (i, make_thm_node name prop1 body');
- val header = thm_header i ([pos, Position.thread_data ()]) name prop1 NONE;
+ val header =
+ thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
val head = PThm (header, thm_body);
val proof =
--- a/src/Pure/term.scala Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/term.scala Thu Aug 15 21:46:43 2019 +0200
@@ -13,7 +13,22 @@
{
/* types and terms */
- type Indexname = (String, Int)
+ sealed case class Indexname(name: String, index: Int)
+ {
+ override def toString: String =
+ if (index == -1) name
+ else {
+ val dot =
+ Symbol.explode(name).reverse match {
+ case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
+ case c :: _ => Symbol.is_digit(c)
+ case _ => true
+ }
+ if (dot) "?" + name + "." + index
+ else if (index != 0) "?" + name + index
+ else "?" + name
+ }
+ }
type Sort = List[String]
val dummyS: Sort = List("")
@@ -32,6 +47,20 @@
case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
case class App(fun: Term, arg: Term) extends Term
+ sealed abstract class Proof
+ case object MinProof extends Proof
+ case class PBound(index: Int) extends Proof
+ case class Abst(name: String, typ: Typ, body: Proof) extends Proof
+ case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
+ case class Appt(fun: Proof, arg: Term) extends Proof
+ case class AppP(fun: Proof, arg: Proof) extends Proof
+ case class Hyp(hyp: Term) extends Proof
+ case class PAxm(name: String, types: List[Typ]) extends Proof
+ case class OfClass(typ: Typ, cls: String) extends Proof
+ case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
+ case class PThm(serial: Long, theory_name: String, pseudo_name: String, types: List[Typ])
+ extends Proof
+
/* Pure logic */
@@ -87,7 +116,7 @@
extends isabelle.Cache(initial_size, max_string)
{
protected def cache_indexname(x: Indexname): Indexname =
- lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
+ lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
protected def cache_sort(x: Sort): Sort =
if (x == dummyS) dummyS
@@ -101,13 +130,24 @@
case Some(y) => y
case None =>
x match {
- case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
+ case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
}
}
}
+ protected def cache_typs(x: List[Typ]): List[Typ] =
+ {
+ if (x.isEmpty) Nil
+ else {
+ lookup(x) match {
+ case Some(y) => y
+ case None => store(x.map(cache_typ(_)))
+ }
+ }
+ }
+
protected def cache_term(x: Term): Term =
{
lookup(x) match {
@@ -117,7 +157,7 @@
case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
- case Bound(index) => store(Bound(cache_int(index)))
+ case Bound(_) => store(x)
case Abs(name, typ, body) =>
store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
@@ -125,11 +165,39 @@
}
}
+ protected def cache_proof(x: Proof): Proof =
+ {
+ if (x == MinProof) MinProof
+ else {
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ x match {
+ case PBound(_) => store(x)
+ case Abst(name, typ, body) =>
+ store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
+ case AbsP(name, hyp, body) =>
+ store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
+ case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
+ case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
+ case Hyp(hyp) => store(Hyp(cache_term(hyp)))
+ case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
+ case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
+ case Oracle(name, prop, types) =>
+ store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
+ case PThm(serial, theory_name, name, types) =>
+ store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
+ }
+ }
+ }
+ }
+
// main methods
def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
def sort(x: Sort): Sort = synchronized { cache_sort(x) }
def typ(x: Typ): Typ = synchronized { cache_typ(x) }
def term(x: Term): Term = synchronized { cache_term(x) }
+ def proof(x: Proof): Proof = synchronized { cache_proof(x) }
def position(x: Position.T): Position.T =
synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
--- a/src/Pure/term_xml.scala Thu Aug 15 16:11:56 2019 +0100
+++ b/src/Pure/term_xml.scala Thu Aug 15 21:46:43 2019 +0200
@@ -21,13 +21,13 @@
variant[Typ](List(
{ case Type(a, b) => (List(a), list(typ)(b)) },
{ case TFree(a, b) => (List(a), sort(b)) },
- { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
+ { case TVar(Indexname(a, b), c) => (List(a, int_atom(b)), sort(c)) }))
def term: T[Term] =
variant[Term](List(
{ case Const(a, b) => (List(a), typ(b)) },
{ case Free(a, b) => (List(a), typ(b)) },
- { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
+ { case Var(Indexname(a, b), c) => (List(a, int_atom(b)), typ(c)) },
{ case Bound(a) => (List(int_atom(a)), Nil) },
{ case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
{ case App(a, b) => (Nil, pair(term, term)(a, b)) }))
@@ -43,15 +43,29 @@
variant[Typ](List(
{ case (List(a), b) => Type(a, list(typ)(b)) },
{ case (List(a), b) => TFree(a, sort(b)) },
- { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
+ { case (List(a, b), c) => TVar(Indexname(a, int_atom(b)), sort(c)) }))
def term: T[Term] =
variant[Term](List(
{ case (List(a), b) => Const(a, typ(b)) },
{ case (List(a), b) => Free(a, typ(b)) },
- { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
+ { case (List(a, b), c) => Var(Indexname(a, int_atom(b)), typ(c)) },
{ case (List(a), Nil) => Bound(int_atom(a)) },
{ case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
{ case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+
+ def proof: T[Proof] =
+ variant[Proof](List(
+ { case (Nil, Nil) => MinProof },
+ { case (List(a), Nil) => PBound(int_atom(a)) },
+ { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
+ { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
+ { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
+ { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
+ { case (Nil, a) => Hyp(term(a)) },
+ { case (List(a), b) => PAxm(a, list(typ)(b)) },
+ { case (List(a), b) => OfClass(typ(b), a) },
+ { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
+ { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
}
}