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

Add the possibility to make request on instances #6

Merged
adbrucker merged 1 commits from nicolas.meric/Isabelle_DOF:request-on-instances-first-draft into master 2021-12-15 22:25:05 +00:00
Conversation 0 Commits 1 Files Changed 3 +143 -26
3 changed files with 143 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

117
src/DOF/Isa_DOF.thy
View File

@ -61,10 +61,10 @@ ML\<open>
val docrefN = "docref";
val docclassN = "doc_class";
(** name components **)
val makeN = "make";
val instances_of_suffixN = "_instances"
(* derived from: theory_markup *)
fun docref_markup_gen refN def name id pos =
@ -202,7 +202,7 @@ struct
end)
type ISA_transformers = {check :
(theory -> term * typ * Position.T -> string -> term option),
elaborate : (theory -> string -> typ -> term -> term)
elaborate : (theory -> string -> typ -> term option -> term)
}
type ISA_transformer_tab = ISA_transformers Symtab.table
@ -666,20 +666,29 @@ fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
let val tab = #ISA_transformer_tab(get_data_global thy)
fun T(Const(s,ty) $ t) = if is_ISA s
then case Symtab.lookup tab s of
NONE => error("undefined inner syntax antiquotation: "^s)
| SOME({check=check, elaborate=elaborate}) => (case check thy (t,ty,pos) s of
NONE => Const(s,ty) $ t
(* checking isa, may raise error though. *)
| SOME t =>
if mk_elaboration
then elaborate thy s ty t
else Const(s,ty) $ t)
NONE => error("undefined inner syntax antiquotation: "^s)
| SOME({check=check, elaborate=elaborate}) =>
case check thy (t,ty,pos) s of
NONE => Const(s,ty) $ t
(* checking isa, may raise error though. *)
| SOME t => if mk_elaboration
then elaborate thy s ty (SOME t)
else Const(s,ty) $ t
(* transforming isa *)
else (Const(s,ty) $ (T t))
|T(t1 $ t2) = T(t1) $ T(t2)
|T(Const(s,ty)) = if is_ISA s
then case Symtab.lookup tab s of
NONE => error("undefined inner syntax antiquotation: "^s)
| SOME({elaborate=elaborate, ...}) =>
if mk_elaboration
then elaborate thy s ty NONE
else Const(s, ty)
(* transforming isa *)
else Const(s, ty)
|T(Abs(s,ty,t)) = Abs(s,ty,T t)
|T t = t
in T term end
in T term end
fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt)
in writeln (String.concatWith "," (Symtab.keys tab)) end
@ -944,6 +953,7 @@ fun ML_isa_check_generic check thy (term, pos) _ =
val _ = check thy (name,pos)
in SOME term end;
fun check_identity _ (term, _, _) _ = SOME term
fun ML_isa_check_typ thy (term, _, pos) s =
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
@ -1014,13 +1024,19 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) s =
else err ("faulty reference to docitem: "^name) pos
in ML_isa_check_generic check thy (term, pos) s end
fun ML_isa_elaborate_generic (thy:theory) isa_name ty term = Const (isa_name, ty) $ term
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 elaborate_instance thy _ _ term = let val instance_name = HOLogic.dest_string term
in case DOF_core.get_value_global instance_name thy of
NONE => error ("No class instance: " ^ instance_name)
| SOME(value) => value
end
fun elaborate_instance thy _ _ term_option =
case term_option of
NONE => error ("Malformed term annotation")
| SOME term => let val instance_name = HOLogic.dest_string term
in case DOF_core.get_value_global instance_name thy of
NONE => error ("No class instance: " ^ instance_name)
| SOME(value) => value
end
(*
The function declare_ISA_class_accessor_and_check_instance uses a prefix
@ -1046,9 +1062,71 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name =
val class_name = Long_Name.qualify qual
(DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind))
in
DOF_core.update_isa_global(class_name, {check=check_instance, elaborate=elaborate_instance}) thy end)
DOF_core.update_isa_global
(class_name, {check=check_instance, elaborate=elaborate_instance}) thy
end)
end
fun elaborate_instances_list thy isa_name _ _ =
let
val base_name = Long_Name.base_name isa_name
fun get_isa_name_without_intances_suffix s =
String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN)))
val base_name_without_suffix = get_isa_name_without_intances_suffix base_name
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
(base_name')
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
(base_name' ^ " List.list")
val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
val table_list = Symtab.dest tab
fun get_instances_name_list _ [] = []
| get_instances_name_list class_name (x::xs) =
let
val (_, docobj_option) = x
in
case docobj_option of
NONE => get_instances_name_list class_name xs
| SOME {cid=cid, value=value, ...} =>
if cid = class_name
then value::get_instances_name_list class_name xs
else get_instances_name_list class_name xs
end
val long_class_name = DOF_core.read_cid_global thy base_name'
val values_list = get_instances_name_list long_class_name table_list
val hol_list_terms_list =
fold
(fn x =>
fn y =>
Const (@{const_name "Cons"}, [class_typ, class_list_typ] ---> class_list_typ) $ x $ y)
values_list (Const (@{const_name "Nil"}, class_list_typ))
in hol_list_terms_list end
fun declare_class_instances_annotation thy doc_class_name =
let
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
val bind' = Binding.suffix_name instances_of_suffixN bind
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
((Binding.name_of doc_class_name) ^ " List.list")
(* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
we can not use "_" for classes names in term antiquotation.
We chose to convert "_" to "-".*)
val conv_class_name' = String.translate (fn #"_" => "-" | x=> String.implode [x])
((Binding.name_of doc_class_name) ^ instances_of_suffixN)
val mixfix_string = "@{" ^ conv_class_name' ^ "}"
in
Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))]
#> (fn thy => let
val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name)
val qual = Long_Name.qualifier long_name
val transformer_name = Long_Name.qualify qual
(DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind'))
val _ = writeln ("transformer_name: " ^ transformer_name)
in
DOF_core.update_isa_global (transformer_name,
{check=check_identity, elaborate= elaborate_instances_list}) thy end)
end
(* utilities *)
fun property_list_dest ctxt X = (map (fn Const ("Isa_DOF.ISA_term", _) $ s => HOLogic.dest_string s
@ -1068,7 +1146,7 @@ setup\<open>DOF_core.update_isa_global("Isa_DOF.typ.typ",
setup\<open>DOF_core.update_isa_global("Isa_DOF.term.term",
{check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
setup\<open>DOF_core.update_isa_global("Isa_DOF.term_repr",
{check=(fn _ => fn (t,_,_) => fn _ => SOME t), elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
{check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
setup\<open>DOF_core.update_isa_global("Isa_DOF.thm.thm",
{check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
setup\<open>DOF_core.update_isa_global("Isa_DOF.file.file",
@ -2132,6 +2210,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
by add_doc_class_cmd function *)
|> ISA_core.declare_ISA_class_accessor_and_check_instance binding
|> (fn thy => (ISA_core.declare_class_instances_annotation thy binding) thy)
end;

2
src/ontologies/Conceptual/Conceptual.thy
View File

@ -46,7 +46,7 @@ Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theo
\<^enum> @{thm [display] A.simps(6)}
\<^enum> ...
\<close>
(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspectwed, of course, by *)
(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by *)
find_theorems (60) name:Conceptual name:A

50
src/tests/Evaluation.thy
View File

@ -25,15 +25,18 @@ Some built-ins remain as unspecified constants:
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.
The TA denotes the HOL list of the values of the instances.
The value of an instance is the record of every attributes of the instance.
This way, we can use the usual functions on lists to make our request.
The emphasis of this presentation is to present the evaluation possibilities and limitations
of the current implementation.
\<close>
text\<open>
case : attribute not initialized
\<close>
section\<open>Term Annotation evaluation\<close>
text\<open>We can validate a term with TA:\<close>
term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
@ -52,7 +55,7 @@ an instance of the class @{doc_class A}:
\<close>
term*\<open>@{A \<open>xcv1\<close>}\<close>
text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class B:
text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class @{doc_class B}:
\<close>
(* Error:
term*\<open>@{B \<open>xcv1\<close>}\<close>*)
@ -103,6 +106,41 @@ ML\<open>
@{thm "refl"}
\<close>
section\<open>Request on instances\<close>
text\<open>We define a new class Z:\<close>
doc_class Z =
z::"int"
text\<open>And some instances:\<close>
text*[test1Z::Z, z=1]\<open>lorem ipsum...\<close>
text*[test2Z::Z, z=4]\<open>lorem ipsum...\<close>
text*[test3Z::Z, z=3]\<open>lorem ipsum...\<close>
text\<open>We want to get all the instances of the @{doc_class Z}:\<close>
value*\<open>@{Z-instances}\<close>
text\<open>Now we want to get the instances of the @{doc_class Z} whose attribute z > 2:\<close>
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances}\<close>
text\<open>We can check that we have the list of instances we wanted:\<close>
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
\<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
text\<open>Now, we want to get all the instances of the @{doc_class A}\<close>
value*\<open>@{A-instances}\<close>
text\<open>Warning: If you make a request on attributes that are undefined in some instances,
you will get a result which includes these unresolved cases.
In the following example, we request the instances of the @{doc_class A}.
But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory Isabelle_DOF.Conceptual}
whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
So in the request result we get an unresolved case because the evaluator can not get
the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>test\<close>}:\<close>
value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
section\<open>Limitations\<close>
text\<open>There are still some limitations.
The terms passed as arguments to the TA are not simplified and their evaluation fails:
\<close>