src/Pure/Syntax/syntax_phases.ML
author wenzelm
Mon Oct 01 16:37:22 2012 +0200 (2012-10-01)
changeset 49674 dbadb4d03cbc
parent 49662 de6be6922c19
child 49685 4341e4d86872
permissions -rw-r--r--
report sort assignment of visible type variables;
     1 (*  Title:      Pure/Syntax/syntax_phases.ML
     2     Author:     Makarius
     3 
     4 Main phases of inner syntax processing, with standard implementations
     5 of parse/unparse operations.
     6 *)
     7 
     8 signature SYNTAX_PHASES =
     9 sig
    10   val decode_sort: term -> sort
    11   val decode_typ: term -> typ
    12   val decode_term: Proof.context ->
    13     Position.report list * term Exn.result -> Position.report list * term Exn.result
    14   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    15   val term_of_typ: Proof.context -> typ -> term
    16   val print_checks: Proof.context -> unit
    17   val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
    18     Context.generic -> Context.generic
    19   val term_check: int -> string -> (Proof.context -> term list -> term list) ->
    20     Context.generic -> Context.generic
    21   val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
    22     Context.generic -> Context.generic
    23   val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
    24     Context.generic -> Context.generic
    25   val typ_check': int -> string ->
    26     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    27     Context.generic -> Context.generic
    28   val term_check': int -> string ->
    29     (term list -> Proof.context -> (term list * Proof.context) option) ->
    30     Context.generic -> Context.generic
    31   val typ_uncheck': int -> string ->
    32     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    33     Context.generic -> Context.generic
    34   val term_uncheck': int -> string ->
    35     (term list -> Proof.context -> (term list * Proof.context) option) ->
    36     Context.generic -> Context.generic
    37 end
    38 
    39 structure Syntax_Phases: SYNTAX_PHASES =
    40 struct
    41 
    42 (** markup logical entities **)
    43 
    44 fun markup_class ctxt c =
    45   [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
    46 
    47 fun markup_type ctxt c =
    48   [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
    49 
    50 fun markup_const ctxt c =
    51   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
    52 
    53 fun markup_free ctxt x =
    54   [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @
    55   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    56    then [Variable.markup_fixed ctxt x]
    57    else []);
    58 
    59 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var];
    60 
    61 fun markup_bound def ps (name, id) =
    62   let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in
    63     Isabelle_Markup.bound ::
    64       map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
    65   end;
    66 
    67 fun markup_entity ctxt c =
    68   (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
    69     SOME "" => []
    70   | SOME b => markup_entity ctxt b
    71   | NONE => c |> Lexicon.unmark
    72      {case_class = markup_class ctxt,
    73       case_type = markup_type ctxt,
    74       case_const = markup_const ctxt,
    75       case_fixed = markup_free ctxt,
    76       case_default = K []});
    77 
    78 
    79 
    80 (** decode parse trees **)
    81 
    82 (* decode_sort *)
    83 
    84 fun decode_sort tm =
    85   let
    86     fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
    87 
    88     fun class s = Lexicon.unmark_class s handle Fail _ => err ();
    89     fun class_pos s = if is_some (Term_Position.decode s) then s else err ();
    90 
    91     fun classes (Const (s, _)) = [class s]
    92       | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
    93       | classes _ = err ();
    94 
    95     fun sort (Const ("_topsort", _)) = []
    96       | sort (Const ("_sort", _) $ cs) = classes cs
    97       | sort (Const (s, _)) = [class s]
    98       | sort (Free (s, _)) = [class_pos s]
    99       | sort _ = err ();
   100   in sort tm end;
   101 
   102 
   103 (* decode_typ *)
   104 
   105 fun decode_typ tm =
   106   let
   107     fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
   108 
   109     fun typ (Free (x, _)) = TFree (x, dummyS)
   110       | typ (Var (xi, _)) = TVar (xi, dummyS)
   111       | typ (Const ("_tfree",_) $ (t as Free _)) = typ t
   112       | typ (Const ("_tvar",_) $ (t as Var _)) = typ t
   113       | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s)
   114       | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) =
   115           TFree (x, decode_sort s)
   116       | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s)
   117       | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) =
   118           TVar (xi, decode_sort s)
   119       | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s)
   120       | typ t =
   121           let
   122             val (head, args) = Term.strip_comb t;
   123             val a =
   124               (case head of
   125                 Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
   126               | _ => err ());
   127           in Type (a, map typ args) end;
   128   in typ tm end;
   129 
   130 
   131 (* parsetree_to_ast *)
   132 
   133 fun parsetree_to_ast ctxt raw trf parsetree =
   134   let
   135     val reports = Unsynchronized.ref ([]: Position.report list);
   136     fun report pos = Position.store_reports reports [pos];
   137 
   138     fun trans a args =
   139       (case trf a of
   140         NONE => Ast.mk_appl (Ast.Constant a) args
   141       | SOME f => f ctxt args);
   142 
   143     fun asts_of_token tok =
   144       if Lexicon.valued_token tok
   145       then [Ast.Variable (Lexicon.str_of_token tok)]
   146       else [];
   147 
   148     fun asts_of_position c tok =
   149       if raw then asts_of_token tok
   150       else
   151         [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok),
   152           Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
   153 
   154     and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
   155           let
   156             val pos = Lexicon.pos_of_token tok;
   157             val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
   158               handle ERROR msg => error (msg ^ Position.here pos);
   159             val _ = report pos (markup_class ctxt) c;
   160           in [Ast.Constant (Lexicon.mark_class c)] end
   161       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
   162           let
   163             val pos = Lexicon.pos_of_token tok;
   164             val Type (c, _) =
   165               Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
   166                 handle ERROR msg => error (msg ^ Position.here pos);
   167             val _ = report pos (markup_type ctxt) c;
   168           in [Ast.Constant (Lexicon.mark_type c)] end
   169       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
   170       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
   171       | asts_of (Parser.Node (a, pts)) =
   172           let
   173             val _ = pts |> List.app
   174               (fn Parser.Node _ => () | Parser.Tip tok =>
   175                 if Lexicon.valued_token tok then ()
   176                 else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
   177           in [trans a (maps asts_of pts)] end
   178       | asts_of (Parser.Tip tok) = asts_of_token tok
   179 
   180     and ast_of pt =
   181       (case asts_of pt of
   182         [ast] => ast
   183       | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
   184 
   185     val ast = Exn.interruptible_capture ast_of parsetree;
   186   in (! reports, ast) end;
   187 
   188 
   189 (* ast_to_term *)
   190 
   191 fun ast_to_term ctxt trf =
   192   let
   193     fun trans a args =
   194       (case trf a of
   195         NONE => Term.list_comb (Syntax.const a, args)
   196       | SOME f => f ctxt args);
   197 
   198     fun term_of (Ast.Constant a) = trans a []
   199       | term_of (Ast.Variable x) = Lexicon.read_var x
   200       | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
   201           trans a (map term_of asts)
   202       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
   203           Term.list_comb (term_of ast, map term_of asts)
   204       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
   205   in term_of end;
   206 
   207 
   208 (* decode_term -- transform parse tree into raw term *)
   209 
   210 fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
   211   | decode_term ctxt (reports0, Exn.Res tm) =
   212       let
   213         fun get_const a =
   214           ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
   215             handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
   216         val get_free = Proof_Context.intern_skolem ctxt;
   217 
   218         val reports = Unsynchronized.ref reports0;
   219         fun report ps = Position.store_reports reports ps;
   220 
   221         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
   222               (case Term_Position.decode_position typ of
   223                 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
   224               | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
   225           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
   226               (case Term_Position.decode_position typ of
   227                 SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
   228               | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
   229           | decode _ qs bs (Abs (x, T, t)) =
   230               let
   231                 val id = serial ();
   232                 val _ = report qs (markup_bound true qs) (x, id);
   233               in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
   234           | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
   235           | decode ps _ _ (Const (a, T)) =
   236               (case try Lexicon.unmark_fixed a of
   237                 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
   238               | NONE =>
   239                   let
   240                     val c =
   241                       (case try Lexicon.unmark_const a of
   242                         SOME c => c
   243                       | NONE => snd (get_const a));
   244                     val _ = report ps (markup_const ctxt) c;
   245                   in Const (c, T) end)
   246           | decode ps _ _ (Free (a, T)) =
   247               (case (get_free a, get_const a) of
   248                 (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
   249               | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
   250               | (_, (false, c)) =>
   251                   if Long_Name.is_qualified c
   252                   then (report ps (markup_const ctxt) c; Const (c, T))
   253                   else (report ps (markup_free ctxt) c; Free (c, T)))
   254           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
   255           | decode ps _ bs (t as Bound i) =
   256               (case try (nth bs) i of
   257                 SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
   258               | NONE => t);
   259 
   260         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
   261       in (! reports, tm') end;
   262 
   263 
   264 
   265 (** parse **)
   266 
   267 (* results *)
   268 
   269 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
   270 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
   271 
   272 fun report_result ctxt pos ambig_msgs results =
   273   (case (proper_results results, failed_results results) of
   274     ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
   275   | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
   276   | _ =>
   277       if null ambig_msgs then
   278         error ("Parse error: ambiguous syntax" ^ Position.here pos)
   279       else error (cat_lines ambig_msgs));
   280 
   281 
   282 (* parse raw asts *)
   283 
   284 fun parse_asts ctxt raw root (syms, pos) =
   285   let
   286     val syn = Proof_Context.syn_of ctxt;
   287     val ast_tr = Syntax.parse_ast_translation syn;
   288 
   289     val toks = Syntax.tokenize syn raw syms;
   290     val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
   291 
   292     val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
   293       handle ERROR msg =>
   294         error (msg ^
   295           implode
   296             (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
   297     val len = length pts;
   298 
   299     val limit = Config.get ctxt Syntax.ambiguity_limit;
   300     val ambig_msgs =
   301       if len <= 1 then []
   302       else
   303         [cat_lines
   304           (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
   305             "\nproduces " ^ string_of_int len ^ " parse trees" ^
   306             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   307             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
   308 
   309   in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end;
   310 
   311 fun parse_tree ctxt root input =
   312   let
   313     val syn = Proof_Context.syn_of ctxt;
   314     val tr = Syntax.parse_translation syn;
   315     val parse_rules = Syntax.parse_rules syn;
   316     val (ambig_msgs, asts) = parse_asts ctxt false root input;
   317     val results =
   318       (map o apsnd o Exn.maps_result)
   319         (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
   320   in (ambig_msgs, results) end;
   321 
   322 
   323 (* parse logical entities *)
   324 
   325 fun parse_failed ctxt pos msg kind =
   326   cat_error msg ("Failed to parse " ^ kind ^
   327     Markup.markup Isabelle_Markup.report
   328       (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
   329 
   330 fun parse_sort ctxt =
   331   Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
   332     (fn (syms, pos) =>
   333       parse_tree ctxt "sort" (syms, pos)
   334       |> uncurry (report_result ctxt pos)
   335       |> decode_sort
   336       |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
   337       handle ERROR msg => parse_failed ctxt pos msg "sort");
   338 
   339 fun parse_typ ctxt =
   340   Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
   341     (fn (syms, pos) =>
   342       parse_tree ctxt "type" (syms, pos)
   343       |> uncurry (report_result ctxt pos)
   344       |> decode_typ
   345       handle ERROR msg => parse_failed ctxt pos msg "type");
   346 
   347 fun parse_term is_prop ctxt =
   348   let
   349     val (markup, kind, root, constrain) =
   350       if is_prop
   351       then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT)
   352       else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I);
   353     val decode = constrain o Term_XML.Decode.term;
   354   in
   355     Syntax.parse_token ctxt decode markup
   356       (fn (syms, pos) =>
   357         let
   358           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
   359           val parsed_len = length (proper_results results);
   360 
   361           val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
   362           val limit = Config.get ctxt Syntax.ambiguity_limit;
   363 
   364           (*brute-force disambiguation via type-inference*)
   365           fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
   366             handle exn as ERROR _ => Exn.Exn exn;
   367 
   368           val results' =
   369             if parsed_len > 1 then
   370               (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
   371                 check results
   372             else results;
   373           val reports' = fst (hd results');
   374 
   375           val errs = map snd (failed_results results');
   376           val checked = map snd (proper_results results');
   377           val checked_len = length checked;
   378 
   379           val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
   380         in
   381           if checked_len = 0 then
   382             report_result ctxt pos []
   383               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
   384           else if checked_len = 1 then
   385             (if parsed_len > 1 andalso ambiguity_warning then
   386               Context_Position.if_visible ctxt warning
   387                 (cat_lines (ambig_msgs @
   388                   ["Fortunately, only one parse tree is type correct" ^
   389                   Position.here (Position.reset_range pos) ^
   390                   ",\nbut you may still want to disambiguate your grammar or your input."]))
   391              else (); report_result ctxt pos [] results')
   392           else
   393             report_result ctxt pos []
   394               [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
   395                 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
   396                   (if checked_len <= limit then ""
   397                    else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   398                   map show_term (take limit checked))))))]
   399         end handle ERROR msg => parse_failed ctxt pos msg kind)
   400   end;
   401 
   402 
   403 (* parse_ast_pattern *)
   404 
   405 fun parse_ast_pattern ctxt (root, str) =
   406   let
   407     val syn = Proof_Context.syn_of ctxt;
   408 
   409     fun constify (ast as Ast.Constant _) = ast
   410       | constify (ast as Ast.Variable x) =
   411           if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
   412           then Ast.Constant x
   413           else ast
   414       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   415 
   416     val (syms, pos) = Syntax.read_token str;
   417   in
   418     parse_asts ctxt true root (syms, pos)
   419     |> uncurry (report_result ctxt pos)
   420     |> constify
   421   end;
   422 
   423 
   424 
   425 (** encode parse trees **)
   426 
   427 (* term_of_sort *)
   428 
   429 fun term_of_sort S =
   430   let
   431     val class = Syntax.const o Lexicon.mark_class;
   432 
   433     fun classes [c] = class c
   434       | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
   435   in
   436     (case S of
   437       [] => Syntax.const "_topsort"
   438     | [c] => class c
   439     | cs => Syntax.const "_sort" $ classes cs)
   440   end;
   441 
   442 
   443 (* term_of_typ *)
   444 
   445 fun term_of_typ ctxt ty =
   446   let
   447     val show_sorts = Config.get ctxt show_sorts;
   448 
   449     fun of_sort t S =
   450       if show_sorts then Syntax.const "_ofsort" $ t $ term_of_sort S
   451       else t;
   452 
   453     fun term_of (Type (a, Ts)) =
   454           Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
   455       | term_of (TFree (x, S)) =
   456           if is_some (Term_Position.decode x) then Syntax.free x
   457           else of_sort (Syntax.const "_tfree" $ Syntax.free x) S
   458       | term_of (TVar (xi, S)) = of_sort (Syntax.const "_tvar" $ Syntax.var xi) S;
   459   in term_of ty end;
   460 
   461 
   462 (* simple_ast_of *)
   463 
   464 fun simple_ast_of ctxt =
   465   let
   466     val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
   467     fun ast_of (Const (c, _)) = Ast.Constant c
   468       | ast_of (Free (x, _)) = Ast.Variable x
   469       | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
   470       | ast_of (t as _ $ _) =
   471           let val (f, args) = strip_comb t
   472           in Ast.mk_appl (ast_of f) (map ast_of args) end
   473       | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
   474       | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
   475   in ast_of end;
   476 
   477 
   478 (* sort_to_ast and typ_to_ast *)
   479 
   480 fun ast_of_termT ctxt trf tm =
   481   let
   482     val ctxt' = Config.put show_sorts false ctxt;
   483     fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
   484       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
   485       | ast_of (Const (a, _)) = trans a []
   486       | ast_of (t as _ $ _) =
   487           (case strip_comb t of
   488             (Const (a, _), args) => trans a args
   489           | (f, args) => Ast.Appl (map ast_of (f :: args)))
   490       | ast_of t = simple_ast_of ctxt t
   491     and trans a args = ast_of (trf a ctxt' dummyT args)
   492       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   493   in ast_of tm end;
   494 
   495 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
   496 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
   497 
   498 
   499 (* term_to_ast *)
   500 
   501 fun term_to_ast idents is_syntax_const ctxt trf tm =
   502   let
   503     val show_types =
   504       Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
   505       Config.get ctxt show_all_types;
   506     val show_structs = Config.get ctxt show_structs;
   507     val show_free_types = Config.get ctxt show_free_types;
   508     val show_all_types = Config.get ctxt show_all_types;
   509     val show_markup = Config.get ctxt show_markup;
   510 
   511     val {structs, fixes} = idents;
   512 
   513     fun mark_atoms ((t as Const (c, _)) $ u) =
   514           if member (op =) Syntax.token_markers c
   515           then t $ u else mark_atoms t $ mark_atoms u
   516       | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
   517       | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
   518       | mark_atoms (t as Const (c, T)) =
   519           if is_syntax_const c then t
   520           else Const (Lexicon.mark_const c, T)
   521       | mark_atoms (t as Free (x, T)) =
   522           let val i = find_index (fn s => s = x) structs + 1 in
   523             if i = 0 andalso member (op =) fixes x then
   524               Const (Lexicon.mark_fixed x, T)
   525             else if i = 1 andalso not show_structs then
   526               Syntax.const "_struct" $ Syntax.const "_indexdefault"
   527             else Syntax.const "_free" $ t
   528           end
   529       | mark_atoms (t as Var (xi, T)) =
   530           if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
   531           else Syntax.const "_var" $ t
   532       | mark_atoms a = a;
   533 
   534     fun prune_typs (t_seen as (Const _, _)) = t_seen
   535       | prune_typs (t as Free (x, ty), seen) =
   536           if ty = dummyT then (t, seen)
   537           else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
   538           else (t, t :: seen)
   539       | prune_typs (t as Var (xi, ty), seen) =
   540           if ty = dummyT then (t, seen)
   541           else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
   542           else (t, t :: seen)
   543       | prune_typs (t_seen as (Bound _, _)) = t_seen
   544       | prune_typs (Abs (x, ty, t), seen) =
   545           let val (t', seen') = prune_typs (t, seen);
   546           in (Abs (x, ty, t'), seen') end
   547       | prune_typs (t1 $ t2, seen) =
   548           let
   549             val (t1', seen') = prune_typs (t1, seen);
   550             val (t2', seen'') = prune_typs (t2, seen');
   551           in (t1' $ t2', seen'') end;
   552 
   553     fun ast_of tm =
   554       (case strip_comb tm of
   555         (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
   556       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   557           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
   558       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   559           Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
   560       | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
   561           let
   562             val X =
   563               if show_markup andalso not show_types orelse B <> dummyT then T
   564               else dummyT;
   565           in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
   566       | (Const ("_idtdummy", T), ts) =>
   567           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
   568       | (const as Const (c, T), ts) =>
   569           if show_all_types
   570           then Ast.mk_appl (constrain const T) (map ast_of ts)
   571           else trans c T ts
   572       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
   573 
   574     and trans a T args = ast_of (trf a ctxt T args)
   575       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
   576 
   577     and constrain t T =
   578       if (show_types orelse show_markup) andalso T <> dummyT then
   579         Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
   580           ast_of_termT ctxt trf (term_of_typ ctxt T)]
   581       else simple_ast_of ctxt t;
   582   in
   583     tm
   584     |> Syntax_Trans.prop_tr'
   585     |> show_types ? (#1 o prune_typs o rpair [])
   586     |> mark_atoms
   587     |> ast_of
   588   end;
   589 
   590 
   591 
   592 (** unparse **)
   593 
   594 local
   595 
   596 fun free_or_skolem ctxt x =
   597   let
   598     val m =
   599       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
   600       then Isabelle_Markup.fixed x
   601       else Isabelle_Markup.intensify;
   602   in
   603     if can Name.dest_skolem x
   604     then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
   605     else ([m, Isabelle_Markup.free], x)
   606   end;
   607 
   608 fun var_or_skolem s =
   609   (case Lexicon.read_variable s of
   610     SOME (x, i) =>
   611       (case try Name.dest_skolem x of
   612         NONE => (Isabelle_Markup.var, s)
   613       | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
   614   | NONE => (Isabelle_Markup.var, s));
   615 
   616 val typing_elem = YXML.output_markup_elem Isabelle_Markup.typing;
   617 
   618 fun unparse_t t_to_ast prt_t markup ctxt t =
   619   let
   620     val show_types =
   621       Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
   622       Config.get ctxt show_all_types;
   623     val show_markup = Config.get ctxt show_markup;
   624 
   625     val syn = Proof_Context.syn_of ctxt;
   626     val prtabs = Syntax.prtabs syn;
   627     val trf = Syntax.print_ast_translation syn;
   628 
   629     fun markup_extern c =
   630       (case Syntax.lookup_const syn c of
   631         SOME "" => ([], c)
   632       | SOME b => markup_extern b
   633       | NONE => c |> Lexicon.unmark
   634          {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
   635           case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
   636           case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
   637           case_fixed = fn x => free_or_skolem ctxt x,
   638           case_default = fn x => ([], x)});
   639 
   640     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
   641       | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
   642       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
   643       | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
   644       | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad, x))
   645       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
   646       | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
   647       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
   648       | token_trans _ _ = NONE;
   649 
   650     fun markup_trans a [Ast.Variable x] = token_trans a x
   651       | markup_trans "_constrain" [t, ty] = constrain_trans t ty
   652       | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
   653       | markup_trans _ _ = NONE
   654 
   655     and constrain_trans t ty =
   656       if not show_types andalso show_markup then
   657         let
   658           val ((bg1, bg2), en) = typing_elem;
   659           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
   660         in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
   661       else NONE
   662 
   663     and pretty_typ_ast m ast = ast
   664       |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
   665       |> Pretty.markup m
   666 
   667     and pretty_ast m ast = ast
   668       |> prt_t ctxt prtabs trf markup_trans markup_extern
   669       |> Pretty.markup m;
   670   in
   671     t_to_ast ctxt (Syntax.print_translation syn) t
   672     |> Ast.normalize ctxt (Syntax.print_rules syn)
   673     |> pretty_ast markup
   674   end;
   675 
   676 in
   677 
   678 val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort;
   679 val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ;
   680 
   681 fun unparse_term ctxt =
   682   let
   683     val thy = Proof_Context.theory_of ctxt;
   684     val syn = Proof_Context.syn_of ctxt;
   685     val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
   686   in
   687     unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
   688       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
   689       Isabelle_Markup.term ctxt
   690   end;
   691 
   692 end;
   693 
   694 
   695 
   696 (** translations **)
   697 
   698 (* type propositions *)
   699 
   700 fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
   701       Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   702   | type_prop_tr' ctxt T [t] =
   703       Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
   704   | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
   705 
   706 
   707 (* type reflection *)
   708 
   709 fun type_tr' ctxt (Type ("itself", [T])) ts =
   710       Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
   711   | type_tr' _ _ _ = raise Match;
   712 
   713 
   714 (* type constraints *)
   715 
   716 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
   717       Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   718   | type_constraint_tr' _ _ _ = raise Match;
   719 
   720 
   721 (* authentic syntax *)
   722 
   723 fun const_ast_tr intern ctxt [Ast.Variable c] =
   724       let
   725         val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
   726         val d = if intern then Lexicon.mark_const c' else c;
   727       in Ast.Constant d end
   728   | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
   729       (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
   730         handle ERROR msg =>
   731           error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
   732   | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
   733 
   734 
   735 (* setup translations *)
   736 
   737 val _ = Context.>> (Context.map_theory
   738  (Sign.add_advanced_trfuns
   739   ([("_context_const", const_ast_tr true),
   740     ("_context_xconst", const_ast_tr false)], [], [], []) #>
   741   Sign.add_advanced_trfunsT
   742    [("_type_prop", type_prop_tr'),
   743     ("\\<^const>TYPE", type_tr'),
   744     ("_type_constraint_", type_constraint_tr')]));
   745 
   746 
   747 
   748 (** check/uncheck **)
   749 
   750 (* context-sensitive (un)checking *)
   751 
   752 type key = int * bool;
   753 
   754 structure Checks = Generic_Data
   755 (
   756   type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
   757   type T =
   758     ((key * ((string * typ check) * stamp) list) list *
   759      (key * ((string * term check) * stamp) list) list);
   760   val empty = ([], []);
   761   val extend = I;
   762   fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
   763     (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
   764      AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
   765 );
   766 
   767 fun print_checks ctxt =
   768   let
   769     fun split_checks checks =
   770       List.partition (fn ((_, un), _) => not un) checks
   771       |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
   772           #> sort (int_ord o pairself fst));
   773     fun pretty_checks kind checks =
   774       checks |> map (fn (i, names) => Pretty.block
   775         [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
   776           Pretty.brk 1, Pretty.strs names]);
   777 
   778     val (typs, terms) = Checks.get (Context.Proof ctxt);
   779     val (typ_checks, typ_unchecks) = split_checks typs;
   780     val (term_checks, term_unchecks) = split_checks terms;
   781   in
   782     pretty_checks "typ_checks" typ_checks @
   783     pretty_checks "term_checks" term_checks @
   784     pretty_checks "typ_unchecks" typ_unchecks @
   785     pretty_checks "term_unchecks" term_unchecks
   786   end |> Pretty.chunks |> Pretty.writeln;
   787 
   788 
   789 local
   790 
   791 fun context_check which (key: key) name f =
   792   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
   793 
   794 fun simple_check eq f xs ctxt =
   795   let val xs' = f ctxt xs
   796   in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
   797 
   798 in
   799 
   800 fun typ_check' stage = context_check apfst (stage, false);
   801 fun term_check' stage = context_check apsnd (stage, false);
   802 fun typ_uncheck' stage = context_check apfst (stage, true);
   803 fun term_uncheck' stage = context_check apsnd (stage, true);
   804 
   805 fun typ_check key name f = typ_check' key name (simple_check (op =) f);
   806 fun term_check key name f = term_check' key name (simple_check (op aconv) f);
   807 fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
   808 fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
   809 
   810 end;
   811 
   812 
   813 local
   814 
   815 fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
   816 fun check_all fs = perhaps_apply (map check_stage fs);
   817 
   818 fun check which uncheck ctxt0 xs0 =
   819   let
   820     val funs = which (Checks.get (Context.Proof ctxt0))
   821       |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
   822       |> Library.sort (int_ord o pairself fst) |> map snd
   823       |> not uncheck ? map rev;
   824   in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
   825 
   826 val apply_typ_check = check fst false;
   827 val apply_term_check = check snd false;
   828 val apply_typ_uncheck = check fst true;
   829 val apply_term_uncheck = check snd true;
   830 
   831 in
   832 
   833 fun check_typs ctxt raw_tys =
   834   let
   835     val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
   836     val _ = Context_Position.if_visible ctxt Output.report sorting_report;
   837   in
   838     tys
   839     |> apply_typ_check ctxt
   840     |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
   841   end;
   842 
   843 fun check_terms ctxt raw_ts =
   844   let
   845     val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
   846     val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
   847 
   848     val tys = map (Logic.mk_type o snd) ps;
   849     val (ts', tys') = ts @ tys
   850       |> apply_term_check ctxt
   851       |> chop (length ts);
   852     val typing_report =
   853       fold2 (fn (pos, _) => fn ty =>
   854         if Position.is_reported pos then
   855           cons (Position.reported_text pos Isabelle_Markup.typing
   856             (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
   857         else I) ps tys' []
   858       |> implode;
   859 
   860     val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
   861   in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
   862 
   863 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
   864 
   865 val uncheck_typs = apply_typ_uncheck;
   866 val uncheck_terms = apply_term_uncheck;
   867 
   868 end;
   869 
   870 
   871 (* standard phases *)
   872 
   873 val _ = Context.>>
   874  (typ_check 0 "standard" Proof_Context.standard_typ_check #>
   875   term_check 0 "standard"
   876     (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
   877   term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
   878   term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
   879 
   880 
   881 
   882 (** install operations **)
   883 
   884 val _ = Syntax.install_operations
   885   {parse_sort = parse_sort,
   886    parse_typ = parse_typ,
   887    parse_term = parse_term false,
   888    parse_prop = parse_term true,
   889    unparse_sort = unparse_sort,
   890    unparse_typ = unparse_typ,
   891    unparse_term = unparse_term,
   892    check_typs = check_typs,
   893    check_terms = check_terms,
   894    check_props = check_props,
   895    uncheck_typs = uncheck_typs,
   896    uncheck_terms = uncheck_terms};
   897 
   898 end;