From b8282b771eac788079812286dd55baef4457e6d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 12 May 2023 20:04:44 +0200 Subject: [PATCH] Cleanup --- Isabelle_DOF-Proofs/Reification_Test.thy | 16 +-- Isabelle_DOF-Proofs/Very_Deep_DOF.thy | 1 - .../Very_Deep_Interpretation.thy | 109 ++---------------- Isabelle_DOF/thys/Isa_DOF.thy | 23 ---- 4 files changed, 20 insertions(+), 129 deletions(-) diff --git a/Isabelle_DOF-Proofs/Reification_Test.thy b/Isabelle_DOF-Proofs/Reification_Test.thy index f408729..768748e 100644 --- a/Isabelle_DOF-Proofs/Reification_Test.thy +++ b/Isabelle_DOF-Proofs/Reification_Test.thy @@ -4,10 +4,10 @@ theory Reification_Test begin ML\ -val ty1 = ISA_core.reify_typ @{typ "int"} -val ty2 = ISA_core.reify_typ @{typ "int \ bool"} -val ty3 = ISA_core.reify_typ @{typ "prop"} -val ty4 = ISA_core.reify_typ @{typ "'a list"} +val ty1 = Meta_ISA_core.reify_typ @{typ "int"} +val ty2 = Meta_ISA_core.reify_typ @{typ "int \ bool"} +val ty3 = Meta_ISA_core.reify_typ @{typ "prop"} +val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"} \ term*\@{typ \int\}\ @@ -19,9 +19,9 @@ term*\@{typ \'a list\}\ value*\@{typ \'a list\}\ ML\ -val t1 = ISA_core.reify_term @{term "1::int"} -val t2 = ISA_core.reify_term @{term "\x. x = 1"} -val t3 = ISA_core.reify_term @{term "[2, 3::int]"} +val t1 = Meta_ISA_core.reify_term @{term "1::int"} +val t2 = Meta_ISA_core.reify_term @{term "\x. x = 1"} +val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"} \ term*\@{term \1::int\}\ value*\@{term \1::int\}\ @@ -45,7 +45,7 @@ value*\@{thms-of \HOL.refl\}\ ML\ val t_schematic = TVar(("'a",0), []) val t = @{term "Tv (Var (STR '''a'', 0)) {}"} -val rt_schematic = ISA_core.reify_typ t_schematic +val rt_schematic = Meta_ISA_core.reify_typ t_schematic val true = rt_schematic = t \ diff --git a/Isabelle_DOF-Proofs/Very_Deep_DOF.thy b/Isabelle_DOF-Proofs/Very_Deep_DOF.thy index 7369005..74e9dcb 100644 --- a/Isabelle_DOF-Proofs/Very_Deep_DOF.thy +++ b/Isabelle_DOF-Proofs/Very_Deep_DOF.thy @@ -15,6 +15,5 @@ term "@{term \\x. P x \ Q\}" term "@{thm \refl\}" term "@{docitem \doc_ref\}" ML\ @{term "@{docitem \doc_ref\}"}\ -(**) end \ No newline at end of file diff --git a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy index 2d1e9ea..51ff20a 100644 --- a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy +++ b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy @@ -32,89 +32,9 @@ consts Isabelle_DOF_trace_attribute :: "string \ (string * string) l subsection\ Semantics \ ML\ -structure ISA_core = +structure Meta_ISA_core = struct -fun check_path check_file ctxt dir (name, pos) = - let - val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be - "lifted" to - type source *) - - val path = Path.append dir (Path.explode name) handle ERROR msg => ISA_core.err msg pos; - val _ = Path.expand path handle ERROR msg => ISA_core.err msg pos; - val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); - val _ = - (case check_file of - NONE => path - | SOME check => (check path handle ERROR msg => ISA_core.err msg pos)); - in path end; - - -fun ML_isa_antiq check_file thy (name, _, pos) = - let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos); - in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end; - - -fun ML_isa_check_generic check thy (term, pos) = - let val name = (HOLogic.dest_string term - handle TERM(_,[t]) => error ("wrong term format: must be string constant: " - ^ Syntax.string_of_term_global thy t )) - val _ = check thy (name,pos) - in SOME term end; - -fun check_identity _ (term, _, _) _ = SOME term - -fun ML_isa_check_typ thy (term, _, pos) _ = - let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) - in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end - in ML_isa_check_generic check thy (term, pos) end - - -fun ML_isa_check_term thy (term, _, pos) _ = - let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) - in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end - in ML_isa_check_generic check thy (term, pos) end - - -fun ML_isa_check_thm thy (term, _, pos) _ = - (* this works for long-names only *) - let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of - NONE => ISA_core.err ("No Theorem:" ^name) pos - | SOME X => X - in ML_isa_check_generic check thy (term, pos) end - - -fun ML_isa_check_file thy (term, _, pos) _ = - let fun check thy (name, pos) = check_path (SOME File.check_file) - (Proof_Context.init_global thy) - (Path.current) - (name, pos); - in ML_isa_check_generic check thy (term, pos) end; - -fun ML_isa_id thy (term,pos) = SOME term - - -fun ML_isa_check_docitem thy (term, req_ty, pos) _ = - let fun check thy (name, _) s = - let val DOF_core.Instance {cid,...} = - DOF_core.get_instance_global name thy - val ns = DOF_core.get_instances (Proof_Context.init_global thy) - |> Name_Space.space_of_table - val {pos=pos', ...} = Name_Space.the_entry ns name - val ctxt = (Proof_Context.init_global thy) - val req_class = case req_ty of - \<^Type>\fun _ T\ => DOF_core.typ_to_cid T - | _ => error("can not infer type for: "^ name) - in if cid <> DOF_core.default_cid - andalso not(DOF_core.is_subclass ctxt cid req_class) - then error("reference ontologically inconsistent: " - ^cid^" vs. "^req_class^ Position.here pos') - else () - end - in ML_isa_check_generic check thy (term, pos) end - - fun ML_isa_check_trace_attribute thy (term, _, pos) s = let val oid = (HOLogic.dest_string term @@ -123,11 +43,6 @@ fun ML_isa_check_trace_attribute thy (term, _, pos) s = val _ = DOF_core.get_instance_global oid thy in SOME term end -fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ = - case term_option of - NONE => error("Wrong term option. You must use a defined term") - | SOME term => Const (isa_name, ty) $ term - fun reify_typ (Type (s, typ_list)) = \<^Const>\Ty\ $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\typ\ (map reify_typ typ_list) | reify_typ (TFree (name, sort)) = @@ -273,16 +188,16 @@ end; (* struct *) \ ML\ -val ty1 = ISA_core.reify_typ @{typ "int"} -val ty2 = ISA_core.reify_typ @{typ "int \ bool"} -val ty3 = ISA_core.reify_typ @{typ "prop"} -val ty4 = ISA_core.reify_typ @{typ "'a list"} +val ty1 = Meta_ISA_core.reify_typ @{typ "int"} +val ty2 = Meta_ISA_core.reify_typ @{typ "int \ bool"} +val ty3 = Meta_ISA_core.reify_typ @{typ "prop"} +val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"} \ ML\ -val t1 = ISA_core.reify_term @{term "1::int"} -val t2 = ISA_core.reify_term @{term "\x. x = 1"} -val t3 = ISA_core.reify_term @{term "[2, 3::int]"} +val t1 = Meta_ISA_core.reify_term @{term "1::int"} +val t2 = Meta_ISA_core.reify_term @{term "\x. x = 1"} +val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"} \ subsection\ Isar - Setup\ @@ -290,8 +205,8 @@ subsection\ Isar - Setup\ They must be declared in the same theory file as the one of the declaration of Isabelle_DOF term anti-quotations !!! *) setup\ -[(\<^type_name>\thm\, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thm) - , (\<^type_name>\thms_of\, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thms_of) +[(\<^type_name>\thm\, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thm) + , (\<^type_name>\thms_of\, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thms_of) , (\<^type_name>\file\, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)] |> fold (fn (n, check, elaborate) => fn thy => let val ns = Sign.tsig_of thy |> Type.type_space @@ -304,8 +219,8 @@ let val ns = Sign.tsig_of thy |> Type.type_space in DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy end) #> -([(\<^const_name>\Isabelle_DOF_typ\, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ) - ,(\<^const_name>\Isabelle_DOF_term\, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term) +([(\<^const_name>\Isabelle_DOF_typ\, ISA_core.ML_isa_check_typ, Meta_ISA_core.ML_isa_elaborate_typ) + ,(\<^const_name>\Isabelle_DOF_term\, ISA_core.ML_isa_check_term, Meta_ISA_core.ML_isa_elaborate_term) ,(\<^const_name>\Isabelle_DOF_docitem\, ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic) ,(\<^const_name>\Isabelle_DOF_trace_attribute\, diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index cf2f4a5..ccb4774 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -670,8 +670,6 @@ fun typ_to_cid (Type(s,[\<^Type>\unit\])) = Long_Name.qualifier s |typ_to_cid _ = error("type is not an ontological type.") -val SPY = Unsynchronized.ref(Bound 0) - fun check_regexps term = let val _ = case fold_aterms Term.add_free_names term [] of n::_ => error("No free variables allowed in monitor regexp:" ^ n) @@ -1064,27 +1062,6 @@ struct fun err msg pos = error (msg ^ Position.here pos); fun warn msg pos = warning (msg ^ Position.here pos); -fun check_path check_file ctxt dir (name, pos) = - let - val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be - "lifted" to - type source *) - - val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos; - val _ = Path.expand path handle ERROR msg => err msg pos; - val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); - val _ = - (case check_file of - NONE => path - | SOME check => (check path handle ERROR msg => err msg pos)); - in path end; - - -fun ML_isa_antiq check_file thy (name, _, pos) = - let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos); - in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end; - - fun ML_isa_check_generic check thy (term, pos) = let val name = (HOLogic.dest_string term handle TERM(_,[t]) => error ("wrong term format: must be string constant: "