diff --git a/MOF.sml b/MOF.sml new file mode 100644 index 00000000..61b787d1 --- /dev/null +++ b/MOF.sml @@ -0,0 +1,71 @@ +structure MOF : sig + type 'a equal + type num + type 'a rexp + type char + type attribute_types + type class_hierarchy + val mt : class_hierarchy + val classes : class_hierarchy -> string list + val all_entities : + class_hierarchy -> ((string * (string * string) rexp) list) list + val all_attributes : class_hierarchy -> ((string * attribute_types) list) list + val remove_overrides : 'b equal -> ('a -> 'b) -> 'a list -> 'a list +end = struct + +type 'a equal = {equal : 'a -> 'a -> bool}; +val equal = #equal : 'a equal -> 'a -> 'a -> bool; + +datatype int = Int_of_integer of IntInf.int; + +datatype num = One | Bit0 of num | Bit1 of num; + +datatype 'a rexp = Empty | Atom of 'a | Alt of 'a rexp * 'a rexp | + Conc of 'a rexp * 'a rexp | Star of 'a rexp; + +datatype char = Zero_char | Char of num; + +datatype attribute_types = File_T of string | Image_file_T of string | + Thms_T of string list | Int_T of int | Bool_T of bool | String_T of string | + Text_T of string | Range_T of int * int option | Enum_T of string list; + +datatype class_hierarchy = + Class_T of + string * class_hierarchy list * (string * attribute_types) list * + (string * (string * string) rexp) list; + +fun eq A_ a b = equal A_ a b; + +fun maps f [] = [] + | maps f (x :: xs) = f x @ maps f xs; + +fun implode _ = raise Fail "String.implode"; + +val mt : class_hierarchy = + Class_T (implode [Char (Bit1 (Bit1 (Bit1 (Bit1 (Bit0 One)))))], [], [], []); + +fun member A_ [] y = false + | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; + +fun map f [] = [] + | map f (x21 :: x22) = f x21 :: map f x22; + +fun classes (Class_T (name, sub_classes, attr, comps)) = + name :: maps classes sub_classes; + +fun entities (Class_T (x1, x2, x3, x4)) = x4; + +fun all_entities (Class_T (name, sub_classes, attr, comps)) = + comps :: map entities sub_classes; + +fun attributes (Class_T (x1, x2, x3, x4)) = x3; + +fun all_attributes (Class_T (name, sub_classes, attr, comps)) = + attr :: map attributes sub_classes; + +fun remove_overrides B_ f [] = [] + | remove_overrides B_ f (a :: r) = + (if member B_ (map f r) (f a) then remove_overrides B_ f r + else a :: remove_overrides B_ f r); + +end; (*struct MOF*) diff --git a/examples/simple/Example.thy b/examples/simple/Example.thy new file mode 100644 index 00000000..4a32d76b --- /dev/null +++ b/examples/simple/Example.thy @@ -0,0 +1,154 @@ +theory Example + imports "../../ontologies/CENELEC_50126" + keywords "Term" :: diag +begin + +section{* Some show-off's of general antiquotations. *} + + +(* some show-off of standard anti-quotations: *) +print_attributes +print_antiquotations + +text{* @{thm refl} of name @{thm [source] refl} + @{thm[mode=Rule] conjI} + @{file "../../Isa_DOF.thy"} + @{value "3+4::int"} + @{const hd} + @{theory List}} + @{term "3"} + @{type bool} + @{term [show_types] "f x = a + x"} *} + + +section{* Example *} + +text*[ass1::assumption] {* Brexit means Brexit *} + +text*[hyp1::hypothesis] {* P means not P *} + + +text*[ass122::srac] {* The overall sampling frequence of the odometer +subsystem is therefore 14 khz, which includes sampling, computing and +result communication times... *} + +text*[t10::test_result] {* This is a meta-test. This could be an ML-command +that governs the external test-execution via, eg., a makefile or specific calls +to a test-environment or test-engine *} + + +text \ As established by @{docref (unchecked) \t10\}, + @{docref (define) \t10\} + the @{docref \t10\} + the @{docref \ass122\} + \ +text \ safety related applicability condition @{srac \ass122\}. + exported constraint @{ec \ass122\}. + \ + +text{* + And some ontologically inconsistent reference: + @{hypothesis \ass1\} as well as + +*} +-- "very wrong" + +text{* + And some ontologically inconsistent reference: + @{assumption \hyp1\} as well as + +*} +-- "very wrong" + + + +text{* + And some ontologically inconsistent reference: + @{test_result \ass122\} as well as + +*} +-- wrong + +text{* + And some other ontologically inconsistent reference: + @{ec \t10\} as well as +*} +-- wrong + + + +section{* Some Tests for Ontology Framework and its CENELEC Instance *} + +declare_reference [lalala::requirement, alpha="main", beta=42] + +declare_reference [lalala::quod] (* shouldn't work *) + +declare_reference [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] + +paragraph*[sdf]{* just a paragraph *} +paragraph* [sdfk] \ just a paragraph - lexical variant \ + +subsection*[sdf]{* shouldn't work, multiple ref. *} + +section*[sedf::requirement, alpja= refl]{* works again. One can hover over the class constraint and + jump to its definition. *} +text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) + +section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, +but wrong doc_class constraint. *} + +section{* Text Antiquotation Infrastructure ... *} + +text{* @{docref \lalala\} -- produces warning. *} +text{* @{docref (unchecked) \lalala\} -- produces no warning. *} + +text{* @{docref \ass122\} -- global reference to a text-item in another file. *} + +text{* @{ec \ass122\} -- global reference to a exported constraint in another file. + Note that the link is actually a srac, which, according to + the ontology, happens to be an "ec". *} + +text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} + + + +text{* Here is a reference to @{docref \sedf\} *} +(* works currently only in connection with the above label-hack. + Try to hover over the sedf - link and activate it !!! *) + + + + + + + + + + + + + +section{* A Small Example for a Command Definition --- just to see how this works in principle. *} + +ML{* +val opt_modes = + Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; + +val _ = + Outer_Syntax.command @{command_keyword Term} "read and print term" + (opt_modes -- Parse.term >> Isar_Cmd.print_term); + +*} + +lemma "True" by simp + +Term "a + b = b + a" + +term "a + b = b + a" + +section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) + + +end + + \ No newline at end of file diff --git a/examples/simple/IdirExample.thy b/examples/simple/IdirExample.thy new file mode 100644 index 00000000..270dbbde --- /dev/null +++ b/examples/simple/IdirExample.thy @@ -0,0 +1,9 @@ +theory IdirExample + imports "../../ontologies/ScientificPaperOnto" + +begin + +text*[p1::Paragraph] {* ceci est un paragraphe *} +text*[abs::Abstract, content = p1]{* *} + +end \ No newline at end of file diff --git a/ontologies/ScientificPaperOnto.thy b/ontologies/ScientificPaperOnto.thy new file mode 100644 index 00000000..6f806120 --- /dev/null +++ b/ontologies/ScientificPaperOnto.thy @@ -0,0 +1,26 @@ +theory ScientificPaperOnto + imports "../Isa_DOF" + +begin + +doc_class Paragraph = + content :: "string list" + +doc_class Abstract = + content :: Paragraph + +doc_class SubSection = + id :: integer + content :: "Paragraph list" + +doc_class Section = + id :: integer + content :: "Paragraph list" + itsSubSection :: "SubSection list" + +doc_class Article = + content :: "(Abstract + Section) list" + where + "(Abstract. + Section*)" +end \ No newline at end of file