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>}.
\<^item> \<open>meta_args\<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> :
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
\<^item> \<open>annotated_text_element\<close> :
\<^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 "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
| @@{command "value*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
)
|
( @@{command "open_monitor*"}
| @@{command "value*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
| @@{command "assert*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
)
\<close>
\<^rail>\<open>
( @@{command "open_monitor*"}
| @@{command "close_monitor*"}
| @@{command "declare_reference*"}
) '[' meta_args ']'
)
) '[' meta_args ']'
| change_status_command
| inspection_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.
\<close>
(*<*)
declare_reference*["text-elements-expls"::technical]
(*>*)
subsection\<open>Ontological Term-Contexts and their Management\<close>
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>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
\<^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> 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
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
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).
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
(\<^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.
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>
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
of this meta-object. The latter leads to a failure of the entire command.
\<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
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>
Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
this may be for a text fragment like
@ -649,7 +665,7 @@ of the \<^isadof> language:
\<newline>
'[' meta_args ']' '\<open>' text '\<close>'
)
| @@{command "assert*"} '[' meta_args ']' '\<open>' term '\<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 [display]\<open>
title*[title::title]\<open>Isabelle/DOF\<close>
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<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>",
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
\<close>}
title*[title::title]\<open>Isabelle/DOF\<close>
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<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>",
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<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
the last element of a list.\<close>
assert*[claim1::assertion] \<open>last[4::int] = 4\<close>
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>
\<close>}
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>\<close>}
\<close>
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
@{boxed_theory_text [display]
\<open>declare[[ Definition_default_class = "definition"]]
declare[[ Theorem_default_class = "theorem"]]
\<close>}
\<open>declare[[Definition_default_class = "definition"]]
declare[[Theorem_default_class = "theorem"]]\<close>}
which allows the above example be shortened to:
@{boxed_theory_text [display]
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>
\<close>}
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>\<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
\<^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
these types. They are just declared abstract types,
``inhabited'' by special constant symbols carrying strings, for
these types. They are just types declared in HOL,
which are ``inhabited'' by special constant symbols carrying strings, for
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
% TODO:
% 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 *)
imports Main
RegExpInterface (* Interface to functional regular automata for monitoring *)
Assert
keywords "+=" ":=" "accepts" "rejects" "invariant"
@ -42,7 +41,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
"define_shortcut*" "define_macro*" :: thy_decl
and "text*" "text-macro*" :: document_body
and "term*" "value*" :: diag
and "term*" "value*" "assert*" :: diag
and "print_doc_classes" "print_doc_items"
"print_doc_class_template" "check_doc_global" :: diag
@ -185,6 +184,7 @@ struct
type docobj = {pos : Position.T,
thy_name : string,
input_term : term,
value : term,
inline : bool,
id : serial,
@ -613,11 +613,12 @@ fun get_value_local oid ctxt = case get_object_local oid ctxt of
| NONE => NONE
(* 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
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,
value=upd value,id=id,
input_term=upd_input_term input_term,
value=upd_value value,id=id,
inline=inline,cid=cid, vcid=vcid})
in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end
| 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)
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 =
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
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
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)
val (strict_monitor_checking, strict_monitor_checking_setup)
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
val (invariants_checking, invariants_checking_setup)
@ -1051,7 +971,6 @@ fun elaborate_instance thy _ _ term_option pos =
| SOME(value) =>
DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy
end
(*DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy*)
(*
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 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
val generalize_term = Term.map_types (generalize_typ 0)
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)
(* could be extended to bool, map, multisets, ... *)
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
"=" => 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 assns' = map conv_attrs trace_attr
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 _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
(* 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,
rejected_cids=rejected_cids,
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)
in thy |> (* update traces of all 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)
then SOME (DOF_core.parse_cid_global thy cid)
else NONE
val value_term = if (cid_long = DOF_core.default_cid)
then (Free ("Undefined_Value", @{typ "unit"}))
val value_terms = if (cid_long = DOF_core.default_cid)
then let
val undefined_value = Free ("Undefined_Value", @{typ "unit"})
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 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
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 (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)
val assns' = map conv_attrs doc_attrs
val (value_term', _(*ty*), _) = calc_update_term thy cid_long assns' defaults
in value_term' end
val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false}
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)
o Context.Theory
in thy |> DOF_core.define_object_global (oid, {pos = pos,
thy_name = Context.theory_name thy,
value = value_term,
inline = is_inline,
id = id,
cid = cid_long,
vcid = vcid})
in thy |> DOF_core.define_object_global (oid, {pos = pos,
thy_name = Context.theory_name thy,
input_term = fst value_terms,
value = snd value_terms,
inline = is_inline,
id = id,
cid = cid_long,
vcid = vcid})
|> register_oid_cid_in_open_monitors oid pos cid_long
|> (fn thy => (check_inv thy; thy))
|> (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,
Syntax.read_term_global thy rhs)
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}
o Context.Theory ) thy ;
thy)
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
end
@ -1831,7 +1766,6 @@ end
\<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
@ -1848,9 +1782,10 @@ Generic value command for arbitrary evaluators, with default using nbe or SML.
signature VALUE_COMMAND =
sig
val value: Proof.context -> term -> term
val value_without_elaboration: 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
-> Toplevel.state -> Toplevel.transition -> unit
val value_cmd: {assert: bool} -> (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string
-> Toplevel.state -> Position.T -> unit
val add_evaluator: binding * (Proof.context -> term -> term)
-> theory -> string * theory
end;
@ -1863,7 +1798,6 @@ structure Evaluators = Theory_Data
(
type T = (Proof.context -> term -> term) Name_Space.table;
val empty = Name_Space.empty_table "evaluator";
val extend = I;
val merge = Name_Space.merge_tables;
)
@ -1892,22 +1826,34 @@ fun value_select name ctxt =
fun value ctxt term = value_select "" ctxt
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
(Proof_Context.theory_of ctxt))
val value_without_elaboration = value_select ""
fun meta_args_exec NONE thy = 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
{is_monitor = false} {is_inline = false}
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
val _ = meta_args_exec meta_args_opt
val ctxt = Toplevel.context_of state;
val name = intern_evaluator ctxt raw_name;
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);
val t' = value_select name ctxt term';
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 p = Print_Mode.with_modes modes (fn () =>
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
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>
(*
@ -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)
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
val _ = meta_args_exec meta_args_opt
val t = Syntax.read_term ctxt s;
val T = Term.type_of t;
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');
in
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
string_of_term, so we pass the Toplevel.transition
*)
fun print_term meta_args_opt (string_list, string) trans = print_item
(fn state =>
fn string =>
string_of_term meta_args_opt (Toplevel.context_of state) string trans)
(string_list, string) trans;
fun print_term meta_args_opt (string_list, string) trans =
let
val pos = Toplevel.pos_of trans
in
print_item (fn state =>
fn string => string_of_term meta_args_opt (Toplevel.context_of state) string pos)
(string_list, string) trans
end
val _ =
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>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;
\<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>
(*
@ -2018,7 +2068,6 @@ val _ =
end
\<close>
ML\<open>
structure ODL_LTX_Converter =
struct
@ -2208,25 +2257,9 @@ val basic_entity = Document_Output.antiquotation_pretty_source
: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory;
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]
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
let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term]
in Value_Command.value ctxt (subterm') end
fun compute_attr_access ctxt attr oid pos pos' = (* template *)
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)
val proj_term = Const(long_name,dummyT --> ty)
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)
@ -2399,7 +2433,8 @@ fun define_inv cid_long ((lbl, pos), inv) thy =
then Free (s, class_scheme_ty)
else Free (s, ty)
| 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
current class. *)
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"
keywords "author*" "abstract*"
"Definition*" "Lemma*" "Theorem*" :: document_body
and "assert*" :: thy_decl
begin
@ -347,39 +345,7 @@ doc_class assertion = math_formal +
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>
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
imports
"Isabelle_DOF-tests.TermAntiquotations"
"Isabelle_DOF-tests.High_Level_Syntax_Invariants"
begin
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,
whose type is the type of the attribute:\<close>
term*\<open>level @{C \<open>xcv2\<close>}\<close>
value*\<open>level @{C \<open>xcv2\<close>}\<close>
term*\<open>B.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>
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''})}"]*)
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