diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index 092ec22..99667e6 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -96,8 +96,10 @@ term "C" text\Voila what happens on the ML level:\ ML\val Type("Conceptual.B.B_ext",[Type("Conceptual.C.C_ext",t)]) = @{typ "C"}; - val @{typ "D"} = Value_Command.Docitem_Parser.cid_2_cidType "Conceptual.D" @{theory}; - val @{typ "E"} = Value_Command.Docitem_Parser.cid_2_cidType "Conceptual.E" @{theory}; + val \<^typ>\D\ = DOF_core.get_onto_class_cid \<^theory> "Conceptual.D" + |> snd ; + val \<^typ>\E\ = DOF_core.get_onto_class_cid \<^theory> "Conceptual.E" + |> snd; \ text*[dfgdfg2::C, z = "None"]\ Lorem ipsum ... @{thm refl} \ diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index fcbba0c..cbbe561 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -262,7 +262,9 @@ struct to be able to reference the class internally. *) - val default_cid = "text" (* the top (default) document class: everything is a text.*) + val default_cid = "text" (* the top (default) document class: everything is a text.*) + + val default_cid_typ = \<^typ>\unit\ (* top document class type *) (* Due to the implementation, is_subclass0 is _NOT_ compatible with DOF classes type synonyms, so they must be resolved to full class names before use. *) @@ -294,6 +296,8 @@ struct val undefined_instance = "undefined_instance" + val undefined_value = Free ("Undefined_Value", default_cid_typ) + val empty_instance = Instance {defined = false, input_term = \<^term>\()\, value = \<^term>\()\, @@ -702,12 +706,6 @@ fun is_subclass (ctxt) s t = is_subclass0 s t ctxt fun is_subclass_global thy s t = let val ctxt = Proof_Context.init_global thy in is_subclass0 s t ctxt end - -fun typ_to_cid (Type(s,[\<^Type>\unit\])) = Long_Name.qualifier s - |typ_to_cid (Type(_,[T])) = typ_to_cid T - |typ_to_cid _ = error("type is not an ontological type.") - - 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) @@ -1313,7 +1311,7 @@ fun elaborate_instances_of thy _ _ term_option _ = without using the burden of ontology classes. ex: text*[sdf]\ Lorem ipsum @{thm refl}\ *) (filter (fn name => DOF_core.cid_of name thy |> equal DOF_core.default_cid)) - |> mk_list \<^typ>\unit\ + |> mk_list DOF_core.default_cid_typ else let val class_typ = class_name |> Syntax.read_typ_global thy @@ -1557,16 +1555,6 @@ val value_without_elaboration = value_select "" structure Docitem_Parser = struct -fun cid_2_cidType cid_long thy = - if cid_long = DOF_core.default_cid then \<^Type>\unit\ - else let fun ty_name cid = cid^"."^ Long_Name.base_name cid ^ Record.extN - fun fathers cid_long = case DOF_core.get_onto_class_global cid_long thy of - DOF_core.Onto_Class {inherits_from=NONE, ...} => [cid_long] - | DOF_core.Onto_Class {inherits_from=SOME(_,father), ...} => - cid_long :: (fathers father) - in fold (fn x => fn y => Type(ty_name x,[y])) (fathers cid_long) \<^Type>\unit\ - end - fun create_default_object thy binding class_name typ = let val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name @@ -1620,7 +1608,7 @@ fun check_classref {is_monitor=is_monitor} (SOME (cid, pos)) thy = in (name_cid_typ, pos) end | check_classref _ NONE _ = pair DOF_core.default_cid DOF_core.default_cid - |> rpair \<^typ>\unit\ + |> rpair DOF_core.default_cid_typ |> rpair Position.none fun calc_update_term {mk_elaboration=mk_elaboration} thy (name, typ) @@ -1893,7 +1881,9 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi else NONE val value_terms = if default_cid then let - val undefined_value = Free (oid ^ "_Undefined_Value", \<^Type>\unit\) + val undefined_value = dest_Free DOF_core.undefined_value + |> apfst (fn x => oid ^ "_" ^ x) + |> Free in (undefined_value, undefined_value) end (* Handle initialization of docitem without a class associated, for example when you just want a document element to be referentiable @@ -2227,7 +2217,7 @@ fun meta_args_2_latex thy sem_attrs transform_attr NONE => let val DOF_core.Instance cid = DOF_core.get_instance_global lab thy in pair (cid |> #cid) (cid |> #cid) - |> rpair \<^typ>\unit\ end + |> rpair DOF_core.default_cid_typ end | SOME(cid,_) => DOF_core.get_onto_class_cid thy cid