Remove obsolete termrepr term anti-quotation
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
- Also some clean-up
This commit is contained in:
Nicolas Méric
parent
826fc489b7
commit
4bd31be71d
|
|
@ -21,7 +21,6 @@ no_notation "Isabelle_DOF_trace_attribute" ("@{trace-attribute _}")
|
|||
|
||||
consts Isabelle_DOF_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
||||
consts Isabelle_DOF_term :: "string \<Rightarrow> term" ("@{term _}")
|
||||
consts Isabelle_DOF_term_repr :: "string \<Rightarrow> term" ("@{termrepr _}")
|
||||
datatype "thm" = Isabelle_DOF_thm string ("@{thm _}") | Thm_content ("proof":proofterm)
|
||||
datatype "thms_of" = Isabelle_DOF_thms_of string ("@{thms-of _}")
|
||||
datatype "file" = Isabelle_DOF_file string ("@{file _}")
|
||||
|
|
@ -269,13 +268,6 @@ case term_option of
|
|||
val traces' = map conv (HOLogic.dest_list traces)
|
||||
in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end
|
||||
|
||||
(* utilities *)
|
||||
|
||||
fun property_list_dest ctxt X =
|
||||
map (fn \<^Const_>\<open>Isabelle_DOF_term for s\<close> => HOLogic.dest_string s
|
||||
|\<^Const_>\<open>Isabelle_DOF_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
|
||||
(HOLogic.dest_list X)
|
||||
|
||||
end; (* struct *)
|
||||
|
||||
\<close>
|
||||
|
|
@ -314,7 +306,6 @@ 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_term\<close>, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_term_repr\<close>, ISA_core.check_identity, ISA_core.ML_isa_elaborate_generic)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
|
||||
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,
|
||||
|
|
|
|||
|
|
@ -39,39 +39,17 @@ text\<open>For now, as the term annotation is not bound to a meta logic which wi
|
|||
in the assertion.
|
||||
\<close>
|
||||
|
||||
(* does not work in batch mode ...
|
||||
(* sample for accessing a property filled with previous assert's of "aa" *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};\<close>
|
||||
|
||||
|
||||
|
||||
assert*[aa::F] " X \<and> Y \<longrightarrow> True" (*example with uni-code *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};
|
||||
app writeln (tl (rev it));\<close>
|
||||
|
||||
|
||||
|
||||
assert*[aa::F] "\<forall>x::bool. X \<and> Y \<longrightarrow> True" (*problem with uni-code *)
|
||||
*)
|
||||
ML\<open>
|
||||
Syntax.read_term_global @{theory} "[@{termrepr ''True @<longrightarrow> True''}]";
|
||||
(* this only works because the isa check is not activated in "term" !!! *)
|
||||
@{term "[@{term '' True @<longrightarrow> True ''}]"}; (* with isa-check *)
|
||||
@{term "[@{termrepr '' True @<longrightarrow> True ''}]"}; (* without isa check *)
|
||||
\<close>
|
||||
(*
|
||||
ML\<open>val [_,_,Const _ $ s,_] = (HOLogic.dest_list @{docitem_attribute property :: aa});
|
||||
val t = HOLogic.dest_string s;
|
||||
holstring_to_bstring @{context} t
|
||||
\<close>
|
||||
*)
|
||||
|
||||
lemma "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops
|
||||
|
||||
|
||||
text\<open>An example for the ontology specification character of the short-cuts such as
|
||||
@{command "assert*"}: in the following, we use the same notation referring to a completely
|
||||
different class. "F" and "assertion" have only in common that they posses the attribute
|
||||
\<^verbatim>\<open>property\<close>: \<close>
|
||||
@{const [names_short] \<open>properties\<close>}: \<close>
|
||||
|
||||
text\<open>Creation just like that: \<close>
|
||||
assert*[ababa::assertion] "3 < (4::int)"
|
||||
|
|
|
|||
|
|
@ -10,18 +10,18 @@ imports
|
|||
TestKit
|
||||
begin
|
||||
|
||||
(*
|
||||
|
||||
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
|
||||
|
||||
ML*[thefunction::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
|
||||
val t = \<^value_>\<open>x @{B \<open>thefunction\<close>}\<close>\<close>
|
||||
ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the
|
||||
resulting toplevel state is preserved.\<close>
|
||||
text-macro*[the::C]\<open> @{B [display] "thefunction"} \<close>
|
||||
text*[the::C]\<open> @{B "thefunction"} \<close>
|
||||
|
||||
text\<open>... and here we reference @{B \<open>thefunction\<close>}.\<close>
|
||||
|
||||
text\<open>... and here we reference @{B [display] \<open>thefunction\<close>}.\<close>
|
||||
|
||||
*)
|
||||
|
||||
section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
|
||||
|
||||
|
|
@ -36,13 +36,6 @@ Some built-ins remain as unspecified constants:
|
|||
\<^item> the docitem TA offers a way to check the reference of class instances
|
||||
without checking the instances type.
|
||||
It must be avoided for certification
|
||||
\<^item> the termrepr TA is left as unspecified constant for now.
|
||||
A major refactoring of code should be done to enable
|
||||
referential equivalence for termrepr, by changing the dependency
|
||||
between the Isa-DOF theory and the Assert theory.
|
||||
The assert-cmd function in Assert should use the value* command
|
||||
functions, which make the elaboration of the term
|
||||
referenced by the TA before passing it to the evaluator
|
||||
|
||||
We also have the possibility to make some requests on classes instances, i.e. on docitems
|
||||
by specifying the doc class.
|
||||
|
|
@ -116,13 +109,13 @@ used in the \<open>b\<close> attribute will be checked, and the type of these cl
|
|||
\<close>
|
||||
value* \<open>@{F \<open>xcv4\<close>}\<close>
|
||||
|
||||
(*
|
||||
|
||||
text\<open>If we want the classes to be checked,
|
||||
we can use the TA which will also check the type of the instances.
|
||||
The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:
|
||||
\<close>
|
||||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
|
||||
*)
|
||||
|
||||
text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
|
||||
value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
|
||||
value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
|
||||
|
|
@ -189,12 +182,12 @@ It uses the same implementation as the \<^emph>\<open>value*\<close>-command and
|
|||
|
||||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
|
||||
we can check logical statements:\<close>
|
||||
(*
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
|
||||
= authored_by @{introduction \<open>introduction4\<close>})\<close>
|
||||
*)
|
||||
|
||||
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{Introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Introduction \<open>introduction4\<close>})\<close>
|
||||
|
||||
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
||||
(* Error:
|
||||
assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
|
||||
|
|
@ -202,19 +195,19 @@ assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
|
|||
text\<open>Assertions must be true, hence the error:\<close>
|
||||
(* Error:
|
||||
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
|
||||
(*
|
||||
|
||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close>
|
||||
text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
|
||||
text*[assertionAA::A]\<open>@{A "assertionA"}\<close>
|
||||
text\<open>... and here we reference @{A \<open>assertionA\<close>}.\<close>
|
||||
|
||||
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
*)
|
||||
|
||||
text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>
|
||||
value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
|
||||
(*
|
||||
|
||||
assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
|
||||
\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -93,49 +93,6 @@ val docclass_markup = docref_markup_gen docclassN
|
|||
|
||||
\<close>
|
||||
|
||||
section\<open> Utilities\<close>
|
||||
|
||||
ML\<open>
|
||||
fun spy x y = (writeln (x ^ y); y)
|
||||
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
|
||||
(* a hacky, but save encoding of unicode comming from the interface to the string format
|
||||
that can be parsed by the inner-syntax string parser ''dfdf''. *)
|
||||
fun bstring_to_holstring ctxt x (* (x:bstring) *) : string =
|
||||
let val term = Syntax.parse_term ctxt (markup2string x)
|
||||
fun hpp x = if x = #"\\" then "@" else
|
||||
if x = #"@" then "@@" else String.implode [x]
|
||||
in term |> Sledgehammer_Util.hackish_string_of_term ctxt
|
||||
|> map hpp o String.explode |> String.concat
|
||||
end;
|
||||
|
||||
|
||||
fun chopper p (x:string) =
|
||||
let fun hss buff [] = rev buff
|
||||
|hss buff (S as a::R) = if p a then let val (front,rest) = chop_prefix p S
|
||||
in hss (String.implode front :: buff) rest end
|
||||
else let val (front,rest) = chop_prefix (not o p) S
|
||||
in hss (String.implode front ::buff) rest end
|
||||
in hss [] (String.explode x) end;
|
||||
|
||||
|
||||
fun holstring_to_bstring ctxt (x:string) : bstring =
|
||||
let fun collapse "" = ""
|
||||
|collapse S = if String.sub(S,0) = #"@"
|
||||
then let val n = String.size S
|
||||
val front = replicate (n div 2) #"@"
|
||||
val back = if (n mod 2)=1 then [#"\\"] else []
|
||||
in String.implode (front @ back) end
|
||||
else S;
|
||||
val t = String.concat (map collapse (chopper (fn x => x = #"@") x));
|
||||
in t |> Syntax.string_of_term ctxt o Syntax.parse_term ctxt end;
|
||||
|
||||
fun fold_and [] = true
|
||||
| fold_and (x::xs) = x andalso (fold_and xs)
|
||||
|
||||
\<close>
|
||||
|
||||
section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
|
||||
|
||||
|
||||
|
|
@ -618,7 +575,14 @@ struct
|
|||
|
||||
val the_closing_ml_invariant = the_invariant snd
|
||||
|
||||
|
||||
(* Monitor infos are not integrated to an instance datatype
|
||||
to avoid issues when comparing objects.
|
||||
Indeed automatas do not have an equality type and then,
|
||||
should two instances with monitor infos be compared, an error will be triggered.
|
||||
So monitor infos are defined in their own name space.
|
||||
They are declared when opening a monitor and have the same
|
||||
reference (the key of the name space table) as their related monitor instance:
|
||||
the name of the instance prefixed by the theory. *)
|
||||
datatype monitor_info = Monitor_Info of
|
||||
{accepted_cids : RegExpInterface.env,
|
||||
rejected_cids : RegExpInterface.env,
|
||||
|
|
@ -868,7 +832,7 @@ fun check_invs get_ml_invs cid_long oid is_monitor thy =
|
|||
|> map (fn (_, inv) => let val ML_Invariant check = inv
|
||||
in check |> #check end)
|
||||
|> map (fn check => check oid is_monitor ctxt)
|
||||
in (fold_and checks) end)
|
||||
in (List.all I checks) end)
|
||||
|
||||
val check_ml_invs = check_invs get_ml_invariants
|
||||
|
||||
|
|
@ -995,7 +959,6 @@ datatype "doc_class" = mk string
|
|||
|
||||
datatype "typ" = Isabelle_DOF_typ string ("@{typ _}")
|
||||
datatype "term" = Isabelle_DOF_term string ("@{term _}")
|
||||
consts Isabelle_DOF_term_repr :: "string \<Rightarrow> term" ("@{termrepr _}")
|
||||
datatype "thm" = Isabelle_DOF_thm string ("@{thm _}")
|
||||
datatype "file" = Isabelle_DOF_file string ("@{file _}")
|
||||
datatype "thy" = Isabelle_DOF_thy string ("@{thy _}")
|
||||
|
|
@ -1325,13 +1288,6 @@ case term_option of
|
|||
val traces' = map conv (HOLogic.dest_list traces)
|
||||
in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end
|
||||
|
||||
(* utilities *)
|
||||
|
||||
fun property_list_dest ctxt X =
|
||||
map (fn \<^Const_>\<open>Isabelle_DOF_term for s\<close> => HOLogic.dest_string s
|
||||
|\<^Const_>\<open>Isabelle_DOF_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
|
||||
(HOLogic.dest_list X)
|
||||
|
||||
end; (* struct *)
|
||||
|
||||
\<close>
|
||||
|
|
@ -1357,11 +1313,9 @@ 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>\<open>Isabelle_DOF_term_repr\<close>,
|
||||
ISA_core.check_identity, ISA_core.ML_isa_elaborate_generic)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
|
||||
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_docitem\<close>,
|
||||
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
|
||||
, (\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,
|
||||
ISA_core.ML_isa_check_trace_attribute, ISA_core.ML_isa_elaborate_trace_attribute)]
|
||||
|> fold (fn (n, check, elaborate) => fn thy =>
|
||||
let val ns = Sign.consts_of thy |> Consts.space_of
|
||||
|
|
@ -1736,7 +1690,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
|
|||
in (moid,map check_for_cid indexed_autoS, monitor_info) end
|
||||
val enabled_monitors = List.mapPartial is_enabled
|
||||
(Name_Space.dest_table (DOF_core.get_monitor_infos (Proof_Context.init_global thy)))
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = (YXML.content_of lhs,pos,opn,
|
||||
Syntax.read_term_global thy rhs)
|
||||
val defined = DOF_core.defined_of oid thy
|
||||
val trace_attr = if defined
|
||||
|
|
@ -1881,7 +1835,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi
|
|||
val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
|
||||
val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false}
|
||||
thy cid_long S defaults_init;
|
||||
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
|
||||
fun conv_attrs ((lhs, pos), rhs) = (YXML.content_of lhs,pos,"=", Syntax.read_term_global thy rhs)
|
||||
val assns' = map conv_attrs doc_attrs
|
||||
val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
|
||||
thy cid_long assns' defaults
|
||||
|
|
@ -2087,7 +2041,7 @@ fun update_instance_command (((oid, pos), cid_pos),
|
|||
then ()
|
||||
else error("incompatible classes:"^cid^":"^cid_long)
|
||||
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = ((markup2string lhs),pos,opn,
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = ((YXML.content_of lhs),pos,opn,
|
||||
Syntax.read_term_global thy rhs)
|
||||
val assns' = map conv_attrs doc_attrs
|
||||
val def_trans_value =
|
||||
|
|
@ -2575,16 +2529,11 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
|
|||
(case raw_stmt of
|
||||
Element.Shows _ =>
|
||||
let val stmt' = Attrib.map_specs (map prep_att) stmt
|
||||
val stmt'' = map (fn (b, ts) =>
|
||||
(b, map (fn (t', t's) =>
|
||||
(DOF_core.transduce_term_global {mk_elaboration=true}
|
||||
(t' , Position.none)
|
||||
(Proof_Context.theory_of ctxt),
|
||||
map (fn t'' =>
|
||||
DOF_core.transduce_term_global {mk_elaboration=true}
|
||||
(t'' , Position.none)
|
||||
(Proof_Context.theory_of ctxt))
|
||||
t's)) ts)) stmt'
|
||||
val stmt'' = stmt' |> map (fn (b, ts) =>
|
||||
(b, ts |> map (fn (t', t's) =>
|
||||
(DOF_core.elaborate_term ctxt t',
|
||||
t's |> map (fn t'' =>
|
||||
DOF_core.elaborate_term ctxt t'')))))
|
||||
in (([], prems, stmt'', NONE), stmt_ctxt) end
|
||||
| Element.Obtains raw_obtains =>
|
||||
let
|
||||
|
|
|
|||
Loading…
Reference in New Issue