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