# HG changeset patch # User wenzelm # Date 1267631035 -3600 # Node ID 991a6af759783b3376e9a70ed3b8740fd195d46c # Parent 89541a30d5c107b4dd9749c95bcb56e2a6c1cac5# Parent 38b291bb4a98699cc4255b2f4b06dc62a6c9e27e merged, resolving some basic conflicts; diff -r 89541a30d5c1 -r 991a6af75978 NEWS --- 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. diff -r 89541a30d5c1 -r 991a6af75978 doc-src/Locales/Locales/Examples3.thy --- 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 diff -r 89541a30d5c1 -r 991a6af75978 doc-src/Locales/Locales/document/Examples3.tex --- 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% diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/AxSem.thy --- 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 @@ "\Vals:v. b" == "(\v. b) \ CONST the_In3" --{* relation on result values, state and auxiliary variables *} -types 'a assn = "res \ state \ 'a \ bool" +types 'a assn = "res \ state \ 'a \ bool" translations - "res" <= (type) "AxSem.res" - "a assn" <= (type) "vals \ state \ a \ bool" + (type) "'a assn" <= (type) "vals \ state \ 'a \ bool" definition assn_imp :: "'a assn \ 'a assn \ bool" (infixr "\" 25) where "P \ Q \ \Y s Z. P Y s Z \ Q Y s Z" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Basis.thy --- 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" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Decl.thy --- 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) "\access::acc_modi\" - "decl" <= (type) "\access::acc_modi,\::'a\" + (type) "decl" <= (type) "\access::acc_modi\" + (type) "decl" <= (type) "\access::acc_modi,\::'a\" subsection {* Member (field or method)*} record member = decl + static :: stat_modi translations - "member" <= (type) "\access::acc_modi,static::bool\" - "member" <= (type) "\access::acc_modi,static::bool,\::'a\" + (type) "member" <= (type) "\access::acc_modi,static::bool\" + (type) "member" <= (type) "\access::acc_modi,static::bool,\::'a\" subsection {* Field *} record field = member + type :: ty translations - "field" <= (type) "\access::acc_modi, static::bool, type::ty\" - "field" <= (type) "\access::acc_modi, static::bool, type::ty,\::'a\" + (type) "field" <= (type) "\access::acc_modi, static::bool, type::ty\" + (type) "field" <= (type) "\access::acc_modi, static::bool, type::ty,\::'a\" types fdecl (* field declaration, cf. 8.3 *) @@ -174,7 +174,7 @@ translations - "fdecl" <= (type) "vname \ field" + (type) "fdecl" <= (type) "vname \ field" subsection {* Method *} @@ -193,17 +193,17 @@ translations - "mhead" <= (type) "\access::acc_modi, static::bool, + (type) "mhead" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty\" - "mhead" <= (type) "\access::acc_modi, static::bool, + (type) "mhead" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty,\::'a\" - "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt\" - "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt,\::'a\" - "methd" <= (type) "\access::acc_modi, static::bool, + (type) "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt\" + (type) "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt,\::'a\" + (type) "methd" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty,mbody::mbody\" - "methd" <= (type) "\access::acc_modi, static::bool, + (type) "methd" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty,mbody::mbody,\::'a\" - "mdecl" <= (type) "sig \ methd" + (type) "mdecl" <= (type) "sig \ methd" definition mhead :: "methd \ mhead" where @@ -306,13 +306,13 @@ = "qtname \ iface" translations - "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list\" - "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list,\::'a\" - "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, + (type) "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list\" + (type) "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list,\::'a\" + (type) "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, isuperIfs::qtname list\" - "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, + (type) "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, isuperIfs::qtname list,\::'a\" - "idecl" <= (type) "qtname \ iface" + (type) "idecl" <= (type) "qtname \ iface" definition ibody :: "iface \ ibody" where "ibody i \ \access=access i,imethods=imethods i\" @@ -337,17 +337,17 @@ = "qtname \ class" translations - "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt\" - "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt,\::'a\" - "class" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "class" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt, super::qtname,superIfs::qtname list\" - "class" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "class" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt, super::qtname,superIfs::qtname list,\::'a\" - "cdecl" <= (type) "qtname \ class" + (type) "cdecl" <= (type) "qtname \ class" definition cbody :: "class \ cbody" where "cbody c \ \access=access c, cfields=cfields c,methods=methods c,init=init c\" @@ -404,8 +404,8 @@ "classes"::"cdecl list" translations - "prog"<= (type) "\ifaces::idecl list,classes::cdecl list\" - "prog"<= (type) "\ifaces::idecl list,classes::cdecl list,\::'a\" + (type) "prog" <= (type) "\ifaces::idecl list,classes::cdecl list\" + (type) "prog" <= (type) "\ifaces::idecl list,classes::cdecl list,\::'a\" abbreviation iface :: "prog \ (qtname, iface) table" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/DeclConcepts.thy --- 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 \ qtname" translations - "fspec" <= (type) "vname \ qtname" + (type) "fspec" <= (type) "vname \ qtname" definition imethds :: "prog \ qtname \ (sig,qtname \ mhead) tables" where "imethds G I diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Eval.thy --- 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 \ (val \ state \ state)" vals = "(val, vvar, val list) sum3" translations - "vvar" <= (type) "val \ (val \ state \ state)" - "vals" <= (type)"(val, vvar, val list) sum3" + (type) "vvar" <= (type) "val \ (val \ state \ 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Name.thy --- 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) \ q" translations - "mname" <= "Name.mname" - "xname" <= "Name.xname" - "tname" <= "Name.tname" - "ename" <= "Name.ename" - "qtname" <= (type) "\pid::pname,tid::tname\" + (type) "qtname" <= (type) "\pid::pname,tid::tname\" (type) "'a qtname_scheme" <= (type) "\pid::pname,tid::tname,\::'a\" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/State.thy --- 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 \ qtname" - "vn" <= (type) "fspec + int" - "obj" <= (type) "\tag::obj_tag, values::vn \ val option\" - "obj" <= (type) "\tag::obj_tag, values::vn \ val option,\::'a\" + (type) "fspec" <= (type) "vname \ qtname" + (type) "vn" <= (type) "fspec + int" + (type) "obj" <= (type) "\tag::obj_tag, values::vn \ val option\" + (type) "obj" <= (type) "\tag::obj_tag, values::vn \ val option,\::'a\" definition the_Arr :: "obj option \ ty \ int \ (vn, val) table" where "the_Arr obj \ SOME (T,k,t). obj = Some \tag=Arr T k,values=t\" @@ -134,7 +134,7 @@ translations "Heap" => "CONST Inl" "Stat" => "CONST Inr" - "oref" <= (type) "loc + qtname" + (type) "oref" <= (type) "loc + qtname" definition fields_table :: "prog \ qtname \ (fspec \ field \ bool) \ (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 \ st" --{* state including abruption information *} translations - "abopt" <= (type) "State.abrupt option" - "abopt" <= (type) "abrupt option" - "state" <= (type) "abopt \ State.st" - "state" <= (type) "abopt \ st" + (type) "abopt" <= (type) "abrupt option" + (type) "state" <= (type) "abopt \ st" abbreviation Norm :: "st \ state" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Table.thy --- 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 \ map_of" translations - (type)"'a \ 'b" <= (type)"'a \ 'b Datatype.option" - (type)"('a, 'b) table" <= (type)"'a \ 'b" + (type) "('a, 'b) table" <= (type) "'a \ 'b" (* ### To map *) lemma map_add_find_left[simp]: diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Term.thy --- 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) "\name::mname,parTs::ty list\" - "sig" <= (type) "\name::mname,parTs::ty list,\::'a\" + (type) "sig" <= (type) "\name::mname,parTs::ty list\" + (type) "sig" <= (type) "\name::mname,parTs::ty list,\::'a\" --{* 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 \ 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 \ ty list" + (type) "term" <= (type) "(expr+stmt,var,expr list) sum3" abbreviation this :: expr where "this == Acc (LVar This)" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Type.thy --- 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)" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/Value.thy --- 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 \ bool" primrec "the_Bool (Bool b) = b" consts the_Intg :: "val \ int" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Bali/WellType.thy --- 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 \ ty option" - "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv\" - "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv,\::'a\" + (type) "lenv" <= (type) "(lname, ty) table" + (type) "lenv" <= (type) "lname \ ty option" + (type) "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv\" + (type) "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv,\::'a\" 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/IMPP/Hoare.thy --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ mrec_dom x" + "mrec_graph x y \ mrec_dom x" apply (induct rule:mrec_graph.induct) apply (rule accpI) apply (erule mrec_rel.cases) by simp lemma f_default: "\ mrec_dom (f, g, x, h) \ 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: diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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 \ make_llist xs; next \ Ref.new tl; - return (Node x next) - done" + return (Node x next) + done" text {* define traverse using the MREC combinator *} diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Library/Numeral_Type.thy --- 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 \ t set)" +translations "CARD('t)" => "CONST card (CONST UNIV \ 't set)" typed_print_translation {* let diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Library/Transitive_Closure_Table.thy --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Map.thy --- 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 "\" 0) +type_notation (xsymbols) + "~=>" (infixr "\" 0) abbreviation empty :: "'a ~=> 'b" where diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/MicroJava/J/Decl.thy --- 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 \ ty" - "sig" <= (type) "mname \ ty list" - "mdecl c" <= (type) "sig \ ty \ c" - "class c" <= (type) "cname \ fdecl list \ (c mdecl) list" - "cdecl c" <= (type) "cname \ (c class)" - "prog c" <= (type) "(c cdecl) list" + (type) "fdecl" <= (type) "vname \ ty" + (type) "sig" <= (type) "mname \ ty list" + (type) "'c mdecl" <= (type) "sig \ ty \ 'c" + (type) "'c class" <= (type) "cname \ fdecl list \ ('c mdecl) list" + (type) "'c cdecl" <= (type) "cname \ ('c class)" + (type) "'c prog" <= (type) "('c cdecl) list" definition "class" :: "'c prog => (cname \ 'c class)" where diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/NanoJava/AxSem.thy --- 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 \ stmt \ assn" etriple = "assn \ expr \ vassn" translations - "assn" \ (type)"state => bool" - "vassn" \ (type)"val => assn" - "triple" \ (type)"assn \ stmt \ assn" - "etriple" \ (type)"assn \ expr \ vassn" + (type) "assn" \ (type) "state => bool" + (type) "vassn" \ (type) "val => assn" + (type) "triple" \ (type) "assn \ stmt \ assn" + (type) "etriple" \ (type) "assn \ expr \ vassn" subsection "Hoare Logic Rules" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/NanoJava/Decl.thy --- 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" \ (type)"fname \ ty" - "mdecl" \ (type)"mname \ ty \ ty \ stmt" - "class" \ (type)"cname \ fdecl list \ mdecl list" - "cdecl" \ (type)"cname \ class" - "prog " \ (type)"cdecl list" + (type) "fdecl" \ (type) "fname \ ty" + (type) "mdecl" \ (type) "mname \ ty \ ty \ stmt" + (type) "class" \ (type) "cname \ fdecl list \ mdecl list" + (type) "cdecl" \ (type) "cname \ class" + (type) "prog " \ (type) "cdecl list" consts diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/NanoJava/State.thy --- 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 \ fields" translations - - "fields" \ (type)"fname => val option" - "obj" \ (type)"cname \ fields" + (type) "fields" \ (type) "fname => val option" + (type) "obj" \ (type) "cname \ fields" definition init_vars :: "('a \ 'b) => ('a \ val)" where "init_vars m == Option.map (\T. Null) o m" @@ -40,10 +39,9 @@ locals :: locals translations - - "heap" \ (type)"loc => obj option" - "locals" \ (type)"vname => val option" - "state" \ (type)"(|heap :: heap, locals :: locals|)" + (type) "heap" \ (type) "loc => obj option" + (type) "locals" \ (type) "vname => val option" + (type) "state" \ (type) "(|heap :: heap, locals :: locals|)" definition del_locs :: "state => state" where "del_locs s \ s (| locals := empty |)" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Product_Type.thy --- 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" ("(_ \/ _)" [21, 20] 20) -syntax (HTML output) - "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) +type_notation (xsymbols) + "*" ("(_ \/ _)" [21, 20] 20) +type_notation (HTML output) + "*" ("(_ \/ _)" [21, 20] 20) consts Pair :: "'a \ 'b \ 'a \ 'b" diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Tools/numeral_syntax.ML --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Tools/record.ML --- 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 = diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Tools/typedef.ML --- 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); diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/Typerep.thy --- 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) diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/UNITY/Union.thy --- 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 & (\G. Acts G \ UNION X Acts --> G \ X)" +notation (xsymbols) + SKIP ("\") and + Join (infixl "\" 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\ _./ _)" 10) + "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _\_./ _)" 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" ("\") - Join :: "['a program, 'a program] => 'a program" (infixl "\" 65) - "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\ _./ _)" 10) - "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _\_./ _)" 10) - subsection{*SKIP*} diff -r 89541a30d5c1 -r 991a6af75978 src/HOL/ex/Numeral.thy --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/Cfun.thy diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/One.thy --- 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" diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/Representable.thy --- 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" \ (type) "udom alg_defl" +translations (type) "TypeRep" \ (type) "udom alg_defl" definition Rep_of :: "'a::rep itself \ TypeRep" @@ -60,7 +60,7 @@ (emb oo (approx i :: 'a \ 'a) oo prj)))" syntax "_REP" :: "type \ TypeRep" ("(1REP/(1'(_')))") -translations "REP(t)" \ "CONST Rep_of TYPE(t)" +translations "REP('t)" \ "CONST Rep_of TYPE('t)" lemma cast_REP: "cast\REP('a::rep) = (emb::'a \ udom) oo (prj::udom \ 'a)" diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/Sprod.thy --- 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" ("(_ \/ _)" [21,20] 20) -syntax (HTML output) - sprod :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) +type_notation (xsymbols) + sprod ("(_ \/ _)" [21,20] 20) +type_notation (HTML output) + sprod ("(_ \/ _)" [21,20] 20) lemma spair_lemma: "(strictify\(\ b. a)\b, strictify\(\ a. b)\a) \ Sprod" diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/Ssum.thy --- 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" ("(_ \/ _)" [21, 20] 20) -syntax (HTML output) - ssum :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) +type_notation (xsymbols) + ssum ("(_ \/ _)" [21, 20] 20) +type_notation (HTML output) + ssum ("(_ \/ _)" [21, 20] 20) + subsection {* Definitions of constructors *} diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/Tr.thy --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/Up.thy --- 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 \ type" ("(_\<^sub>\)" [1000] 999) +type_notation (xsymbols) + u ("(_\<^sub>\)" [1000] 999) primrec Ifup :: "('a \ 'b::pcpo) \ 'a u \ 'b" where "Ifup f Ibottom = \" diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/ex/Strict_Fun.thy --- 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 \ 'b. f\\ = \}" by simp_all -syntax (xsymbols) - sfun :: "type \ type \ type" (infixr "\!" 0) +type_notation (xsymbols) + sfun (infixr "\!" 0) text {* TODO: Define nice syntax for abstraction, application. *} diff -r 89541a30d5c1 -r 991a6af75978 src/HOLCF/holcf_logic.ML --- 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; diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/General/name_space.ML --- 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 *) diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Isar/local_syntax.ML --- 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; diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Isar/proof_context.ML --- 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; + diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/ML/ml_antiquote.ML --- 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 *) diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Proof/extraction.ML --- 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 **) diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Syntax/lexicon.ML --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Syntax/printer.ML --- 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; diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Syntax/syn_ext.ML --- 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; diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Syntax/syn_trans.ML --- 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); diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Syntax/syntax.ML --- 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; diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/Syntax/type_ext.ML --- 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')]) [] ([], []); diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/pure_thy.ML --- 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 ("(_/ \\ _)", [1, 0], 0)), - ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), - ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), - ("_idtyp", typ "id => type => idt", Mixfix ("_\\_", [], 0)), - ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), - ("_type_constraint_", typ "'a", NoSyn), - ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - (const "==", typ "'a => 'a => prop", Infixr ("\\", 2)), - (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), - ("_DDDOT", typ "aprop", Delimfix "\\"), - ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), - ("_DDDOT", typ "logic", Delimfix "\\")] + [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), + ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), + ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), + ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), + ("_idtyp", typ "id => type => idt", Mixfix ("_\\_", [], 0)), + ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), + ("_type_constraint_", typ "'a", NoSyn), + ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), + (const "==", typ "'a => 'a => prop", Infixr ("\\", 2)), + (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), + (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), + ("_DDDOT", typ "aprop", Delimfix "\\"), + ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), + ("_DDDOT", typ "logic", Delimfix "\\")] #> Sign.add_modesyntax_i ("", false) [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))] #> Sign.add_modesyntax_i ("HTML", false) diff -r 89541a30d5c1 -r 991a6af75978 src/Pure/sign.ML --- 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); diff -r 89541a30d5c1 -r 991a6af75978 src/Sequents/Sequents.thy --- 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 diff -r 89541a30d5c1 -r 991a6af75978 src/ZF/Induct/Comb.thy --- 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 \ comb", "q \ comb") (infixl "@@" 90) +notation (xsymbols) + app (infixl "\" 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 == \ contract^*" -syntax (xsymbols) - "comb.app" :: "[i, i] => i" (infixl "\" 90) - inductive domains "contract" \ "comb \ comb" intros diff -r 89541a30d5c1 -r 991a6af75978 src/ZF/List_ZF.thy --- 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])" diff -r 89541a30d5c1 -r 991a6af75978 src/ZF/UNITY/Union.thy --- 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\program & SKIP \ X & (\G \ program. Acts(G) \ (\F \ X. Acts(F)) --> G \ X)" +notation (xsymbols) + SKIP ("\") and + Join (infixl "\" 65) + syntax "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) +syntax (xsymbols) + "_JOIN1" :: "[pttrns, i] => i" ("(3\ _./ _)" 10) + "_JOIN" :: "[pttrn, i, i] => i" ("(3\ _ \ _./ _)" 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 ("\") and - Join (infixl "\" 65) - -syntax (xsymbols) - "_JOIN1" :: "[pttrns, i] => i" ("(3\ _./ _)" 10) - "_JOIN" :: "[pttrn, i, i] => i" ("(3\ _ \ _./ _)" 10) - subsection{*SKIP*}