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

eager-and-lazy-elaboration #17

Merged
nicolas.meric merged 4 commits from nicolas.meric/Isabelle_DOF:eager-and-lazy-elaboration into main 2022-03-30 06:48:33 +00:00
Conversation 0 Commits 4 Files Changed 7 +250 -361
7 changed files with 250 additions and 361 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -324,21 +324,28 @@ is currently only available in the SML API's of the kernel.
as specified in @{technical \<open>odl-manual0\<close>}. as specified in @{technical \<open>odl-manual0\<close>}.
\<^item> \<open>meta_args\<close> : \<^item> \<open>meta_args\<close> :
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close> \<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
\<^item> \<^emph>\<open>evaluator\<close>: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML,
falling back to normalization by evaluation if this fails. Alternatively a specific
evaluator can be selected using square brackets; typical evaluators use the
current set of code equations to normalize and include \<open>simp\<close> for fully
symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
\<^item> \<open>upd_meta_args\<close> : \<^item> \<open>upd_meta_args\<close> :
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close> \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
\<^item> \<open>annotated_text_element\<close> : \<^item> \<open>annotated_text_element\<close> :
\<^rail>\<open> \<^rail>\<open>
( ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>' ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
| @@{command "ML*"} ('[' meta_args ']')? '\<open>' SML_code '\<close>' | @@{command "ML*"} ('[' meta_args ']')? '\<open>' SML_code '\<close>'
| @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>' | @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
| @@{command "value*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>' | @@{command "value*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
) | @@{command "assert*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
| )
( @@{command "open_monitor*"} \<close>
\<^rail>\<open>
( @@{command "open_monitor*"}
| @@{command "close_monitor*"} | @@{command "close_monitor*"}
| @@{command "declare_reference*"} | @@{command "declare_reference*"}
) '[' meta_args ']' ) '[' meta_args ']'
)
| change_status_command | change_status_command
| inspection_command | inspection_command
| macro_command | macro_command
@ -399,23 +406,35 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command. \<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
\<close> \<close>
(*<*)
declare_reference*["text-elements-expls"::technical]
(*>*)
subsection\<open>Ontological Term-Contexts and their Management\<close> subsection\<open>Ontological Term-Contexts and their Management\<close>
text\<open>The major commands providing term-contexts are text\<open>The major commands providing term-contexts are
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and \<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>. \<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
\<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
Wrt. creation, track-ability and checking they are analogous to the ontological text and Wrt. creation, track-ability and checking they are analogous to the ontological text and
code-commands. However the argument terms may contain term-antiquotations stemming from an code-commands. However the argument terms may contain term-antiquotations stemming from an
ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
to a meta-object belonging to the document class \<open>A\<close>, for example). to a meta-object belonging to the document class \<open>A\<close>, for example).
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting (\<^eg> replaced) by a term denoting the meta-object.
This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
executable HOL-functions to interact with meta-objects. executable HOL-functions to interact with meta-objects.
The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context
(see @{technical (unchecked) \<open>text-elements-expls\<close>}).
% TODO:
% Section reference @{docitem (unchecked) \<open>text-elements-expls\<close>} has not the right number
This is particularly useful to explore formal definitions wrt. their border cases.
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof> Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
of this meta-object. The latter leads to a failure of the entire command. of this meta-object. The latter leads to a failure of the entire command.
\<close> \<close>
(*<*) (*<*)
@ -619,9 +638,6 @@ during the editing process but is only visible in the integrated source but usua
a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each
document class also a class-type which is declared in the HOL environment.\<close> document class also a class-type which is declared in the HOL environment.\<close>
(*<*)
declare_reference*["text-elements-expls"::example]
(*>*)
text*[s23::example, main_author = "Some(@{author \<open>bu\<close>})"]\<open> text*[s23::example, main_author = "Some(@{author \<open>bu\<close>})"]\<open>
Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example, Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
this may be for a text fragment like this may be for a text fragment like
@ -649,7 +665,7 @@ of the \<^isadof> language:
\<newline> \<newline>
'[' meta_args ']' '\<open>' text '\<close>' '[' meta_args ']' '\<open>' text '\<close>'
) )
| @@{command "assert*"} '[' meta_args ']' '\<open>' term '\<close>'
\<close> \<close>
\<close> \<close>
@ -680,14 +696,13 @@ text\<open>
\<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>: \<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
title*[title::title]\<open>Isabelle/DOF\<close> title*[title::title]\<open>Isabelle/DOF\<close>
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close> subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>", author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>", orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close> affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
author*[bu::author, email = "\<open>wolff@lri.fr\<close>", author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close> affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>\<close>}
\<close>}
\<close> \<close>
@ -701,8 +716,7 @@ text\<open>We want to check the consequences of this definition and can add the
text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed
the last element of a list.\<close> the last element of a list.\<close>
assert*[claim1::assertion] \<open>last[4::int] = 4\<close> assert*[claim1::assertion] \<open>last[4::int] = 4\<close>
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close> assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>\<close>}
\<close>}
\<close> \<close>
text\<open> text\<open>
@ -714,14 +728,12 @@ However, in order to avoid the somewhat tedious consequence:
the choice of the default class can be influenced by setting globally an attribute such as the choice of the default class can be influenced by setting globally an attribute such as
@{boxed_theory_text [display] @{boxed_theory_text [display]
\<open>declare[[ Definition_default_class = "definition"]] \<open>declare[[Definition_default_class = "definition"]]
declare[[ Theorem_default_class = "theorem"]] declare[[Theorem_default_class = "theorem"]]\<close>}
\<close>}
which allows the above example be shortened to: which allows the above example be shortened to:
@{boxed_theory_text [display] @{boxed_theory_text [display]
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close> \<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>\<close>}
\<close>}
\<close> \<close>
subsection\<open>The Ontology \<^verbatim>\<open>technical_report\<close>\<close> subsection\<open>The Ontology \<^verbatim>\<open>technical_report\<close>\<close>
@ -993,8 +1005,8 @@ text\<open>
entities, \<^eg>, \<^ML_type>\<open>term\<close> (\<open>\<lambda>\<close>-term), \<^ML_type>\<open>typ\<close>, or entities, \<^eg>, \<^ML_type>\<open>term\<close> (\<open>\<lambda>\<close>-term), \<^ML_type>\<open>typ\<close>, or
\<^ML_type>\<open>thm\<close>, we represent the types of the implementation language \<^ML_type>\<open>thm\<close>, we represent the types of the implementation language
\<^emph>\<open>inside\<close> the HOL type system. We do, however, not reflect the data of \<^emph>\<open>inside\<close> the HOL type system. We do, however, not reflect the data of
these types. They are just declared abstract types, these types. They are just types declared in HOL,
``inhabited'' by special constant symbols carrying strings, for which are ``inhabited'' by special constant symbols carrying strings, for
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>. example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
% TODO: % TODO:
% Update meta-types implementation explanation to the new implementation % Update meta-types implementation explanation to the new implementation

BIN
src/DOF/.Isa_DOF.thy.marks Normal file
View File

Binary file not shown.

82
src/DOF/Assert.thy
View File

@ -1,82 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
section \<open> Little theory implementing the an assertion command in Isabelle/HOL. \<close>
text\<open>This command is useful for certification documents allowing to validate
corner-cases of (executable) definitions. \<close>
theory Assert
imports Main
keywords "assert" ::thy_decl
begin
subsection\<open>Core\<close>
ML\<open>
local
(* Reimplementation needed because not exported from ML structure Value_Command *)
fun value_maybe_select some_name =
case some_name
of NONE => Value_Command.value
| SOME name => Value_Command.value_select name;
in
(* Reimplementation needed because not exported from ML structure Value_Command *)
val opt_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
(* Reimplementation needed because not exported from ML structure Value_Command *)
val opt_evaluator =
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
(* Reimplementation structure Value_Command due to tiny modification of value_cmd. *)
fun assert_cmd some_name modes raw_t ctxt (* state*) =
let
(* val ctxt = Toplevel.context_of state; *)
val t = Syntax.read_term ctxt raw_t;
val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Proof_Context.augment t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
val _ =
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) =>
Toplevel.keep ( (assert_cmd some_name modes t) o Toplevel.context_of) ));
end
\<close>
subsection\<open> Test: \<close>
(*
assert ""
assert "3 = 4"
assert "False"
assert "5 * 5 = 25"
*)
subsection\<open>Example\<close>
assert "True \<and> True "
assert "(5::int) * 5 = 25 "
end

70
src/DOF/AssertLong.thy
View File

@ -1,70 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
theory AssertLong
imports Main
keywords "assert" ::thy_decl
begin
ML\<open>
fun value_maybe_select some_name =
case some_name
of NONE => Value_Command.value
| SOME name => Value_Command.value_select name;
val TT = Unsynchronized.ref (HOLogic.boolT);
fun value_cmd2 some_name modes raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val t' = case ty' of @{typ "bool"} => t' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Variable.auto_fixes t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
\<close>
ML\<open>value_cmd2\<close>
definition ASSERT :: "bool \<Rightarrow> bool" where "ASSERT p == (p=True)"
ML\<open>val x = @{code "ASSERT"}\<close>
ML\<open>
val opt_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
val opt_evaluator =
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
val _ =
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) =>
let val _ = writeln t in
(* Toplevel.keep (Value_Command.value_cmd some_name modes (enclose "ASSERT(" ")" t)) *)
Toplevel.keep (value_cmd2 some_name modes t)
end));
\<close>
assert "True"
assert "True \<and> True "
ML\<open>!TT ;
@{term "True"}\<close>

317
src/DOF/Isa_DOF.thy
View File

@ -31,7 +31,6 @@ that provide direct support in the PIDE framework. \<close>
theory Isa_DOF (* Isabelle Document Ontology Framework *) theory Isa_DOF (* Isabelle Document Ontology Framework *)
imports Main imports Main
RegExpInterface (* Interface to functional regular automata for monitoring *) RegExpInterface (* Interface to functional regular automata for monitoring *)
Assert
keywords "+=" ":=" "accepts" "rejects" "invariant" keywords "+=" ":=" "accepts" "rejects" "invariant"
@ -42,7 +41,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
"define_shortcut*" "define_macro*" :: thy_decl "define_shortcut*" "define_macro*" :: thy_decl
and "text*" "text-macro*" :: document_body and "text*" "text-macro*" :: document_body
and "term*" "value*" :: diag and "term*" "value*" "assert*" :: diag
and "print_doc_classes" "print_doc_items" and "print_doc_classes" "print_doc_items"
"print_doc_class_template" "check_doc_global" :: diag "print_doc_class_template" "check_doc_global" :: diag
@ -185,6 +184,7 @@ struct
type docobj = {pos : Position.T, type docobj = {pos : Position.T,
thy_name : string, thy_name : string,
input_term : term,
value : term, value : term,
inline : bool, inline : bool,
id : serial, id : serial,
@ -613,11 +613,12 @@ fun get_value_local oid ctxt = case get_object_local oid ctxt of
| NONE => NONE | NONE => NONE
(* missing : setting terms to ground (no type-schema vars, no schema vars. )*) (* missing : setting terms to ground (no type-schema vars, no schema vars. )*)
fun update_value_global oid upd thy = fun update_value_global oid upd_input_term upd_value thy =
case get_object_global oid thy of case get_object_global oid thy of
SOME{pos,thy_name,value,inline,id,cid,vcid} => SOME{pos,thy_name, input_term, value,inline,id,cid,vcid} =>
let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name,
value=upd value,id=id, input_term=upd_input_term input_term,
value=upd_value value,id=id,
inline=inline,cid=cid, vcid=vcid}) inline=inline,cid=cid, vcid=vcid})
in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end
| NONE => error("undefined doc object: "^oid) | NONE => error("undefined doc object: "^oid)
@ -701,60 +702,10 @@ fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt)
fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt)
in writeln (String.concatWith "," (Symtab.keys tab)) end in writeln (String.concatWith "," (Symtab.keys tab)) end
fun print_doc_items b ctxt =
let val {docobj_tab={tab = x, ...},...}= get_data ctxt;
val _ = writeln "=====================================";
fun dfg true = "true"
|dfg false= "false"
fun print_item (n, SOME({cid,vcid,id,pos,thy_name,inline,value})) =
(writeln ("docitem: "^n);
writeln (" type: "^cid);
case vcid of NONE => () | SOME (s) =>
writeln (" virtual type: "^ s);
writeln (" origine: "^thy_name);
writeln (" inline: "^dfg inline);
writeln (" value: "^(Syntax.string_of_term ctxt value))
)
| print_item (n, NONE) =
(writeln ("forward reference for docitem: "^n));
in map print_item (Symtab.dest x);
writeln "=====================================\n\n\n" end;
fun print_docclass_template cid ctxt =
let val cid_long = read_cid ctxt cid (* assure that given cid is really a long_cid *)
val brute_hierarchy = (get_attributes_local cid_long ctxt)
val flatten_hrchy = flat o (map(fn(lname, attrS) =>
map (fn (s,_,_)=>(lname,(Binding.name_of s))) attrS))
fun filter_overrides [] = []
|filter_overrides ((ln,s)::S) = (ln,s):: filter_overrides(filter(fn(_,s')=> s<>s')S)
val hierarchy = map (fn(ln,s)=>ln^"."^s)(filter_overrides(flatten_hrchy brute_hierarchy))
val args = String.concatWith "=%\n , " (" label=,type":: hierarchy);
val template = "\\newisadof{"^cid_long^"}%\n["^args^"=%\n][1]\n{%\n#1%\n}\n\n";
in writeln template end;
fun print_doc_classes b ctxt =
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
val _ = writeln "=====================================";
fun print_attr (n, ty, NONE) = (Binding.print n)
| print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")")
fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm)
fun print_virtual {virtual} = Bool.toString virtual
fun print_class (n, {attribute_decl, id, inherits_from, name, virtual, params, thy_name, rejectS, rex,invs}) =
(case inherits_from of
NONE => writeln ("docclass: "^n)
| SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + ");
writeln (" name: "^(Binding.print name));
writeln (" virtual: "^(print_virtual virtual));
writeln (" origin: "^thy_name);
writeln (" attrs: "^commas (map print_attr attribute_decl));
writeln (" invs: "^commas (map print_inv invs))
);
in map print_class (Symtab.dest docclass_tab);
writeln "=====================================\n\n\n"
end;
fun print_doc_class_tree ctxt P T = fun print_doc_class_tree ctxt P T =
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt; let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
val class_tab:(string * docclass_struct)list = (Symtab.dest docclass_tab) val class_tab:(string * docclass_struct)list = (Symtab.dest docclass_tab)
@ -769,38 +720,7 @@ fun print_doc_class_tree ctxt P T =
in ".0 .\n" ^ tree 1 roots end in ".0 .\n" ^ tree 1 roots end
val (strict_monitor_checking, strict_monitor_checking_setup)
fun check_doc_global (strict_checking : bool) ctxt =
let val {docobj_tab={tab = x, ...}, monitor_tab, ...} = get_data ctxt;
val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x)
val T = map fst (Symtab.dest monitor_tab)
in if null S
then if null T then ()
else error("Global consistency error - there are open monitors: "
^ String.concatWith "," T)
else error("Global consistency error - Unresolved forward references: "
^ String.concatWith "," S)
end
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_doc_classes\<close> "print document classes"
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_doc_class_template\<close>
"print document class latex template"
(Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_doc_items\<close> "print document items"
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>check_doc_global\<close> "check global document consistency"
(Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of)));
val (strict_monitor_checking, strict_monitor_checking_setup)
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false); = Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
val (invariants_checking, invariants_checking_setup) val (invariants_checking, invariants_checking_setup)
@ -1051,7 +971,6 @@ fun elaborate_instance thy _ _ term_option pos =
| SOME(value) => | SOME(value) =>
DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy
end end
(*DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy*)
(* (*
The function declare_ISA_class_accessor_and_check_instance uses a prefix The function declare_ISA_class_accessor_and_check_instance uses a prefix
@ -1323,7 +1242,8 @@ fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),so
fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term]) fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term])
fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) term = fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
(S:(string * Position.T * string * term)list) term =
let val cid_ty = cid_2_cidType cid_long thy let val cid_ty = cid_2_cidType cid_long thy
val generalize_term = Term.map_types (generalize_typ 0) val generalize_term = Term.map_types (generalize_typ 0)
fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t
@ -1357,7 +1277,8 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
|join _ = error("implicit fusion operation not defined for attribute: "^ lhs) |join _ = error("implicit fusion operation not defined for attribute: "^ lhs)
(* could be extended to bool, map, multisets, ... *) (* could be extended to bool, map, multisets, ... *)
val rhs' = instantiate_term tyenv' (generalize_term rhs) val rhs' = instantiate_term tyenv' (generalize_term rhs)
val rhs'' = DOF_core.transduce_term_global {mk_elaboration=false} (rhs',pos) thy val rhs'' = DOF_core.transduce_term_global {mk_elaboration=mk_elaboration}
(rhs',pos) thy
in case opr of in case opr of
"=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term "=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term
| ":=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term | ":=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term
@ -1402,7 +1323,11 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
val assns' = map conv_attrs trace_attr val assns' = map conv_attrs trace_attr
fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy)) fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy))
fun def_trans oid = #1 o (calc_update_term thy (cid_of oid) assns') fun def_trans_input_term oid =
#1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns')
fun def_trans_value oid =
#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
(* check that any transition is possible : *) (* check that any transition is possible : *)
@ -1414,7 +1339,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
in Symtab.update(n, {accepted_cids=accepted_cids, in Symtab.update(n, {accepted_cids=accepted_cids,
rejected_cids=rejected_cids, rejected_cids=rejected_cids,
automatas=aS}) tab end automatas=aS}) tab end
fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans mon_oid) fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid)
val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS)
in thy |> (* update traces of all enabled monitors *) in thy |> (* update traces of all enabled monitors *)
fold (update_trace) (enabled_monitors) fold (update_trace) (enabled_monitors)
@ -1492,8 +1417,10 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
| SOME (cid,_) => if (DOF_core.is_virtual cid thy) | SOME (cid,_) => if (DOF_core.is_virtual cid thy)
then SOME (DOF_core.parse_cid_global thy cid) then SOME (DOF_core.parse_cid_global thy cid)
else NONE else NONE
val value_term = if (cid_long = DOF_core.default_cid) val value_terms = if (cid_long = DOF_core.default_cid)
then (Free ("Undefined_Value", @{typ "unit"})) then let
val undefined_value = Free ("Undefined_Value", @{typ "unit"})
in (undefined_value, undefined_value) end
(* (*
Handle initialization of docitem without a class associated, Handle initialization of docitem without a class associated,
for example when you just want a document element to be referenceable for example when you just want a document element to be referenceable
@ -1504,21 +1431,26 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
val defaults_init = create_default_object thy cid_long val defaults_init = create_default_object thy cid_long
fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term); fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term);
val S = map conv (DOF_core.get_attribute_defaults cid_long thy); val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init; val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false}
thy cid_long S defaults_init;
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs val assns' = map conv_attrs doc_attrs
val (value_term', _(*ty*), _) = calc_update_term thy cid_long assns' defaults val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false}
in value_term' end thy cid_long assns' defaults
val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
thy cid_long assns' defaults
in (input_term, value_term') end
val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor)
o Context.Theory o Context.Theory
in thy |> DOF_core.define_object_global (oid, {pos = pos, in thy |> DOF_core.define_object_global (oid, {pos = pos,
thy_name = Context.theory_name thy, thy_name = Context.theory_name thy,
value = value_term, input_term = fst value_terms,
inline = is_inline, value = snd value_terms,
id = id, inline = is_inline,
cid = cid_long, id = id,
vcid = vcid}) cid = cid_long,
vcid = vcid})
|> register_oid_cid_in_open_monitors oid pos cid_long |> register_oid_cid_in_open_monitors oid pos cid_long
|> (fn thy => (check_inv thy; thy)) |> (fn thy => (check_inv thy; thy))
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
@ -1546,12 +1478,15 @@ fun update_instance_command (((oid:string,pos),cid_pos),
fun conv_attrs (((lhs, pos), opn), rhs) = ((markup2string lhs),pos,opn, fun conv_attrs (((lhs, pos), opn), rhs) = ((markup2string lhs),pos,opn,
Syntax.read_term_global thy rhs) Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs val assns' = map conv_attrs doc_attrs
val def_trans = (#1 o (calc_update_term thy cid_long assns')) val def_trans_input_term =
#1 o (calc_update_term {mk_elaboration=false} thy cid_long assns')
val def_trans_value =
#1 o (calc_update_term {mk_elaboration=true} thy cid_long assns')
fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false}
o Context.Theory ) thy ; o Context.Theory ) thy ;
thy) thy)
in in
thy |> DOF_core.update_value_global oid (def_trans) thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value
|> check_inv |> check_inv
end end
@ -1831,7 +1766,6 @@ end
\<close> \<close>
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close> ML \<comment> \<open>c.f. \<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close>
(* (*
The value* command uses the same code as the value command The value* command uses the same code as the value command
@ -1848,9 +1782,10 @@ Generic value command for arbitrary evaluators, with default using nbe or SML.
signature VALUE_COMMAND = signature VALUE_COMMAND =
sig sig
val value: Proof.context -> term -> term val value: Proof.context -> term -> term
val value_without_elaboration: Proof.context -> term -> term
val value_select: string -> Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term
val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string val value_cmd: {assert: bool} -> (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string
-> Toplevel.state -> Toplevel.transition -> unit -> Toplevel.state -> Position.T -> unit
val add_evaluator: binding * (Proof.context -> term -> term) val add_evaluator: binding * (Proof.context -> term -> term)
-> theory -> string * theory -> theory -> string * theory
end; end;
@ -1863,7 +1798,6 @@ structure Evaluators = Theory_Data
( (
type T = (Proof.context -> term -> term) Name_Space.table; type T = (Proof.context -> term -> term) Name_Space.table;
val empty = Name_Space.empty_table "evaluator"; val empty = Name_Space.empty_table "evaluator";
val extend = I;
val merge = Name_Space.merge_tables; val merge = Name_Space.merge_tables;
) )
@ -1892,22 +1826,34 @@ fun value_select name ctxt =
fun value ctxt term = value_select "" ctxt fun value ctxt term = value_select "" ctxt
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>) (DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
(Proof_Context.theory_of ctxt)) (Proof_Context.theory_of ctxt))
val value_without_elaboration = value_select ""
fun meta_args_exec NONE thy = thy fun meta_args_exec NONE thy = thy
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy = |meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
thy |> (ODL_Command_Parser.create_and_check_docitem thy |> (ODL_Command_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false} {is_monitor = false} {is_inline = false}
oid pos (I cid_pos) (I doc_attrs)) oid pos (I cid_pos) (I doc_attrs))
fun value_cmd meta_args_opt raw_name modes raw_t state trans = fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t state pos =
let let
val _ = meta_args_exec meta_args_opt val _ = meta_args_exec meta_args_opt
val ctxt = Toplevel.context_of state; val ctxt = Toplevel.context_of state;
val name = intern_evaluator ctxt raw_name; val name = intern_evaluator ctxt raw_name;
val t = Syntax.read_term ctxt raw_t; val t = Syntax.read_term ctxt raw_t;
val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , Toplevel.pos_of trans) val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos)
(Proof_Context.theory_of ctxt); (Proof_Context.theory_of ctxt);
val t' = value_select name ctxt term'; val t' = value_select name ctxt term';
val ty' = Term.type_of t'; val ty' = Term.type_of t';
val ty' = if assert
then case ty' of
\<^typ>\<open>bool\<close> => ty'
| _ => error "Assertion expressions must be boolean."
else ty'
val t' = if assert
then case t' of
\<^term>\<open>True\<close> => t'
| _ => error "Assertion failed."
else t'
val ctxt' = Proof_Context.augment t' ctxt; val ctxt' = Proof_Context.augment t' ctxt;
val p = Print_Mode.with_modes modes (fn () => val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
@ -1928,8 +1874,16 @@ val opt_evaluator =
val opt_attributes = Scan.option ODL_Command_Parser.attributes val opt_attributes = Scan.option ODL_Command_Parser.attributes
fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans =
Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state trans) trans let val pos = Toplevel.pos_of trans
in
Toplevel.keep (fn state => value_cmd {assert=false} meta_args_opt name modes t state pos) trans
end
fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans =
let val pos = Toplevel.pos_of trans
in
Toplevel.keep (fn state => value_cmd {assert=true} meta_args_opt name modes t state pos) trans
end
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/isar_cmd.ML\<close>\<close> \<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/isar_cmd.ML\<close>\<close>
(* (*
@ -1937,13 +1891,13 @@ fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans =
and adds the possibility to check Term Annotation Antiquotations (TA) and adds the possibility to check Term Annotation Antiquotations (TA)
with the help of DOF_core.transduce_term_global function with the help of DOF_core.transduce_term_global function
*) *)
fun string_of_term meta_args_opt ctxt s trans = fun string_of_term meta_args_opt ctxt s pos =
let let
val _ = meta_args_exec meta_args_opt val _ = meta_args_exec meta_args_opt
val t = Syntax.read_term ctxt s; val t = Syntax.read_term ctxt s;
val T = Term.type_of t; val T = Term.type_of t;
val ctxt' = Proof_Context.augment t ctxt; val ctxt' = Proof_Context.augment t ctxt;
val _ = DOF_core.transduce_term_global {mk_elaboration=false} (t , Toplevel.pos_of trans) val _ = DOF_core.transduce_term_global {mk_elaboration=false} (t , pos)
(Proof_Context.theory_of ctxt'); (Proof_Context.theory_of ctxt');
in in
Pretty.string_of Pretty.string_of
@ -1958,11 +1912,14 @@ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
We want to have the current position to pass it to transduce_term_global in We want to have the current position to pass it to transduce_term_global in
string_of_term, so we pass the Toplevel.transition string_of_term, so we pass the Toplevel.transition
*) *)
fun print_term meta_args_opt (string_list, string) trans = print_item fun print_term meta_args_opt (string_list, string) trans =
(fn state => let
fn string => val pos = Toplevel.pos_of trans
string_of_term meta_args_opt (Toplevel.context_of state) string trans) in
(string_list, string) trans; print_item (fn state =>
fn string => string_of_term meta_args_opt (Toplevel.context_of state) string pos)
(string_list, string) trans
end
val _ = val _ =
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term" Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
@ -1983,9 +1940,102 @@ val _ = Theory.setup
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd #> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd); #> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>assert*\<close> "evaluate and assert term"
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
>> (fn (meta_args_opt, eval_args ) => pass_trans_to_assert_value_cmd meta_args_opt eval_args));
end; end;
\<close> \<close>
ML\<open>
fun print_doc_classes b ctxt =
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = DOF_core.get_data ctxt;
val _ = writeln "=====================================";
fun print_attr (n, ty, NONE) = (Binding.print n)
| print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")")
fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm)
fun print_virtual {virtual} = Bool.toString virtual
fun print_class (n, {attribute_decl, id, inherits_from, name, virtual, params, thy_name, rejectS, rex,invs}) =
(case inherits_from of
NONE => writeln ("docclass: "^n)
| SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + ");
writeln (" name: "^(Binding.print name));
writeln (" virtual: "^(print_virtual virtual));
writeln (" origin: "^thy_name);
writeln (" attrs: "^commas (map print_attr attribute_decl));
writeln (" invs: "^commas (map print_inv invs))
);
in map print_class (Symtab.dest docclass_tab);
writeln "=====================================\n\n\n"
end;
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_doc_classes\<close> "print document classes"
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of)));
fun print_docclass_template cid ctxt =
let val cid_long = DOF_core.read_cid ctxt cid (* assure that given cid is really a long_cid *)
val brute_hierarchy = (DOF_core.get_attributes_local cid_long ctxt)
val flatten_hrchy = flat o (map(fn(lname, attrS) =>
map (fn (s,_,_)=>(lname,(Binding.name_of s))) attrS))
fun filter_overrides [] = []
|filter_overrides ((ln,s)::S) = (ln,s):: filter_overrides(filter(fn(_,s')=> s<>s')S)
val hierarchy = map (fn(ln,s)=>ln^"."^s)(filter_overrides(flatten_hrchy brute_hierarchy))
val args = String.concatWith "=%\n , " (" label=,type":: hierarchy);
val template = "\\newisadof{"^cid_long^"}%\n["^args^"=%\n][1]\n{%\n#1%\n}\n\n";
in writeln template end;
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_doc_class_template\<close>
"print document class latex template"
(Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of)));
fun print_doc_items b ctxt =
let val {docobj_tab={tab = x, ...},...}= DOF_core.get_data ctxt;
val _ = writeln "=====================================";
fun dfg true = "true"
|dfg false= "false"
fun print_item (n, SOME({cid,vcid,id,pos,thy_name,inline, input_term, value})) =
(writeln ("docitem: "^n);
writeln (" type: "^cid);
case vcid of NONE => () | SOME (s) =>
writeln (" virtual type: "^ s);
writeln (" origine: "^thy_name);
writeln (" inline: "^dfg inline);
writeln (" input_term: "
^ (Syntax.string_of_term
ctxt (Value_Command.value_without_elaboration ctxt input_term)));
writeln (" value: "
^ (Syntax.string_of_term
ctxt (Value_Command.value_without_elaboration ctxt value)))
)
| print_item (n, NONE) =
(writeln ("forward reference for docitem: "^n));
in map print_item (Symtab.dest x);
writeln "=====================================\n\n\n" end;
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_doc_items\<close> "print document items"
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of)));
fun check_doc_global (strict_checking : bool) ctxt =
let val {docobj_tab={tab = x, ...}, monitor_tab, ...} = DOF_core.get_data ctxt;
val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x)
val T = map fst (Symtab.dest monitor_tab)
in if null S
then if null T then ()
else error("Global consistency error - there are open monitors: "
^ String.concatWith "," T)
else error("Global consistency error - Unresolved forward references: "
^ String.concatWith "," S)
end
val _ =
Outer_Syntax.command \<^command_keyword>\<open>check_doc_global\<close> "check global document consistency"
(Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of)));
\<close>
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close> \<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
(* (*
@ -2018,7 +2068,6 @@ val _ =
end end
\<close> \<close>
ML\<open> ML\<open>
structure ODL_LTX_Converter = structure ODL_LTX_Converter =
struct struct
@ -2208,25 +2257,9 @@ val basic_entity = Document_Output.antiquotation_pretty_source
: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; : binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory;
fun symbex_attr_access0 ctxt proj_term term = fun symbex_attr_access0 ctxt proj_term term =
(* term assumed to be ground type, (f term) not necessarily *) let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term]
let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term] in Value_Command.value ctxt (subterm') end
val ty = type_of (subterm')
(* Debug :
val _ = writeln ("calculate_attr_access raw term: "
^ Syntax.string_of_term ctxt subterm')
*)
val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT)
$ subterm'
$ Free("_XXXXXXX", ty))
val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term')));
in case HOLogic.dest_Trueprop (Thm.concl_of thm) of
Free("_XXXXXXX", @{typ "bool"}) => @{const "True"}
| @{const "HOL.Not"} $ Free("_XXXXXXX", @{typ "bool"}) => @{const "False"}
| Const(@{const_name "HOL.eq"},_) $ lhs $ Free("_XXXXXXX", _ )=> lhs
| Const(@{const_name "HOL.eq"},_) $ Free("_XXXXXXX", _ ) $ rhs => rhs
| _ => error ("could not reduce attribute term: " ^
Syntax.string_of_term ctxt subterm')
end
fun compute_attr_access ctxt attr oid pos pos' = (* template *) fun compute_attr_access ctxt attr oid pos pos' = (* template *)
case DOF_core.get_value_global oid (Context.theory_of ctxt) of case DOF_core.get_value_global oid (Context.theory_of ctxt) of
@ -2242,6 +2275,7 @@ fun compute_attr_access ctxt attr oid pos pos' = (* template *)
^ oid ^ Position.here pos) ^ oid ^ Position.here pos)
val proj_term = Const(long_name,dummyT --> ty) val proj_term = Const(long_name,dummyT --> ty)
in symbex_attr_access0 ctxt proj_term term end in symbex_attr_access0 ctxt proj_term term end
(*in Value_Command.value ctxt term end*)
| NONE => error("identifier not a docitem reference" ^ Position.here pos) | NONE => error("identifier not a docitem reference" ^ Position.here pos)
@ -2399,7 +2433,8 @@ fun define_inv cid_long ((lbl, pos), inv) thy =
then Free (s, class_scheme_ty) then Free (s, class_scheme_ty)
else Free (s, ty) else Free (s, ty)
| update_attribute_type _ _ t = t | update_attribute_type _ _ t = t
val inv_ty = Syntax.read_typ (Proof_Context.init_global thy) ("'a " ^ cid_long ^ schemeN) val inv_ty = Syntax.read_typ (Proof_Context.init_global thy)
(Name.aT ^ " " ^ cid_long ^ schemeN)
(* Update the type of each attribute update function to match the type of the (* Update the type of each attribute update function to match the type of the
current class. *) current class. *)
val inv_term' = update_attribute_type thy inv_ty inv_term val inv_term' = update_attribute_type thy inv_ty inv_term

34
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -17,8 +17,6 @@ theory scholarly_paper
imports "../../DOF/Isa_COL" imports "../../DOF/Isa_COL"
keywords "author*" "abstract*" keywords "author*" "abstract*"
"Definition*" "Lemma*" "Theorem*" :: document_body "Definition*" "Lemma*" "Theorem*" :: document_body
and "assert*" :: thy_decl
begin begin
@ -347,39 +345,7 @@ doc_class assertion = math_formal +
properties :: "term list" properties :: "term list"
ML\<open>
(* TODO : Rework this code and make it closer to Definition*. There is still
a rest of "abstract classes in it: any class possessing a properties attribute
is admissible to this command, not just ... *)
local open ODL_Command_Parser in
fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
prop) =
let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy))
fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]")
::doc_attrs
fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
fun mks thy = case DOF_core.get_object_global_opt oid thy of
SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
| SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
| NONE => (create_and_check_docitem
{is_monitor = false} {is_inline = false}
oid pos cid_pos (conv_attrs thy) thy)
val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global
in
(* Toplevel.keep (check o Toplevel.context_of) *)
Toplevel.theory (fn thy => (check thy; mks thy))
end
val attributes = attributes (* re-export *)
end
val _ =
Outer_Syntax.command @{command_keyword "assert*"}
"evaluate and print term"
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
\<close>
subsubsection*[ex_ass::example]\<open>Example\<close> subsubsection*[ex_ass::example]\<open>Example\<close>
text\<open>Assertions allow for logical statements to be checked in the global context). \<close> text\<open>Assertions allow for logical statements to be checked in the global context). \<close>

32
src/tests/Evaluation.thy
View File

@ -6,6 +6,7 @@ theory
Evaluation Evaluation
imports imports
"Isabelle_DOF-tests.TermAntiquotations" "Isabelle_DOF-tests.TermAntiquotations"
"Isabelle_DOF-tests.High_Level_Syntax_Invariants"
begin begin
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close> section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
@ -84,8 +85,8 @@ value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
text\<open>If the attribute of the instance is not initialized, we get an undefined value, text\<open>If the attribute of the instance is not initialized, we get an undefined value,
whose type is the type of the attribute:\<close> whose type is the type of the attribute:\<close>
term*\<open>level @{C \<open>xcv2\<close>}\<close> term*\<open>B.level @{C \<open>xcv2\<close>}\<close>
value*\<open>level @{C \<open>xcv2\<close>}\<close> value*\<open>B.level @{C \<open>xcv2\<close>}\<close>
text\<open>The value of a TA is the term itself:\<close> text\<open>The value of a TA is the term itself:\<close>
term*\<open>C.g @{C \<open>xcv2\<close>}\<close> term*\<open>C.g @{C \<open>xcv2\<close>}\<close>
@ -170,4 +171,31 @@ to update the instance @{docitem \<open>xcv4\<close>}:
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*) update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
section\<open>\<^theory_text>\<open>assert*\<close>-Annotated assertion-commands\<close>
text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context.
It uses the same implementation as the \<^emph>\<open>value*\<close>-command and has the same limitations.
\<close>
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-tests.High_Level_Syntax_Invariants\<close>
we can check logical statements:\<close>
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
= authored_by @{introduction \<open>introduction4\<close>})\<close>
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
(* Error:
assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
text\<open>Assertions must be true, hence the error:\<close>
(* Error:
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
end end