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