# HG changeset patch # User wenzelm # Date 1302194509 -7200 # Node ID 992892b482962a31d6a8e4368a0a5b70d819edbe # Parent 79be89e07589b2af83762029e062f4e98141039d# Parent 01401287c3f735d5ce8041e7ed1ee3e0696d76c0 merged diff -r 79be89e07589 -r 992892b48296 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Thu Apr 07 14:51:28 2011 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Thu Apr 07 18:41:49 2011 +0200 @@ -57,7 +57,7 @@ let fun Lambda_ast_tr [pats, body] = Ast.fold_ast_p @{syntax_const "_cabs"} - (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body) + (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body) | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts); in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end; *} diff -r 79be89e07589 -r 992892b48296 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Apr 07 18:41:49 2011 +0200 @@ -456,7 +456,7 @@ fun con1 authentic n (con,args) = Library.foldl capp (c_ast authentic con, argvars n args) fun case1 authentic (n, c) = - app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n) + app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n) fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args) fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom} val case_constant = Ast.Constant (syntax (case_const dummyT)) diff -r 79be89e07589 -r 992892b48296 src/HOL/List.thy --- a/src/HOL/List.thy Thu Apr 07 14:51:28 2011 +0200 +++ b/src/HOL/List.thy Thu Apr 07 18:41:49 2011 +0200 @@ -385,7 +385,7 @@ let val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT); val e = if opti then singl e else e; - val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e; + val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e; val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const @{const_syntax dummy_pattern} $ NilC; diff -r 79be89e07589 -r 992892b48296 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Thu Apr 07 18:41:49 2011 +0200 @@ -624,7 +624,7 @@ else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[])); fun lookup_tr ctxt [s, x] = - (case Syntax.strip_positions x of + (case Term_Position.strip_positions x of Free (n,_) => gen_lookup_tr ctxt s n | _ => raise Match); @@ -656,7 +656,7 @@ end; fun update_tr ctxt [s, x, v] = - (case Syntax.strip_positions x of + (case Term_Position.strip_positions x of Free (n, _) => gen_update_tr false ctxt n v s | _ => raise Match); diff -r 79be89e07589 -r 992892b48296 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/General/pretty.ML Thu Apr 07 18:41:49 2011 +0200 @@ -34,6 +34,8 @@ val strs: string list -> T val markup: Markup.T -> T list -> T val mark: Markup.T -> T -> T + val mark_str: Markup.T * string -> T + val marks_str: Markup.T list * string -> T val keyword: string -> T val command: string -> T val markup_chunks: Markup.T -> T list -> T @@ -138,9 +140,12 @@ val strs = block o breaks o map str; fun markup m prts = markup_block m (0, prts); -fun mark m prt = markup m [prt]; -fun keyword name = mark Markup.keyword (str name); -fun command name = mark Markup.command (str name); +fun mark m prt = if m = Markup.empty then prt else markup m [prt]; +fun mark_str (m, s) = mark m (str s); +fun marks_str (ms, s) = fold_rev mark ms (str s); + +fun keyword name = mark_str (Markup.keyword, name); +fun command name = mark_str (Markup.command, name); fun markup_chunks m prts = markup m (fbreaks prts); val chunks = markup_chunks Markup.empty; diff -r 79be89e07589 -r 992892b48296 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/IsaMakefile Thu Apr 07 18:41:49 2011 +0200 @@ -188,7 +188,7 @@ Syntax/syn_trans.ML \ Syntax/syntax.ML \ Syntax/syntax_phases.ML \ - Syntax/type_ext.ML \ + Syntax/term_position.ML \ System/isabelle_process.ML \ System/isabelle_system.ML \ System/isar.ML \ diff -r 79be89e07589 -r 992892b48296 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 07 18:41:49 2011 +0200 @@ -400,40 +400,6 @@ | NONE => x); -(* default token translations *) - -local - -fun free_or_skolem ctxt x = - (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x)) - else Pretty.mark Markup.free (Pretty.str x)) - |> Pretty.mark - (if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x - else Markup.hilite); - -fun var_or_skolem _ s = - (case Lexicon.read_variable s of - SOME (x, i) => - (case try Name.dest_skolem x of - NONE => Pretty.mark Markup.var (Pretty.str s) - | SOME x' => Pretty.mark Markup.skolem (Pretty.str (Term.string_of_vname (x', i)))) - | NONE => Pretty.mark Markup.var (Pretty.str s)); - -fun plain_markup m _ s = Pretty.mark m (Pretty.str s); - -val token_trans = - Syntax.tokentrans_mode "" - [("tfree", plain_markup Markup.tfree), - ("tvar", plain_markup Markup.tvar), - ("free", free_or_skolem), - ("bound", plain_markup Markup.bound), - ("var", var_or_skolem), - ("numeral", plain_markup Markup.numeral), - ("inner_string", plain_markup Markup.inner_string)]; - -in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end; - - (** prepare terms and propositions **) diff -r 79be89e07589 -r 992892b48296 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Isar/specification.ML Thu Apr 07 18:41:49 2011 +0200 @@ -122,7 +122,9 @@ val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars; - val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss; + val Asss = + (map o map) snd raw_specss + |> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt)); val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss) |> fold Name.declare xs; val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names); diff -r 79be89e07589 -r 992892b48296 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/ROOT.ML Thu Apr 07 18:41:49 2011 +0200 @@ -114,16 +114,16 @@ use "sorts.ML"; use "type.ML"; use "logic.ML"; -use "Syntax/lexicon.ML"; -use "Syntax/simple_syntax.ML"; (* inner syntax *) +use "Syntax/term_position.ML"; +use "Syntax/lexicon.ML"; +use "Syntax/simple_syntax.ML"; use "Syntax/ast.ML"; use "Syntax/syn_ext.ML"; use "Syntax/parser.ML"; -use "Syntax/type_ext.ML"; use "Syntax/syn_trans.ML"; use "Syntax/mixfix.ML"; use "Syntax/printer.ML"; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/ast.ML Thu Apr 07 18:41:49 2011 +0200 @@ -14,6 +14,7 @@ exception AST of string * ast list val pretty_ast: ast -> Pretty.T val pretty_rule: ast * ast -> Pretty.T + val strip_positions: ast -> ast val head_of_rule: ast * ast -> string val rule_error: ast * ast -> string option val fold_ast: string -> ast list -> ast @@ -57,8 +58,8 @@ fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a) | pretty_ast (Variable x) = - (case Lexicon.decode_position x of - SOME pos => Lexicon.pretty_position pos + (case Term_Position.decode x of + SOME pos => Term_Position.pretty pos | NONE => Pretty.str x) | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); @@ -66,7 +67,17 @@ Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]; -(* head_of_ast, head_of_rule *) +(* strip_positions *) + +fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) = + if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Term_Position.decode x) + then mk_appl (strip_positions u) (map strip_positions asts) + else Appl (map strip_positions (t :: u :: v :: asts)) + | strip_positions (Appl asts) = Appl (map strip_positions asts) + | strip_positions ast = ast; + + +(* head_of_ast and head_of_rule *) fun head_of_ast (Constant a) = a | head_of_ast (Appl (Constant a :: _)) = a diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/lexicon.ML Thu Apr 07 18:41:49 2011 +0200 @@ -44,9 +44,6 @@ val is_marked: string -> bool val dummy_type: term val fun_type: term - val pretty_position: Position.T -> Pretty.T - val encode_position: Position.T -> string - val decode_position: string -> Position.T option end; signature LEXICON = @@ -459,24 +456,4 @@ exp = length fracpart} end; - -(* positions *) - -val position_dummy = ""; -val position_text = XML.Text position_dummy; - -fun pretty_position pos = - Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy]; - -fun encode_position pos = - YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text])); - -fun decode_position str = - (case YXML.parse_body str handle Fail msg => error msg of - [XML.Elem ((name, props), [arg])] => - if name = Markup.positionN andalso arg = position_text - then SOME (Position.of_properties props) - else NONE - | _ => NONE); - end; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/mixfix.ML Thu Apr 07 18:41:49 2011 +0200 @@ -119,7 +119,7 @@ val mfix = map mfix_of type_decls; val _ = map2 check_args type_decls mfix; val xconsts = map #1 type_decls; - in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end; + in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end; (* syn_ext_consts *) @@ -160,7 +160,7 @@ apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap); in Syn_Ext.syn_ext' true is_logtype - mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) + mfix xconsts ([], binder_trs, binder_trs', []) ([], []) end; end; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Apr 07 18:41:49 2011 +0200 @@ -33,14 +33,15 @@ val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs val merge_prtabs: prtabs -> prtabs -> prtabs - val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring, - extern_const: string -> xstring} -> Proof.context -> bool -> prtabs -> + val pretty_term_ast: bool -> Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> - (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 -> string -> Pretty.T option) -> + (string -> Markup.T list * xstring) -> + Ast.ast -> Pretty.T list + val pretty_typ_ast: Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> - (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list + (string -> string -> Pretty.T option) -> + (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list end; structure Printer: PRINTER = @@ -166,68 +167,55 @@ val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0))); -fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 = +fun pretty type_mode curried ctxt tabs trf token_trans markup_extern ast0 = let - val {extern_class, extern_type, extern_const} = extern; val show_brackets = Config.get ctxt show_brackets; - fun token_trans a x = - (case tokentrf a of - NONE => - if member (op =) Syn_Ext.standard_token_classes a - then SOME (Pretty.str x) else NONE - | SOME f => SOME (f ctxt x)); - (*default applications: prefix / postfix*) val appT = - if type_mode then Type_Ext.tappl_ast_tr' + if type_mode then Syn_Trans.tappl_ast_tr' else if curried then Syn_Trans.applC_ast_tr' else Syn_Trans.appl_ast_tr'; fun synT _ ([], args) = ([], args) - | synT markup (Arg p :: symbs, t :: args) = - let val (Ts, args') = synT markup (symbs, args); + | synT m (Arg p :: symbs, t :: args) = + let val (Ts, args') = synT m (symbs, args); in (astT (t, p) @ Ts, args') end - | synT markup (TypArg p :: symbs, t :: args) = + | synT m (TypArg p :: symbs, t :: args) = let - val (Ts, args') = synT markup (symbs, args); + val (Ts, args') = synT m (symbs, args); in if type_mode then (astT (t, p) @ Ts, args') else - (pretty extern (Config.put pretty_priority p ctxt) - tabs trf tokentrf true curried t @ Ts, args') + (pretty true curried (Config.put pretty_priority p ctxt) + tabs trf token_trans markup_extern t @ Ts, args') end - | synT markup (String s :: symbs, args) = - let val (Ts, args') = synT markup (symbs, args); - in (markup (Pretty.str s) :: Ts, args') end - | synT markup (Space s :: symbs, args) = - let val (Ts, args') = synT markup (symbs, args); + | synT m (String s :: symbs, args) = + let val (Ts, args') = synT m (symbs, args); + in (Pretty.marks_str (m, s) :: Ts, args') end + | synT m (Space s :: symbs, args) = + let val (Ts, args') = synT m (symbs, args); in (Pretty.str s :: Ts, args') end - | synT markup (Block (i, bsymbs) :: symbs, args) = + | synT m (Block (i, bsymbs) :: symbs, args) = let - val (bTs, args') = synT markup (bsymbs, args); - val (Ts, args'') = synT markup (symbs, args'); + val (bTs, args') = synT m (bsymbs, args); + val (Ts, args'') = synT m (symbs, args'); val T = if i < 0 then Pretty.unbreakable (Pretty.block bTs) else Pretty.blk (i, bTs); in (T :: Ts, args'') end - | synT markup (Break i :: symbs, args) = + | synT m (Break i :: symbs, args) = let - val (Ts, args') = synT markup (symbs, args); + val (Ts, args') = synT m (symbs, args); val T = if i < 0 then Pretty.fbrk else Pretty.brk i; in (T :: Ts, args') end - and parT markup (pr, args, p, p': int) = #1 (synT markup + and parT m (pr, args, p, p': int) = #1 (synT m (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr)) then [Block (1, Space "(" :: pr @ [Space ")"])] else pr, args)) - 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 atomT a = Pretty.marks_str (markup_extern a) and prefixT (_, a, [], _) = [atomT a] | prefixT (c, _, args, p) = astT (appT (c, args), p) @@ -239,18 +227,12 @@ and combT (tup as (c, a, args, p)) = let val nargs = length args; - 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 | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs) | prnt ((pr, n, p') :: prnps, tbs) = - if nargs = n then parT markup (pr, args, p, p') + if nargs = n then parT (#1 (markup_extern a)) (pr, args, p, p') else if nargs > n andalso not type_mode then astT (appT (splitT n ([c], args)), p) else prnt (prnps, tbs); @@ -264,7 +246,7 @@ | tokentrT _ _ = NONE and astT (c as Ast.Constant a, p) = combT (c, a, [], p) - | astT (ast as Ast.Variable x, _) = [Ast.pretty_ast ast] + | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast] | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p) | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]); @@ -273,14 +255,13 @@ (* pretty_term_ast *) -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; +fun pretty_term_ast curried ctxt prtabs trf tokentrf extern ast = + pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast; (* pretty_typ_ast *) -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; +fun pretty_typ_ast ctxt prtabs trf tokentrf extern ast = + pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast; end; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Thu Apr 07 18:41:49 2011 +0200 @@ -15,11 +15,7 @@ val mk_trfun: string * 'a -> string * ('a * stamp) val eq_trfun: ('a * stamp) * ('a * stamp) -> bool val escape: string -> string - val tokentrans_mode: - string -> (string * (Proof.context -> string -> Pretty.T)) list -> - (string * string * (Proof.context -> string -> Pretty.T)) list - val standard_token_classes: string list - val standard_token_markers: string list + val token_markers: string list end; signature SYN_EXT = @@ -45,30 +41,26 @@ Syn_Ext of { xprods: xprod list, consts: string list, - prmodes: string list, parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, parse_rules: (Ast.ast * Ast.ast) list, parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, print_rules: (Ast.ast * Ast.ast) list, - print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, - token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list} + print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} val mfix_delims: string -> string list val mfix_args: string -> int val syn_ext': bool -> (string -> bool) -> mfix list -> string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list - -> (string * string * (Proof.context -> string -> Pretty.T)) list - -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> + (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext val syn_ext: mfix list -> string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list - -> (string * string * (Proof.context -> string -> Pretty.T)) list - -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> + (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext val syn_ext_const_names: string list -> syn_ext val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext val syn_ext_trfuns: @@ -81,7 +73,6 @@ (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext - val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext val pure_ext: syn_ext end; @@ -330,19 +321,17 @@ Syn_Ext of { xprods: xprod list, consts: string list, - prmodes: string list, parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, parse_rules: (Ast.ast * Ast.ast) list, parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, print_rules: (Ast.ast * Ast.ast) list, - print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, - token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}; + print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}; (* syn_ext *) -fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) = +fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) = let val (parse_ast_translation, parse_translation, print_translation, print_ast_translation) = trfuns; @@ -355,23 +344,20 @@ Syn_Ext { xprods = xprods, consts = union (op =) consts mfix_consts, - prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns), parse_ast_translation = parse_ast_translation, parse_rules = parse_rules' @ parse_rules, parse_translation = parse_translation, print_translation = print_translation, print_rules = map swap parse_rules' @ print_rules, - print_ast_translation = print_ast_translation, - token_translation = tokentrfuns} + print_ast_translation = print_ast_translation} end; val syn_ext = syn_ext' true (K false); -fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []); -fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules; -fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns [] ([], []); -fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []); +fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []); +fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; +fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []); fun syn_ext_trfuns (atrs, trs, tr's, atr's) = let fun simple (name, (f, s)) = (name, (K f, s)) in @@ -383,17 +369,10 @@ fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2; -(* token translations *) - -fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; +(* pure_ext *) -val standard_token_classes = - ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"]; - -val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes; - - -(* pure_ext *) +val token_markers = + ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"]; val pure_ext = syn_ext' false (K false) [Mfix ("_", spropT --> propT, "", [0], 0), @@ -403,9 +382,8 @@ Mfix ("'(_')", spropT --> spropT, "", [0], max_pri), Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3), Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)] - standard_token_markers + token_markers ([], [], [], []) - [] ([], []); end; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Thu Apr 07 18:41:49 2011 +0200 @@ -33,6 +33,8 @@ signature SYN_TRANS1 = sig include SYN_TRANS0 + val no_brackets: unit -> bool + val no_type_brackets: unit -> bool val non_typed_tr': (term list -> term) -> typ -> term list -> term val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term val constrainAbsC: string @@ -52,6 +54,7 @@ signature SYN_TRANS = sig include SYN_TRANS1 + val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val abs_tr': Proof.context -> term -> term val prop_tr': term -> term val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast @@ -61,12 +64,29 @@ structure Syn_Trans: SYN_TRANS = struct +(* print mode *) + +val bracketsN = "brackets"; +val no_bracketsN = "no_brackets"; + +fun no_brackets () = + find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) + (print_mode_value ()) = SOME no_bracketsN; + +val type_bracketsN = "type_brackets"; +val no_type_bracketsN = "no_type_brackets"; + +fun no_type_brackets () = + find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) + (print_mode_value ()) <> SOME type_bracketsN; + + (** parse (ast) translations **) (* strip_positions *) -fun strip_positions_ast_tr [ast] = Type_Ext.strip_positions_ast ast +fun strip_positions_ast_tr [ast] = Ast.strip_positions ast | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts); @@ -76,6 +96,18 @@ | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); +(* type syntax *) + +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] + | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); + +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) + | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); + +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) + | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); + + (* application *) fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) @@ -191,7 +223,7 @@ 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) = - if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) + if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) else list_comb (c $ update_name_tr [t] $ (Lexicon.fun_type $ @@ -247,6 +279,22 @@ fun non_typed_tr'' f x _ ts = f x ts; +(* type syntax *) + +fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) + | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] + | tappl_ast_tr' (f, ty :: tys) = + Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; + +fun fun_ast_tr' asts = + if no_brackets () orelse no_type_brackets () then raise Match + else + (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); + + (* application *) fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) @@ -387,7 +435,7 @@ (* meta implication *) fun impl_ast_tr' (*"==>"*) asts = - if Type_Ext.no_brackets () then raise Match + if no_brackets () then raise Match else (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of (prems as _ :: _ :: _, concl) => @@ -484,6 +532,9 @@ val pure_trfuns = ([("_strip_positions", strip_positions_ast_tr), ("_constify", constify_ast_tr), + ("_tapp", tapp_ast_tr), + ("_tappl", tappl_ast_tr), + ("_bracket", bracket_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr), ("_lambda", lambda_ast_tr), @@ -503,7 +554,8 @@ ("_update_name", update_name_tr), ("_index", index_tr)], ([]: (string * (term list -> term)) list), - [("_abs", abs_ast_tr'), + [("\\<^type>fun", fun_ast_tr'), + ("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), ("_pttrns", idtyp_ast_tr' "_pttrns"), ("\\<^const>==>", impl_ast_tr'), diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu Apr 07 18:41:49 2011 +0200 @@ -16,10 +16,15 @@ sig include LEXICON0 include SYN_EXT0 - include TYPE_EXT0 include SYN_TRANS1 include MIXFIX1 include PRINTER0 + val positions_raw: Config.raw + val positions: bool Config.T + val ambiguity_enabled: bool Config.T + val ambiguity_level_raw: Config.raw + val ambiguity_level: int Config.T + val ambiguity_limit: int Config.T val read_token: string -> Symbol_Pos.T list * Position.T val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T val parse_sort: Proof.context -> string -> sort @@ -95,9 +100,6 @@ val string_of_sort_global: theory -> sort -> string val pp: Proof.context -> Pretty.pp val pp_global: theory -> Pretty.pp - val lookup_tokentr: - (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list -> - string list -> string -> (Proof.context -> string -> Pretty.T) option type ruletab type syntax val eq_syntax: syntax * syntax -> bool @@ -112,8 +114,6 @@ val print_rules: syntax -> string -> (Ast.ast * Ast.ast) list val print_ast_translation: syntax -> string -> Proof.context -> Ast.ast list -> Ast.ast (*exception Match*) - val token_translation: syntax -> string list -> - string -> (Proof.context -> string -> Pretty.T) option val prtabs: syntax -> Printer.prtabs type mode val mode_default: mode @@ -125,12 +125,6 @@ val print_trans: syntax -> unit val print_syntax: syntax -> unit val guess_infix: syntax -> string -> mixfix option - val positions_raw: Config.raw - val positions: bool Config.T - val ambiguity_enabled: bool Config.T - val ambiguity_level_raw: Config.raw - val ambiguity_level: int Config.T - val ambiguity_limit: int Config.T datatype 'a trrule = Parse_Rule of 'a * 'a | Print_Rule of 'a * 'a | @@ -147,8 +141,6 @@ (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax - val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> - syntax -> syntax val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_const_gram: bool -> (string -> bool) -> mode -> (string * typ * mixfix) list -> syntax -> syntax @@ -161,6 +153,21 @@ (** inner syntax operations **) +(* configuration options *) + +val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true); +val positions = Config.bool positions_raw; + +val ambiguity_enabled = + Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true)); + +val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1); +val ambiguity_level = Config.int ambiguity_level_raw; + +val ambiguity_limit = + Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10)); + + (* read token -- with optional YXML encoding of position *) fun read_token str = @@ -432,51 +439,12 @@ -(** tables of token translation functions **) - -fun lookup_tokentr tabs modes = - let val trs = - distinct (eq_fst (op = : string * string -> bool)) - (maps (these o AList.lookup (op =) tabs) (modes @ [""])) - in fn c => Option.map fst (AList.lookup (op =) trs c) end; - -fun merge_tokentrtabs tabs1 tabs2 = - let - fun eq_tr ((c1, (_, s1: stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2; - - fun name (s, _) = implode (tl (Symbol.explode s)); - - fun merge mode = - let - val trs1 = these (AList.lookup (op =) tabs1 mode); - val trs2 = these (AList.lookup (op =) tabs2 mode); - val trs = distinct eq_tr (trs1 @ trs2); - in - (case duplicates (eq_fst (op =)) trs of - [] => (mode, trs) - | dups => error ("More than one token translation function in mode " ^ - quote mode ^ " for " ^ commas_quote (map name dups))) - end; - in map merge (distinct (op =) (map fst (tabs1 @ tabs2))) end; - -fun extend_tokentrtab tokentrs tabs = - let - fun ins_tokentr (m, c, f) = - AList.default (op =) (m, []) - #> AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ()))); - in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end; - - - (** tables of translation rules **) type ruletab = (Ast.ast * Ast.ast) list Symtab.table; fun dest_ruletab tab = maps snd (Symtab.dest tab); - -(* empty, update, merge ruletabs *) - val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r)); val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r)); fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2); @@ -498,7 +466,6 @@ print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table, print_ruletab: ruletab, print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, - tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list, prtabs: Printer.prtabs} * stamp; fun rep_syntax (Syntax (tabs, _)) = tabs; @@ -514,7 +481,6 @@ fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab; fun print_rules (Syntax ({print_ruletab, ...}, _)) = Symtab.lookup_list print_ruletab; fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab; -fun token_translation (Syntax ({tokentrtab, ...}, _)) = lookup_tokentr tokentrtab; fun prtabs (Syntax ({prtabs, ...}, _)) = prtabs; @@ -537,7 +503,6 @@ print_trtab = Symtab.empty, print_ruletab = Symtab.empty, print_ast_trtab = Symtab.empty, - tokentrtab = [], prtabs = Printer.empty_prtabs}, stamp ()); @@ -545,12 +510,11 @@ fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let - val {input, lexicon, gram, consts = consts1, prmodes = prmodes1, - parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, - print_ast_trtab, tokentrtab, prtabs} = tabs; - val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2, - parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, - print_ast_translation, token_translation} = syn_ext; + val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab, + parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; + val Syn_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation, + parse_rules, parse_translation, print_translation, print_rules, + print_ast_translation} = syn_ext; val new_xprods = if inout then distinct (op =) (filter_out (member (op =) input) xprods) else []; fun if_inout xs = if inout then xs else []; @@ -560,7 +524,7 @@ lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon, gram = Parser.extend_gram new_xprods gram, consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2), - prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)), + prmodes = insert (op =) mode prmodes, parse_ast_trtab = update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab, @@ -568,7 +532,6 @@ print_trtab = update_tr'tab print_translation print_trtab, print_ruletab = update_ruletab print_rules print_ruletab, print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab, - tokentrtab = extend_tokentrtab token_translation tokentrtab, prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ()) end; @@ -577,12 +540,10 @@ fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let - val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _, - parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, - print_ast_translation, token_translation = _} = syn_ext; - val {input, lexicon, gram, consts, prmodes, - parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, - print_ast_trtab, tokentrtab, prtabs} = tabs; + val Syn_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules, + parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; + val {input, lexicon, gram, consts, prmodes, parse_ast_trtab, parse_ruletab, + parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; val input' = if inout then subtract (op =) xprods input else input; val changed = length input <> length input'; fun if_inout xs = if inout then xs else []; @@ -599,7 +560,6 @@ print_trtab = remove_tr'tab print_translation print_trtab, print_ruletab = remove_ruletab print_rules print_ruletab, print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab, - tokentrtab = tokentrtab, prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ()) end; @@ -609,16 +569,14 @@ fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) = let val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1, - prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, - parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1, - print_trtab = print_trtab1, print_ruletab = print_ruletab1, - print_ast_trtab = print_ast_trtab1, tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1; + prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1, + parse_trtab = parse_trtab1, print_trtab = print_trtab1, print_ruletab = print_ruletab1, + print_ast_trtab = print_ast_trtab1, prtabs = prtabs1} = tabs1; val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2, - prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, - parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2, - print_trtab = print_trtab2, print_ruletab = print_ruletab2, - print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2; + prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2, + parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2, + print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2; in Syntax ({input = Library.merge (op =) (input1, input2), @@ -633,17 +591,13 @@ print_trtab = merge_tr'tabs print_trtab1 print_trtab2, print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2, print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2, - tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2, prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ()) end; (* basic syntax *) -val basic_syntax = - empty_syntax - |> update_syntax mode_default Type_Ext.type_ext - |> update_syntax mode_default Syn_Ext.pure_ext; +val basic_syntax = update_syntax mode_default Syn_Ext.pure_ext empty_syntax; val basic_nonterms = (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes", @@ -678,10 +632,8 @@ fun pretty_ruletab name tab = Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab)); - fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs); - val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, - print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs; + print_ruletab, print_ast_trtab, ...} = tabs; in [pretty_strs_qs "consts:" consts, pretty_trtab "parse_ast_translation:" parse_ast_trtab, @@ -689,8 +641,7 @@ pretty_trtab "parse_translation:" parse_trtab, pretty_trtab "print_translation:" print_trtab, pretty_ruletab "print_rules:" print_ruletab, - pretty_trtab "print_ast_translation:" print_ast_trtab, - Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)] + pretty_trtab "print_ast_translation:" print_ast_trtab] end; in @@ -714,24 +665,6 @@ -(** read **) (* FIXME rename!? *) - -(* configuration options *) - -val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true); -val positions = Config.bool positions_raw; - -val ambiguity_enabled = - Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true)); - -val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1); -val ambiguity_level = Config.int ambiguity_level_raw; - -val ambiguity_limit = - Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10)); - - - (** prepare translation rules **) (* rules *) @@ -784,7 +717,6 @@ val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns; val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns; -val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns; fun update_type_gram add prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls); @@ -798,7 +730,7 @@ (*export parts of internal Syntax structures*) val syntax_tokenize = tokenize; -open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer; +open Lexicon Syn_Ext Syn_Trans Mixfix Printer; val tokenize = syntax_tokenize; end; @@ -807,6 +739,5 @@ open Basic_Syntax; forget_structure "Syn_Ext"; -forget_structure "Type_Ext"; forget_structure "Mixfix"; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Apr 07 18:41:49 2011 +0200 @@ -119,7 +119,7 @@ | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) = if constrain_pos then Ast.Appl [Ast.Constant "_constrain", ast_of pt, - Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))] + Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))] else ast_of pt | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts) | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); @@ -172,11 +172,11 @@ fun report ps = Position.reports reports ps; fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = - (case Syntax.decode_position_term typ of + (case Term_Position.decode_position typ of SOME p => decode (p :: ps) qs bs t | NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = - (case Syntax.decode_position_term typ of + (case Term_Position.decode_position typ of SOME q => decode ps (q :: qs) bs t | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) | decode _ qs bs (Abs (x, T, t)) = @@ -418,7 +418,7 @@ fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts) | term_of (TFree (x, S)) = - if is_some (Lexicon.decode_position x) then Lexicon.free x + if is_some (Term_Position.decode x) then Lexicon.free x else 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; @@ -475,7 +475,7 @@ val {structs, fixes} = idents; fun mark_atoms ((t as Const (c, _)) $ u) = - if member (op =) Syntax.standard_token_markers c + if member (op =) Syntax.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) @@ -553,46 +553,66 @@ local -fun unparse_t t_to_ast prt_t markup ctxt curried t = +fun free_or_skolem ctxt x = + let + val m = + if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt + then Markup.fixed x + else Markup.hilite; + in + if can Name.dest_skolem x + then ([m, Markup.skolem], ProofContext.revert_skolem ctxt x) + else ([m, Markup.free], x) + end; + +fun var_or_skolem s = + (case Lexicon.read_variable s of + SOME (x, i) => + (case try Name.dest_skolem x of + NONE => (Markup.var, s) + | SOME x' => (Markup.skolem, Term.string_of_vname (x', i))) + | NONE => (Markup.var, s)); + +fun unparse_t t_to_ast prt_t markup ctxt t = let val syn = ProofContext.syn_of ctxt; - val tokentr = Syntax.token_translation syn (print_mode_value ()); + + fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) + | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) + | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) + | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) + | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) + | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) + | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) + | token_trans _ _ = NONE; + + val markup_extern = Lexicon.unmark + {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x), + case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x), + case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x), + case_fixed = fn x => free_or_skolem ctxt x, + case_default = fn x => ([], x)}; in t_to_ast ctxt (Syntax.print_translation syn) t |> Ast.normalize ctxt (Syntax.print_rules syn) - |> prt_t ctxt curried (Syntax.prtabs syn) (Syntax.print_ast_translation syn) tokentr + |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern |> Pretty.markup markup end; in -fun unparse_sort ctxt = - let - val tsig = ProofContext.tsig_of ctxt; - val extern = {extern_class = Type.extern_class tsig, extern_type = I}; - in unparse_t sort_to_ast (Printer.pretty_typ_ast extern) Markup.sort ctxt false end; - -fun unparse_typ ctxt = - let - val tsig = ProofContext.tsig_of ctxt; - val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig}; - in unparse_t typ_to_ast (Printer.pretty_typ_ast extern) Markup.typ ctxt false end; +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort; +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ; fun unparse_term ctxt = let val thy = ProofContext.theory_of ctxt; val syn = ProofContext.syn_of ctxt; - val tsig = ProofContext.tsig_of ctxt; val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt); - val is_syntax_const = Syntax.is_const syn; - val consts = ProofContext.consts_of ctxt; - val extern = - {extern_class = Type.extern_class tsig, - extern_type = Type.extern_type tsig, - extern_const = Consts.extern consts}; in - unparse_t (term_to_ast idents is_syntax_const) (Printer.pretty_term_ast extern) - Markup.term ctxt (not (Pure_Thy.old_appl_syntax thy)) + unparse_t (term_to_ast idents (Syntax.is_const syn)) + (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) + Markup.term ctxt end; end; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/term_position.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/term_position.ML Thu Apr 07 18:41:49 2011 +0200 @@ -0,0 +1,55 @@ +(* Title: Pure/Syntax/term_position.ML + Author: Makarius + +Encoded position within term syntax trees. +*) + +signature TERM_POSITION = +sig + val pretty: Position.T -> Pretty.T + val encode: Position.T -> string + val decode: string -> Position.T option + val decode_position: term -> Position.T option + val is_position: term -> bool + val strip_positions: term -> term +end; + +structure Term_Position: TERM_POSITION = +struct + +(* markup *) + +val position_dummy = ""; +val position_text = XML.Text position_dummy; + +fun pretty pos = + Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy]; + +fun encode pos = + YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text])); + +fun decode str = + (case YXML.parse_body str handle Fail msg => error msg of + [XML.Elem ((name, props), [arg])] => + if name = Markup.positionN andalso arg = position_text + then SOME (Position.of_properties props) + else NONE + | _ => NONE); + + +(* positions within parse trees *) + +fun decode_position (Free (x, _)) = decode x + | decode_position _ = NONE; + +val is_position = is_some o decode_position; + +fun strip_positions ((t as Const (c, _)) $ u $ v) = + if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v + then strip_positions u + else t $ strip_positions u $ strip_positions v + | strip_positions (t $ u) = strip_positions t $ strip_positions u + | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) + | strip_positions t = t; + +end; diff -r 79be89e07589 -r 992892b48296 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Thu Apr 07 14:51:28 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,146 +0,0 @@ -(* Title: Pure/Syntax/type_ext.ML - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen - -Utilities for input and output of types. The concrete syntax of types. -*) - -signature TYPE_EXT0 = -sig - val decode_position_term: term -> Position.T option - val is_position: term -> bool - val strip_positions: term -> term - val strip_positions_ast: Ast.ast -> Ast.ast - val no_brackets: unit -> bool - val no_type_brackets: unit -> bool -end; - -signature TYPE_EXT = -sig - include TYPE_EXT0 - val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast - val type_ext: Syn_Ext.syn_ext -end; - -structure Type_Ext: TYPE_EXT = -struct - -(** input utils **) - -(* positions *) - -fun decode_position_term (Free (x, _)) = Lexicon.decode_position x - | decode_position_term _ = NONE; - -val is_position = is_some o decode_position_term; - -fun strip_positions ((t as Const (c, _)) $ u $ v) = - if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v - then strip_positions u - else t $ strip_positions u $ strip_positions v - | strip_positions (t $ u) = strip_positions t $ strip_positions u - | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) - | strip_positions t = t; - -fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) = - if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x) - then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts) - else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts)) - | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts) - | strip_positions_ast ast = ast; - - - -(** the type syntax **) - -(* print mode *) - -val bracketsN = "brackets"; -val no_bracketsN = "no_brackets"; - -fun no_brackets () = - find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) - (print_mode_value ()) = SOME no_bracketsN; - -val type_bracketsN = "type_brackets"; -val no_type_bracketsN = "no_type_brackets"; - -fun no_type_brackets () = - find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) - (print_mode_value ()) <> SOME type_bracketsN; - - -(* parse ast translations *) - -fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] - | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); - -fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) - | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); - -fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) - | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); - - -(* print ast translations *) - -fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) - | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] - | tappl_ast_tr' (f, ty :: tys) = - Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; - -fun fun_ast_tr' (*"\\<^type>fun"*) asts = - if no_brackets () orelse no_type_brackets () then raise Match - else - (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); - - -(* type_ext *) - -fun typ c = Type (c, []); - -val class_nameT = typ "class_name"; -val type_nameT = typ "type_name"; - -val sortT = typ "sort"; -val classesT = typ "classes"; -val typesT = typ "types"; - -local open Lexicon Syn_Ext in - -val type_ext = syn_ext' false (K false) - [Mfix ("_", tidT --> typeT, "", [], max_pri), - Mfix ("_", tvarT --> typeT, "", [], max_pri), - Mfix ("_", type_nameT --> typeT, "", [], max_pri), - Mfix ("_", idT --> type_nameT, "_type_name", [], max_pri), - Mfix ("_", longidT --> type_nameT, "_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 ("_", class_nameT --> sortT, "", [], max_pri), - Mfix ("_", idT --> class_nameT, "_class_name", [], max_pri), - Mfix ("_", longidT --> class_nameT, "_class_name", [], max_pri), - Mfix ("{}", sortT, "_topsort", [], max_pri), - Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), - Mfix ("_", class_nameT --> classesT, "", [], max_pri), - Mfix ("_,_", [class_nameT, classesT] ---> classesT, "_classes", [], max_pri), - Mfix ("_ _", [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri), - Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri), - Mfix ("_", typeT --> typesT, "", [], max_pri), - Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), - 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, "\\<^type>dummy", [], max_pri)] - ["_type_prop"] - (map Syn_Ext.mk_trfun - [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)], - [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')]) - [] - ([], []); - -end; - -end; diff -r 79be89e07589 -r 992892b48296 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/pure_thy.ML Thu Apr 07 18:41:49 2011 +0200 @@ -65,7 +65,31 @@ (Binding.name "dummy", 0, NoSyn)] #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms) #> Sign.add_syntax_i - [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), + [("", typ "tid => type", Delimfix "_"), + ("", typ "tvar => type", Delimfix "_"), + ("", typ "type_name => type", Delimfix "_"), + ("_type_name", typ "id => type_name", Delimfix "_"), + ("_type_name", typ "longid => type_name", Delimfix "_"), + ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)), + ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)), + ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], Syntax.max_pri)), + ("", typ "class_name => sort", Delimfix "_"), + ("_class_name", typ "id => class_name", Delimfix "_"), + ("_class_name", typ "longid => class_name", Delimfix "_"), + ("_topsort", typ "sort", Delimfix "{}"), + ("_sort", typ "classes => sort", Delimfix "{_}"), + ("", typ "class_name => classes", Delimfix "_"), + ("_classes", typ "class_name => classes => classes", Delimfix "_,_"), + ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [Syntax.max_pri, 0], Syntax.max_pri)), + ("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"), + ("", typ "type => types", Delimfix "_"), + ("_types", typ "type => types => types", Delimfix "_,/ _"), + ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ => _)", [1, 0], 0)), + ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [0, 0], 0)), + ("", typ "type => type", Delimfix "'(_')"), + ("\\<^type>dummy", typ "type", Delimfix "'_"), + ("_type_prop", typ "'a", NoSyn), + ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), ("_abs", typ "'a", NoSyn), ("", typ "'a => args", Delimfix "_"), ("_args", typ "'a => args => args", Delimfix "_,/ _"), diff -r 79be89e07589 -r 992892b48296 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Apr 07 14:51:28 2011 +0200 +++ b/src/Pure/sign.ML Thu Apr 07 18:41:49 2011 +0200 @@ -103,10 +103,6 @@ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val add_advanced_trfunsT: (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory - val add_tokentrfuns: - (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory - val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list - -> theory -> theory val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory val new_group: theory -> theory @@ -488,9 +484,6 @@ end; -val add_tokentrfuns = map_syn o Syntax.extend_tokentrfuns; -fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); - (* translation rules *)