nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Intermediate Version 

- attribute value generation
- update interpreted
- type-checking integrated but crashes
- news on scholarly_paper …
This commit is contained in:
Burkhart Wolff 2018-04-27 10:34:24 +02:00
parent 0474c47957
commit 5bcd4c19b1
4 changed files with 387 additions and 249 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

221
Isa_DOF.thy
View File

@ -13,9 +13,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
keywords "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*" "text*"
"open_monitor*" "close_monitor*" "declare_reference*"
"update_instance*" ::thy_decl
and
"doc_class" :: thy_decl
"update_instance*" "doc_class" ::thy_decl
begin
@ -27,9 +26,10 @@ typedecl "thm"
-- \<open> and others in the future : file, http, thy, ... \<close>
consts mk_typ :: "string \<Rightarrow> typ" ("@{typ _}")
consts mk_term :: "string \<Rightarrow> term" ("@{term _}")
consts mk_thm :: "string \<Rightarrow> thm" ("@{thm _}")
consts mk_typ :: "string \<Rightarrow> typ" ("@{typ _}")
consts mk_term :: "string \<Rightarrow> term" ("@{term _}")
consts mk_thm :: "string \<Rightarrow> thm" ("@{thm _}")
consts mk_docitem :: "string \<Rightarrow> 'a" ("@{docitem _}")
term "@{typ ''int => int''}"
@ -268,13 +268,13 @@ fun declare_anoobject_local ctxt cid =
fun get_object_global oid thy = let val {tab,...} = fst(get_data_global thy)
in case Symtab.lookup tab oid of
NONE => error"undefined reference"
NONE => error("undefined reference: "^oid)
|SOME(bbb) => bbb
end
fun get_object_local oid ctxt = let val {tab,...} = fst(get_data ctxt)
in case Symtab.lookup tab oid of
NONE => error"undefined reference"
NONE => error("undefined reference: "^oid)
|SOME(bbb) => bbb
end
@ -331,6 +331,25 @@ fun get_attribute_long_name_local cid attr ctxt =
fun get_attribute_long_name cid attr thy = get_attribute_long_name_local cid attr
(Proof_Context.init_global thy)
fun get_value_global oid thy = case get_object_global oid thy of
SOME{value=term,...} => SOME term
| NONE => NONE
fun get_value_local oid ctxt = case get_object_local oid ctxt of
SOME{value=term,...} => SOME term
| NONE => NONE
fun update_value_global oid upd thy =
case get_object_global oid thy of
SOME{pos,thy_name,value,id,cid} =>
let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name,
value=upd value,id=id, cid=cid})
in map_data_global (apfst(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end
| NONE => error("undefined doc object: "^oid)
fun writeln_classrefs ctxt = let val tab = snd(get_data ctxt)
in writeln (String.concatWith "," (Symtab.keys tab)) end
@ -355,8 +374,13 @@ val attribute =
val attribute_upd =
Parse.position Parse.const
-- (Parse.$$$ "+=" || Parse.$$$ "=")
-- ( Parse.$$$ "+" || Parse.$$$ "=")
(* -- ( Parse.keyword_with (fn x => "+=" = x) || Parse.keyword_with (fn x=> ":=" = x)) *)
-- Parse.!!! Parse.term;
(*
Token.T list ->
(((string * Position.T) * string) * string) *
Token.T list*)
(*
Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ uncheckedN)
@ -380,8 +404,28 @@ val attributes_upd =
val SPY = Unsynchronized.ref ([]:((term * Position.T) * term) list)
fun convert((Const(s,ty),_), t) X = Const(s^"_update", range_type ty)
$ Abs("uuu_", type_of t, t) $ X
|convert _ _ = error("Big drama")
fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs),
val base = @{term "undefined"}
fun check_classref (SOME(cid,pos')) thy =
let val _ = if not (DOF_core.is_defined_cid_global cid thy)
then error("document class undefined") else ()
val cid_long = DOF_core.name2doc_class_name thy cid
val {id, name=bind_target,...} = the(DOF_core.get_doc_class_global cid_long thy)
val markup = docclass_markup false cid id (Binding.pos_of bind_target);
val ctxt = Context.Theory thy
val _ = Context_Position.report_generic ctxt pos' markup;
in cid_long
end
| check_classref NONE _ = DOF_core.default_cid
fun enriched_document_command markdown (((((oid,pos),cid_pos),
doc_attrs: ((string * Position.T) * string) list),
xstring_opt:(xstring * Position.T) option),
toks:Input.source)
: Toplevel.transition -> Toplevel.transition =
@ -390,38 +434,52 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs),
val _ = Position.report pos (docref_markup true oid id pos);
(* creates a markup label for this position and reports it to the PIDE framework;
this label is used as jump-target for point-and-click feature. *)
val undef = @{term "undefined"}
fun check_classref (SOME(cid,pos')) thy =
let val _ = if not (DOF_core.is_defined_cid_global cid thy)
then error("document class undefined") else ()
val cid_long = DOF_core.name2doc_class_name thy cid
val {id, name=bind_target,...} = the(DOF_core.get_doc_class_global cid_long thy)
val markup = docclass_markup false cid id (Binding.pos_of bind_target);
val ctxt = Context.Theory thy
val _ = Context_Position.report_generic ctxt pos' markup;
in cid_long
end
| check_classref NONE _ = DOF_core.default_cid
fun enrich_trans class_ref thy =
let val name = Context.theory_name thy
val cid_long = check_classref class_ref thy
fun enrich_trans thy =
let val cid_long = check_classref cid_pos thy
fun read_assn ((lhs, pos), rhs) = ((Syntax.read_term_global thy lhs,pos),
Syntax.read_term_global thy rhs)
val assns = map (read_assn ) doc_attrs
val _ = (SPY:=assns)
val assns = map read_assn doc_attrs
val _ = (SPY:=assns)
val defaults = base (* this calculation ignores the defaults *)
val value_term = (fold convert assns defaults) |> (Sign.cert_term thy)
val name = Context.theory_name thy
in thy |> DOF_core.define_object_global (oid, {pos=pos,
thy_name=name,
value = undef,
value = value_term,
id=id,
cid=cid_long})
end
fun check_text thy = (Thy_Output.output_text (Toplevel.theory_toplevel thy) markdown toks; thy)
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
in
Toplevel.theory(enrich_trans cid_pos #> check_text)
Toplevel.theory(enrich_trans #> check_text)
(* Thanks Frederic Tuong! ! ! *)
end;
fun update_instance_command (((oid:string,pos),cid_pos),
doc_attrs: (((string*Position.T)*string)*string)list)
: Toplevel.transition -> Toplevel.transition =
let
fun upd thy =
let val cid = case DOF_core.get_object_global oid thy of
SOME{cid,...} => cid
| NONE => error("undefined doc_class.")
val cid_long = check_classref cid_pos thy
val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long then ()
else error("incompatible classes:"^cid^":"^cid_long)
fun read_assn (((lhs, pos), opn), rhs) =
let val _ = writeln opn in
((Syntax.read_term_global thy lhs,pos), (* this is problematic,
lhs need to be qualified *)
Syntax.read_term_global thy rhs)
end
(* Missing: Check that attributes are legal here *)
val assns = map read_assn doc_attrs
val _ = (SPY:=assns)
in thy |> DOF_core.update_value_global oid ((fold convert assns) #> (Sign.cert_term thy))
end
in Toplevel.theory(upd)
end
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
@ -471,12 +529,10 @@ val _ =
"close a document reference monitor"
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
(Toplevel.theory (I)))); (* dummy so far *)
val _ =
Outer_Syntax.command @{command_keyword "update_instance*"}
"update meta-attributes of an instance of a document class"
(attributes_upd >> (fn (((oid,pos),cid),doc_attrs) =>
(Toplevel.theory (I)))); (* dummy so far *)
(attributes_upd >> (fn args => update_instance_command args));
end (* struct *)
@ -523,16 +579,16 @@ val doc_ref_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
{unchecked = false, define= false} (* default *);
fun doc_class_ref_antiquotation name cid_decl =
fun docitem_ref_antiquotation name cid_decl =
let fun open_par x = if x then "\\label{"
else "\\autoref{"
else "\\autoref{"
val close = "}"
in
Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- Args.cartouche_input))
(fn {context = ctxt, source = src:Token.src, state} =>
fn ({unchecked = x, define= y}, source:Input.source) =>
(Thy_Output.output_text state {markdown=false} #>
check_and_mark ctxt
check_and_mark ctxt
cid_decl
({strict_checking = not x})
(Input.pos_of source) #>
@ -540,28 +596,43 @@ fun doc_class_ref_antiquotation name cid_decl =
source)
end
fun check_and_mark_term ctxt oid =
let val thy = Context.theory_of ctxt;
in if DOF_core.is_defined_oid_global oid thy
then let val {pos=pos_decl,id,cid,value,...} = the(DOF_core.get_object_global oid thy)
val markup = docref_markup false oid id pos_decl;
val _ = Context_Position.report_generic ctxt pos_decl markup;
(* this sends a report for a ref application to the PIDE interface ... *)
val _ = if cid = DOF_core.default_cid
then error("anonymous "^ DOF_core.default_cid ^ " class has no value" )
else ()
in value end
else error("undefined document reference:"^oid)
end
val X = (Scan.lift Args.cartouche_input : Input.source context_parser) >> (fn inp => "")
fun docitem_value_ML_antiquotation binding =
ML_Antiquotation.inline binding
(fn (ctxt, toks) => (Scan.lift (Args.cartouche_input)
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
(check_and_mark_term ctxt (Input.source_content inp))))
(ctxt, toks))
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
val _ = Theory.setup (doc_class_ref_antiquotation @{binding docref} DOF_core.default_cid)
val _ = Theory.setup((docitem_ref_antiquotation @{binding docref} DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^*)
(docitem_ref_antiquotation @{binding docitem_ref} DOF_core.default_cid) #>
docitem_value_ML_antiquotation @{binding docitem_value})
end (* struct *)
*}
section{* Syntax for Ontologies (the '' View'' Part III) *}
ML{* Type_Infer_Context.infer_types *}
ML{*
type_of; Syntax.string_of_term; Type.typ_instance; Args.term; Syntax.parse_term;
Syntax.check_term;
Syntax.unparse_term;
val x = @{term "None::(string option)"}
val t = Syntax.parse_term @{context} "None::(string option)"
val t' = Syntax.read_term @{context} "None::(string option)"
(*
val y = Type_Infer_Context.infer_types @{context} [(Syntax.parse_term @{context} "None")]
handle TYPE _ => error"bla";
*)
*}
section{* Syntax for Ontologies (the '' View'' Part III) *}
ML{*
structure OntoParser =
struct
@ -621,8 +692,8 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
" in doc class:" ^ class);
SOME(bind,ty,mf))
else error("no overloading allowed.")
val gen_antiquotation = OntoLinkParser.doc_class_ref_antiquotation
val fields2 = map_filter (check_n_filter thy) fields
val gen_antiquotation = OntoLinkParser.docitem_ref_antiquotation
val _ = map_filter (check_n_filter thy) fields
in thy |> Record.add_record overloaded (params', binding) parent (tag_attr::fields)
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
@ -651,16 +722,7 @@ end (* struct *)
section{* Testing and Validation *}
ML{* (* Parsing combinators in Scan *)
op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c;
op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b;
op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e;
op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e;
Scan.repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a;
Scan.option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a;
*}
ML{* ignore *}
ML{*
Binding.print;
Syntax.read_sort;
@ -670,35 +732,6 @@ Syntax.pretty_typ;
Parse.document_source;
*}
ML{*
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.document_command;
Toplevel.exit: Toplevel.transition -> Toplevel.transition;
Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
Toplevel.ignored: Position.T -> Toplevel.transition;
Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition;
Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition;
Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
Toplevel.present_local_theory:
(xstring * Position.T) option ->
(Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
(* where text treatment and antiquotation parsing happens *)
(*fun document_command markdown (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
NONE => ignore (output_text state markdown txt)
| SOME (_, pos) =>
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *)
Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
Toplevel.transition -> Toplevel.transition;
*}
ML\<open>
open Markup;
Markup.binding;

298
MyCommentedIsabelle.thy
View File

@ -13,14 +13,44 @@ section "Isabelle/Pure bootstrap";
text \<open> @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
text "It's even roughly commented ... "
(* Paradigmatic Example for Antiquotation programming *)
text \<open> @{footnote \<open>sdf\<close> }\<close>
section{* Stuff - Interesting operators (just sample code) *}
(* Vorbild *)
text \<open> @{footnote \<open>sdf\<close> }\<close>
subsection\<open> Global State Management\<close>
subsubsection\<open> Mechanism 1 : configuration flags of fixed type. \<close>
(* General combinators (in Pure/General/basics.ML)*)
ML{*
(*
exception Bind
exception Chr
exception Div
exception Domain
exception Fail of string
exception Match
exception Overflow
exception Size
exception Span
exception Subscript
*)
exnName : exn -> string ; (* -- very interisting to query an unknown exception *)
exnMessage : exn -> string ;
op ! : 'a Unsynchronized.ref -> 'a;
op := : ('a Unsynchronized.ref * 'a) -> unit;
op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c; (* reversed function composition *)
op o : (('b -> 'c) * ('a -> 'b)) -> 'a -> 'c;
op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e;
op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e;
op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
op ? : bool * ('a -> 'a) -> 'a -> 'a;
ignore: 'a -> unit;
op before : ('a * unit) -> 'a;
I: 'a -> 'a;
K: 'a -> 'b -> 'a
*}
section\<open> Global Isar State Management\<close>
subsection\<open> Mechanism 1 : configuration flags of fixed type. \<close>
ML{*
Config.get @{context} Thy_Output.quotes;
@ -47,7 +77,7 @@ fun output ctxt prts =
*)
*}
subsubsection\<open> Mechanism 2 : global arbitrary data structure that is attached to the global and
subsection\<open> Mechanism 2 : global arbitrary data structure that is attached to the global and
local Isabelle context $\theta$ \<close>
ML {*
@ -67,17 +97,9 @@ structure Data = Generic_Data
*}
(* General combinators (in Pure/General/basics.ML)*)
ML{*
op #>; (* reversed function composition *)
op |--;
op --|;
op --;
op ?;
*}
subsubsection\<open> Kernel: terms, types, thms \<close>
section\<open> Kernel: terms, types, thms \<close>
subsection{* Terms and Types *}
text \<open>A basic data-structure of the kernel is term.ML \<close>
ML{* open Term;
(*
@ -99,30 +121,27 @@ ML{* open Term;
exception TYPE of string * typ list * term list
exception TERM of string * term list
*)
(* there is a joker type that can be added as place-holder during term construction.*)
Term.dummyT : typ
*}
ML{* Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) *}
text{* there is a joker type that can be added as place-holder during term construction.
Jokers can be eliminated by the type inference. *}
ML{* Term.dummyT : typ *}
subsection{* Type-Inference *}
text{* Jokers can be eliminated by the type inference. *}
ML{*
Sign.typ_instance: theory -> typ * typ -> bool;
Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int;
Sign.const_type: theory -> string -> typ option;
Sign.certify_term: theory -> term -> term * typ * int;
Sign.cert_term: theory -> term -> term;
Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*)
Sign.cert_term: theory -> term -> term; (* short-cut for the latter *)
*}
text{* This is actually an abstract wrapper on the structure Type which contains the heart of
the type inference. *}
ML{*
Type.typ_instance: Type.tsig -> typ * typ -> bool
(* raises TYPE_MATCH *)
*}
text{* @{ML "Sign.certify_term"} is actually an abstract wrapper on the structure Type
which contains the heart of the type inference. *}
text{* Type generalization is no longer part of the standard API. Here is a way to
overcome this:*}
overcome this by a self-baked generalization function:*}
ML{*
val ty = @{typ "'a option"};
@ -132,14 +151,13 @@ val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort
Sign.typ_instance @{theory} (ty', generalize_typ ty)
*}
subsubsection\<open> Front End: Parsing issues \<close>
(* Tokens and Bindings *)
ML{*
section\<open> Front End: \<close>
subsection{* Parsing issues *}
text{* Tokens and Bindings *}
ML{*
(* Core: Token.T *)
@ -149,38 +167,61 @@ ML{*
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
*)
(* conversion between these two : *)
fun parser2contextparser pars (ctxt, toks) = let val (a, toks') = pars toks
in (a,(ctxt, toks')) end;
val _ = parser2contextparser : 'a parser -> 'a context_parser;
(* bah, is the same as Scan.lift *)
val _ = Scan.lift Args.cartouche_input : Input.source context_parser;
Token.is_command;
Token.content_of; (* textueller kern eines Tokens. *)
val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position,
where \<dieresis>positions\<dieresis> are absolute references to a file *)
Binding.make;
Binding.make: bstring * Position.T -> binding;
Binding.pos_of @{binding erzerzer};
Position.here;
Position.here: Position.T -> string;
(* Bindings *)
ML\<open>val X = @{here};\<close>
*}
(* Scanning and combinator parsing. *)
subsection {*Scanning and combinator parsing. *}
ML\<open>
Scan.peek;
Scan.peek : ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd);
Scan.optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a;
Scan.option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a;
Scan.repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a;
Scan.lift;
Scan.optional;
Scan.lift : ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c);
Scan.lift (Parse.position Args.cartouche_input);
(* "parsers" are actually interpreters; an 'a parser is a function that parses
\<close>
text{* "parsers" are actually interpreters; an 'a parser is a function that parses
an input stream and computes(=evaluates, computes) it into 'a.
Since the semantics of an Isabelle command is a transition => transition
or theory \<Rightarrow> theory function, i.e. a global system transition.
parsers of that type can be constructed and be bound as call-back functions
to a table in the Toplevel-structure of Isar.
The type 'a parser is already defined in the structure Toekn.
*)
The type 'a parser is already defined in the structure Token.
*}
text{* Syntax operations : Interface for parsing, type-checking, "reading"
(both) and pretty-printing.
Note that this is a late-binding interface, i.e. a collection of "hooks".
The real work is done ... see below.
Encapsulates the data structure "syntax" --- the table with const symbols,
print and ast translations, ... The latter is accessible, e.g. from a Proof
context via Proof_Context.syn_of.
*}
ML\<open>
Parse.nat: int parser;
Parse.int: int parser;
Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser;
@ -192,75 +233,7 @@ Parse.position: 'a parser -> ('a * Position.T) parser;
(* Examples *)
Parse.position Args.cartouche_input;
(* More High-level, more Isar-specific Parsers *)
Args.name;
Args.const;
Args.cartouche_input: Input.source parser;
Args.text_token: Token.T parser;
val Z = let val attribute = Parse.position Parse.name --
Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ;
(* this leads to constructions like the following, where a parser for a *)
fn name => (Thy_Output.antiquotation name (Scan.lift (Parse.position Args.cartouche_input)));
\<close>
(* Bindings *)
ML\<open>val X = @{here};\<close>
(* Output: Very Low Level *)
ML\<open>
Output.output; (* output is the structure for the "hooks" with the target devices. *)
Output.output "bla_1:";
\<close>
ML\<open>
Thy_Output.verbatim_text;
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.antiquotation:
binding ->
'a context_parser ->
({context: Proof.context, source: Token.src, state: Toplevel.state} -> 'a -> string) ->
theory -> theory;
Thy_Output.output: Proof.context -> Pretty.T list -> string;
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.output : Proof.context -> Pretty.T list -> string;
\<close>
(* Context and Theory: *)
ML{*
Context.theory_name;
Theory.check;
Context.map_theory;
(* Theory.map_thy; *)
Theory.begin_theory;
Theory.check;
(* Outer_Syntax.pretty_command; not exported*)
Theory.setup; (* The thing to extend the table of "command"s with parser - callbacks. *)
*}
(* Syntax operations : Interface for parsing, type-checking, "reading"
(both) and pretty-printing.
Note that this is a late-binding interface, i.e. a collection of "hooks".
The real work is done ... see below.
Encapsulates the data structure "syntax" --- the table with const symbols,
print and ast translations, ... The latter is accessible, e.g. from a Proof
context via Proof_Context.syn_of.
*)
ML{*
Syntax.parse_sort;
Syntax.parse_typ;
@ -293,6 +266,65 @@ ML{*
fun read_terms ctxt =
grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt;
*}
ML\<open>
(* More High-level, more Isar-specific Parsers *)
Args.name;
Args.const;
Args.cartouche_input: Input.source parser;
Args.text_token: Token.T parser;
val Z = let val attribute = Parse.position Parse.name --
Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ;
(* this leads to constructions like the following, where a parser for a *)
fn name => (Thy_Output.antiquotation name (Scan.lift (Parse.position Args.cartouche_input)));
\<close>
subsection {* Output: Very Low Level *}
ML\<open>
Output.output; (* output is the structure for the "hooks" with the target devices. *)
Output.output "bla_1:";
\<close>
subsection {* Output: High Level *}
ML\<open>
Thy_Output.verbatim_text;
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.antiquotation:
binding ->
'a context_parser ->
({context: Proof.context, source: Token.src, state: Toplevel.state} -> 'a -> string) ->
theory -> theory;
Thy_Output.output: Proof.context -> Pretty.T list -> string;
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.output : Proof.context -> Pretty.T list -> string;
\<close>
section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *}
ML{*
open Context
*}
ML{*
Context.theory_name;
Theory.check;
Context.map_theory;
(* Theory.map_thy; *)
Theory.begin_theory;
Theory.check;
(* Outer_Syntax.pretty_command; not exported*)
Theory.setup; (* The thing to extend the table of "command"s with parser - callbacks. *)
*}
(*
Main phases of inner syntax processing, with standard implementations
@ -675,8 +707,38 @@ fun document_antiq check_file ctxt (name, pos) =
end;
*}
ML{* Type_Infer_Context.infer_types *}
ML{* Type_Infer_Context.prepare_positions *}
section {*Transaction Management in the Isar-Engine : The Toplevel *}
ML{* Type_Infer_Context.prepare_positions *}
ML{*
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.document_command;
Toplevel.exit: Toplevel.transition -> Toplevel.transition;
Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
Toplevel.ignored: Position.T -> Toplevel.transition;
Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition;
Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition;
Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
Toplevel.present_local_theory:
(xstring * Position.T) option ->
(Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
(* where text treatment and antiquotation parsing happens *)
(*fun document_command markdown (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
NONE => ignore (output_text state markdown txt)
| SOME (_, pos) =>
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *)
Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
Toplevel.transition -> Toplevel.transition;
*}
end

96
examples/simple/Article.thy
View File

@ -11,9 +11,67 @@ text*[tit::title]{* Using The Isabelle Ontology Framework*}
text*[stit::subtitle] \<open>Linking the Formal with the Informal\<close>
text*[auth1::author, affiliation="''University of Sheffield''"]\<open>Achim Brucker\<close>
text*[auth2::author, affiliation="''Centrale-Supelec''"]\<open>Idir Ait-Adune\<close>
text*[auth3::author, affiliation="''IRT-SystemX''"]\<open>Paolo Crizzifulli\<close>
text*[auth4::author, affiliation="''Universit\\'e Paris-Sud''"]\<open>Burkhart Wolff\<close>
text*[auth2::author, affiliation="''Centrale-Supelec''"] \<open>Idir Ait-Sadoune\<close>
text*[auth3::author, affiliation="''IRT-SystemX''"] \<open>Paolo Crisafulli\<close>
text*[auth4::author, affiliation="''Universit\\'e Paris-Sud''"]\<open>Burkhart Wolff\<close>
text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system
framework with many similarities to Eclipse; it is mostly known as part of
Isabelle/HOL, an interactive theorem proving and code generation environment.
Recently, an Document Ontology Framework has been developed as a plugin in
Isabelle/Isar, allowing to do both conventional typesetting \emph{as well}
as formal development. A particular asset is the possibility to control the links
between the formal and informal aspects of a document
via a modeling language for document ontologies and a (novel use of)
Isabelle's antiquotation mechanism. *}
section*[intro::introduction, comment="''This is a comment''"]{* Introduction *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,
phasellus amet id massa nunc, pede suscipit repellendus, in ut tortor eleifend augue
pretium consectetuer. Lectus accumsan velit ultrices, mauris amet, id elit aliquam aptent id,
felis duis. Mattis molestie semper gravida in ullamcorper ut, id accumsan, fusce id
sed nibh ut lorem integer, maecenas sed mi purus non nunc, morbi pretium tortor.*}
section* [bgrnd :: introduction] {* Background: Isabelle and Isabelle_DOF *}
text{* As mentioned in @{introduction \<open>intro\<close>} ... *}
(*update_instance*[bgrnd, main_author = "Some(''bu'')", formula="@{term ''a + b = b + a''}"] *)
update_instance*[bgrnd, comment2 = "''bu''"]
term scholarly_paper.introduction.comment2_update
ML{*
val thy = @{theory};
val oid = "bgrnd"
val (cid,value) = case DOF_core.get_object_global oid thy of
SOME{cid,value,...} => (cid, value)
| NONE => raise TERM("XX",[]);
val term'' = @{docitem_value \<open>bgrnd\<close>};
val term' = Sign.certify_term @{theory} value;
simplify;
*}
term "scholarly_paper.author.affiliation_update"
term "scholarly_paper.abstract.keyword_list_update"
term "scholarly_paper.introduction.comment2_update"
ML{* val a $ b $ c = @{term "X\<lparr>affiliation:='' ''\<rparr>"}; fold;
*}
ML{* !AnnoTextelemParser.SPY;
fun convert((Const(s,_),_), t) X = Const(s^"_update", dummyT)
$ Abs("uuu_", type_of t, t)
$ X
val base = @{term "undefined"}
val converts = fold convert (!AnnoTextelemParser.SPY) base
*}
term "\<lparr>author.tag_attribute=undefined,affiliation=undefined\<rparr>"
ML{* !AnnoTextelemParser.SPY *}
@ -28,40 +86,14 @@ ML{*
val x = @{code "HORX"}
*}
text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system
framework with many similarities to Eclipse; it is mostly known as part of
Isabelle/HOL, an interactive theorem proving and code generation environment.
Recently, an Document Ontology Framework has been developed as a plugin in
Isabelle/Isar, allowing to do both conventional typesetting \emph{as well}
as formal development. A particular asset is the possibility to control the links
between the formal and informal aspects of a document
via (a novel use of) Isabelle's antiquotation mechanism. *}
section*[intro::introduction, comment="''This is a comment''"]{* Introduction *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,
phasellus amet id massa nunc, pede suscipit repellendus, in ut tortor eleifend augue
pretium consectetuer. Lectus accumsan velit ultrices, mauris amet, id elit aliquam aptent id,
felis duis. Mattis molestie semper gravida in ullamcorper ut, id accumsan, fusce id
sed nibh ut lorem integer, maecenas sed mi purus non nunc, morbi pretium tortor.*}
section* [bgrnd :: text_section] {* Background: Isabelle and Isabelle_DOF *}
text{* As mentioned in @{introduction \<open>intro\<close>} ... *}
term "a + b = b + a"
(*
@{term ''a + b = b + a''}
@{typ ''a list''}
@{thm ''refl''}
@{thms ''[refl,sym]''}
*)
update_instance*[bgrnd, main_author = "Some(''bu'')", formula="@{term ''a + b = b + a''}"]
term related_work.main_author_update
section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*}
text*[x]{* @{technical \<open>ontomod\<close>} *}
text*[x]{* @{technical \<open>ontomod\<close>} @{technical \<open>bgrnd\<close>}*}
subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood. @{technical \<open>ontomod\<close>} *}
text{* @{technical \<open>ontomod\<close>}*}

21
ontologies/scholarly_paper.thy
View File

@ -13,20 +13,29 @@ doc_class subtitle =
-- \<open>adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \<close>
doc_class author =
email :: "string"
orcid :: "string option" <= "None"
affiliation :: "string"
doc_class abstract =
keyword_list :: "string list" <= "[]"
doc_class text_section =
main_author :: "author option" <= None
(*
doc_class text_section =
main_author :: "string option" <= None
*)
doc_class introduction = text_section +
comment :: string
comment2 :: string
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
formula :: "term list"
text{* A very rough formatting style could be modeled as follows:*}
datatype mesure = points "int" | inch "int" | textwidth "int" (* given by the inverse of the integer *)
@ -81,9 +90,11 @@ text{* Besides subtyping, there is another relation between
text{* @{cite bla} *}
doc_class article =
trace :: "(title + subtitle + author+ abstract +
introduction + technical + example +
conclusion + bibliography) list"
style_id :: string <= "''LNCS''"
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
trace :: "(title + subtitle + author+ abstract +
introduction + technical + example +
conclusion + bibliography) list"
where "(title ~
[subtitle] ~
(author)+ ~