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

Starting systematic testing and debugging of 

- default attribute construction
- attribute evaluation
This commit is contained in:
Burkhart Wolff 2018-08-20 11:36:04 +02:00
parent 0bc3120dca
commit 4ffcf185ff
3 changed files with 59 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isa_DOF.thy
View File

@ -839,10 +839,10 @@ fun calculate_attr_access_check ctxt attr oid = (* template *)
case DOF_core.get_value_local oid (Context.the_proof ctxt) of
SOME term => let val ctxt = Context.the_proof ctxt
val SOME{cid,...} = DOF_core.get_object_local oid ctxt
val (pr_name,_,ty) = case DOF_core.get_attribute_long_name_local cid attr ctxt of
val (long_cid, attr_b,ty) = case DOF_core.get_attribute_long_name_local cid attr ctxt of
SOME f => f
| NONE => error ("attribute undefined for ref"^ oid)
val proj_term = Const(pr_name,ty) (* pr_name should be long_name *)
val proj_term = Const(long_cid^"."^attr_b,dummyT --> ty)
val term = calculate_attr_access ctxt proj_term term
in (ML_Syntax.atomic o ML_Syntax.print_term) term end
| NONE => error "identifier not a docitem reference"

15
ontologies/Conceptual.thy
View File

@ -3,18 +3,25 @@ theory Conceptual
begin
doc_class A =
x :: "string"
x :: int
doc_class B =
y :: "string list" <= "[]"
x :: "string" (* attributes live in their own name-space *)
y :: "string list" <= "[]" (* and can have arbitrary type constructors *)
(* LaTeX may have problems with this, though *)
doc_class C = B +
z :: "A option" <= None
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
referring to a document class. Mathematical
relations over document items can be modeled. *)
datatype enum = X1 | X2 | X3
doc_class D = B +
a1 :: enum <= "X2"
x :: "string" <= "''def''" (* overriding default *)
a1 :: enum <= "X2" (* class - definitions may be mixed
with arbitrary HOL-commands, thus
also local definitions of enumerations *)
a2 :: int <= 0
doc_class F =

50
test/conceptual/Attributes.thy
View File

@ -2,9 +2,8 @@ theory Attributes
imports "../../ontologies/Conceptual"
begin
text* [dfgdfg::B, y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl}}\<close>
text*[dfgdfg::B, y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl}}\<close>
term "B"
text\<open> @{docitem_ref \<open>dfgdfg\<close>} }\<close>
print_doc_classes
@ -14,10 +13,53 @@ print_doc_items
ML\<open>
val ({tab = x, ...},y)= DOF_core.get_data @{context};
writeln "================";
Symtab.dest x;
Symtab.dest y;
\<close>
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
term "C.z ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
ML\<open>
DOF_core.get_attribute_long_name "Conceptual.A" "x" @{theory};
DOF_core.get_attribute_long_name "Conceptual.B" "x" @{theory};
DOF_core.get_attribute_long_name "Conceptual.B" "y" @{theory};
DOF_core.get_attribute_long_name "Conceptual.C" "x" @{theory};
DOF_core.get_attribute_long_name "Conceptual.C" "y" @{theory};
DOF_core.get_attribute_long_name "Conceptual.C" "z" @{theory};
(* this is only partially correct : the attribute longnames should be:
Conceptual.A.x
Conceptual.B.x
Conceptual.B.y
Conceptual.B.x
Conceptual.B.y
Conceptual.C.z
*)
\<close>
ML\<open>
DOF_core.get_default_local "Conceptual.A" "x" @{context};
DOF_core.get_default_local "Conceptual.B" "x" @{context};
DOF_core.get_default_local "Conceptual.B" "y" @{context};
DOF_core.get_default_local "Conceptual.C" "x" @{context};
DOF_core.get_default_local "Conceptual.C" "y" @{context};
DOF_core.get_default_local "Conceptual.C" "z" @{context};
\<close>
ML\<open>
DOF_core.get_value_local "sdf" @{context};
DOF_core.get_value_local "sdfg" @{context};
DOF_core.get_value_local "xxxy" @{context};
DOF_core.get_value_local "dfgdfg" @{context};
\<close>
ML\<open>
val Type X = @{typ "A"}
\<close>
ML\<open>val t = @{docitem_attr y::dfgdfg} \<close>