--- a/NEWS Wed Mar 03 15:19:34 2010 +0100
+++ b/NEWS Wed Mar 03 16:43:55 2010 +0100
@@ -6,15 +6,20 @@
*** General ***
-* Authentic syntax for *all* term constants: provides simple and
-robust correspondence between formal entities and concrete syntax.
-Substantial INCOMPATIBILITY concerning low-level syntax translations
-(translation rules and translation functions in ML). Some hints on
-upgrading:
+* Authentic syntax for *all* logical entities (type classes, type
+constructors, term constants): provides simple and robust
+correspondence between formal entities and concrete syntax. Within
+the parse tree / AST representations, "constants" are decorated by
+their category (class, type, const) and spelled out explicitly with
+their full internal name.
+
+Substantial INCOMPATIBILITY concerning low-level syntax declarations
+and translations (translation rules and translation functions in ML).
+Some hints on upgrading:
- Many existing uses of 'syntax' and 'translations' can be replaced
- by more modern 'notation' and 'abbreviation', which are
- independent of this issue.
+ by more modern 'type_notation', 'notation' and 'abbreviation',
+ which are independent of this issue.
- 'translations' require markup within the AST; the term syntax
provides the following special forms:
@@ -27,16 +32,29 @@
system indicates accidental variables via the error "rhs contains
extra variables".
+ Type classes and type constructors are marked according to their
+ concrete syntax. Some old translations rules need to be written
+ for the "type" category, using type constructor application
+ instead of pseudo-term application of the default category
+ "logic".
+
- 'parse_translation' etc. in ML may use the following
antiquotations:
+ @{class_syntax c} -- type class c within parse tree / AST
+ @{term_syntax c} -- type constructor c within parse tree / AST
@{const_syntax c} -- ML version of "CONST c" above
@{syntax_const c} -- literally c (checked wrt. 'syntax' declarations)
+ - Literal types within 'typed_print_translations', i.e. those *not*
+ represented as pseudo-terms are represented verbatim. Use @{class
+ c} or @{type_name c} here instead of the above syntax
+ antiquotations.
+
Note that old non-authentic syntax was based on unqualified base
-names, so all of the above would coincide. Recall that 'print_syntax'
-and ML_command "set Syntax.trace_ast" help to diagnose syntax
-problems.
+names, so all of the above "constant" names would coincide. Recall
+that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
+diagnose syntax problems.
* Type constructors admit general mixfix syntax, not just infix.
--- a/doc-src/Locales/Locales/Examples3.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Wed Mar 03 16:43:55 2010 +0100
@@ -63,7 +63,7 @@
statements:
@{subgoals [display]}
This is Presburger arithmetic, which can be solved by the
- method @{text arith}. *}
+ method @{text arith}. *}
by arith+
txt {* \normalsize In order to show the equations, we put ourselves
in a situation where the lattice theorems can be used in a
--- a/doc-src/Locales/Locales/document/Examples3.tex Wed Mar 03 15:19:34 2010 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Mar 03 16:43:55 2010 +0100
@@ -141,7 +141,7 @@
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
\end{isabelle}
This is Presburger arithmetic, which can be solved by the
- method \isa{arith}.%
+ method \isa{arith}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
--- a/src/HOL/Bali/AxSem.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/AxSem.thy Wed Mar 03 16:43:55 2010 +0100
@@ -58,10 +58,9 @@
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
- "res" <= (type) "AxSem.res"
- "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
+ (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
"P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
--- a/src/HOL/Bali/Basis.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Mar 03 16:43:55 2010 +0100
@@ -213,11 +213,6 @@
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
-translations
- "option"<= (type) "Option.option"
- "list" <= (type) "List.list"
- "sum3" <= (type) "Basis.sum3"
-
section "quantifiers for option type"
--- a/src/HOL/Bali/Decl.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Decl.thy Wed Mar 03 16:43:55 2010 +0100
@@ -149,24 +149,24 @@
access :: acc_modi
translations
- "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
- "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
+ (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
+ (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
subsection {* Member (field or method)*}
record member = decl +
static :: stat_modi
translations
- "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
- "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
+ (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
+ (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
subsection {* Field *}
record field = member +
type :: ty
translations
- "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
- "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
+ (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
+ (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
types
fdecl (* field declaration, cf. 8.3 *)
@@ -174,7 +174,7 @@
translations
- "fdecl" <= (type) "vname \<times> field"
+ (type) "fdecl" <= (type) "vname \<times> field"
subsection {* Method *}
@@ -193,17 +193,17 @@
translations
- "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty\<rparr>"
- "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,\<dots>::'a\<rparr>"
- "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
- "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
- "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
+ (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
+ (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,mbody::mbody\<rparr>"
- "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
- "mdecl" <= (type) "sig \<times> methd"
+ (type) "mdecl" <= (type) "sig \<times> methd"
definition mhead :: "methd \<Rightarrow> mhead" where
@@ -306,13 +306,13 @@
= "qtname \<times> iface"
translations
- "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
- "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
- "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+ (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
+ (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
+ (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
isuperIfs::qtname list\<rparr>"
- "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+ (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
isuperIfs::qtname list,\<dots>::'a\<rparr>"
- "idecl" <= (type) "qtname \<times> iface"
+ (type) "idecl" <= (type) "qtname \<times> iface"
definition ibody :: "iface \<Rightarrow> ibody" where
"ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
@@ -337,17 +337,17 @@
= "qtname \<times> class"
translations
- "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt\<rparr>"
- "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
- "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,
super::qtname,superIfs::qtname list\<rparr>"
- "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,
super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
- "cdecl" <= (type) "qtname \<times> class"
+ (type) "cdecl" <= (type) "qtname \<times> class"
definition cbody :: "class \<Rightarrow> cbody" where
"cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
@@ -404,8 +404,8 @@
"classes"::"cdecl list"
translations
- "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
- "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
+ (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
+ (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
abbreviation
iface :: "prog \<Rightarrow> (qtname, iface) table"
--- a/src/HOL/Bali/DeclConcepts.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Mar 03 16:43:55 2010 +0100
@@ -1377,7 +1377,7 @@
fspec = "vname \<times> qtname"
translations
- "fspec" <= (type) "vname \<times> qtname"
+ (type) "fspec" <= (type) "vname \<times> qtname"
definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
"imethds G I
--- a/src/HOL/Bali/Eval.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Mar 03 16:43:55 2010 +0100
@@ -99,8 +99,8 @@
types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
vals = "(val, vvar, val list) sum3"
translations
- "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
- "vals" <= (type)"(val, vvar, val list) sum3"
+ (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+ (type) "vals" <= (type) "(val, vvar, val list) sum3"
text {* To avoid redundancy and to reduce the number of rules, there is only
one evaluation rule for each syntactic term. This is also true for variables
--- a/src/HOL/Bali/Name.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Name.thy Wed Mar 03 16:43:55 2010 +0100
@@ -78,11 +78,7 @@
qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
translations
- "mname" <= "Name.mname"
- "xname" <= "Name.xname"
- "tname" <= "Name.tname"
- "ename" <= "Name.ename"
- "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
+ (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
--- a/src/HOL/Bali/State.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/State.thy Wed Mar 03 16:43:55 2010 +0100
@@ -33,10 +33,10 @@
"values" :: "(vn, val) table"
translations
- "fspec" <= (type) "vname \<times> qtname"
- "vn" <= (type) "fspec + int"
- "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
- "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
+ (type) "fspec" <= (type) "vname \<times> qtname"
+ (type) "vn" <= (type) "fspec + int"
+ (type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
+ (type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
"the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
@@ -134,7 +134,7 @@
translations
"Heap" => "CONST Inl"
"Stat" => "CONST Inr"
- "oref" <= (type) "loc + qtname"
+ (type) "oref" <= (type) "loc + qtname"
definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
"fields_table G C P
@@ -213,9 +213,9 @@
= "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
- "globs" <= (type) "(oref , obj) table"
- "heap" <= (type) "(loc , obj) table"
-(* "locals" <= (type) "(lname, val) table" *)
+ (type) "globs" <= (type) "(oref , obj) table"
+ (type) "heap" <= (type) "(loc , obj) table"
+(* (type) "locals" <= (type) "(lname, val) table" *)
datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
@@ -567,10 +567,8 @@
state = "abopt \<times> st" --{* state including abruption information *}
translations
- "abopt" <= (type) "State.abrupt option"
- "abopt" <= (type) "abrupt option"
- "state" <= (type) "abopt \<times> State.st"
- "state" <= (type) "abopt \<times> st"
+ (type) "abopt" <= (type) "abrupt option"
+ (type) "state" <= (type) "abopt \<times> st"
abbreviation
Norm :: "st \<Rightarrow> state"
--- a/src/HOL/Bali/Table.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Table.thy Wed Mar 03 16:43:55 2010 +0100
@@ -42,8 +42,7 @@
where "table_of \<equiv> map_of"
translations
- (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
- (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
+ (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
(* ### To map *)
lemma map_add_find_left[simp]:
--- a/src/HOL/Bali/Term.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Term.thy Wed Mar 03 16:43:55 2010 +0100
@@ -88,7 +88,7 @@
statement *}
translations
- "locals" <= (type) "(lname, val) table"
+ (type) "locals" <= (type) "(lname, val) table"
datatype inv_mode --{* invocation mode for method calls *}
= Static --{* static *}
@@ -100,8 +100,8 @@
parTs::"ty list"
translations
- "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
- "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
+ (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
+ (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
--{* function codes for unary operations *}
datatype unop = UPlus -- {*{\tt +} unary plus*}
@@ -237,11 +237,8 @@
types "term" = "(expr+stmt,var,expr list) sum3"
translations
- "sig" <= (type) "mname \<times> ty list"
- "var" <= (type) "Term.var"
- "expr" <= (type) "Term.expr"
- "stmt" <= (type) "Term.stmt"
- "term" <= (type) "(expr+stmt,var,expr list) sum3"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "term" <= (type) "(expr+stmt,var,expr list) sum3"
abbreviation this :: expr
where "this == Acc (LVar This)"
--- a/src/HOL/Bali/Type.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Type.thy Wed Mar 03 16:43:55 2010 +0100
@@ -30,11 +30,6 @@
= PrimT prim_ty --{* primitive type *}
| RefT ref_ty --{* reference type *}
-translations
- "prim_ty" <= (type) "Type.prim_ty"
- "ref_ty" <= (type) "Type.ref_ty"
- "ty" <= (type) "Type.ty"
-
abbreviation "NT == RefT NullT"
abbreviation "Iface I == RefT (IfaceT I)"
abbreviation "Class C == RefT (ClassT C)"
--- a/src/HOL/Bali/Value.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/Value.thy Wed Mar 03 16:43:55 2010 +0100
@@ -17,9 +17,6 @@
| Addr loc --{* addresses, i.e. locations of objects *}
-translations "val" <= (type) "Term.val"
- "loc" <= (type) "Term.loc"
-
consts the_Bool :: "val \<Rightarrow> bool"
primrec "the_Bool (Bool b) = b"
consts the_Intg :: "val \<Rightarrow> int"
--- a/src/HOL/Bali/WellType.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Mar 03 16:43:55 2010 +0100
@@ -37,10 +37,10 @@
lcl:: "lenv" --{* local environment *}
translations
- "lenv" <= (type) "(lname, ty) table"
- "lenv" <= (type) "lname \<Rightarrow> ty option"
- "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
- "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
+ (type) "lenv" <= (type) "(lname, ty) table"
+ (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
+ (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
+ (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
abbreviation
@@ -238,9 +238,9 @@
section "Typing for terms"
-types tys = "ty + ty list"
+types tys = "ty + ty list"
translations
- "tys" <= (type) "ty + ty list"
+ (type) "tys" <= (type) "ty + ty list"
inductive
--- a/src/HOL/IMPP/Hoare.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/IMPP/Hoare.thy Wed Mar 03 16:43:55 2010 +0100
@@ -18,7 +18,7 @@
types 'a assn = "'a => state => bool"
translations
- "a assn" <= (type)"a => state => bool"
+ (type) "'a assn" <= (type) "'a => state => bool"
definition
state_not_singleton :: bool where
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Mar 03 16:43:55 2010 +0100
@@ -286,14 +286,14 @@
by auto
lemma graph_implies_dom:
- "mrec_graph x y \<Longrightarrow> mrec_dom x"
+ "mrec_graph x y \<Longrightarrow> mrec_dom x"
apply (induct rule:mrec_graph.induct)
apply (rule accpI)
apply (erule mrec_rel.cases)
by simp
lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
- unfolding mrec_def
+ unfolding mrec_def
by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
lemma f_di_reverse:
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Mar 03 16:43:55 2010 +0100
@@ -27,8 +27,8 @@
[simp del]: "make_llist [] = return Empty"
| "make_llist (x#xs) = do tl \<leftarrow> make_llist xs;
next \<leftarrow> Ref.new tl;
- return (Node x next)
- done"
+ return (Node x next)
+ done"
text {* define traverse using the MREC combinator *}
--- a/src/HOL/Library/Numeral_Type.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Wed Mar 03 16:43:55 2010 +0100
@@ -32,7 +32,7 @@
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
-translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
+translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
typed_print_translation {*
let
--- a/src/HOL/Library/Transitive_Closure_Table.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Wed Mar 03 16:43:55 2010 +0100
@@ -107,25 +107,25 @@
proof (cases as)
case Nil
with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
- by auto
+ by auto
from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
- by (auto elim: rtrancl_path_appendE)
+ by (auto elim: rtrancl_path_appendE)
from xs have "length cs < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: cs less(2))+
+ by (rule less(1)) (iprover intro: cs less(2))+
next
case (Cons d ds)
with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
- by auto
+ by auto
with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
and ay: "rtrancl_path r a (bs @ a # cs) y"
- by (auto elim: rtrancl_path_appendE)
+ by (auto elim: rtrancl_path_appendE)
from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
- by (rule rtrancl_path_trans)
+ by (rule rtrancl_path_trans)
from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: xy less(2))+
+ by (rule less(1)) (iprover intro: xy less(2))+
qed
qed
qed
--- a/src/HOL/Map.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Map.thy Wed Mar 03 16:43:55 2010 +0100
@@ -12,10 +12,10 @@
begin
types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0)
-translations (type) "a ~=> b " <= (type) "a => b option"
+translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
-syntax (xsymbols)
- "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0)
+type_notation (xsymbols)
+ "~=>" (infixr "\<rightharpoonup>" 0)
abbreviation
empty :: "'a ~=> 'b" where
--- a/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 16:43:55 2010 +0100
@@ -23,12 +23,12 @@
translations
- "fdecl" <= (type) "vname \<times> ty"
- "sig" <= (type) "mname \<times> ty list"
- "mdecl c" <= (type) "sig \<times> ty \<times> c"
- "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
- "cdecl c" <= (type) "cname \<times> (c class)"
- "prog c" <= (type) "(c cdecl) list"
+ (type) "fdecl" <= (type) "vname \<times> ty"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
+ (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
+ (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
+ (type) "'c prog" <= (type) "('c cdecl) list"
definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where
--- a/src/HOL/NanoJava/AxSem.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/NanoJava/AxSem.thy Wed Mar 03 16:43:55 2010 +0100
@@ -13,10 +13,10 @@
triple = "assn \<times> stmt \<times> assn"
etriple = "assn \<times> expr \<times> vassn"
translations
- "assn" \<leftharpoondown> (type)"state => bool"
- "vassn" \<leftharpoondown> (type)"val => assn"
- "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
- "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
+ (type) "assn" \<leftharpoondown> (type) "state => bool"
+ (type) "vassn" \<leftharpoondown> (type) "val => assn"
+ (type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
+ (type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"
subsection "Hoare Logic Rules"
--- a/src/HOL/NanoJava/Decl.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/NanoJava/Decl.thy Wed Mar 03 16:43:55 2010 +0100
@@ -38,11 +38,11 @@
= "cdecl list"
translations
- "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
- "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
- "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
- "cdecl" \<leftharpoondown> (type)"cname \<times> class"
- "prog " \<leftharpoondown> (type)"cdecl list"
+ (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
+ (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
+ (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
+ (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
+ (type) "prog " \<leftharpoondown> (type) "cdecl list"
consts
--- a/src/HOL/NanoJava/State.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Mar 03 16:43:55 2010 +0100
@@ -23,9 +23,8 @@
obj = "cname \<times> fields"
translations
-
- "fields" \<leftharpoondown> (type)"fname => val option"
- "obj" \<leftharpoondown> (type)"cname \<times> fields"
+ (type) "fields" \<leftharpoondown> (type) "fname => val option"
+ (type) "obj" \<leftharpoondown> (type) "cname \<times> fields"
definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
"init_vars m == Option.map (\<lambda>T. Null) o m"
@@ -40,10 +39,9 @@
locals :: locals
translations
-
- "heap" \<leftharpoondown> (type)"loc => obj option"
- "locals" \<leftharpoondown> (type)"vname => val option"
- "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
+ (type) "heap" \<leftharpoondown> (type) "loc => obj option"
+ (type) "locals" \<leftharpoondown> (type) "vname => val option"
+ (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
definition del_locs :: "state => state" where
"del_locs s \<equiv> s (| locals := empty |)"
--- a/src/HOL/Product_Type.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Product_Type.thy Wed Mar 03 16:43:55 2010 +0100
@@ -142,10 +142,10 @@
by rule+
qed
-syntax (xsymbols)
- "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
-syntax (HTML output)
- "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+ "*" ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (HTML output)
+ "*" ("(_ \<times>/ _)" [21, 20] 20)
consts
Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
--- a/src/HOL/Tools/numeral_syntax.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Wed Mar 03 16:43:55 2010 +0100
@@ -69,7 +69,7 @@
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
+fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
--- a/src/HOL/Tools/record.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Tools/record.ML Wed Mar 03 16:43:55 2010 +0100
@@ -697,10 +697,8 @@
let
fun get_sort env xi =
the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
- val map_sort = Sign.intern_sort thy;
in
- Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
- |> Sign.intern_tycons thy
+ Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
end;
@@ -752,8 +750,8 @@
val more' = mk_ext rest;
in
- (* FIXME authentic syntax *)
- list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
+ list_comb
+ (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
@@ -857,7 +855,7 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy;
+ val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
fun strip_fields T =
(case T of
@@ -922,8 +920,7 @@
fun mk_type_abbr subst name alphas =
let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
- Syntax.term_of_typ (! Syntax.show_sorts)
- (Sign.extern_typ thy (Envir.norm_type subst abbrT))
+ Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
end;
fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
@@ -946,14 +943,14 @@
fun record_ext_type_tr' name =
let
- val ext_type_name = suffix ext_typeN name;
+ val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
in (ext_type_name, tr') end;
fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
let
- val ext_type_name = suffix ext_typeN name;
+ val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
(list_comb (Syntax.const ext_type_name, ts));
@@ -1949,8 +1946,7 @@
val (args', more) = chop_last args;
fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
fun build Ts =
- fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args'))
- more;
+ fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
in
if more = HOLogic.unit
then build (map_range recT (parent_len + 1))
@@ -1960,27 +1956,25 @@
val r_rec0 = mk_rec all_vars_more 0;
val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
- fun r n = Free (rN, rec_schemeT n)
+ fun r n = Free (rN, rec_schemeT n);
val r0 = r 0;
- fun r_unit n = Free (rN, recT n)
+ fun r_unit n = Free (rN, recT n);
val r_unit0 = r_unit 0;
- val w = Free (wN, rec_schemeT 0)
+ val w = Free (wN, rec_schemeT 0);
(* print translations *)
- val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
-
val record_ext_type_abbr_tr's =
let
- val trnames = external_names (hd extension_names);
+ val trname = hd extension_names;
val last_ext = unsuffix ext_typeN (fst extension);
- in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
+ in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
val record_ext_type_tr's =
let
(*avoid conflict with record_type_abbr_tr's*)
- val trnames = if parent_len > 0 then external_names extension_name else [];
+ val trnames = if parent_len > 0 then [extension_name] else [];
in map record_ext_type_tr' trnames end;
val advanced_print_translation =
--- a/src/HOL/Tools/typedef.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Wed Mar 03 16:43:55 2010 +0100
@@ -118,7 +118,7 @@
fun add_def theory =
if def then
theory
- |> Sign.add_consts_i [(name, setT', NoSyn)] (* FIXME authentic syntax *)
+ |> Sign.add_consts_i [(name, setT', NoSyn)]
|> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
--- a/src/HOL/Typerep.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/Typerep.thy Wed Mar 03 16:43:55 2010 +0100
@@ -33,7 +33,7 @@
typed_print_translation {*
let
fun typerep_tr' show_sorts (*"typerep"*)
- (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
+ (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
(Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
--- a/src/HOL/UNITY/Union.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/UNITY/Union.thy Wed Mar 03 16:43:55 2010 +0100
@@ -35,21 +35,22 @@
safety_prop :: "'a program set => bool"
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+notation (xsymbols)
+ SKIP ("\<bottom>") and
+ Join (infixl "\<squnion>" 65)
+
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+ "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
translations
"JN x: A. B" == "CONST JOIN A (%x. B)"
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
-syntax (xsymbols)
- SKIP :: "'a program" ("\<bottom>")
- Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
- "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
- "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
-
subsection{*SKIP*}
--- a/src/HOL/ex/Numeral.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOL/ex/Numeral.thy Wed Mar 03 16:43:55 2010 +0100
@@ -327,7 +327,7 @@
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
in case T
- of Type (@{type_syntax fun}, [_, T']) =>
+ of Type (@{type_name fun}, [_, T']) =>
if not (! show_types) andalso can Term.dest_Type T' then t'
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
--- a/src/HOLCF/One.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/One.thy Wed Mar 03 16:43:55 2010 +0100
@@ -10,7 +10,7 @@
types one = "unit lift"
translations
- "one" <= (type) "unit lift"
+ (type) "one" <= (type) "unit lift"
definition
ONE :: "one"
--- a/src/HOLCF/Representable.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Representable.thy Wed Mar 03 16:43:55 2010 +0100
@@ -50,7 +50,7 @@
text "A TypeRep is an algebraic deflation over the universe of values."
types TypeRep = "udom alg_defl"
-translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
definition
Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
@@ -60,7 +60,7 @@
(emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
syntax "_REP" :: "type \<Rightarrow> TypeRep" ("(1REP/(1'(_')))")
-translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
lemma cast_REP:
"cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
--- a/src/HOLCF/Sprod.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Sprod.thy Wed Mar 03 16:43:55 2010 +0100
@@ -22,10 +22,10 @@
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
-syntax (xsymbols)
- sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
-syntax (HTML output)
- sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (xsymbols)
+ sprod ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (HTML output)
+ sprod ("(_ \<otimes>/ _)" [21,20] 20)
lemma spair_lemma:
"(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
--- a/src/HOLCF/Ssum.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Ssum.thy Wed Mar 03 16:43:55 2010 +0100
@@ -24,10 +24,11 @@
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
-syntax (xsymbols)
- ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
-syntax (HTML output)
- ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+ ssum ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (HTML output)
+ ssum ("(_ \<oplus>/ _)" [21, 20] 20)
+
subsection {* Definitions of constructors *}
--- a/src/HOLCF/Tr.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Tr.thy Wed Mar 03 16:43:55 2010 +0100
@@ -14,7 +14,7 @@
tr = "bool lift"
translations
- "tr" <= (type) "bool lift"
+ (type) "tr" <= (type) "bool lift"
definition
TT :: "tr" where
--- a/src/HOLCF/Up.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Up.thy Wed Mar 03 16:43:55 2010 +0100
@@ -14,8 +14,8 @@
datatype 'a u = Ibottom | Iup 'a
-syntax (xsymbols)
- "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
+type_notation (xsymbols)
+ u ("(_\<^sub>\<bottom>)" [1000] 999)
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
"Ifup f Ibottom = \<bottom>"
--- a/src/HOLCF/ex/Strict_Fun.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/ex/Strict_Fun.thy Wed Mar 03 16:43:55 2010 +0100
@@ -12,8 +12,8 @@
= "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
by simp_all
-syntax (xsymbols)
- sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0)
+type_notation (xsymbols)
+ sfun (infixr "\<rightarrow>!" 0)
text {* TODO: Define nice syntax for abstraction, application. *}
--- a/src/HOLCF/holcf_logic.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/holcf_logic.ML Wed Mar 03 16:43:55 2010 +0100
@@ -31,21 +31,14 @@
(* basic types *)
-fun mk_btyp t (S,T) = Type (t,[S,T]);
-
-local
- val intern_type = Sign.intern_type @{theory};
- val u = intern_type "u";
-in
+fun mk_btyp t (S, T) = Type (t, [S, T]);
-val cfun_arrow = intern_type "->";
+val cfun_arrow = @{type_name "->"};
val op ->> = mk_btyp cfun_arrow;
-val mk_ssumT = mk_btyp (intern_type "++");
-val mk_sprodT = mk_btyp (intern_type "**");
-fun mk_uT T = Type (u, [T]);
-val trT = Type (intern_type "tr" , []);
-val oneT = Type (intern_type "one", []);
+val mk_ssumT = mk_btyp (@{type_name "++"});
+val mk_sprodT = mk_btyp (@{type_name "**"});
+fun mk_uT T = Type (@{type_name u}, [T]);
+val trT = @{typ tr};
+val oneT = @{typ one};
end;
-
-end;
--- a/src/Pure/General/name_space.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 03 16:43:55 2010 +0100
@@ -46,7 +46,6 @@
val qualified_path: bool -> binding -> naming -> naming
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
- val external_names: naming -> string -> string list
val declare: bool -> naming -> binding -> T -> string * T
type 'a table = T * 'a Symtab.table
val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
@@ -309,8 +308,6 @@
val pfxs = mandatory_prefixes spec;
in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
-fun external_names naming = #2 o accesses naming o Binding.qualified_name;
-
(* declaration *)
--- a/src/Pure/Isar/local_syntax.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Isar/local_syntax.ML Wed Mar 03 16:43:55 2010 +0100
@@ -4,13 +4,11 @@
Local syntax depending on theory syntax.
*)
-val show_structs = Unsynchronized.ref false;
-
signature LOCAL_SYNTAX =
sig
type T
val syn_of: T -> Syntax.syntax
- val structs_of: T -> string list
+ val idents_of: T -> {structs: string list, fixes: string list}
val init: theory -> T
val rebuild: theory -> T -> T
datatype kind = Type | Const | Fixed
@@ -19,7 +17,6 @@
val restore_mode: T -> T -> T
val update_modesyntax: theory -> bool -> Syntax.mode ->
(kind * (string * typ * mixfix)) list -> T -> T
- val extern_term: T -> term -> term
end;
structure Local_Syntax: LOCAL_SYNTAX =
@@ -49,8 +46,7 @@
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
-fun idents_of (Syntax {idents, ...}) = idents;
-val structs_of = #1 o idents_of;
+fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
(* build syntax *)
@@ -125,21 +121,4 @@
fun update_modesyntax thy add mode args syntax =
syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
-
-(* extern_term *)
-
-fun extern_term syntax =
- let
- val (structs, fixes) = idents_of syntax;
- fun map_free (t as Free (x, T)) =
- let val i = find_index (fn s => s = x) structs + 1 in
- if i = 0 andalso member (op =) fixes x then
- Term.Const (Syntax.mark_fixed x, T)
- else if i = 1 andalso not (! show_structs) then
- Syntax.const "_struct" $ Syntax.const "_indexdefault"
- else t
- end
- | map_free t = t;
- in Term.map_aterms map_free end;
-
end;
--- a/src/Pure/Isar/proof_context.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 03 16:43:55 2010 +0100
@@ -363,15 +363,11 @@
(Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
| NONE => Pretty.mark Markup.var (Pretty.str s));
-fun class_markup _ c = (* FIXME authentic syntax *)
- Pretty.mark (Markup.tclassN, []) (Pretty.str c);
-
fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
val token_trans =
Syntax.tokentrans_mode ""
- [("class", class_markup),
- ("tfree", plain_markup Markup.tfree),
+ [("tfree", plain_markup Markup.tfree),
("tvar", plain_markup Markup.tvar),
("free", free_or_skolem),
("bound", plain_markup Markup.bound),
@@ -601,14 +597,12 @@
{get_sort = get_sort thy (Variable.def_sort ctxt),
map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
- map_free = intern_skolem ctxt (Variable.def_type ctxt false),
- map_type = Sign.intern_tycons thy,
- map_sort = Sign.intern_sort thy}
+ map_free = intern_skolem ctxt (Variable.def_type ctxt false)}
end;
fun decode_term ctxt =
- let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt
- in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
+ let val {get_sort, map_const, map_free} = term_context ctxt
+ in Syntax.decode_term get_sort map_const map_free end;
end;
@@ -677,26 +671,23 @@
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token Markup.sort text;
- val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
- (Sign.intern_sort (theory_of ctxt)) (syms, pos)
+ val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
in S end;
fun parse_typ ctxt text =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = theory_of ctxt;
val get_sort = get_sort thy (Variable.def_sort ctxt);
-
val (syms, pos) = Syntax.parse_token Markup.typ text;
- val T = Sign.intern_tycons thy
- (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
- handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
+ val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+ handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
in T end;
fun parse_term T ctxt text =
let
val thy = theory_of ctxt;
- val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
+ val {get_sort, map_const, map_free} = term_context ctxt;
val (T', _) = TypeInfer.paramify_dummies T 0;
val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
@@ -704,29 +695,35 @@
fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
handle ERROR msg => SOME msg;
- val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
- map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
+ val t =
+ Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
+ ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
in t end;
-fun unparse_sort ctxt S =
- Syntax.standard_unparse_sort ctxt (syn_of ctxt) (Sign.extern_sort (theory_of ctxt) S);
+fun unparse_sort ctxt =
+ Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
+ ctxt (syn_of ctxt);
-fun unparse_typ ctxt T =
- Syntax.standard_unparse_typ ctxt (syn_of ctxt) (Sign.extern_typ (theory_of ctxt) T);
+fun unparse_typ ctxt =
+ let
+ val thy = theory_of ctxt;
+ val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
+ in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
-fun unparse_term ctxt t =
+fun unparse_term ctxt =
let
val thy = theory_of ctxt;
val syntax = syntax_of ctxt;
val consts = consts_of ctxt;
+ val extern =
+ {extern_class = Sign.extern_class thy,
+ extern_type = Sign.extern_type thy,
+ extern_const = Consts.extern consts};
in
- t
- |> Sign.extern_term thy
- |> Local_Syntax.extern_term syntax
- |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
- (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
+ Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
+ (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
end;
in
@@ -1010,18 +1007,20 @@
in Syntax.Constant d end
| const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+val typ = Simple_Syntax.read_typ;
+
in
val _ = Context.>> (Context.map_theory
- (Sign.add_syntax
- [("_context_const", "id => logic", Delimfix "CONST _"),
- ("_context_const", "id => aprop", Delimfix "CONST _"),
- ("_context_const", "longid => logic", Delimfix "CONST _"),
- ("_context_const", "longid => aprop", Delimfix "CONST _"),
- ("_context_xconst", "id => logic", Delimfix "XCONST _"),
- ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
- ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
- ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
+ (Sign.add_syntax_i
+ [("_context_const", typ "id => logic", Delimfix "CONST _"),
+ ("_context_const", typ "id => aprop", Delimfix "CONST _"),
+ ("_context_const", typ "longid => logic", Delimfix "CONST _"),
+ ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
+ ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
Sign.add_advanced_trfuns
([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
@@ -1032,8 +1031,8 @@
local
-fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
- SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
+fun type_syntax (Type (c, args), mx) =
+ SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
| type_syntax _ = NONE;
fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
@@ -1345,7 +1344,7 @@
val prt_term = Syntax.pretty_term ctxt;
(*structures*)
- val structs = Local_Syntax.structs_of (syntax_of ctxt);
+ val {structs, ...} = Local_Syntax.idents_of (syntax_of ctxt);
val prt_structs =
if null structs then []
else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
@@ -1415,3 +1414,4 @@
end;
end;
+
--- a/src/Pure/ML/ml_antiquote.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Mar 03 16:43:55 2010 +0100
@@ -104,7 +104,7 @@
fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
Sign.read_class thy s
- |> syn ? Long_Name.base_name (* FIXME authentic syntax *)
+ |> syn ? Syntax.mark_class
|> ML_Syntax.print_string);
val _ = inline "class" (class false);
@@ -130,7 +130,7 @@
val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
-val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Long_Name.base_name c)); (* FIXME authentic syntax *)
+val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
(* constants *)
--- a/src/Pure/Proof/extraction.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Mar 03 16:43:55 2010 +0100
@@ -207,9 +207,11 @@
let val thy' = add_syntax thy
in fn s =>
let val t = Logic.varify (Syntax.read_prop_global thy' s)
- in (map Logic.dest_equals (Logic.strip_imp_prems t),
- Logic.dest_equals (Logic.strip_imp_concl t))
- end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
+ in
+ (map Logic.dest_equals (Logic.strip_imp_prems t),
+ Logic.dest_equals (Logic.strip_imp_concl t))
+ handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
+ end
end;
(** preprocessor **)
--- a/src/Pure/Syntax/lexicon.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Syntax/lexicon.ML Wed Mar 03 16:43:55 2010 +0100
@@ -30,12 +30,17 @@
val read_int: string -> int option
val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
val read_float: string -> {mant: int, exp: int}
- val fixedN: string
- val mark_fixed: string -> string
- val unmark_fixed: string -> string
- val constN: string
- val mark_const: string -> string
- val unmark_const: string -> string
+ val mark_class: string -> string val unmark_class: string -> string
+ val mark_type: string -> string val unmark_type: string -> string
+ val mark_const: string -> string val unmark_const: string -> string
+ val mark_fixed: string -> string val unmark_fixed: string -> string
+ val unmark:
+ {case_class: string -> 'a,
+ case_type: string -> 'a,
+ case_const: string -> 'a,
+ case_fixed: string -> 'a,
+ case_default: string -> 'a} -> string -> 'a
+ val is_marked: string -> bool
end;
signature LEXICON =
@@ -333,15 +338,32 @@
in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
-(* specific identifiers *)
+(* logical entities *)
+
+fun marker s = (prefix s, unprefix s);
+
+val (mark_class, unmark_class) = marker "\\<^class>";
+val (mark_type, unmark_type) = marker "\\<^type>";
+val (mark_const, unmark_const) = marker "\\<^const>";
+val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
-val fixedN = "\\<^fixed>";
-val mark_fixed = prefix fixedN;
-val unmark_fixed = unprefix fixedN;
+fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
+ (case try unmark_class s of
+ SOME c => case_class c
+ | NONE =>
+ (case try unmark_type s of
+ SOME c => case_type c
+ | NONE =>
+ (case try unmark_const s of
+ SOME c => case_const c
+ | NONE =>
+ (case try unmark_fixed s of
+ SOME c => case_fixed c
+ | NONE => case_default s))));
-val constN = "\\<^const>";
-val mark_const = prefix constN;
-val unmark_const = unprefix constN;
+val is_marked =
+ unmark {case_class = K true, case_type = K true, case_const = K true,
+ case_fixed = K true, case_default = K false};
(* read numbers *)
@@ -371,7 +393,7 @@
val ten = ord "0" + 10;
val a = ord "a";
val A = ord "A";
-val _ = a > A orelse sys_error "Bad ASCII";
+val _ = a > A orelse raise Fail "Bad ASCII";
fun remap_hex c =
let val x = ord c in
--- a/src/Pure/Syntax/printer.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Syntax/printer.ML Wed Mar 03 16:43:55 2010 +0100
@@ -11,29 +11,32 @@
val show_types: bool Unsynchronized.ref
val show_no_free_types: bool Unsynchronized.ref
val show_all_types: bool Unsynchronized.ref
+ val show_structs: bool Unsynchronized.ref
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
signature PRINTER =
sig
include PRINTER0
- val term_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
+ val sort_to_ast: Proof.context ->
+ (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
val typ_to_ast: Proof.context ->
(string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
- val sort_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
+ val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
+ (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
type prtabs
val empty_prtabs: prtabs
val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
val merge_prtabs: prtabs -> prtabs -> prtabs
- val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
- -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
- -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
- val pretty_typ_ast: Proof.context -> bool -> prtabs
- -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
- -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+ val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
+ extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+ val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> bool -> prtabs ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
end;
structure Printer: PRINTER =
@@ -47,6 +50,7 @@
val show_brackets = Unsynchronized.ref false;
val show_no_free_types = Unsynchronized.ref false;
val show_all_types = Unsynchronized.ref false;
+val show_structs = Unsynchronized.ref false;
fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
@@ -84,8 +88,7 @@
fun ast_of_termT ctxt trf tm =
let
- fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
- | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
| ast_of (Const (a, _)) = trans a []
| ast_of (t as _ $ _) =
@@ -105,19 +108,32 @@
(** term_to_ast **)
-fun mark_freevars ((t as Const (c, _)) $ u) =
- if member (op =) SynExt.standard_token_markers c then (t $ u)
- else t $ mark_freevars u
- | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
- | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
- | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
- | mark_freevars (t as Var (xi, T)) =
- if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
- else Lexicon.const "_var" $ t
- | mark_freevars a = a;
+fun ast_of_term idents consts ctxt trf
+ show_all_types no_freeTs show_types show_sorts show_structs tm =
+ let
+ val {structs, fixes} = idents;
-fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
- let
+ fun mark_atoms ((t as Const (c, T)) $ u) =
+ if member (op =) SynExt.standard_token_markers c
+ then t $ u else mark_atoms t $ mark_atoms u
+ | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
+ | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
+ | mark_atoms (t as Const (c, T)) =
+ if member (op =) consts c then t
+ else Const (Lexicon.mark_const c, T)
+ | mark_atoms (t as Free (x, T)) =
+ let val i = find_index (fn s => s = x) structs + 1 in
+ if i = 0 andalso member (op =) fixes x then
+ Const (Lexicon.mark_fixed x, T)
+ else if i = 1 andalso not show_structs then
+ Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
+ else Lexicon.const "_free" $ t
+ end
+ | mark_atoms (t as Var (xi, T)) =
+ if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
+ else Lexicon.const "_var" $ t
+ | mark_atoms a = a;
+
fun prune_typs (t_seen as (Const _, _)) = t_seen
| prune_typs (t as Free (x, ty), seen) =
if ty = dummyT then (t, seen)
@@ -148,9 +164,9 @@
Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
| (Const ("_idtdummy", T), ts) =>
Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
- | (c' as Const (c, T), ts) =>
+ | (const as Const (c, T), ts) =>
if show_all_types
- then Ast.mk_appl (constrain c' T) (map ast_of ts)
+ then Ast.mk_appl (constrain const T) (map ast_of ts)
else trans c T ts
| (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
@@ -162,18 +178,18 @@
if show_types andalso T <> dummyT then
Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
- else simple_ast_of t
+ else simple_ast_of t;
in
tm
|> SynTrans.prop_tr'
- |> (if show_types then #1 o prune_typs o rpair [] else I)
- |> mark_freevars
+ |> show_types ? (#1 o prune_typs o rpair [])
+ |> mark_atoms
|> ast_of
end;
-fun term_to_ast ctxt trf tm =
- ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
- (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
+fun term_to_ast idents consts ctxt trf tm =
+ ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
+ (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
@@ -267,8 +283,10 @@
| is_chain [Arg _] = true
| is_chain _ = false;
-fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
let
+ val {extern_class, extern_type, extern_const} = extern;
+
fun token_trans a x =
(case tokentrf a of
NONE =>
@@ -291,7 +309,7 @@
val (Ts, args') = synT markup (symbs, args);
in
if type_mode then (astT (t, p) @ Ts, args')
- else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
+ else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args')
end
| synT markup (String s :: symbs, args) =
let val (Ts, args') = synT markup (symbs, args);
@@ -312,7 +330,6 @@
val (Ts, args') = synT markup (symbs, args);
val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
in (T :: Ts, args') end
- | synT _ (_ :: _, []) = sys_error "synT"
and parT markup (pr, args, p, p': int) = #1 (synT markup
(if p > p' orelse
@@ -320,13 +337,12 @@
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
- and atomT a =
- (case try Lexicon.unmark_const a of
- SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
- | NONE =>
- (case try Lexicon.unmark_fixed a of
- SOME x => the (token_trans "_free" x)
- | NONE => Pretty.str a))
+ and atomT a = a |> Lexicon.unmark
+ {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)),
+ case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)),
+ case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)),
+ case_fixed = fn x => the (token_trans "_free" x),
+ case_default = Pretty.str}
and prefixT (_, a, [], _) = [atomT a]
| prefixT (c, _, args, p) = astT (appT (c, args), p)
@@ -334,15 +350,16 @@
and splitT 0 ([x], ys) = (x, ys)
| splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
| splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
- | splitT _ _ = sys_error "splitT"
and combT (tup as (c, a, args, p)) =
let
val nargs = length args;
- val markup = Pretty.mark
- (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
- (Markup.fixed (Lexicon.unmark_fixed a)))
- handle Fail _ => I;
+ val markup = a |> Lexicon.unmark
+ {case_class = Pretty.mark o Markup.tclass,
+ case_type = Pretty.mark o Markup.tycon,
+ case_const = Pretty.mark o Markup.const,
+ case_fixed = Pretty.mark o Markup.fixed,
+ case_default = K I};
(*find matching table entry, or print as prefix / postfix*)
fun prnt ([], []) = prefixT tup
@@ -371,15 +388,16 @@
(* pretty_term_ast *)
-fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
- pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
+ pretty extern ctxt (mode_tabs prtabs (print_mode_value ()))
trf tokentrf false curried ast 0;
(* pretty_typ_ast *)
-fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
- pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
+ pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
+ ctxt (mode_tabs prtabs (print_mode_value ()))
trf tokentrf true false ast 0;
end;
--- a/src/Pure/Syntax/syn_ext.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Wed Mar 03 16:43:55 2010 +0100
@@ -282,7 +282,8 @@
if not (exists is_index args) then (const, typ, [])
else
let
- val indexed_const = if const <> "" then "_indexed_" ^ const
+ val indexed_const =
+ if const <> "" then const ^ "_indexed"
else err_in_mfix "Missing constant name for indexed syntax" mfix;
val rangeT = Term.range_type typ handle Match =>
err_in_mfix "Missing structure argument for indexed syntax" mfix;
@@ -387,7 +388,7 @@
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
val standard_token_classes =
- ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
+ ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
--- a/src/Pure/Syntax/syn_trans.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Wed Mar 03 16:43:55 2010 +0100
@@ -34,16 +34,16 @@
val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
val constrainAbsC: string
val pure_trfuns:
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (string * (term list -> term)) list *
+ (string * (term list -> term)) list *
+ (string * (Ast.ast list -> Ast.ast)) list
val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
val struct_trfuns: string list ->
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (bool -> typ -> term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (string * (term list -> term)) list *
+ (string * (bool -> typ -> term list -> term)) list *
+ (string * (Ast.ast list -> Ast.ast)) list
end;
signature SYN_TRANS =
@@ -131,7 +131,7 @@
fun mk_type ty =
Lexicon.const "_constrain" $
- Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
+ Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
| ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
@@ -143,7 +143,7 @@
(* meta propositions *)
-fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"
+fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
| aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
@@ -195,7 +195,8 @@
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
- list_comb (c $ update_name_tr [t] $ (Lexicon.const "fun" $ ty $ Lexicon.const "dummy"), ts)
+ list_comb (c $ update_name_tr [t] $
+ (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
@@ -368,7 +369,7 @@
fun is_prop Ts t =
fastype_of1 (Ts, t) = propT handle TERM _ => false;
- fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
+ fun is_term (Const ("Pure.term", _) $ _) = true
| is_term _ = false;
fun tr' _ (t as Const _) = t
@@ -381,7 +382,7 @@
| tr' Ts (t as Bound _) =
if is_prop Ts t then aprop t else t
| tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
- | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
+ | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
else tr' Ts t1 $ tr' Ts t2
| tr' Ts (t as t1 $ t2) =
@@ -568,7 +569,7 @@
val free_fixed = Term.map_aterms
(fn t as Const (c, T) =>
- (case try (unprefix Lexicon.fixedN) c of
+ (case try Lexicon.unmark_fixed c of
NONE => t
| SOME x => Free (x, T))
| t => t);
--- a/src/Pure/Syntax/syntax.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Mar 03 16:43:55 2010 +0100
@@ -29,7 +29,10 @@
val mode_default: mode
val mode_input: mode
val merge_syntaxes: syntax -> syntax -> syntax
- val basic_syn: syntax
+ val empty_syntax: syntax
+ val basic_syntax:
+ {read_class: theory -> xstring -> string,
+ read_type: theory -> xstring -> string} -> syntax
val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
@@ -41,25 +44,24 @@
val ambiguity_limit: int Unsynchronized.ref
val standard_parse_term: Pretty.pp -> (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
- (string -> bool * string) -> (string -> string option) ->
- (typ -> typ) -> (sort -> sort) -> Proof.context ->
+ (string -> bool * string) -> (string -> string option) -> Proof.context ->
(string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
val standard_parse_typ: Proof.context -> syntax ->
- ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
- Symbol_Pos.T list * Position.T -> typ
- val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
- Symbol_Pos.T list * Position.T -> sort
+ ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+ val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
datatype 'a trrule =
ParseRule of 'a * 'a |
PrintRule of 'a * 'a |
ParsePrintRule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
- val standard_unparse_term: (string -> xstring) ->
- Proof.context -> syntax -> bool -> term -> Pretty.T
- val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
- val update_consts: string list -> syntax -> syntax
+ val standard_unparse_term: {structs: string list, fixes: string list} ->
+ {extern_class: string -> xstring, extern_type: string -> xstring,
+ extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
+ val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> syntax -> typ -> Pretty.T
+ val standard_unparse_sort: {extern_class: string -> xstring} ->
+ Proof.context -> syntax -> sort -> Pretty.T
val update_trfuns:
(string * ((ast list -> ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
@@ -300,7 +302,7 @@
lexicon =
if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
gram = if changed then Parser.extend_gram gram xprods else gram,
- consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
+ consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
parse_ast_trtab =
update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -381,9 +383,9 @@
(* basic syntax *)
-val basic_syn =
+fun basic_syntax read =
empty_syntax
- |> update_syntax mode_default TypeExt.type_ext
+ |> update_syntax mode_default (TypeExt.type_ext read)
|> update_syntax mode_default SynExt.pure_ext;
val basic_nonterms =
@@ -547,26 +549,25 @@
map (Pretty.string_of_term pp) (take limit results)))
end;
-fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
- ctxt is_logtype syn ty (syms, pos) =
+fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
read ctxt is_logtype syn ty (syms, pos)
- |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
+ |> map (TypeExt.decode_term get_sort map_const map_free)
|> disambig (Printer.pp_show_brackets pp) check;
(* read types *)
-fun standard_parse_typ ctxt syn get_sort map_sort (syms, pos) =
+fun standard_parse_typ ctxt syn get_sort (syms, pos) =
(case read ctxt (K false) syn SynExt.typeT (syms, pos) of
- [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
+ [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
| _ => error (ambiguity_msg pos));
(* read sorts *)
-fun standard_parse_sort ctxt syn map_sort (syms, pos) =
+fun standard_parse_sort ctxt syn (syms, pos) =
(case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
- [t] => TypeExt.sort_of_term map_sort t
+ [t] => TypeExt.sort_of_term t
| _ => error (ambiguity_msg pos));
@@ -640,8 +641,8 @@
fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
let
- val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
- val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
+ val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
+ val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
in
Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
(lookup_tokentr tokentrtab (print_mode_value ()))
@@ -650,14 +651,16 @@
in
-fun standard_unparse_term extern =
- unparse_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
+fun standard_unparse_term idents extern =
+ unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
-fun standard_unparse_typ ctxt syn =
- unparse_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
+fun standard_unparse_typ extern ctxt syn =
+ unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
-fun standard_unparse_sort ctxt syn =
- unparse_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
+fun standard_unparse_sort {extern_class} ctxt syn =
+ unparse_t (K Printer.sort_to_ast)
+ (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+ Markup.sort ctxt syn false;
end;
@@ -667,7 +670,6 @@
fun ext_syntax f decls = update_syntax mode_default (f decls);
-val update_consts = ext_syntax SynExt.syn_ext_const_names;
val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
--- a/src/Pure/Syntax/type_ext.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML Wed Mar 03 16:43:55 2010 +0100
@@ -1,19 +1,17 @@
(* Title: Pure/Syntax/type_ext.ML
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-Utilities for input and output of types. Also the concrete syntax of
-types, which is required to bootstrap Pure.
+Utilities for input and output of types. The concrete syntax of types.
*)
signature TYPE_EXT0 =
sig
- val sort_of_term: (sort -> sort) -> term -> sort
- val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
- val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
+ val sort_of_term: term -> sort
+ val term_sorts: term -> (indexname * sort) list
+ val typ_of_term: (indexname -> sort) -> term -> typ
val type_constraint: typ -> term -> term
val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
- (string -> bool * string) -> (string -> string option) ->
- (typ -> typ) -> (sort -> sort) -> term -> term
+ (string -> bool * string) -> (string -> string option) -> term -> term
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
@@ -25,7 +23,9 @@
val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val sortT: typ
- val type_ext: SynExt.syn_ext
+ val type_ext:
+ {read_class: theory -> string -> string,
+ read_type: theory -> string -> string} -> SynExt.syn_ext
end;
structure TypeExt: TYPE_EXT =
@@ -35,30 +35,28 @@
(* sort_of_term *)
-fun sort_of_term (map_sort: sort -> sort) tm =
+fun sort_of_term tm =
let
- fun classes (Const (c, _)) = [c]
- | classes (Free (c, _)) = [c]
- | classes (Const ("_class", _) $ Free (c, _)) = [c]
- | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
- | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
- | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
- | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+ fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+
+ fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+
+ fun classes (Const (s, _)) = [class s]
+ | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
+ | classes _ = err ();
fun sort (Const ("_topsort", _)) = []
- | sort (Const (c, _)) = [c]
- | sort (Free (c, _)) = [c]
- | sort (Const ("_class", _) $ Free (c, _)) = [c]
+ | sort (Const (s, _)) = [class s]
| sort (Const ("_sort", _) $ cs) = classes cs
- | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
- in map_sort (sort tm) end;
+ | sort _ = err ();
+ in sort tm end;
(* term_sorts *)
-fun term_sorts map_sort tm =
+fun term_sorts tm =
let
- val sort_of = sort_of_term map_sort;
+ val sort_of = sort_of_term;
fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
insert (op =) ((x, ~1), sort_of cs)
@@ -76,11 +74,11 @@
(* typ_of_term *)
-fun typ_of_term get_sort map_sort t =
+fun typ_of_term get_sort tm =
let
- fun typ_of (Free (x, _)) =
- if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
- else Type (x, [])
+ fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
+
+ fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
| typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
| typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
| typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
@@ -90,17 +88,16 @@
| typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
| typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
TVar (xi, get_sort xi)
- | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
- | typ_of tm =
+ | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
+ | typ_of t =
let
- val (t, ts) = Term.strip_comb tm;
+ val (head, args) = Term.strip_comb t;
val a =
- (case t of
- Const (x, _) => x
- | Free (x, _) => x
- | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
- in Type (a, map typ_of ts) end;
- in typ_of t end;
+ (case head of
+ Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
+ | _ => err ());
+ in Type (a, map typ_of args) end;
+ in typ_of tm end;
(* decode_term -- transform parse tree into raw term *)
@@ -109,30 +106,30 @@
if T = dummyT then t
else Const ("_type_constraint_", T --> T) $ t;
-fun decode_term get_sort map_const map_free map_type map_sort tm =
+fun decode_term get_sort map_const map_free tm =
let
- val sort_env = term_sorts map_sort tm;
- val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
+ val sort_env = term_sorts tm;
+ val decodeT = typ_of_term (get_sort sort_env);
fun decode (Const ("_constrain", _) $ t $ typ) =
type_constraint (decodeT typ) (decode t)
| decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
if T = dummyT then Abs (x, decodeT typ, decode t)
- else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
- | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
+ else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+ | decode (Abs (x, T, t)) = Abs (x, T, decode t)
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
let val c =
(case try Lexicon.unmark_const a of
SOME c => c
| NONE => snd (map_const a))
- in Const (c, map_type T) end
+ in Const (c, T) end
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
- (SOME x, _) => Free (x, map_type T)
- | (_, (true, c)) => Const (c, map_type T)
- | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
- | decode (Var (xi, T)) = Var (xi, map_type T)
+ (SOME x, _) => Free (x, T)
+ | (_, (true, c)) => Const (c, T)
+ | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
+ | decode (Var (xi, T)) = Var (xi, T)
| decode (t as Bound _) = t;
in decode tm end;
@@ -144,10 +141,9 @@
fun term_of_sort S =
let
- fun class c = Lexicon.const "_class" $ Lexicon.free c;
+ val class = Lexicon.const o Lexicon.mark_class;
- fun classes [] = sys_error "term_of_sort"
- | classes [c] = class c
+ fun classes [c] = class c
| classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
in
(case S of
@@ -165,7 +161,8 @@
if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
else t;
- fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
+ fun term_of (Type (a, Ts)) =
+ Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
| term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
| term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
in term_of ty end;
@@ -193,15 +190,29 @@
(* parse ast translations *)
-fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
- | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+val class_ast = Ast.Constant o Lexicon.mark_class;
+val type_ast = Ast.Constant o Lexicon.mark_type;
+
+fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
+ | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
+
+fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
+ Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
+ | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
-fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
- Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
- | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
+fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
+ | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
+
+fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
+ Ast.Appl [type_ast (read_type c), ty]
+ | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+
+fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
+ Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
+ | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
- Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
+ Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
| bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
@@ -212,10 +223,10 @@
| tappl_ast_tr' (f, ty :: tys) =
Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
-fun fun_ast_tr' (*"fun"*) asts =
+fun fun_ast_tr' (*"\\<^type>fun"*) asts =
if no_brackets () orelse no_type_brackets () then raise Match
else
- (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
+ (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
(dom as _ :: _ :: _, cod)
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
| _ => raise Match);
@@ -229,20 +240,20 @@
local open Lexicon SynExt in
-val type_ext = syn_ext' false (K false)
+fun type_ext {read_class, read_type} = syn_ext' false (K false)
[Mfix ("_", tidT --> typeT, "", [], max_pri),
Mfix ("_", tvarT --> typeT, "", [], max_pri),
- Mfix ("_", idT --> typeT, "", [], max_pri),
- Mfix ("_", longidT --> typeT, "", [], max_pri),
+ Mfix ("_", idT --> typeT, "_type_name", [], max_pri),
+ Mfix ("_", longidT --> typeT, "_type_name", [], max_pri),
Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("'_()::_", sortT --> typeT, "_dummy_ofsort", [0], max_pri),
- Mfix ("_", idT --> sortT, "", [], max_pri),
- Mfix ("_", longidT --> sortT, "", [], max_pri),
+ Mfix ("_", idT --> sortT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> sortT, "_class_name", [], max_pri),
Mfix ("{}", sortT, "_topsort", [], max_pri),
Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri),
- Mfix ("_", idT --> classesT, "", [], max_pri),
- Mfix ("_", longidT --> classesT, "", [], max_pri),
+ Mfix ("_", idT --> classesT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> classesT, "_class_name", [], max_pri),
Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri),
Mfix ("_,_", [longidT, classesT] ---> classesT, "_classes", [], max_pri),
Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
@@ -251,16 +262,21 @@
Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
Mfix ("_", typeT --> typesT, "", [], max_pri),
Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri),
- Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0),
+ Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "\\<^type>fun", [1, 0], 0),
Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0),
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
- Mfix ("'_", typeT, "dummy", [], max_pri)]
- []
+ Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
+ ["_type_prop"]
(map SynExt.mk_trfun
- [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
+ [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
+ ("_classes", classes_tr o read_class o ProofContext.theory_of),
+ ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
+ ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),
+ ("_tappl", tappl_ast_tr o read_type o ProofContext.theory_of),
+ ("_bracket", K bracket_ast_tr)],
[],
[],
- map SynExt.mk_trfun [("fun", K fun_ast_tr')])
+ map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
[]
([], []);
--- a/src/Pure/pure_thy.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/pure_thy.ML Wed Mar 03 16:43:55 2010 +0100
@@ -225,6 +225,8 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
+
+val tycon = Syntax.mark_type;
val const = Syntax.mark_const;
val typeT = Syntax.typeT;
@@ -318,21 +320,21 @@
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
- [("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
- ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
- ("_type_constraint_", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
- (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
- ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
- ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
+ [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+ ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
+ ("_type_constraint_", typ "'a", NoSyn),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+ (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
+ (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+ ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+ ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
#> Sign.add_modesyntax_i ("", false)
[(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_modesyntax_i ("HTML", false)
--- a/src/Pure/sign.ML Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Pure/sign.ML Wed Mar 03 16:43:55 2010 +0100
@@ -56,10 +56,7 @@
val intern_sort: theory -> sort -> sort
val extern_sort: theory -> sort -> sort
val intern_typ: theory -> typ -> typ
- val extern_typ: theory -> typ -> typ
val intern_term: theory -> term -> term
- val extern_term: theory -> term -> term
- val intern_tycons: theory -> typ -> typ
val the_type_decl: theory -> string -> Type.decl
val arity_number: theory -> string -> int
val arity_sorts: theory -> string -> sort -> sort list
@@ -157,7 +154,7 @@
make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
@@ -266,41 +263,10 @@
| map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
| map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
-val add_classesT = Term.fold_atyps
- (fn TFree (_, S) => fold (insert (op =)) S
- | TVar (_, S) => fold (insert (op =)) S
- | _ => I);
-
-fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
- | add_tyconsT _ = I;
-
-val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
-
-fun mapping add_names f t =
- let
- fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
- val tab = map_filter f' (add_names t []);
- fun get x = the_default x (AList.lookup (op =) tab x);
- in get end;
-
-fun typ_mapping f g thy T =
- T |> map_typ
- (mapping add_classesT (f thy) T)
- (mapping add_tyconsT (g thy) T);
-
-fun term_mapping f g h thy t =
- t |> map_term
- (mapping (Term.fold_types add_classesT) (f thy) t)
- (mapping (Term.fold_types add_tyconsT) (g thy) t)
- (mapping add_consts (h thy) t);
-
in
-val intern_typ = typ_mapping intern_class intern_type;
-val extern_typ = typ_mapping extern_class extern_type;
-val intern_term = term_mapping intern_class intern_type intern_const;
-val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
-val intern_tycons = typ_mapping (K I) intern_type;
+fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
+fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
end;
@@ -424,6 +390,27 @@
val cert_arity = prep_arity (K I) certify_sort;
+(* type syntax entities *)
+
+local
+
+fun read_type thy text =
+ let
+ val (syms, pos) = Syntax.read_token text;
+ val c = intern_type thy (Symbol_Pos.content syms);
+ val _ = the_type_decl thy c;
+ val _ = Position.report (Markup.tycon c) pos;
+ in c end;
+
+in
+
+val _ = Context.>>
+ (Context.map_theory
+ (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
+
+end;
+
+
(** signature extension functions **) (*exception ERROR/TYPE*)
@@ -438,11 +425,13 @@
(* add type constructors *)
+val type_syntax = Syntax.mark_type oo full_name;
+
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val syn' =
Syntax.update_type_gram true Syntax.mode_default
- (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
+ (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
val decls = map (fn (a, n, _) => (a, n)) types;
val tsig' = fold (Type.add_type naming) decls tsig;
in (naming, syn', tsig', consts) end);
@@ -452,9 +441,8 @@
fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
val tsig' = fold (Type.add_nonterminal naming) ns tsig;
- in (naming, syn', tsig', consts) end);
+ in (naming, syn, tsig', consts) end);
(* add type abbreviations *)
@@ -465,7 +453,7 @@
val ctxt = ProofContext.init thy;
val syn' =
Syntax.update_type_gram true Syntax.mode_default
- [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
+ [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming abbr tsig;
@@ -495,8 +483,8 @@
fun type_notation add mode args =
let
- fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
- SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
+ fun type_syntax (Type (c, args), mx) =
+ SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
| type_syntax _ = NONE;
in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
@@ -579,9 +567,8 @@
fun primitive_class (bclass, classes) thy =
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
- in (naming, syn', tsig', consts) end)
+ in (naming, syn, tsig', consts) end)
|> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
--- a/src/Sequents/Sequents.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/Sequents/Sequents.thy Wed Mar 03 16:43:55 2010 +0100
@@ -65,7 +65,7 @@
(* parse translation for sequences *)
-fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
+fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
Const (@{const_syntax SeqO'}, dummyT) $ f
--- a/src/ZF/Induct/Comb.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/ZF/Induct/Comb.thy Wed Mar 03 16:43:55 2010 +0100
@@ -23,6 +23,9 @@
| S
| app ("p \<in> comb", "q \<in> comb") (infixl "@@" 90)
+notation (xsymbols)
+ app (infixl "\<bullet>" 90)
+
text {*
Inductive definition of contractions, @{text "-1->"} and
(multi-step) reductions, @{text "--->"}.
@@ -39,9 +42,6 @@
contract_multi :: "[i,i] => o" (infixl "--->" 50)
where "p ---> q == <p,q> \<in> contract^*"
-syntax (xsymbols)
- "comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90)
-
inductive
domains "contract" \<subseteq> "comb \<times> comb"
intros
--- a/src/ZF/List_ZF.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/ZF/List_ZF.thy Wed Mar 03 16:43:55 2010 +0100
@@ -15,8 +15,8 @@
syntax
- "[]" :: i ("[]")
- "_List" :: "is => i" ("[(_)]")
+ "_Nil" :: i ("[]")
+ "_List" :: "is => i" ("[(_)]")
translations
"[x, xs]" == "CONST Cons(x, [xs])"
--- a/src/ZF/UNITY/Union.thy Wed Mar 03 15:19:34 2010 +0100
+++ b/src/ZF/UNITY/Union.thy Wed Mar 03 16:43:55 2010 +0100
@@ -40,23 +40,22 @@
"safety_prop(X) == X\<subseteq>program &
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
+notation (xsymbols)
+ SKIP ("\<bottom>") and
+ Join (infixl "\<squnion>" 65)
+
syntax
"_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
"_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
translations
"JN x:A. B" == "CONST JOIN(A, (%x. B))"
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "CONST JOIN(CONST state,(%x. B))"
-notation (xsymbols)
- SKIP ("\<bottom>") and
- Join (infixl "\<squnion>" 65)
-
-syntax (xsymbols)
- "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
- "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
-
subsection{*SKIP*}