# HG changeset patch # User wenzelm # Date 1565898403 -7200 # Node ID 011196c029e155da26dcd8d978cc5b45fd79b656 # Parent fcf3b891ccb14f011eee31bdb34aff209c9dafc6# Parent f3fbc7f3559d3d73153d532d30874366ef158c90 merged diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/General/cache.scala --- 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) } } diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/PIDE/document.scala --- 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 diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/Proof/extraction.ML --- 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 diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/Thy/export.scala --- 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 } diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/Thy/export_theory.ML --- 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 _ = diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/Thy/export_theory.scala --- 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 */ diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/proofterm.ML --- 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 = diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/term.scala --- 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)) }) } diff -r fcf3b891ccb1 -r 011196c029e1 src/Pure/term_xml.scala --- 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)) })) } }