src/Pure/Syntax/syntax_phases.ML
author wenzelm
Sat Apr 16 15:25:25 2011 +0200 (2011-04-16)
changeset 42359 6ca5407863ed
parent 42358 b47d41d9f4b5
child 42360 da8817d01e7c
permissions -rw-r--r--
prefer local name spaces;
tuned signatures;
tuned;
     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 term_sorts: term -> (indexname * sort) list
    11   val typ_of_term: (indexname -> sort) -> term -> typ
    12   val decode_term: Proof.context ->
    13     Position.reports * term Exn.result -> Position.reports * term Exn.result
    14   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    15   val term_of_typ: Proof.context -> typ -> term
    16 end
    17 
    18 structure Syntax_Phases: SYNTAX_PHASES =
    19 struct
    20 
    21 (** markup logical entities **)
    22 
    23 fun markup_class ctxt c =
    24   [Name_Space.markup_entry (Type.class_space (ProofContext.tsig_of ctxt)) c];
    25 
    26 fun markup_type ctxt c =
    27   [Name_Space.markup_entry (Type.type_space (ProofContext.tsig_of ctxt)) c];
    28 
    29 fun markup_const ctxt c =
    30   [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
    31 
    32 fun markup_free ctxt x =
    33   [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    34   (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
    35    else [Markup.hilite]);
    36 
    37 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
    38 
    39 fun markup_bound def id =
    40   [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
    41 
    42 fun markup_entity ctxt c =
    43   (case Syntax.lookup_const (ProofContext.syn_of ctxt) c of
    44     SOME "" => []
    45   | SOME b => markup_entity ctxt b
    46   | NONE => c |> Lexicon.unmark
    47      {case_class = markup_class ctxt,
    48       case_type = markup_type ctxt,
    49       case_const = markup_const ctxt,
    50       case_fixed = markup_free ctxt,
    51       case_default = K []});
    52 
    53 
    54 
    55 (** decode parse trees **)
    56 
    57 (* sort_of_term *)
    58 
    59 fun sort_of_term tm =
    60   let
    61     fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    62 
    63     fun class s = Lexicon.unmark_class s handle Fail _ => err ();
    64 
    65     fun classes (Const (s, _)) = [class s]
    66       | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
    67       | classes _ = err ();
    68 
    69     fun sort (Const ("_topsort", _)) = []
    70       | sort (Const (s, _)) = [class s]
    71       | sort (Const ("_sort", _) $ cs) = classes cs
    72       | sort _ = err ();
    73   in sort tm end;
    74 
    75 
    76 (* term_sorts *)
    77 
    78 fun term_sorts tm =
    79   let
    80     val sort_of = sort_of_term;
    81 
    82     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
    83           insert (op =) ((x, ~1), sort_of cs)
    84       | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
    85           insert (op =) ((x, ~1), sort_of cs)
    86       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
    87           insert (op =) (xi, sort_of cs)
    88       | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
    89           insert (op =) (xi, sort_of cs)
    90       | add_env (Abs (_, _, t)) = add_env t
    91       | add_env (t1 $ t2) = add_env t1 #> add_env t2
    92       | add_env _ = I;
    93   in add_env tm [] end;
    94 
    95 
    96 (* typ_of_term *)
    97 
    98 fun typ_of_term get_sort tm =
    99   let
   100     fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
   101 
   102     fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
   103       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
   104       | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
   105       | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
   106       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
   107       | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
   108           TFree (x, get_sort (x, ~1))
   109       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
   110       | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
   111           TVar (xi, get_sort xi)
   112       | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
   113       | typ_of t =
   114           let
   115             val (head, args) = Term.strip_comb t;
   116             val a =
   117               (case head of
   118                 Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
   119               | _ => err ());
   120           in Type (a, map typ_of args) end;
   121   in typ_of tm end;
   122 
   123 
   124 (* parsetree_to_ast *)
   125 
   126 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   127   let
   128     val get_class = ProofContext.read_class ctxt;
   129     val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
   130 
   131     val reports = Unsynchronized.ref ([]: Position.reports);
   132     fun report pos = Position.reports reports [pos];
   133 
   134     fun trans a args =
   135       (case trf a of
   136         NONE => Ast.mk_appl (Ast.Constant a) args
   137       | SOME f => f ctxt args);
   138 
   139     fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
   140           let
   141             val c = get_class (Lexicon.str_of_token tok);
   142             val _ = report (Lexicon.pos_of_token tok) (markup_class ctxt) c;
   143           in [Ast.Constant (Lexicon.mark_class c)] end
   144       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
   145           let
   146             val c = get_type (Lexicon.str_of_token tok);
   147             val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
   148           in [Ast.Constant (Lexicon.mark_type c)] end
   149       | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
   150           if constrain_pos then
   151             [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
   152               Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
   153           else [ast_of pt]
   154       | asts_of (Parser.Node (a, pts)) =
   155           let
   156             val _ = pts |> List.app
   157               (fn Parser.Node _ => () | Parser.Tip tok =>
   158                 if Lexicon.valued_token tok then ()
   159                 else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
   160           in [trans a (maps asts_of pts)] end
   161       | asts_of (Parser.Tip tok) =
   162           if Lexicon.valued_token tok
   163           then [Ast.Variable (Lexicon.str_of_token tok)]
   164           else []
   165 
   166     and ast_of pt =
   167       (case asts_of pt of
   168         [ast] => ast
   169       | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
   170 
   171     val ast = Exn.interruptible_capture ast_of parsetree;
   172   in (! reports, ast) end;
   173 
   174 
   175 (* ast_to_term *)
   176 
   177 fun ast_to_term ctxt trf =
   178   let
   179     fun trans a args =
   180       (case trf a of
   181         NONE => Term.list_comb (Lexicon.const a, args)
   182       | SOME f => f ctxt args);
   183 
   184     fun term_of (Ast.Constant a) = trans a []
   185       | term_of (Ast.Variable x) = Lexicon.read_var x
   186       | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
   187           trans a (map term_of asts)
   188       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
   189           Term.list_comb (term_of ast, map term_of asts)
   190       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
   191   in term_of end;
   192 
   193 
   194 (* decode_term -- transform parse tree into raw term *)
   195 
   196 fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
   197   | decode_term ctxt (reports0, Exn.Result tm) =
   198       let
   199         fun get_const a =
   200           ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
   201             handle ERROR _ => (false, Consts.intern (ProofContext.consts_of ctxt) a));
   202         val get_free = ProofContext.intern_skolem ctxt;
   203 
   204         val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
   205 
   206         val reports = Unsynchronized.ref reports0;
   207         fun report ps = Position.reports reports ps;
   208 
   209         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
   210               (case Term_Position.decode_position typ of
   211                 SOME p => decode (p :: ps) qs bs t
   212               | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
   213           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
   214               (case Term_Position.decode_position typ of
   215                 SOME q => decode ps (q :: qs) bs t
   216               | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
   217           | decode _ qs bs (Abs (x, T, t)) =
   218               let
   219                 val id = serial_string ();
   220                 val _ = report qs (markup_bound true) id;
   221               in Abs (x, T, decode [] [] (id :: bs) t) end
   222           | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
   223           | decode ps _ _ (Const (a, T)) =
   224               (case try Lexicon.unmark_fixed a of
   225                 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
   226               | NONE =>
   227                   let
   228                     val c =
   229                       (case try Lexicon.unmark_const a of
   230                         SOME c => c
   231                       | NONE => snd (get_const a));
   232                     val _ = report ps (markup_const ctxt) c;
   233                   in Const (c, T) end)
   234           | decode ps _ _ (Free (a, T)) =
   235               (case (get_free a, get_const a) of
   236                 (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
   237               | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
   238               | (_, (false, c)) =>
   239                   if Long_Name.is_qualified c
   240                   then (report ps (markup_const ctxt) c; Const (c, T))
   241                   else (report ps (markup_free ctxt) c; Free (c, T)))
   242           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
   243           | decode ps _ bs (t as Bound i) =
   244               (case try (nth bs) i of
   245                 SOME id => (report ps (markup_bound false) id; t)
   246               | NONE => t);
   247 
   248         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
   249       in (! reports, tm') end;
   250 
   251 
   252 
   253 (** parse **)
   254 
   255 (* results *)
   256 
   257 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
   258 
   259 fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
   260 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
   261 
   262 fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
   263 
   264 fun report_result ctxt pos results =
   265   (case (proper_results results, failed_results results) of
   266     ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
   267   | ([(reports, x)], _) => (report ctxt reports; x)
   268   | _ => error (ambiguity_msg pos));
   269 
   270 
   271 (* parse raw asts *)
   272 
   273 fun parse_asts ctxt raw root (syms, pos) =
   274   let
   275     val syn = ProofContext.syn_of ctxt;
   276     val ast_tr = Syntax.parse_ast_translation syn;
   277 
   278     val toks = Syntax.tokenize syn raw syms;
   279     val _ = List.app (Lexicon.report_token ctxt) toks;
   280 
   281     val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
   282       handle ERROR msg =>
   283         error (msg ^
   284           implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
   285     val len = length pts;
   286 
   287     val limit = Config.get ctxt Syntax.ambiguity_limit;
   288     val _ =
   289       if len <= Config.get ctxt Syntax.ambiguity_level then ()
   290       else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
   291       else
   292         (Context_Position.if_visible ctxt warning (cat_lines
   293           (("Ambiguous input" ^ Position.str_of pos ^
   294             "\nproduces " ^ string_of_int len ^ " parse trees" ^
   295             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   296             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
   297 
   298     val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
   299     val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
   300   in map parsetree_to_ast pts end;
   301 
   302 fun parse_raw ctxt root input =
   303   let
   304     val syn = ProofContext.syn_of ctxt;
   305     val tr = Syntax.parse_translation syn;
   306     val parse_rules = Syntax.parse_rules syn;
   307   in
   308     parse_asts ctxt false root input
   309     |> (map o apsnd o Exn.maps_result)
   310         (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr))
   311   end;
   312 
   313 
   314 (* parse logical entities *)
   315 
   316 fun parse_failed ctxt pos msg kind =
   317   cat_error msg ("Failed to parse " ^ kind ^
   318     Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
   319 
   320 fun parse_sort ctxt text =
   321   let
   322     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
   323     val S =
   324       parse_raw ctxt "sort" (syms, pos)
   325       |> report_result ctxt pos
   326       |> sort_of_term
   327       handle ERROR msg => parse_failed ctxt pos msg "sort";
   328   in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
   329 
   330 fun parse_typ ctxt text =
   331   let
   332     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
   333     val T =
   334       parse_raw ctxt "type" (syms, pos)
   335       |> report_result ctxt pos
   336       |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t)
   337       handle ERROR msg => parse_failed ctxt pos msg "type";
   338   in T end;
   339 
   340 fun parse_term is_prop ctxt text =
   341   let
   342     val (markup, kind, root, constrain) =
   343       if is_prop
   344       then (Markup.prop, "proposition", "prop", Type.constraint propT)
   345       else (Markup.term, "term", Config.get ctxt Syntax.root, I);
   346     val (syms, pos) = Syntax.parse_token ctxt markup text;
   347   in
   348     let
   349       val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
   350       val ambiguity = length (proper_results results);
   351 
   352       val level = Config.get ctxt Syntax.ambiguity_level;
   353       val limit = Config.get ctxt Syntax.ambiguity_limit;
   354 
   355       fun ambig_msg () =
   356         if ambiguity > 1 andalso ambiguity <= level then
   357           "Got more than one parse tree.\n\
   358           \Retry with smaller syntax_ambiguity_level for more information."
   359         else "";
   360 
   361       (*brute-force disambiguation via type-inference*)
   362       fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
   363         handle exn as ERROR _ => Exn.Exn exn;
   364 
   365       val results' =
   366         if ambiguity > 1 then
   367           (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
   368             check results
   369         else results;
   370       val reports' = fst (hd results');
   371 
   372       val errs = map snd (failed_results results');
   373       val checked = map snd (proper_results results');
   374       val len = length checked;
   375 
   376       val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
   377     in
   378       if len = 0 then
   379         report_result ctxt pos
   380           [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
   381       else if len = 1 then
   382         (if ambiguity > level then
   383           Context_Position.if_visible ctxt warning
   384             "Fortunately, only one parse tree is type correct.\n\
   385             \You may still want to disambiguate your grammar or your input."
   386         else (); report_result ctxt pos results')
   387       else
   388         report_result ctxt pos
   389           [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
   390             (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
   391               (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   392               map show_term (take limit checked))))))]
   393     end handle ERROR msg => parse_failed ctxt pos msg kind
   394   end;
   395 
   396 
   397 (* parse_ast_pattern *)
   398 
   399 fun parse_ast_pattern ctxt (root, str) =
   400   let
   401     val syn = ProofContext.syn_of ctxt;
   402 
   403     fun constify (ast as Ast.Constant _) = ast
   404       | constify (ast as Ast.Variable x) =
   405           if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
   406           then Ast.Constant x
   407           else ast
   408       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   409 
   410     val (syms, pos) = Syntax.read_token str;
   411   in
   412     parse_asts ctxt true root (syms, pos)
   413     |> report_result ctxt pos
   414     |> constify
   415   end;
   416 
   417 
   418 
   419 (** encode parse trees **)
   420 
   421 (* term_of_sort *)
   422 
   423 fun term_of_sort S =
   424   let
   425     val class = Lexicon.const o Lexicon.mark_class;
   426 
   427     fun classes [c] = class c
   428       | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   429   in
   430     (case S of
   431       [] => Lexicon.const "_topsort"
   432     | [c] => class c
   433     | cs => Lexicon.const "_sort" $ classes cs)
   434   end;
   435 
   436 
   437 (* term_of_typ *)
   438 
   439 fun term_of_typ ctxt ty =
   440   let
   441     val show_sorts = Config.get ctxt show_sorts;
   442 
   443     fun of_sort t S =
   444       if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   445       else t;
   446 
   447     fun term_of (Type (a, Ts)) =
   448           Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
   449       | term_of (TFree (x, S)) =
   450           if is_some (Term_Position.decode x) then Syntax.free x
   451           else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S
   452       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S;
   453   in term_of ty end;
   454 
   455 
   456 (* simple_ast_of *)
   457 
   458 fun simple_ast_of ctxt =
   459   let
   460     val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
   461     fun ast_of (Const (c, _)) = Ast.Constant c
   462       | ast_of (Free (x, _)) = Ast.Variable x
   463       | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
   464       | ast_of (t as _ $ _) =
   465           let val (f, args) = strip_comb t
   466           in Ast.mk_appl (ast_of f) (map ast_of args) end
   467       | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
   468       | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
   469   in ast_of end;
   470 
   471 
   472 (* sort_to_ast and typ_to_ast *)
   473 
   474 fun ast_of_termT ctxt trf tm =
   475   let
   476     val ctxt' = Config.put show_sorts false ctxt;
   477     fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
   478       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
   479       | ast_of (Const (a, _)) = trans a []
   480       | ast_of (t as _ $ _) =
   481           (case strip_comb t of
   482             (Const (a, _), args) => trans a args
   483           | (f, args) => Ast.Appl (map ast_of (f :: args)))
   484       | ast_of t = simple_ast_of ctxt t
   485     and trans a args = ast_of (trf a ctxt' dummyT args)
   486       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   487   in ast_of tm end;
   488 
   489 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
   490 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
   491 
   492 
   493 (* term_to_ast *)
   494 
   495 fun term_to_ast idents is_syntax_const ctxt trf tm =
   496   let
   497     val show_types =
   498       Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
   499       Config.get ctxt show_all_types;
   500     val show_structs = Config.get ctxt show_structs;
   501     val show_free_types = Config.get ctxt show_free_types;
   502     val show_all_types = Config.get ctxt show_all_types;
   503 
   504     val {structs, fixes} = idents;
   505 
   506     fun mark_atoms ((t as Const (c, _)) $ u) =
   507           if member (op =) Syntax.token_markers c
   508           then t $ u else mark_atoms t $ mark_atoms u
   509       | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
   510       | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
   511       | mark_atoms (t as Const (c, T)) =
   512           if is_syntax_const c then t
   513           else Const (Lexicon.mark_const c, T)
   514       | mark_atoms (t as Free (x, T)) =
   515           let val i = find_index (fn s => s = x) structs + 1 in
   516             if i = 0 andalso member (op =) fixes x then
   517               Const (Lexicon.mark_fixed x, T)
   518             else if i = 1 andalso not show_structs then
   519               Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
   520             else Lexicon.const "_free" $ t
   521           end
   522       | mark_atoms (t as Var (xi, T)) =
   523           if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
   524           else Lexicon.const "_var" $ t
   525       | mark_atoms a = a;
   526 
   527     fun prune_typs (t_seen as (Const _, _)) = t_seen
   528       | prune_typs (t as Free (x, ty), seen) =
   529           if ty = dummyT then (t, seen)
   530           else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
   531           else (t, t :: seen)
   532       | prune_typs (t as Var (xi, ty), seen) =
   533           if ty = dummyT then (t, seen)
   534           else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
   535           else (t, t :: seen)
   536       | prune_typs (t_seen as (Bound _, _)) = t_seen
   537       | prune_typs (Abs (x, ty, t), seen) =
   538           let val (t', seen') = prune_typs (t, seen);
   539           in (Abs (x, ty, t'), seen') end
   540       | prune_typs (t1 $ t2, seen) =
   541           let
   542             val (t1', seen') = prune_typs (t1, seen);
   543             val (t2', seen'') = prune_typs (t2, seen');
   544           in (t1' $ t2', seen'') end;
   545 
   546     fun ast_of tm =
   547       (case strip_comb tm of
   548         (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
   549       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   550           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
   551       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   552           Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
   553       | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
   554           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
   555       | (Const ("_idtdummy", T), ts) =>
   556           Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
   557       | (const as Const (c, T), ts) =>
   558           if show_all_types
   559           then Ast.mk_appl (constrain const T) (map ast_of ts)
   560           else trans c T ts
   561       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
   562 
   563     and trans a T args = ast_of (trf a ctxt T args)
   564       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
   565 
   566     and constrain t T =
   567       if show_types andalso T <> dummyT then
   568         Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
   569           ast_of_termT ctxt trf (term_of_typ ctxt T)]
   570       else simple_ast_of ctxt t;
   571   in
   572     tm
   573     |> Syntax_Trans.prop_tr'
   574     |> show_types ? (#1 o prune_typs o rpair [])
   575     |> mark_atoms
   576     |> ast_of
   577   end;
   578 
   579 
   580 
   581 (** unparse **)
   582 
   583 local
   584 
   585 fun free_or_skolem ctxt x =
   586   let
   587     val m =
   588       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
   589       then Markup.fixed x
   590       else Markup.hilite;
   591   in
   592     if can Name.dest_skolem x
   593     then ([m, Markup.skolem], ProofContext.revert_skolem ctxt x)
   594     else ([m, Markup.free], x)
   595   end;
   596 
   597 fun var_or_skolem s =
   598   (case Lexicon.read_variable s of
   599     SOME (x, i) =>
   600       (case try Name.dest_skolem x of
   601         NONE => (Markup.var, s)
   602       | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
   603   | NONE => (Markup.var, s));
   604 
   605 fun unparse_t t_to_ast prt_t markup ctxt t =
   606   let
   607     val syn = ProofContext.syn_of ctxt;
   608 
   609     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
   610       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
   611       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
   612       | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
   613       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
   614       | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
   615       | token_trans "_inner_string" x = SOME (Pretty.mark_str (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.tclass x], ProofContext.extern_class ctxt x),
   624           case_type = fn x => ([Markup.tycon x], ProofContext.extern_type ctxt x),
   625           case_const = fn x => ([Markup.const x], ProofContext.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 Markup.sort;
   638 val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
   639 
   640 fun unparse_term ctxt =
   641   let
   642     val thy = ProofContext.theory_of ctxt;
   643     val syn = ProofContext.syn_of ctxt;
   644     val idents = Local_Syntax.idents_of (ProofContext.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       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       Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   661   | type_prop_tr' ctxt T [t] =
   662       Lexicon.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 (Lexicon.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 (Lexicon.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', _) = ProofContext.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]] =
   688       Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
   689   | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
   690 
   691 
   692 (* setup translations *)
   693 
   694 val _ = Context.>> (Context.map_theory
   695  (Sign.add_advanced_trfuns
   696   ([("_context_const", const_ast_tr true),
   697     ("_context_xconst", const_ast_tr false)], [], [], []) #>
   698   Sign.add_advanced_trfunsT
   699    [("_type_prop", type_prop_tr'),
   700     ("\\<^const>TYPE", type_tr'),
   701     ("_type_constraint_", type_constraint_tr')]));
   702 
   703 
   704 
   705 (** install operations **)
   706 
   707 val _ = Syntax.install_operations
   708   {parse_sort = parse_sort,
   709    parse_typ = parse_typ,
   710    parse_term = parse_term false,
   711    parse_prop = parse_term true,
   712    unparse_sort = unparse_sort,
   713    unparse_typ = unparse_typ,
   714    unparse_term = unparse_term};
   715 
   716 end;