# HG changeset patch # User wenzelm # Date 1302106639 -7200 # Node ID 4ea47da3d19bac0d530e45affc93967ee4347f5e # Parent 5ff3a11e18caace5617c7d027e96658fa2f94557# Parent 097c93dcd87727f8a72605d8f7cf875fc348a044 merged diff -r 5ff3a11e18ca -r 4ea47da3d19b NEWS --- 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) diff -r 5ff3a11e18ca -r 4ea47da3d19b doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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} diff -r 5ff3a11e18ca -r 4ea47da3d19b doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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}% diff -r 5ff3a11e18ca -r 4ea47da3d19b etc/symbols --- 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 @@ \ code: 0x0003b8 font: Isabelle \ code: 0x0003b9 font: Isabelle \ code: 0x0003ba font: Isabelle -\ code: 0x0003bb font: Isabelle +\ code: 0x0003bb font: Isabelle abbrev: % \ code: 0x0003bc font: Isabelle \ code: 0x0003bd font: Isabelle \ code: 0x0003be font: Isabelle diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Groups.thy --- 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 = diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Library/Cardinality.thy --- 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 \ '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" diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Product_Type.thy --- 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 "\(x,y). f x y" and "split (\x. f x)" as "\(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 *} diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Tools/numeral_syntax.ML --- 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; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Tools/record.ML --- 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 diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Tools/string_syntax.ML --- 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); diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/Typerep.thy --- 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 *} diff -r 5ff3a11e18ca -r 4ea47da3d19b src/HOL/ex/Numeral.thy --- 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 diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/IsaMakefile --- 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 \ diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Isar/isar_cmd.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; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Isar/local_syntax.ML --- 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; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Isar/proof_context.ML --- 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 = diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/ROOT.ML --- 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*) diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/local_syntax.ML --- /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; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/printer.ML --- 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 diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/syn_ext.ML --- 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}; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/syn_trans.ML --- 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; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/syntax.ML --- 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"; + diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/syntax_phases.ML --- /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; diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/Syntax/type_ext.ML --- 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 **) diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/pure_thy.ML --- 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), diff -r 5ff3a11e18ca -r 4ea47da3d19b src/Pure/sign.ML --- 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 diff -r 5ff3a11e18ca -r 4ea47da3d19b src/ZF/Tools/numeral_syntax.ML --- 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;