--- a/NEWS Wed Apr 06 13:08:44 2011 +0200
+++ b/NEWS Wed Apr 06 18:17:19 2011 +0200
@@ -97,6 +97,9 @@
content, no inclusion in structure Syntax. INCOMPATIBILITY, refer to
qualified names like Ast.Constant etc.
+* Typed print translation: discontinued show_sorts argument, which is
+already available via context of "advanced" translation.
+
New in Isabelle2011 (January 2011)
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Apr 06 13:08:44 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Apr 06 18:17:19 2011 +0200
@@ -804,8 +804,7 @@
val parse_ast_translation : (string * (ast list -> ast)) list
val parse_translation : (string * (term list -> term)) list
val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
+val typed_print_translation : (string * (typ -> term list -> term)) list
val print_ast_translation : (string * (ast list -> ast)) list
\end{ttbox}
@@ -827,7 +826,7 @@
val print_translation:
(string * (Proof.context -> term list -> term)) list
val typed_print_translation:
- (string * (Proof.context -> bool -> typ -> term list -> term)) list
+ (string * (Proof.context -> typ -> term list -> term)) list
val print_ast_translation:
(string * (Proof.context -> ast list -> ast)) list
\end{ttbox}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Apr 06 13:08:44 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Apr 06 18:17:19 2011 +0200
@@ -824,8 +824,7 @@
val parse_ast_translation : (string * (ast list -> ast)) list
val parse_translation : (string * (term list -> term)) list
val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
+val typed_print_translation : (string * (typ -> term list -> term)) list
val print_ast_translation : (string * (ast list -> ast)) list
\end{ttbox}
@@ -847,7 +846,7 @@
val print_translation:
(string * (Proof.context -> term list -> term)) list
val typed_print_translation:
- (string * (Proof.context -> bool -> typ -> term list -> term)) list
+ (string * (Proof.context -> typ -> term list -> term)) list
val print_ast_translation:
(string * (Proof.context -> ast list -> ast)) list
\end{ttbox}%
--- a/etc/symbols Wed Apr 06 13:08:44 2011 +0200
+++ b/etc/symbols Wed Apr 06 18:17:19 2011 +0200
@@ -124,7 +124,7 @@
\<theta> code: 0x0003b8 font: Isabelle
\<iota> code: 0x0003b9 font: Isabelle
\<kappa> code: 0x0003ba font: Isabelle
-\<lambda> code: 0x0003bb font: Isabelle
+\<lambda> code: 0x0003bb font: Isabelle abbrev: %
\<mu> code: 0x0003bc font: Isabelle
\<nu> code: 0x0003bd font: Isabelle
\<xi> code: 0x0003be font: Isabelle
--- a/src/HOL/Groups.thy Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Groups.thy Wed Apr 06 18:17:19 2011 +0200
@@ -125,13 +125,15 @@
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
typed_print_translation (advanced) {*
-let
- fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
- if not (null ts) orelse T = dummyT
- orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
- then raise Match
- else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
+ let
+ fun tr' c = (c, fn ctxt => fn T => fn ts =>
+ if not (null ts) orelse T = dummyT
+ orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
+ then raise Match
+ else
+ Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
+ Syntax_Phases.term_of_typ ctxt T);
+ in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
*} -- {* show types that are presumably too general *}
class plus =
--- a/src/HOL/Library/Cardinality.thy Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Library/Cardinality.thy Wed Apr 06 18:17:19 2011 +0200
@@ -34,12 +34,11 @@
translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
-typed_print_translation {*
-let
- fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
- Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
-in [(@{const_syntax card}, card_univ_tr')]
-end
+typed_print_translation (advanced) {*
+ let
+ fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] =
+ Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T;
+ in [(@{const_syntax card}, card_univ_tr')] end
*}
lemma card_unit [simp]: "CARD(unit) = 1"
--- a/src/HOL/Product_Type.thy Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Product_Type.thy Wed Apr 06 18:17:19 2011 +0200
@@ -232,8 +232,8 @@
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
typed_print_translation {*
let
- fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
- | split_guess_names_tr' _ T [Abs (x, xT, t)] =
+ fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
+ | split_guess_names_tr' T [Abs (x, xT, t)] =
(case (head_of t) of
Const (@{const_syntax prod_case}, _) => raise Match
| _ =>
@@ -245,7 +245,7 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
- | split_guess_names_tr' _ T [t] =
+ | split_guess_names_tr' T [t] =
(case head_of t of
Const (@{const_syntax prod_case}, _) => raise Match
| _ =>
@@ -257,7 +257,7 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
- | split_guess_names_tr' _ _ _ = raise Match;
+ | split_guess_names_tr' _ _ = raise Match;
in [(@{const_syntax prod_case}, split_guess_names_tr')] end
*}
--- a/src/HOL/Tools/numeral_syntax.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Wed Apr 06 18:17:19 2011 +0200
@@ -69,15 +69,17 @@
in
-fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
+fun numeral_tr' ctxt (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
- else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
+ else
+ Syntax.const @{syntax_const "_constrain"} $ syntax_numeral t $
+ Syntax_Phases.term_of_typ ctxt T
in list_comb (t', ts) end
- | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
+ | numeral_tr' _ T (t :: ts) =
if T = dummyT then list_comb (syntax_numeral t, ts)
else raise Match
- | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
+ | numeral_tr' _ _ _ = raise Match;
end;
--- a/src/HOL/Tools/record.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Tools/record.ML Wed Apr 06 18:17:19 2011 +0200
@@ -662,7 +662,7 @@
fun get_sort env xi =
the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
in
- Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
+ Syntax_Phases.typ_of_term (get_sort (Syntax_Phases.term_sorts t)) t
end;
@@ -708,9 +708,9 @@
val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
handle Type.TYPE_MATCH => err "type is no proper record (extension)";
- val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
val alphas' =
- map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
+ map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
+ (#1 (split_last alphas));
val more' = mk_ext rest;
in
@@ -819,8 +819,6 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
-
fun strip_fields T =
(case T of
Type (ext, args as _ :: _) =>
@@ -847,11 +845,15 @@
val (fields, (_, moreT)) = split_last (strip_fields T);
val _ = null fields andalso raise Match;
- val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
+ val u =
+ foldr1 field_types_tr'
+ (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
in
if not (! print_type_as_fields) orelse null fields then raise Match
else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
- else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
+ else
+ Syntax.const @{syntax_const "_record_type_scheme"} $ u $
+ Syntax_Phases.term_of_typ ctxt moreT
end;
(*try to reconstruct the record name type abbreviation from
@@ -865,7 +867,7 @@
fun mk_type_abbr subst name args =
let val abbrT = Type (name, map (varifyT o TFree) args)
- in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
+ in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
--- a/src/HOL/Tools/string_syntax.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Tools/string_syntax.ML Wed Apr 06 18:17:19 2011 +0200
@@ -68,7 +68,7 @@
(case Syntax.explode_xstr xstr of
[] =>
Ast.Appl
- [Ast.Constant Syntax.constrainC,
+ [Ast.Constant @{syntax_const "_constrain"},
Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
| cs => mk_string cs)
| string_ast_tr asts = raise Ast.AST ("string_tr", asts);
--- a/src/HOL/Typerep.thy Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/Typerep.thy Wed Apr 06 18:17:19 2011 +0200
@@ -30,13 +30,13 @@
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
*}
-typed_print_translation {*
+typed_print_translation (advanced) {*
let
- fun typerep_tr' show_sorts (*"typerep"*)
+ fun typerep_tr' ctxt (*"typerep"*)
(Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
(Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
- (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
+ (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
| typerep_tr' _ T ts = raise Match;
in [(@{const_syntax typerep}, typerep_tr')] end
*}
--- a/src/HOL/ex/Numeral.thy Wed Apr 06 13:08:44 2011 +0200
+++ b/src/HOL/ex/Numeral.thy Wed Apr 06 18:17:19 2011 +0200
@@ -301,7 +301,7 @@
| int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
dig 1 (int_of_num' n)
| int_of_num' (Const (@{const_syntax One}, _)) = 1;
- fun num_tr' ctxt show_sorts T [n] =
+ fun num_tr' ctxt T [n] =
let
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
@@ -309,7 +309,7 @@
case T of
Type (@{type_name fun}, [_, T']) =>
if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
- else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
+ else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
| T' => if T' = dummyT then t' else raise Match
end;
in [(@{const_syntax of_num}, num_tr')] end
--- a/src/Pure/IsaMakefile Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/IsaMakefile Wed Apr 06 18:17:19 2011 +0200
@@ -121,7 +121,6 @@
Isar/isar_syn.ML \
Isar/keyword.ML \
Isar/local_defs.ML \
- Isar/local_syntax.ML \
Isar/local_theory.ML \
Isar/locale.ML \
Isar/method.ML \
@@ -180,6 +179,7 @@
ROOT.ML \
Syntax/ast.ML \
Syntax/lexicon.ML \
+ Syntax/local_syntax.ML \
Syntax/mixfix.ML \
Syntax/parser.ML \
Syntax/printer.ML \
@@ -187,6 +187,7 @@
Syntax/syn_ext.ML \
Syntax/syn_trans.ML \
Syntax/syntax.ML \
+ Syntax/syntax_phases.ML \
Syntax/type_ext.ML \
System/isabelle_process.ML \
System/isabelle_system.ML \
--- a/src/Pure/Isar/isar_cmd.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Apr 06 18:17:19 2011 +0200
@@ -148,8 +148,7 @@
fun typed_print_translation (a, (txt, pos)) =
ML_Lex.read pos txt
|> ML_Context.expression pos
- ("val typed_print_translation: (string * (" ^ advancedT a ^
- "bool -> typ -> term list -> term)) list")
+ ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
|> Context.theory_map;
@@ -161,11 +160,9 @@
fun read_trrules thy raw_rules =
let
val ctxt = ProofContext.init_global thy;
- val type_ctxt = ProofContext.type_context ctxt;
- val syn = ProofContext.syn_of ctxt;
in
raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
- Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s)))
+ Syntax_Phases.parse_ast_pattern ctxt (Sign.intern_type thy r, s)))
end;
fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
--- a/src/Pure/Isar/local_syntax.ML Wed Apr 06 13:08:44 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-(* Title: Pure/Isar/local_syntax.ML
- Author: Makarius
-
-Local syntax depending on theory syntax.
-*)
-
-signature LOCAL_SYNTAX =
-sig
- type T
- val syn_of: T -> Syntax.syntax
- val idents_of: T -> {structs: string list, fixes: string list}
- val init: theory -> T
- val rebuild: theory -> T -> T
- datatype kind = Type | Const | Fixed
- val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
- val set_mode: Syntax.mode -> T -> T
- val restore_mode: T -> T -> T
- val update_modesyntax: theory -> bool -> Syntax.mode ->
- (kind * (string * typ * mixfix)) list -> T -> T
-end;
-
-structure Local_Syntax: LOCAL_SYNTAX =
-struct
-
-(* datatype T *)
-
-type local_mixfix =
- (string * bool) * (*name, fixed?*)
- ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
-
-datatype T = Syntax of
- {thy_syntax: Syntax.syntax,
- local_syntax: Syntax.syntax,
- mode: Syntax.mode,
- mixfixes: local_mixfix list,
- idents: string list * string list};
-
-fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
- Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
- mode = mode, mixfixes = mixfixes, idents = idents};
-
-fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
- make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
-
-fun is_consistent thy (Syntax {thy_syntax, ...}) =
- Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
-
-fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
-fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
-
-
-(* build syntax *)
-
-fun build_syntax thy mode mixfixes (idents as (structs, _)) =
- let
- val thy_syntax = Sign.syn_of thy;
- fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
- | update_gram ((false, add, m), decls) =
- Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
-
- val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
- val local_syntax = thy_syntax
- |> Syntax.update_trfuns
- (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
- map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
- |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
- in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
-
-fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
-
-fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
- if is_consistent thy syntax then syntax
- else build_syntax thy mode mixfixes idents;
-
-
-(* mixfix declarations *)
-
-datatype kind = Type | Const | Fixed;
-
-local
-
-fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
- | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
- | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
- | prep_mixfix add mode (Fixed, (x, T, mx)) =
- SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
-
-fun prep_struct (Fixed, (c, _, Structure)) = SOME c
- | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
- | prep_struct _ = NONE;
-
-in
-
-fun update_syntax add thy raw_decls
- (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
- (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
- [] => syntax
- | decls =>
- let
- val new_mixfixes = map_filter (prep_mixfix add mode) decls;
- val new_structs = map_filter prep_struct decls;
- val mixfixes' = rev new_mixfixes @ mixfixes;
- val structs' =
- if add then structs @ new_structs
- else subtract (op =) new_structs structs;
- val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
- in build_syntax thy mode mixfixes' (structs', fixes') end);
-
-val add_syntax = update_syntax true;
-
-end;
-
-
-(* syntax mode *)
-
-fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
- (thy_syntax, local_syntax, mode, mixfixes, idents));
-
-fun restore_mode (Syntax {mode, ...}) = set_mode mode;
-
-fun update_modesyntax thy add mode args syntax =
- syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
-
-end;
--- a/src/Pure/Isar/proof_context.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 06 18:17:19 2011 +0200
@@ -26,6 +26,7 @@
val naming_of: Proof.context -> Name_Space.naming
val restore_naming: Proof.context -> Proof.context -> Proof.context
val full_name: Proof.context -> binding -> string
+ val syntax_of: Proof.context -> Local_Syntax.T
val syn_of: Proof.context -> Syntax.syntax
val tsig_of: Proof.context -> Type.tsig
val set_defsort: sort -> Proof.context -> Proof.context
@@ -63,13 +64,11 @@
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> typ -> string -> term
val allow_dummies: Proof.context -> Proof.context
+ val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
val check_tvar: Proof.context -> indexname * sort -> indexname * sort
val check_tfree: Proof.context -> string * sort -> string * sort
- val type_context: Proof.context -> Syntax.type_context
- val term_context: Proof.context -> Syntax.term_context
- val decode_term: Proof.context ->
- Position.reports * term Exn.result -> Position.reports * term Exn.result
val standard_infer_types: Proof.context -> term list -> term list
+ val intern_skolem: Proof.context -> string -> string option
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
val read_term_abbrev: Proof.context -> string -> term
@@ -264,7 +263,6 @@
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
val consts_of = #1 o #consts o rep_context;
-val const_space = Consts.space_of o consts_of;
val the_const_constraint = Consts.the_constraint o consts_of;
val facts_of = #facts o rep_context;
@@ -524,6 +522,22 @@
end;
+(* skolem variables *)
+
+fun intern_skolem ctxt x =
+ let
+ val _ = no_skolem false x;
+ val sko = lookup_skolem ctxt x;
+ val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
+ val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
+ in
+ if Variable.is_const ctxt x then NONE
+ else if is_some sko then sko
+ else if not is_const orelse is_declared then SOME x
+ else NONE
+ end;
+
+
(* read_term *)
fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
@@ -616,9 +630,7 @@
end;
-(* decoding raw terms (syntax trees) *)
-
-(* types *)
+(* sort constraints *)
fun get_sort ctxt raw_text =
let
@@ -651,44 +663,6 @@
fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
-local
-
-fun intern_skolem ctxt def_type x =
- let
- val _ = no_skolem false x;
- val sko = lookup_skolem ctxt x;
- val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
- val is_declared = is_some (def_type (x, ~1));
- in
- if Variable.is_const ctxt x then NONE
- else if is_some sko then sko
- else if not is_const orelse is_declared then SOME x
- else NONE
- end;
-
-in
-
-fun type_context ctxt : Syntax.type_context =
- {get_class = read_class ctxt,
- get_type = #1 o dest_Type o read_type_name_proper ctxt false,
- markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
- markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
-
-fun term_context ctxt : Syntax.term_context =
- {get_sort = get_sort ctxt,
- get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
- handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
- get_free = intern_skolem ctxt (Variable.def_type ctxt false),
- markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
- markup_free = fn x =>
- [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
- (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
- markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
-
-val decode_term = Syntax.decode_term o term_context;
-
-end;
-
(* certify terms *)
@@ -746,93 +720,6 @@
-(** inner syntax operations **)
-
-local
-
-fun parse_failed ctxt pos msg kind =
- cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
-
-fun parse_sort ctxt text =
- let
- val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
- val S =
- Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg "sort";
- in Type.minimize_sort (tsig_of ctxt) S end;
-
-fun parse_typ ctxt text =
- let
- val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
- val T =
- Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg "type";
- in T end;
-
-fun parse_term T ctxt text =
- let
- val (T', _) = Type_Infer.paramify_dummies T 0;
- val (markup, kind) =
- if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
- val (syms, pos) = Syntax.parse_token ctxt markup text;
-
- val default_root = Config.get ctxt Syntax.default_root;
- val root =
- (case T' of
- Type (c, _) =>
- if c <> "prop" andalso Type.is_logtype (tsig_of ctxt) c
- then default_root else c
- | _ => default_root);
-
- fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
- handle exn as ERROR _ => Exn.Exn exn;
- val t =
- Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
- root (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg kind;
- in t end;
-
-
-fun unparse_sort ctxt =
- Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}
- ctxt (syn_of ctxt);
-
-fun unparse_typ ctxt =
- let
- val tsig = tsig_of ctxt;
- val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
- in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
-
-fun unparse_term ctxt =
- let
- val tsig = tsig_of ctxt;
- val syntax = syntax_of ctxt;
- val consts = consts_of ctxt;
- val extern =
- {extern_class = Type.extern_class tsig,
- extern_type = Type.extern_type tsig,
- extern_const = Consts.extern consts};
- in
- Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
- (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt)))
- end;
-
-in
-
-val _ = Syntax.install_operations
- {parse_sort = parse_sort,
- parse_typ = parse_typ,
- parse_term = parse_term dummyT,
- parse_prop = parse_term propT,
- unparse_sort = unparse_sort,
- unparse_typ = unparse_typ,
- unparse_term = unparse_term};
-
-end;
-
-
-
(** export results **)
fun common_export is_goal inner outer =
--- a/src/Pure/ROOT.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/ROOT.ML Wed Apr 06 18:17:19 2011 +0200
@@ -170,9 +170,10 @@
use "Isar/object_logic.ML";
use "Isar/rule_cases.ML";
use "Isar/auto_bind.ML";
-use "Isar/local_syntax.ML";
use "type_infer.ML";
+use "Syntax/local_syntax.ML";
use "Isar/proof_context.ML";
+use "Syntax/syntax_phases.ML";
use "Isar/local_defs.ML";
(*proof term operations*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/local_syntax.ML Wed Apr 06 18:17:19 2011 +0200
@@ -0,0 +1,124 @@
+(* Title: Pure/Syntax/local_syntax.ML
+ Author: Makarius
+
+Local syntax depending on theory syntax.
+*)
+
+signature LOCAL_SYNTAX =
+sig
+ type T
+ val syn_of: T -> Syntax.syntax
+ val idents_of: T -> {structs: string list, fixes: string list}
+ val init: theory -> T
+ val rebuild: theory -> T -> T
+ datatype kind = Type | Const | Fixed
+ val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
+ val set_mode: Syntax.mode -> T -> T
+ val restore_mode: T -> T -> T
+ val update_modesyntax: theory -> bool -> Syntax.mode ->
+ (kind * (string * typ * mixfix)) list -> T -> T
+end;
+
+structure Local_Syntax: LOCAL_SYNTAX =
+struct
+
+(* datatype T *)
+
+type local_mixfix =
+ (string * bool) * (*name, fixed?*)
+ ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
+
+datatype T = Syntax of
+ {thy_syntax: Syntax.syntax,
+ local_syntax: Syntax.syntax,
+ mode: Syntax.mode,
+ mixfixes: local_mixfix list,
+ idents: string list * string list};
+
+fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
+ Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
+ mode = mode, mixfixes = mixfixes, idents = idents};
+
+fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
+ make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
+
+fun is_consistent thy (Syntax {thy_syntax, ...}) =
+ Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
+
+fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
+fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
+
+
+(* build syntax *)
+
+fun build_syntax thy mode mixfixes (idents as (structs, _)) =
+ let
+ val thy_syntax = Sign.syn_of thy;
+ fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
+ | update_gram ((false, add, m), decls) =
+ Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+
+ val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
+ val local_syntax = thy_syntax
+ |> Syntax.update_trfuns
+ (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
+ map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
+ |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
+ in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
+
+fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
+
+fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
+ if is_consistent thy syntax then syntax
+ else build_syntax thy mode mixfixes idents;
+
+
+(* mixfix declarations *)
+
+datatype kind = Type | Const | Fixed;
+
+local
+
+fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
+ | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
+ | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
+ | prep_mixfix add mode (Fixed, (x, T, mx)) =
+ SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
+
+fun prep_struct (Fixed, (c, _, Structure)) = SOME c
+ | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
+ | prep_struct _ = NONE;
+
+in
+
+fun update_syntax add thy raw_decls
+ (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
+ (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
+ [] => syntax
+ | decls =>
+ let
+ val new_mixfixes = map_filter (prep_mixfix add mode) decls;
+ val new_structs = map_filter prep_struct decls;
+ val mixfixes' = rev new_mixfixes @ mixfixes;
+ val structs' =
+ if add then structs @ new_structs
+ else subtract (op =) new_structs structs;
+ val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
+ in build_syntax thy mode mixfixes' (structs', fixes') end);
+
+val add_syntax = update_syntax true;
+
+end;
+
+
+(* syntax mode *)
+
+fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
+ (thy_syntax, local_syntax, mode, mixfixes, idents));
+
+fun restore_mode (Syntax {mode, ...}) = set_mode mode;
+
+fun update_modesyntax thy add mode args syntax =
+ syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
+
+end;
--- a/src/Pure/Syntax/printer.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Syntax/printer.ML Wed Apr 06 18:17:19 2011 +0200
@@ -28,12 +28,6 @@
signature PRINTER =
sig
include PRINTER0
- val sort_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
- val typ_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
- val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
type prtabs
val empty_prtabs: prtabs
val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
@@ -41,18 +35,17 @@
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 ->
- (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (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 -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
(string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
end;
structure Printer: PRINTER =
struct
-
(** options for printing **)
val show_brackets_default = Unsynchronized.ref false;
@@ -81,150 +74,6 @@
-(** misc utils **)
-
-(* apply print (ast) translation function *)
-
-fun apply_trans ctxt fns args =
- let
- fun app_first [] = raise Match
- | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
- in app_first fns end;
-
-fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
-
-
-(* simple_ast_of *)
-
-fun simple_ast_of ctxt =
- let
- val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
- fun ast_of (Const (c, _)) = Ast.Constant c
- | ast_of (Free (x, _)) = Ast.Variable x
- | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
- | ast_of (t as _ $ _) =
- let val (f, args) = strip_comb t
- in Ast.mk_appl (ast_of f) (map ast_of args) end
- | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
- | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
- in ast_of end;
-
-
-
-(** sort_to_ast, typ_to_ast **)
-
-fun ast_of_termT ctxt trf tm =
- let
- val ctxt' = Config.put show_sorts false ctxt;
- fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
- | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
- | ast_of (Const (a, _)) = trans a []
- | ast_of (t as _ $ _) =
- (case strip_comb t of
- (Const (a, _), args) => trans a args
- | (f, args) => Ast.Appl (map ast_of (f :: args)))
- | ast_of t = simple_ast_of ctxt t
- and trans a args =
- ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
- handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
- in ast_of tm end;
-
-fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
-fun typ_to_ast ctxt trf T =
- ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
-
-
-
-(** term_to_ast **)
-
-fun term_to_ast idents consts ctxt trf tm =
- let
- val show_types =
- Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
- Config.get ctxt show_all_types;
- val show_sorts = Config.get ctxt show_sorts;
- val show_structs = Config.get ctxt show_structs;
- val show_free_types = Config.get ctxt show_free_types;
- val show_all_types = Config.get ctxt show_all_types;
-
- val {structs, fixes} = idents;
-
- fun mark_atoms ((t as Const (c, T)) $ u) =
- if member (op =) Syn_Ext.standard_token_markers c
- then t $ u else mark_atoms t $ mark_atoms u
- | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
- | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
- | mark_atoms (t as Const (c, T)) =
- if member (op =) consts c then t
- else Const (Lexicon.mark_const c, T)
- | mark_atoms (t as Free (x, T)) =
- let val i = find_index (fn s => s = x) structs + 1 in
- if i = 0 andalso member (op =) fixes x then
- Const (Lexicon.mark_fixed x, T)
- else if i = 1 andalso not show_structs then
- Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
- else Lexicon.const "_free" $ t
- end
- | mark_atoms (t as Var (xi, T)) =
- if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
- else Lexicon.const "_var" $ t
- | mark_atoms a = a;
-
- fun prune_typs (t_seen as (Const _, _)) = t_seen
- | prune_typs (t as Free (x, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
- else (t, t :: seen)
- | prune_typs (t as Var (xi, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
- else (t, t :: seen)
- | prune_typs (t_seen as (Bound _, _)) = t_seen
- | prune_typs (Abs (x, ty, t), seen) =
- let val (t', seen') = prune_typs (t, seen);
- in (Abs (x, ty, t'), seen') end
- | prune_typs (t1 $ t2, seen) =
- let
- val (t1', seen') = prune_typs (t1, seen);
- val (t2', seen'') = prune_typs (t2, seen');
- in (t1' $ t2', seen'') end;
-
- fun ast_of tm =
- (case strip_comb tm of
- (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
- | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
- | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
- | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
- | (Const ("_idtdummy", T), ts) =>
- Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
- | (const as Const (c, T), ts) =>
- if show_all_types
- then Ast.mk_appl (constrain const T) (map ast_of ts)
- else trans c T ts
- | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
-
- and trans a T args =
- ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
- handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
-
- and constrain t T =
- if show_types andalso T <> dummyT then
- Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
- ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
- else simple_ast_of ctxt t;
- in
- tm
- |> Syn_Trans.prop_tr'
- |> show_types ? (#1 o prune_typs o rpair [])
- |> mark_atoms
- |> ast_of
- end;
-
-
-
(** type prtabs **)
datatype symb =
@@ -408,7 +257,7 @@
in
(case tokentrT a args of
SOME prt => [prt]
- | NONE => astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs))
+ | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs))
end
and tokentrT a [Ast.Variable x] = token_trans a x
--- a/src/Pure/Syntax/syn_ext.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Wed Apr 06 18:17:19 2011 +0200
@@ -7,7 +7,6 @@
signature SYN_EXT0 =
sig
val dddot_indexname: indexname
- val constrainC: string
val typeT: typ
val spropT: typ
val default_root: string Config.T
@@ -20,6 +19,7 @@
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
end;
signature SYN_EXT =
@@ -49,8 +49,7 @@
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 -> bool -> typ -> 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}
@@ -59,14 +58,14 @@
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 -> bool -> typ -> 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
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 -> bool -> typ -> 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
@@ -75,15 +74,14 @@
val syn_ext_trfuns:
(string * ((Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
- (string * ((bool -> typ -> term list -> term) * stamp)) list *
+ (string * ((typ -> term list -> term) * stamp)) list *
(string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
val syn_ext_advanced_trfuns:
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
- (string * ((Proof.context -> bool -> typ -> 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 standard_token_markers: string list
val pure_ext: syn_ext
end;
@@ -94,7 +92,6 @@
(** misc definitions **)
val dddot_indexname = ("dddot", 0);
-val constrainC = "_constrain";
(* syntactic categories *)
@@ -337,8 +334,7 @@
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 -> bool -> typ -> 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};
--- a/src/Pure/Syntax/syn_trans.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Wed Apr 06 18:17:19 2011 +0200
@@ -33,8 +33,8 @@
signature SYN_TRANS1 =
sig
include SYN_TRANS0
- val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term
- val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
+ 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
val abs_tr: term list -> term
val pure_trfuns:
@@ -42,13 +42,11 @@
(string * (term list -> term)) list *
(string * (term list -> term)) list *
(string * (Ast.ast list -> Ast.ast)) list
- val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
val struct_trfuns: string list ->
(string * (Ast.ast list -> Ast.ast)) list *
(string * (term list -> term)) list *
- (string * (bool -> typ -> term list -> term)) list *
+ (string * (typ -> term list -> term)) list *
(string * (Ast.ast list -> Ast.ast)) list
- type type_context
end;
signature SYN_TRANS =
@@ -58,11 +56,6 @@
val prop_tr': term -> term
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
- val parsetree_to_ast: Proof.context -> type_context -> bool ->
- (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
- Parser.parsetree -> Position.reports * Ast.ast Exn.result
- val ast_to_term: Proof.context ->
- (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
end;
structure Syn_Trans: SYN_TRANS =
@@ -250,8 +243,8 @@
(* types *)
-fun non_typed_tr' f _ _ ts = f ts;
-fun non_typed_tr'' f x _ _ ts = f x ts;
+fun non_typed_tr' f _ ts = f ts;
+fun non_typed_tr'' f x _ ts = f x ts;
(* application *)
@@ -360,15 +353,6 @@
| idtyp_ast_tr' _ _ = raise Match;
-(* type propositions *)
-
-fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
- Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
- | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
- Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
- | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
-
-
(* meta propositions *)
fun prop_tr' tm =
@@ -414,20 +398,6 @@
| _ => raise Match);
-(* type reflection *)
-
-fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
- Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
- | type_tr' _ _ _ = raise Match;
-
-
-(* type constraints *)
-
-fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
- Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
- | type_constraint_tr' _ _ _ = raise Match;
-
-
(* dependent / nondependent quantifiers *)
fun var_abs mark (x, T, b) =
@@ -539,75 +509,7 @@
("\\<^const>==>", impl_ast_tr'),
("_index", index_ast_tr')]);
-val pure_trfunsT =
- [("_type_prop", type_prop_tr'),
- ("\\<^const>TYPE", type_tr'),
- ("_type_constraint_", type_constraint_tr')];
-
fun struct_trfuns structs =
([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
-
-
-(** parsetree_to_ast **)
-
-type type_context =
- {get_class: string -> string,
- get_type: string -> string,
- markup_class: string -> Markup.T list,
- markup_type: string -> Markup.T list};
-
-fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree =
- let
- val {get_class, get_type, markup_class, markup_type} = type_context;
-
- val reports = Unsynchronized.ref ([]: Position.reports);
- fun report pos = Position.reports reports [pos];
-
- fun trans a args =
- (case trf a of
- NONE => Ast.mk_appl (Ast.Constant a) args
- | SOME f => f ctxt args);
-
- fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
- let
- val c = get_class (Lexicon.str_of_token tok);
- val _ = report (Lexicon.pos_of_token tok) markup_class c;
- in Ast.Constant (Lexicon.mark_class c) end
- | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
- let
- val c = get_type (Lexicon.str_of_token tok);
- val _ = report (Lexicon.pos_of_token tok) markup_type c;
- in Ast.Constant (Lexicon.mark_type c) end
- | 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))]
- 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);
-
- val ast = Exn.interruptible_capture ast_of parsetree;
- in (! reports, ast) end;
-
-
-
-(** ast_to_term **)
-
-fun ast_to_term ctxt trf =
- let
- fun trans a args =
- (case trf a of
- NONE => Term.list_comb (Lexicon.const a, args)
- | SOME f => f ctxt args);
-
- fun term_of (Ast.Constant a) = trans a []
- | term_of (Ast.Variable x) = Lexicon.read_var x
- | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
- trans a (map term_of asts)
- | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
- Term.list_comb (term_of ast, map term_of asts)
- | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
- in term_of end;
-
end;
--- a/src/Pure/Syntax/syntax.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Apr 06 18:17:19 2011 +0200
@@ -95,9 +95,26 @@
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
val is_keyword: syntax -> string -> bool
+ val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
+ val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list
+ val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option
+ val parse_rules: syntax -> string -> (Ast.ast * Ast.ast) list
+ val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option
+ val print_translation: syntax -> string ->
+ Proof.context -> typ -> term list -> term (*exception Match*)
+ 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
val mode_input: mode
@@ -114,36 +131,21 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
- val standard_parse_sort: Proof.context -> type_context -> syntax ->
- Symbol_Pos.T list * Position.T -> sort
- val standard_parse_typ: Proof.context -> type_context -> syntax ->
- ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
- val standard_parse_term: (term -> term Exn.result) ->
- Proof.context -> type_context -> term_context -> syntax ->
- string -> Symbol_Pos.T list * Position.T -> term
datatype 'a trrule =
Parse_Rule of 'a * 'a |
Print_Rule of 'a * 'a |
Parse_Print_Rule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
- val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> Ast.ast
- val standard_unparse_sort: {extern_class: string -> xstring} ->
- Proof.context -> syntax -> sort -> Pretty.T
- val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
- Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_term: {structs: string list, fixes: string list} ->
- {extern_class: string -> xstring, extern_type: string -> xstring,
- extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
val update_trfuns:
(string * ((Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
- (string * ((bool -> typ -> term list -> term) * stamp)) list *
+ (string * ((typ -> term list -> term) * stamp)) list *
(string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
val update_advanced_trfuns:
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
- (string * ((Proof.context -> bool -> typ -> 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
@@ -394,11 +396,11 @@
(* parse (ast) translations *)
-fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
-
fun err_dup_trfun name c =
error ("More than one " ^ name ^ " for " ^ quote c);
+fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
+
fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
@@ -410,7 +412,20 @@
(* print (ast) translations *)
-fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+fun apply_tr' tab c ctxt T args =
+ let
+ val fns = map fst (Symtab.lookup_list tab c);
+ fun app_first [] = raise Match
+ | app_first (f :: fs) = f ctxt T args handle Match => app_first fs;
+ in app_first fns end;
+
+fun apply_ast_tr' tab c ctxt args =
+ let
+ val fns = map fst (Symtab.lookup_list tab c);
+ fun app_first [] = raise Match
+ | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
+ in app_first fns end;
+
fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
@@ -420,12 +435,14 @@
(** tables of token translation functions **)
fun lookup_tokentr tabs modes =
- let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) 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)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
+ fun eq_tr ((c1, (_, s1: stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
fun name (s, _) = implode (tl (Symbol.explode s));
@@ -478,15 +495,28 @@
parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
parse_ruletab: ruletab,
parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
- print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
+ 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;
fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
+fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
+fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram;
+
+fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
+fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
+fun parse_rules (Syntax ({parse_ruletab, ...}, _)) = Symtab.lookup_list parse_ruletab;
+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;
type mode = string * bool;
val mode_default = ("", true);
@@ -700,131 +730,6 @@
val ambiguity_limit =
Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
-fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-
-
-(* results *)
-
-fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
-fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
-
-fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
-
-fun report_result ctxt pos results =
- (case (proper_results results, failed_results results) of
- ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
- | ([(reports, x)], _) => (report ctxt reports; x)
- | _ => error (ambiguity_msg pos));
-
-
-(* read_asts *)
-
-fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
- let
- val {lexicon, gram, parse_ast_trtab, ...} = tabs;
- val toks = Lexicon.tokenize lexicon raw syms;
- val _ = List.app (Lexicon.report_token ctxt) toks;
-
- val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
- handle ERROR msg =>
- error (msg ^
- implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
- val len = length pts;
-
- val limit = Config.get ctxt ambiguity_limit;
- val _ =
- if len <= Config.get ctxt ambiguity_level then ()
- else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
- else
- (Context_Position.if_visible ctxt warning (cat_lines
- (("Ambiguous input" ^ Position.str_of pos ^
- "\nproduces " ^ string_of_int len ^ " parse trees" ^
- (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
-
- val constrain_pos = not raw andalso Config.get ctxt positions;
- val parsetree_to_ast =
- Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab);
- in map parsetree_to_ast pts end;
-
-
-(* read_raw *)
-
-fun read_raw ctxt type_ctxt (syn as Syntax (tabs, _)) root input =
- let
- val {parse_ruletab, parse_trtab, ...} = tabs;
- val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
- val ast_to_term = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab);
- in
- read_asts ctxt type_ctxt syn false root input
- |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
- end;
-
-
-(* read sorts *)
-
-fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
- read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos)
- |> report_result ctxt pos
- |> Type_Ext.sort_of_term;
-
-
-(* read types *)
-
-fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
- read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos)
- |> report_result ctxt pos
- |> (fn t => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t);
-
-
-(* read terms -- brute-force disambiguation via type-inference *)
-
-fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
- let
- val results =
- read_raw ctxt type_ctxt syn root (syms, pos)
- |> map (Type_Ext.decode_term term_ctxt);
-
- val level = Config.get ctxt ambiguity_level;
- val limit = Config.get ctxt ambiguity_limit;
-
- val ambiguity = length (proper_results results);
-
- fun ambig_msg () =
- if ambiguity > 1 andalso ambiguity <= level then
- "Got more than one parse tree.\n\
- \Retry with smaller syntax_ambiguity_level for more information."
- else "";
-
- val results' =
- if ambiguity > 1 then
- (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results
- else results;
- val reports' = fst (hd results');
-
- val errs = map snd (failed_results results');
- val checked = map snd (proper_results results');
- val len = length checked;
-
- val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
- in
- if len = 0 then
- report_result ctxt pos
- [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
- else if len = 1 then
- (if ambiguity > level then
- Context_Position.if_visible ctxt warning
- "Fortunately, only one parse tree is type correct.\n\
- \You may still want to disambiguate your grammar or your input."
- else (); report_result ctxt pos results')
- else
- report_result ctxt pos
- [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
- (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
- (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map show_term (take limit checked))))))]
- end;
-
(** prepare translation rules **)
@@ -872,55 +777,6 @@
end;
-(* read_rule_pattern *)
-
-fun read_rule_pattern ctxt type_ctxt syn (root, str) =
- let
- fun constify (ast as Ast.Constant _) = ast
- | constify (ast as Ast.Variable x) =
- if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
- else ast
- | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
-
- val (syms, pos) = read_token str;
- in
- read_asts ctxt type_ctxt syn true root (syms, pos)
- |> report_result ctxt pos
- |> constify
- end;
-
-
-
-(** unparse terms, typs, sorts **)
-
-local
-
-fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
- let
- val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
- val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
- in
- Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
- (lookup_tokentr tokentrtab (print_mode_value ()))
- (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
- end;
-
-in
-
-fun standard_unparse_sort {extern_class} ctxt syn =
- unparse_t (K Printer.sort_to_ast)
- (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
- Markup.sort ctxt syn false;
-
-fun standard_unparse_typ extern ctxt syn =
- unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
-
-fun standard_unparse_term idents extern =
- unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
-
-end;
-
-
(** modify syntax **)
@@ -941,7 +797,9 @@
(*export parts of internal Syntax structures*)
+val syntax_tokenize = tokenize;
open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer;
+val tokenize = syntax_tokenize;
end;
@@ -950,6 +808,5 @@
forget_structure "Syn_Ext";
forget_structure "Type_Ext";
-forget_structure "Syn_Trans";
forget_structure "Mixfix";
-forget_structure "Printer";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 18:17:19 2011 +0200
@@ -0,0 +1,648 @@
+(* Title: Pure/Syntax/syntax_phases.ML
+ Author: Makarius
+
+Main phases of inner syntax processing, with standard implementations
+of parse/unparse operations.
+*)
+
+signature SYNTAX_PHASES =
+sig
+ val term_sorts: term -> (indexname * sort) list
+ val typ_of_term: (indexname -> sort) -> term -> typ
+ val decode_term: Proof.context ->
+ Position.reports * term Exn.result -> Position.reports * term Exn.result
+ val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
+ val term_of_typ: Proof.context -> typ -> term
+end
+
+structure Syntax_Phases: SYNTAX_PHASES =
+struct
+
+(** decode parse trees **)
+
+(* sort_of_term *)
+
+fun sort_of_term tm =
+ let
+ fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+
+ fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+
+ fun classes (Const (s, _)) = [class s]
+ | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
+ | classes _ = err ();
+
+ fun sort (Const ("_topsort", _)) = []
+ | sort (Const (s, _)) = [class s]
+ | sort (Const ("_sort", _) $ cs) = classes cs
+ | sort _ = err ();
+ in sort tm end;
+
+
+(* term_sorts *)
+
+fun term_sorts tm =
+ let
+ val sort_of = sort_of_term;
+
+ fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
+ insert (op =) ((x, ~1), sort_of cs)
+ | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
+ insert (op =) ((x, ~1), sort_of cs)
+ | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
+ insert (op =) (xi, sort_of cs)
+ | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
+ insert (op =) (xi, sort_of cs)
+ | add_env (Abs (_, _, t)) = add_env t
+ | add_env (t1 $ t2) = add_env t1 #> add_env t2
+ | add_env _ = I;
+ in add_env tm [] end;
+
+
+(* typ_of_term *)
+
+fun typ_of_term get_sort tm =
+ let
+ fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
+
+ fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
+ | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
+ | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
+ | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
+ | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
+ | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
+ TFree (x, get_sort (x, ~1))
+ | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
+ | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
+ TVar (xi, get_sort xi)
+ | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
+ | typ_of t =
+ let
+ val (head, args) = Term.strip_comb t;
+ val a =
+ (case head of
+ Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
+ | _ => err ());
+ in Type (a, map typ_of args) end;
+ in typ_of tm end;
+
+
+(* parsetree_to_ast *)
+
+fun parsetree_to_ast ctxt constrain_pos trf parsetree =
+ let
+ val tsig = ProofContext.tsig_of ctxt;
+
+ val get_class = ProofContext.read_class ctxt;
+ val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
+ fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c];
+ fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c];
+
+ val reports = Unsynchronized.ref ([]: Position.reports);
+ fun report pos = Position.reports reports [pos];
+
+ fun trans a args =
+ (case trf a of
+ NONE => Ast.mk_appl (Ast.Constant a) args
+ | SOME f => f ctxt args);
+
+ fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
+ let
+ val c = get_class (Lexicon.str_of_token tok);
+ val _ = report (Lexicon.pos_of_token tok) markup_class c;
+ in Ast.Constant (Lexicon.mark_class c) end
+ | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
+ let
+ val c = get_type (Lexicon.str_of_token tok);
+ val _ = report (Lexicon.pos_of_token tok) markup_type c;
+ in Ast.Constant (Lexicon.mark_type c) end
+ | 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))]
+ 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);
+
+ val ast = Exn.interruptible_capture ast_of parsetree;
+ in (! reports, ast) end;
+
+
+(* ast_to_term *)
+
+fun ast_to_term ctxt trf =
+ let
+ fun trans a args =
+ (case trf a of
+ NONE => Term.list_comb (Lexicon.const a, args)
+ | SOME f => f ctxt args);
+
+ fun term_of (Ast.Constant a) = trans a []
+ | term_of (Ast.Variable x) = Lexicon.read_var x
+ | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
+ trans a (map term_of asts)
+ | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
+ Term.list_comb (term_of ast, map term_of asts)
+ | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
+ in term_of end;
+
+
+(* decode_term -- transform parse tree into raw term *)
+
+fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+ | decode_term ctxt (reports0, Exn.Result tm) =
+ let
+ val consts = ProofContext.consts_of ctxt;
+ fun get_const a =
+ ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
+ handle ERROR _ => (false, Consts.intern consts a));
+ val get_free = ProofContext.intern_skolem ctxt;
+ fun markup_const c = [Name_Space.markup_entry (Consts.space_of consts) c];
+ fun markup_free x =
+ [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+ (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
+ else [Markup.hilite]);
+ fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
+ fun markup_bound def id =
+ [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
+
+ val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
+
+ val reports = Unsynchronized.ref reports0;
+ fun report ps = Position.reports reports ps;
+
+ fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
+ (case Syntax.decode_position_term 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
+ 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)) =
+ let
+ val id = serial_string ();
+ val _ = report qs (markup_bound true) id;
+ in Abs (x, T, decode [] [] (id :: bs) t) end
+ | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
+ | decode ps _ _ (Const (a, T)) =
+ (case try Lexicon.unmark_fixed a of
+ SOME x => (report ps markup_free x; Free (x, T))
+ | NONE =>
+ let
+ val c =
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (get_const a));
+ val _ = report ps markup_const c;
+ in Const (c, T) end)
+ | decode ps _ _ (Free (a, T)) =
+ (case (get_free a, get_const a) of
+ (SOME x, _) => (report ps markup_free x; Free (x, T))
+ | (_, (true, c)) => (report ps markup_const c; Const (c, T))
+ | (_, (false, c)) =>
+ if Long_Name.is_qualified c
+ then (report ps markup_const c; Const (c, T))
+ else (report ps markup_free c; Free (c, T)))
+ | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
+ | decode ps _ bs (t as Bound i) =
+ (case try (nth bs) i of
+ SOME id => (report ps (markup_bound false) id; t)
+ | NONE => t);
+
+ val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+ in (! reports, tm') end;
+
+
+
+(** parse **)
+
+(* results *)
+
+fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
+
+fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
+fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
+
+fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
+
+fun report_result ctxt pos results =
+ (case (proper_results results, failed_results results) of
+ ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
+ | ([(reports, x)], _) => (report ctxt reports; x)
+ | _ => error (ambiguity_msg pos));
+
+
+(* parse raw asts *)
+
+fun parse_asts ctxt raw root (syms, pos) =
+ let
+ val syn = ProofContext.syn_of ctxt;
+ val ast_tr = Syntax.parse_ast_translation syn;
+
+ val toks = Syntax.tokenize syn raw syms;
+ val _ = List.app (Lexicon.report_token ctxt) toks;
+
+ val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
+ handle ERROR msg =>
+ error (msg ^
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+ val len = length pts;
+
+ val limit = Config.get ctxt Syntax.ambiguity_limit;
+ val _ =
+ if len <= Config.get ctxt Syntax.ambiguity_level then ()
+ else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
+ else
+ (Context_Position.if_visible ctxt warning (cat_lines
+ (("Ambiguous input" ^ Position.str_of pos ^
+ "\nproduces " ^ string_of_int len ^ " parse trees" ^
+ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
+
+ val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
+ val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
+ in map parsetree_to_ast pts end;
+
+fun parse_raw ctxt root input =
+ let
+ val syn = ProofContext.syn_of ctxt;
+ val tr = Syntax.parse_translation syn;
+ val parse_rules = Syntax.parse_rules syn;
+ in
+ parse_asts ctxt false root input
+ |> (map o apsnd o Exn.maps_result)
+ (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr))
+ end;
+
+
+(* parse logical entities *)
+
+fun parse_failed ctxt pos msg kind =
+ cat_error msg ("Failed to parse " ^ kind ^
+ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
+
+fun parse_sort ctxt text =
+ let
+ val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
+ val S =
+ parse_raw ctxt "sort" (syms, pos)
+ |> report_result ctxt pos
+ |> sort_of_term
+ handle ERROR msg => parse_failed ctxt pos msg "sort";
+ in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
+
+fun parse_typ ctxt text =
+ let
+ val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
+ val T =
+ parse_raw ctxt "type" (syms, pos)
+ |> report_result ctxt pos
+ |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t)
+ handle ERROR msg => parse_failed ctxt pos msg "type";
+ in T end;
+
+fun parse_term T ctxt text =
+ let
+ val (T', _) = Type_Infer.paramify_dummies T 0;
+ val (markup, kind) =
+ if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
+ val (syms, pos) = Syntax.parse_token ctxt markup text;
+
+ val default_root = Config.get ctxt Syntax.default_root;
+ val root =
+ (case T' of
+ Type (c, _) =>
+ if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c
+ then default_root else c
+ | _ => default_root);
+ in
+ let
+ val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
+ val ambiguity = length (proper_results results);
+
+ val level = Config.get ctxt Syntax.ambiguity_level;
+ val limit = Config.get ctxt Syntax.ambiguity_limit;
+
+ fun ambig_msg () =
+ if ambiguity > 1 andalso ambiguity <= level then
+ "Got more than one parse tree.\n\
+ \Retry with smaller syntax_ambiguity_level for more information."
+ else "";
+
+ (*brute-force disambiguation via type-inference*)
+ fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
+ handle exn as ERROR _ => Exn.Exn exn;
+
+ val results' =
+ if ambiguity > 1 then
+ (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
+ check results
+ else results;
+ val reports' = fst (hd results');
+
+ val errs = map snd (failed_results results');
+ val checked = map snd (proper_results results');
+ val len = length checked;
+
+ val show_term = Syntax.string_of_term (Config.put Syntax.show_brackets true ctxt);
+ in
+ if len = 0 then
+ report_result ctxt pos
+ [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
+ else if len = 1 then
+ (if ambiguity > level then
+ Context_Position.if_visible ctxt warning
+ "Fortunately, only one parse tree is type correct.\n\
+ \You may still want to disambiguate your grammar or your input."
+ else (); report_result ctxt pos results')
+ else
+ report_result ctxt pos
+ [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
+ (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
+ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+ map show_term (take limit checked))))))]
+ end handle ERROR msg => parse_failed ctxt pos msg kind
+ end;
+
+
+(* parse_ast_pattern *)
+
+fun parse_ast_pattern ctxt (root, str) =
+ let
+ val syn = ProofContext.syn_of ctxt;
+
+ fun constify (ast as Ast.Constant _) = ast
+ | constify (ast as Ast.Variable x) =
+ if Syntax.is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
+ else ast
+ | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
+
+ val (syms, pos) = Syntax.read_token str;
+ in
+ parse_asts ctxt true root (syms, pos)
+ |> report_result ctxt pos
+ |> constify
+ end;
+
+
+
+(** encode parse trees **)
+
+(* term_of_sort *)
+
+fun term_of_sort S =
+ let
+ val class = Lexicon.const o Lexicon.mark_class;
+
+ fun classes [c] = class c
+ | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
+ in
+ (case S of
+ [] => Lexicon.const "_topsort"
+ | [c] => class c
+ | cs => Lexicon.const "_sort" $ classes cs)
+ end;
+
+
+(* term_of_typ *)
+
+fun term_of_typ ctxt ty =
+ let
+ val show_sorts = Config.get ctxt show_sorts;
+
+ fun of_sort t S =
+ if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
+ else t;
+
+ fun term_of (Type (a, Ts)) =
+ Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
+ | term_of (TFree (x, S)) =
+ if is_some (Lexicon.decode_position 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;
+
+
+(* simple_ast_of *)
+
+fun simple_ast_of ctxt =
+ let
+ val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
+ fun ast_of (Const (c, _)) = Ast.Constant c
+ | ast_of (Free (x, _)) = Ast.Variable x
+ | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
+ | ast_of (t as _ $ _) =
+ let val (f, args) = strip_comb t
+ in Ast.mk_appl (ast_of f) (map ast_of args) end
+ | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
+ | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+ in ast_of end;
+
+
+(* sort_to_ast and typ_to_ast *)
+
+fun ast_of_termT ctxt trf tm =
+ let
+ val ctxt' = Config.put show_sorts false ctxt;
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
+ | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
+ | ast_of (Const (a, _)) = trans a []
+ | ast_of (t as _ $ _) =
+ (case strip_comb t of
+ (Const (a, _), args) => trans a args
+ | (f, args) => Ast.Appl (map ast_of (f :: args)))
+ | ast_of t = simple_ast_of ctxt t
+ and trans a args = ast_of (trf a ctxt' dummyT args)
+ handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
+ in ast_of tm end;
+
+fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
+
+
+(* term_to_ast *)
+
+fun term_to_ast idents is_syntax_const ctxt trf tm =
+ let
+ val show_types =
+ Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+ Config.get ctxt show_all_types;
+ val show_structs = Config.get ctxt show_structs;
+ val show_free_types = Config.get ctxt show_free_types;
+ val show_all_types = Config.get ctxt show_all_types;
+
+ val {structs, fixes} = idents;
+
+ fun mark_atoms ((t as Const (c, _)) $ u) =
+ if member (op =) Syntax.standard_token_markers c
+ then t $ u else mark_atoms t $ mark_atoms u
+ | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
+ | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
+ | mark_atoms (t as Const (c, T)) =
+ if is_syntax_const c then t
+ else Const (Lexicon.mark_const c, T)
+ | mark_atoms (t as Free (x, T)) =
+ let val i = find_index (fn s => s = x) structs + 1 in
+ if i = 0 andalso member (op =) fixes x then
+ Const (Lexicon.mark_fixed x, T)
+ else if i = 1 andalso not show_structs then
+ Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
+ else Lexicon.const "_free" $ t
+ end
+ | mark_atoms (t as Var (xi, T)) =
+ if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
+ else Lexicon.const "_var" $ t
+ | mark_atoms a = a;
+
+ fun prune_typs (t_seen as (Const _, _)) = t_seen
+ | prune_typs (t as Free (x, ty), seen) =
+ if ty = dummyT then (t, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
+ else (t, t :: seen)
+ | prune_typs (t as Var (xi, ty), seen) =
+ if ty = dummyT then (t, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+ else (t, t :: seen)
+ | prune_typs (t_seen as (Bound _, _)) = t_seen
+ | prune_typs (Abs (x, ty, t), seen) =
+ let val (t', seen') = prune_typs (t, seen);
+ in (Abs (x, ty, t'), seen') end
+ | prune_typs (t1 $ t2, seen) =
+ let
+ val (t1', seen') = prune_typs (t1, seen);
+ val (t2', seen'') = prune_typs (t2, seen');
+ in (t1' $ t2', seen'') end;
+
+ fun ast_of tm =
+ (case strip_comb tm of
+ (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
+ | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
+ Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+ | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
+ Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
+ | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
+ Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+ | (Const ("_idtdummy", T), ts) =>
+ Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
+ | (const as Const (c, T), ts) =>
+ if show_all_types
+ then Ast.mk_appl (constrain const T) (map ast_of ts)
+ else trans c T ts
+ | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
+
+ and trans a T args = ast_of (trf a ctxt T args)
+ handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
+
+ and constrain t T =
+ if show_types andalso T <> dummyT then
+ Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
+ ast_of_termT ctxt trf (term_of_typ ctxt T)]
+ else simple_ast_of ctxt t;
+ in
+ tm
+ |> Syn_Trans.prop_tr'
+ |> show_types ? (#1 o prune_typs o rpair [])
+ |> mark_atoms
+ |> ast_of
+ end;
+
+
+
+(** unparse **)
+
+local
+
+fun unparse_t t_to_ast prt_t markup ctxt curried t =
+ let
+ val syn = ProofContext.syn_of ctxt;
+ val tokentr = Syntax.token_translation syn (print_mode_value ());
+ 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
+ |> 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;
+
+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))
+ end;
+
+end;
+
+
+
+(** translations **)
+
+(* type propositions *)
+
+fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
+ Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
+ | type_prop_tr' ctxt T [t] =
+ Lexicon.const "_ofclass" $ term_of_typ ctxt T $ t
+ | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
+
+
+(* type reflection *)
+
+fun type_tr' ctxt (Type ("itself", [T])) ts =
+ Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt T, ts)
+ | type_tr' _ _ _ = raise Match;
+
+
+(* type constraints *)
+
+fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
+ Term.list_comb (Lexicon.const "_constrain" $ t $ term_of_typ ctxt T, ts)
+ | type_constraint_tr' _ _ _ = raise Match;
+
+
+(* setup translations *)
+
+val _ = Context.>> (Context.map_theory
+ (Sign.add_advanced_trfunsT
+ [("_type_prop", type_prop_tr'),
+ ("\\<^const>TYPE", type_tr'),
+ ("_type_constraint_", type_constraint_tr')]));
+
+
+
+(** install operations **)
+
+val _ = Syntax.install_operations
+ {parse_sort = parse_sort,
+ parse_typ = parse_typ,
+ parse_term = parse_term dummyT,
+ parse_prop = parse_term propT,
+ unparse_sort = unparse_sort,
+ unparse_typ = unparse_typ,
+ unparse_term = unparse_term};
+
+end;
--- a/src/Pure/Syntax/type_ext.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML Wed Apr 06 18:17:19 2011 +0200
@@ -6,16 +6,10 @@
signature TYPE_EXT0 =
sig
- val sort_of_term: term -> sort
- val term_sorts: term -> (indexname * sort) list
- val typ_of_term: (indexname -> sort) -> term -> typ
+ 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
- type term_context
- val decode_term: term_context ->
- Position.reports * term Exn.result -> Position.reports * term Exn.result
- val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
end;
@@ -23,9 +17,7 @@
signature TYPE_EXT =
sig
include TYPE_EXT0
- val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
- val sortT: typ
val type_ext: Syn_Ext.syn_ext
end;
@@ -34,79 +26,12 @@
(** input utils **)
-(* sort_of_term *)
-
-fun sort_of_term tm =
- let
- fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
-
- fun class s = Lexicon.unmark_class s handle Fail _ => err ();
-
- fun classes (Const (s, _)) = [class s]
- | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
- | classes _ = err ();
-
- fun sort (Const ("_topsort", _)) = []
- | sort (Const (s, _)) = [class s]
- | sort (Const ("_sort", _) $ cs) = classes cs
- | sort _ = err ();
- in sort tm end;
-
-
-(* term_sorts *)
-
-fun term_sorts tm =
- let
- val sort_of = sort_of_term;
-
- fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
- insert (op =) ((x, ~1), sort_of cs)
- | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
- insert (op =) ((x, ~1), sort_of cs)
- | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
- insert (op =) (xi, sort_of cs)
- | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
- insert (op =) (xi, sort_of cs)
- | add_env (Abs (_, _, t)) = add_env t
- | add_env (t1 $ t2) = add_env t1 #> add_env t2
- | add_env _ = I;
- in add_env tm [] end;
-
-
-(* typ_of_term *)
-
-fun typ_of_term get_sort tm =
- let
- fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
-
- fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
- | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
- | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
- | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
- | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
- | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
- TFree (x, get_sort (x, ~1))
- | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
- | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
- TVar (xi, get_sort xi)
- | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
- | typ_of t =
- let
- val (head, args) = Term.strip_comb t;
- val a =
- (case head of
- Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
- | _ => err ());
- in Type (a, map typ_of args) end;
- in typ_of tm end;
-
-
(* positions *)
-fun decode_position (Free (x, _)) = Lexicon.decode_position x
- | decode_position _ = NONE;
+fun decode_position_term (Free (x, _)) = Lexicon.decode_position x
+ | decode_position_term _ = NONE;
-val is_position = is_some o decode_position;
+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
@@ -124,107 +49,6 @@
| strip_positions_ast ast = ast;
-(* decode_term -- transform parse tree into raw term *)
-
-fun markup_bound def id =
- [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
-
-type term_context =
- {get_sort: (indexname * sort) list -> indexname -> sort,
- get_const: string -> bool * string,
- get_free: string -> string option,
- markup_const: string -> Markup.T list,
- markup_free: string -> Markup.T list,
- markup_var: indexname -> Markup.T list};
-
-fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
- | decode_term (term_context: term_context) (reports0, Exn.Result tm) =
- let
- val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
- val decodeT = typ_of_term (get_sort (term_sorts tm));
-
- val reports = Unsynchronized.ref reports0;
- fun report ps = Position.reports reports ps;
-
- fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
- (case 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 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)) =
- let
- val id = serial_string ();
- val _ = report qs (markup_bound true) id;
- in Abs (x, T, decode [] [] (id :: bs) t) end
- | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
- | decode ps _ _ (Const (a, T)) =
- (case try Lexicon.unmark_fixed a of
- SOME x => (report ps markup_free x; Free (x, T))
- | NONE =>
- let
- val c =
- (case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => snd (get_const a));
- val _ = report ps markup_const c;
- in Const (c, T) end)
- | decode ps _ _ (Free (a, T)) =
- (case (get_free a, get_const a) of
- (SOME x, _) => (report ps markup_free x; Free (x, T))
- | (_, (true, c)) => (report ps markup_const c; Const (c, T))
- | (_, (false, c)) =>
- if Long_Name.is_qualified c
- then (report ps markup_const c; Const (c, T))
- else (report ps markup_free c; Free (c, T)))
- | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
- | decode ps _ bs (t as Bound i) =
- (case try (nth bs) i of
- SOME id => (report ps (markup_bound false) id; t)
- | NONE => t);
-
- val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
- in (! reports, tm') end;
-
-
-
-(** output utils **)
-
-(* term_of_sort *)
-
-fun term_of_sort S =
- let
- val class = Lexicon.const o Lexicon.mark_class;
-
- fun classes [c] = class c
- | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
- in
- (case S of
- [] => Lexicon.const "_topsort"
- | [c] => class c
- | cs => Lexicon.const "_sort" $ classes cs)
- end;
-
-
-(* term_of_typ *)
-
-fun term_of_typ show_sorts ty =
- let
- fun of_sort t S =
- if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
- else t;
-
- fun term_of (Type (a, Ts)) =
- Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
- | term_of (TFree (x, S)) =
- if is_some (Lexicon.decode_position 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;
-
-
(** the type syntax **)
--- a/src/Pure/pure_thy.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/pure_thy.ML Wed Apr 06 18:17:19 2011 +0200
@@ -146,7 +146,6 @@
#> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
#> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
#> Sign.add_trfuns Syntax.pure_trfuns
- #> Sign.add_trfunsT Syntax.pure_trfunsT
#> Sign.local_path
#> Sign.add_consts_i
[(Binding.name "term", typ "'a => prop", NoSyn),
--- a/src/Pure/sign.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/Pure/sign.ML Wed Apr 06 18:17:19 2011 +0200
@@ -95,15 +95,14 @@
(string * (term list -> term)) list *
(string * (term list -> term)) list *
(string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
- val add_trfunsT:
- (string * (bool -> typ -> term list -> term)) list -> theory -> theory
+ val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
val add_advanced_trfuns:
(string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
(string * (Proof.context -> term list -> term)) list *
(string * (Proof.context -> term list -> term)) list *
(string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_advanced_trfunsT:
- (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
+ (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
--- a/src/ZF/Tools/numeral_syntax.ML Wed Apr 06 13:08:44 2011 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML Wed Apr 06 18:17:19 2011 +0200
@@ -1,16 +1,13 @@
(* Title: ZF/Tools/numeral_syntax.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-Concrete syntax for generic numerals. Assumes consts and syntax of
-theory Bin.
+Concrete syntax for generic numerals.
*)
signature NUMERAL_SYNTAX =
sig
val make_binary: int -> int list
val dest_binary: int list -> int
- val int_tr: term list -> term
- val int_tr': bool -> typ -> term list -> term
val setup: theory -> theory
end;
@@ -73,17 +70,15 @@
(* translation of integer constant tokens to and from binary *)
-fun int_tr (*"_Int"*) [t as Free (str, _)] =
+fun int_tr [t as Free (str, _)] =
Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
- | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
+ | int_tr ts = raise TERM ("int_tr", ts);
-fun int_tr' _ _ (*"integ_of"*) [t] =
- Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
- | int_tr' (_: bool) (_: typ) _ = raise Match;
+fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
+ | int_tr' _ = raise Match;
val setup =
- (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
- Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
+ Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [(@{const_syntax integ_of}, int_tr')], []);
end;