Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Cleanup
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2023-05-12 20:04:44 +02:00
parent 1cfc4ac88a
commit b8282b771e
4 changed files with 20 additions and 129 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
Isabelle_DOF-Proofs/Reification_Test.thy
View File

@ -4,10 +4,10 @@ theory Reification_Test
begin begin
ML\<open> ML\<open>
val ty1 = ISA_core.reify_typ @{typ "int"} val ty1 = Meta_ISA_core.reify_typ @{typ "int"}
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"} val ty2 = Meta_ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = ISA_core.reify_typ @{typ "prop"} val ty3 = Meta_ISA_core.reify_typ @{typ "prop"}
val ty4 = ISA_core.reify_typ @{typ "'a list"} val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"}
\<close> \<close>
term*\<open>@{typ \<open>int\<close>}\<close> term*\<open>@{typ \<open>int\<close>}\<close>
@ -19,9 +19,9 @@ term*\<open>@{typ \<open>'a list\<close>}\<close>
value*\<open>@{typ \<open>'a list\<close>}\<close> value*\<open>@{typ \<open>'a list\<close>}\<close>
ML\<open> ML\<open>
val t1 = ISA_core.reify_term @{term "1::int"} val t1 = Meta_ISA_core.reify_term @{term "1::int"}
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"} val t2 = Meta_ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = ISA_core.reify_term @{term "[2, 3::int]"} val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"}
\<close> \<close>
term*\<open>@{term \<open>1::int\<close>}\<close> term*\<open>@{term \<open>1::int\<close>}\<close>
value*\<open>@{term \<open>1::int\<close>}\<close> value*\<open>@{term \<open>1::int\<close>}\<close>
@ -45,7 +45,7 @@ value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
ML\<open> ML\<open>
val t_schematic = TVar(("'a",0), []) val t_schematic = TVar(("'a",0), [])
val t = @{term "Tv (Var (STR '''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 val true = rt_schematic = t
\<close> \<close>

1
Isabelle_DOF-Proofs/Very_Deep_DOF.thy
View File

@ -15,6 +15,5 @@ term "@{term \<open>\<forall>x. P x \<longrightarrow> Q\<close>}"
term "@{thm \<open>refl\<close>}" term "@{thm \<open>refl\<close>}"
term "@{docitem \<open>doc_ref\<close>}" term "@{docitem \<open>doc_ref\<close>}"
ML\<open> @{term "@{docitem \<open>doc_ref\<close>}"}\<close> ML\<open> @{term "@{docitem \<open>doc_ref\<close>}"}\<close>
(**)
end end

109
Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
View File

@ -32,89 +32,9 @@ consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) l
subsection\<open> Semantics \<close> subsection\<open> Semantics \<close>
ML\<open> ML\<open>
structure ISA_core = structure Meta_ISA_core =
struct 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>\<open>fun _ T\<close> => 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 = fun ML_isa_check_trace_attribute thy (term, _, pos) s =
let let
val oid = (HOLogic.dest_string term 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 val _ = DOF_core.get_instance_global oid thy
in SOME term end 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)) = fun reify_typ (Type (s, typ_list)) =
\<^Const>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list) \<^Const>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list)
| reify_typ (TFree (name, sort)) = | reify_typ (TFree (name, sort)) =
@ -273,16 +188,16 @@ end; (* struct *)
\<close> \<close>
ML\<open> ML\<open>
val ty1 = ISA_core.reify_typ @{typ "int"} val ty1 = Meta_ISA_core.reify_typ @{typ "int"}
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"} val ty2 = Meta_ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = ISA_core.reify_typ @{typ "prop"} val ty3 = Meta_ISA_core.reify_typ @{typ "prop"}
val ty4 = ISA_core.reify_typ @{typ "'a list"} val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"}
\<close> \<close>
ML\<open> ML\<open>
val t1 = ISA_core.reify_term @{term "1::int"} val t1 = Meta_ISA_core.reify_term @{term "1::int"}
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"} val t2 = Meta_ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = ISA_core.reify_term @{term "[2, 3::int]"} val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"}
\<close> \<close>
subsection\<open> Isar - Setup\<close> subsection\<open> Isar - Setup\<close>
@ -290,8 +205,8 @@ subsection\<open> Isar - Setup\<close>
They must be declared in the same theory file as the one of the declaration They must be declared in the same theory file as the one of the declaration
of Isabelle_DOF term anti-quotations !!! *) of Isabelle_DOF term anti-quotations !!! *)
setup\<open> setup\<open>
[(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thm) [(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thm)
, (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thms_of) , (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thms_of)
, (\<^type_name>\<open>file\<close>, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)] , (\<^type_name>\<open>file\<close>, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)]
|> fold (fn (n, check, elaborate) => fn thy => |> fold (fn (n, check, elaborate) => fn thy =>
let val ns = Sign.tsig_of thy |> Type.type_space 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 in DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy
end) end)
#> #>
([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ) ([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, Meta_ISA_core.ML_isa_elaborate_typ)
,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term) ,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, Meta_ISA_core.ML_isa_elaborate_term)
,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>, ,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic) ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>, ,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,

23
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -670,8 +670,6 @@ fun typ_to_cid (Type(s,[\<^Type>\<open>unit\<close>])) = Long_Name.qualifier s
|typ_to_cid _ = error("type is not an ontological type.") |typ_to_cid _ = error("type is not an ontological type.")
val SPY = Unsynchronized.ref(Bound 0)
fun check_regexps term = fun check_regexps term =
let val _ = case fold_aterms Term.add_free_names term [] of let val _ = case fold_aterms Term.add_free_names term [] of
n::_ => error("No free variables allowed in monitor regexp:" ^ n) 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 err msg pos = error (msg ^ Position.here pos);
fun warn msg pos = warning (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) = fun ML_isa_check_generic check thy (term, pos) =
let val name = (HOLogic.dest_string term let val name = (HOLogic.dest_string term
handle TERM(_,[t]) => error ("wrong term format: must be string constant: " handle TERM(_,[t]) => error ("wrong term format: must be string constant: "