--- 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;
*}
--- 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))
--- 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;
--- 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);
--- 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;
--- 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 \
--- 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 **)
--- 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);
--- 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";
--- 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
--- 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 = "<position>";
-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;
--- 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;
--- 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;
--- 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;
--- 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'),
--- 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";
--- 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;
--- /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 = "<position>";
+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;
--- 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;
--- 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 "_,/ _"),
--- 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 *)