report sort assignment of visible type variables;
authorwenzelm
Mon Oct 01 16:37:22 2012 +0200 (2012-10-01)
changeset 49674dbadb4d03cbc
parent 49673 2a088cff1e7b
child 49675 d9c2fb37d92a
report sort assignment of visible type variables;
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/Pure/Isar/proof_context.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/term_position.ML
src/Pure/pure_thy.ML
src/Pure/term.ML
src/Pure/variable.ML
src/Tools/jEdit/src/isabelle_rendering.scala
     1.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Oct 01 12:05:05 2012 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Oct 01 16:37:22 2012 +0200
     1.3 @@ -30,11 +30,13 @@
     1.4  parse_translation {*
     1.5  let
     1.6    fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
     1.7 -  fun finite_vec_tr [t, u as Free (x, _)] =
     1.8 +  fun finite_vec_tr [t, u] =
     1.9 +    (case Term_Position.strip_positions u of
    1.10 +      v as Free (x, _) =>
    1.11          if Lexicon.is_tid x then
    1.12 -          vec t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
    1.13 +          vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax finite})
    1.14          else vec t u
    1.15 -    | finite_vec_tr [t, u] = vec t u
    1.16 +    | _ => vec t u)
    1.17  in
    1.18    [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
    1.19  end
     2.1 --- a/src/Pure/Isar/proof_context.ML	Mon Oct 01 12:05:05 2012 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Oct 01 16:37:22 2012 +0200
     2.3 @@ -70,7 +70,8 @@
     2.4    val read_arity: Proof.context -> xstring * string list * string -> arity
     2.5    val cert_arity: Proof.context -> arity -> arity
     2.6    val allow_dummies: Proof.context -> Proof.context
     2.7 -  val prepare_sorts: Proof.context -> typ list -> typ list
     2.8 +  val prepare_sortsT: Proof.context -> typ list -> string * typ list
     2.9 +  val prepare_sorts: Proof.context -> term list -> string * term list
    2.10    val check_tfree: Proof.context -> string * sort -> string * sort
    2.11    val intern_skolem: Proof.context -> string -> string option
    2.12    val read_term_pattern: Proof.context -> string -> term
    2.13 @@ -615,13 +616,15 @@
    2.14  
    2.15  (* sort constraints *)
    2.16  
    2.17 -fun prepare_sorts ctxt tys =
    2.18 +local
    2.19 +
    2.20 +fun prepare_sorts_env ctxt tys =
    2.21    let
    2.22      val tsig = tsig_of ctxt;
    2.23      val defaultS = Type.defaultS tsig;
    2.24  
    2.25      fun constraint (xi, S) env =
    2.26 -      if S = dummyS then env
    2.27 +      if S = dummyS orelse Term_Position.is_positionS S then env
    2.28        else
    2.29          Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
    2.30            handle Vartab.DUP _ =>
    2.31 @@ -644,18 +647,57 @@
    2.32              error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
    2.33                " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
    2.34                " for type variable " ^ quote (Term.string_of_vname' xi)));
    2.35 -  in
    2.36 -    (map o map_atyps)
    2.37 -      (fn T =>
    2.38 -        if Term_Position.is_positionT T then T
    2.39 -        else
    2.40 -          (case T of
    2.41 -            TFree (x, _) => TFree (x, get_sort (x, ~1))
    2.42 -          | TVar (xi, _) => TVar (xi, get_sort xi)
    2.43 -          | _ => T)) tys
    2.44 -  end;
    2.45 +
    2.46 +    fun add_report raw_S S reports =
    2.47 +      (case Term_Position.decode_positionS raw_S of
    2.48 +        SOME pos =>
    2.49 +          if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
    2.50 +            (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
    2.51 +              :: reports
    2.52 +          else reports
    2.53 +      | NONE => reports);
    2.54 +
    2.55 +    val reports =
    2.56 +      (fold o fold_atyps)
    2.57 +        (fn T =>
    2.58 +          if Term_Position.is_positionT T then I
    2.59 +          else
    2.60 +            (case T of
    2.61 +              TFree (x, raw_S) => add_report raw_S (get_sort (x, ~1))
    2.62 +            | TVar (xi, raw_S) => add_report raw_S (get_sort xi)
    2.63 +            | _ => I)) tys [];
    2.64 +
    2.65 +  in (implode (map #2 reports), get_sort) end;
    2.66  
    2.67 -fun check_tfree ctxt v = dest_TFree (singleton (prepare_sorts ctxt) (TFree v));
    2.68 +fun replace_sortsT get_sort =
    2.69 +  map_atyps
    2.70 +    (fn T =>
    2.71 +      if Term_Position.is_positionT T then T
    2.72 +      else
    2.73 +        (case T of
    2.74 +          TFree (x, _) => TFree (x, get_sort (x, ~1))
    2.75 +        | TVar (xi, _) => TVar (xi, get_sort xi)
    2.76 +        | _ => T));
    2.77 +
    2.78 +in
    2.79 +
    2.80 +fun prepare_sortsT ctxt tys =
    2.81 +  let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys
    2.82 +  in (sorting_report, map (replace_sortsT get_sort) tys) end;
    2.83 +
    2.84 +fun prepare_sorts ctxt tms =
    2.85 +  let
    2.86 +    val tys = rev ((fold o fold_types) cons tms []);
    2.87 +    val (sorting_report, get_sort) = prepare_sorts_env ctxt tys;
    2.88 +  in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end;
    2.89 +
    2.90 +fun check_tfree ctxt v =
    2.91 +  let
    2.92 +    val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
    2.93 +    val _ = Context_Position.if_visible ctxt Output.report sorting_report;
    2.94 +  in a end;
    2.95 +
    2.96 +end;
    2.97  
    2.98  
    2.99  (* certify terms *)
     3.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Mon Oct 01 12:05:05 2012 +0200
     3.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Mon Oct 01 16:37:22 2012 +0200
     3.3 @@ -48,6 +48,7 @@
     3.4    val typN: string val typ: Markup.T
     3.5    val termN: string val term: Markup.T
     3.6    val propN: string val prop: Markup.T
     3.7 +  val sortingN: string val sorting: Markup.T
     3.8    val typingN: string val typing: Markup.T
     3.9    val ML_keywordN: string val ML_keyword: Markup.T
    3.10    val ML_delimiterN: string val ML_delimiter: Markup.T
    3.11 @@ -200,6 +201,7 @@
    3.12  val (termN, term) = markup_elem "term";
    3.13  val (propN, prop) = markup_elem "prop";
    3.14  
    3.15 +val (sortingN, sorting) = markup_elem "sorting";
    3.16  val (typingN, typing) = markup_elem "typing";
    3.17  
    3.18  
     4.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Mon Oct 01 12:05:05 2012 +0200
     4.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Mon Oct 01 16:37:22 2012 +0200
     4.3 @@ -108,6 +108,7 @@
     4.4    val TERM = "term"
     4.5    val PROP = "prop"
     4.6  
     4.7 +  val SORTING = "sorting"
     4.8    val TYPING = "typing"
     4.9  
    4.10    val ATTRIBUTE = "attribute"
     5.1 --- a/src/Pure/Syntax/syntax.ML	Mon Oct 01 12:05:05 2012 +0200
     5.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Oct 01 16:37:22 2012 +0200
     5.3 @@ -539,11 +539,12 @@
     5.4    ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
     5.5  
     5.6  val basic_nonterms =
     5.7 -  (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
     5.8 +  Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
     5.9      "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
    5.10      "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
    5.11 -    "float_position", "xnum_position", "index", "struct", "id_position",
    5.12 -    "longid_position", "str_position", "type_name", "class_name"]);
    5.13 +    "float_position", "xnum_position", "index", "struct", "tid_position",
    5.14 +    "tvar_position", "id_position", "longid_position", "str_position",
    5.15 +    "type_name", "class_name"];
    5.16  
    5.17  
    5.18  
     6.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon Oct 01 12:05:05 2012 +0200
     6.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Oct 01 16:37:22 2012 +0200
     6.3 @@ -86,14 +86,16 @@
     6.4      fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
     6.5  
     6.6      fun class s = Lexicon.unmark_class s handle Fail _ => err ();
     6.7 +    fun class_pos s = if is_some (Term_Position.decode s) then s else err ();
     6.8  
     6.9      fun classes (Const (s, _)) = [class s]
    6.10        | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
    6.11        | classes _ = err ();
    6.12  
    6.13      fun sort (Const ("_topsort", _)) = []
    6.14 +      | sort (Const ("_sort", _) $ cs) = classes cs
    6.15        | sort (Const (s, _)) = [class s]
    6.16 -      | sort (Const ("_sort", _) $ cs) = classes cs
    6.17 +      | sort (Free (s, _)) = [class_pos s]
    6.18        | sort _ = err ();
    6.19    in sort tm end;
    6.20  
    6.21 @@ -138,7 +140,18 @@
    6.22          NONE => Ast.mk_appl (Ast.Constant a) args
    6.23        | SOME f => f ctxt args);
    6.24  
    6.25 -    fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    6.26 +    fun asts_of_token tok =
    6.27 +      if Lexicon.valued_token tok
    6.28 +      then [Ast.Variable (Lexicon.str_of_token tok)]
    6.29 +      else [];
    6.30 +
    6.31 +    fun asts_of_position c tok =
    6.32 +      if raw then asts_of_token tok
    6.33 +      else
    6.34 +        [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok),
    6.35 +          Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
    6.36 +
    6.37 +    and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    6.38            let
    6.39              val pos = Lexicon.pos_of_token tok;
    6.40              val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
    6.41 @@ -153,11 +166,8 @@
    6.42                  handle ERROR msg => error (msg ^ Position.here pos);
    6.43              val _ = report pos (markup_type ctxt) c;
    6.44            in [Ast.Constant (Lexicon.mark_type c)] end
    6.45 -      | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
    6.46 -          if raw then [ast_of pt]
    6.47 -          else
    6.48 -            [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
    6.49 -              Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
    6.50 +      | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
    6.51 +      | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
    6.52        | asts_of (Parser.Node (a, pts)) =
    6.53            let
    6.54              val _ = pts |> List.app
    6.55 @@ -165,10 +175,7 @@
    6.56                  if Lexicon.valued_token tok then ()
    6.57                  else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
    6.58            in [trans a (maps asts_of pts)] end
    6.59 -      | asts_of (Parser.Tip tok) =
    6.60 -          if Lexicon.valued_token tok
    6.61 -          then [Ast.Variable (Lexicon.str_of_token tok)]
    6.62 -          else []
    6.63 +      | asts_of (Parser.Tip tok) = asts_of_token tok
    6.64  
    6.65      and ast_of pt =
    6.66        (case asts_of pt of
    6.67 @@ -823,27 +830,34 @@
    6.68  
    6.69  in
    6.70  
    6.71 -fun check_typs ctxt =
    6.72 -  Proof_Context.prepare_sorts ctxt #>
    6.73 -  apply_typ_check ctxt #>
    6.74 -  Term_Sharing.typs (Proof_Context.theory_of ctxt);
    6.75 +fun check_typs ctxt raw_tys =
    6.76 +  let
    6.77 +    val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
    6.78 +    val _ = Context_Position.if_visible ctxt Output.report sorting_report;
    6.79 +  in
    6.80 +    tys
    6.81 +    |> apply_typ_check ctxt
    6.82 +    |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
    6.83 +  end;
    6.84  
    6.85  fun check_terms ctxt raw_ts =
    6.86    let
    6.87 -    val (ts, ps) = raw_ts
    6.88 -      |> Term.burrow_types (Proof_Context.prepare_sorts ctxt)
    6.89 -      |> Type_Infer_Context.prepare_positions ctxt;
    6.90 +    val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
    6.91 +    val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
    6.92 +
    6.93      val tys = map (Logic.mk_type o snd) ps;
    6.94      val (ts', tys') = ts @ tys
    6.95        |> apply_term_check ctxt
    6.96        |> chop (length ts);
    6.97 -    val _ =
    6.98 -      map2 (fn (pos, _) => fn ty =>
    6.99 +    val typing_report =
   6.100 +      fold2 (fn (pos, _) => fn ty =>
   6.101          if Position.is_reported pos then
   6.102 -          Markup.markup (Position.markup pos Isabelle_Markup.typing)
   6.103 -            (Syntax.string_of_typ ctxt (Logic.dest_type ty))
   6.104 -        else "") ps tys'
   6.105 -      |> implode |> Output.report
   6.106 +          cons (Position.reported_text pos Isabelle_Markup.typing
   6.107 +            (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
   6.108 +        else I) ps tys' []
   6.109 +      |> implode;
   6.110 +
   6.111 +    val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
   6.112    in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
   6.113  
   6.114  fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
     7.1 --- a/src/Pure/Syntax/term_position.ML	Mon Oct 01 12:05:05 2012 +0200
     7.2 +++ b/src/Pure/Syntax/term_position.ML	Mon Oct 01 16:37:22 2012 +0200
     7.3 @@ -11,8 +11,10 @@
     7.4    val decode: string -> Position.T option
     7.5    val decode_position: term -> (Position.T * typ) option
     7.6    val decode_positionT: typ -> Position.T option
     7.7 +  val decode_positionS: sort -> Position.T option
     7.8    val is_position: term -> bool
     7.9    val is_positionT: typ -> bool
    7.10 +  val is_positionS: sort -> bool
    7.11    val strip_positions: term -> term
    7.12  end;
    7.13  
    7.14 @@ -50,11 +52,15 @@
    7.15  fun decode_positionT (TFree (x, _)) = decode x
    7.16    | decode_positionT _ = NONE;
    7.17  
    7.18 +fun decode_positionS [x] = decode x
    7.19 +  | decode_positionS _ = NONE;
    7.20 +
    7.21  val is_position = is_some o decode_position;
    7.22  val is_positionT = is_some o decode_positionT;
    7.23 +val is_positionS = is_some o decode_positionS;
    7.24  
    7.25  fun strip_positions ((t as Const (c, _)) $ u $ v) =
    7.26 -      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
    7.27 +      if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
    7.28        then strip_positions u
    7.29        else t $ strip_positions u $ strip_positions v
    7.30    | strip_positions (t $ u) = strip_positions t $ strip_positions u
     8.1 --- a/src/Pure/pure_thy.ML	Mon Oct 01 12:05:05 2012 +0200
     8.2 +++ b/src/Pure/pure_thy.ML	Mon Oct 01 16:37:22 2012 +0200
     8.3 @@ -70,8 +70,8 @@
     8.4      ("",            typ "prop' => prop'",              Delimfix "'(_')"),
     8.5      ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
     8.6      ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
     8.7 -    ("",            typ "tid => type",                 Delimfix "_"),
     8.8 -    ("",            typ "tvar => type",                Delimfix "_"),
     8.9 +    ("",            typ "tid_position => type",        Delimfix "_"),
    8.10 +    ("",            typ "tvar_position => type",       Delimfix "_"),
    8.11      ("",            typ "type_name => type",           Delimfix "_"),
    8.12      ("_type_name",  typ "id => type_name",             Delimfix "_"),
    8.13      ("_type_name",  typ "longid => type_name",         Delimfix "_"),
    8.14 @@ -137,6 +137,8 @@
    8.15      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
    8.16      ("_update_name", typ "idt",                        NoSyn),
    8.17      ("_constrainAbs", typ "'a",                        NoSyn),
    8.18 +    ("_position_sort", typ "tid => tid_position",      Delimfix "_"),
    8.19 +    ("_position_sort", typ "tvar => tvar_position",    Delimfix "_"),
    8.20      ("_position",   typ "id => id_position",           Delimfix "_"),
    8.21      ("_position",   typ "longid => longid_position",   Delimfix "_"),
    8.22      ("_position",   typ "str_token => str_position",   Delimfix "_"),
     9.1 --- a/src/Pure/term.ML	Mon Oct 01 12:05:05 2012 +0200
     9.2 +++ b/src/Pure/term.ML	Mon Oct 01 16:37:22 2012 +0200
     9.3 @@ -467,7 +467,7 @@
     9.4  
     9.5  fun burrow_types f ts =
     9.6    let
     9.7 -    val Ts = rev (fold (fold_types cons) ts []);
     9.8 +    val Ts = rev ((fold o fold_types) cons ts []);
     9.9      val Ts' = f Ts;
    9.10      val (ts', []) = fold_map replace_types ts Ts';
    9.11    in ts' end;
    10.1 --- a/src/Pure/variable.ML	Mon Oct 01 12:05:05 2012 +0200
    10.2 +++ b/src/Pure/variable.ML	Mon Oct 01 16:37:22 2012 +0200
    10.3 @@ -214,7 +214,8 @@
    10.4  (* constraints *)
    10.5  
    10.6  fun constrain_tvar (xi, S) =
    10.7 -  if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);
    10.8 +  if S = dummyS orelse Term_Position.is_positionS S
    10.9 +  then Vartab.delete_safe xi else Vartab.update (xi, S);
   10.10  
   10.11  fun declare_constraints t = map_constraints (fn (types, sorts) =>
   10.12    let
    11.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Oct 01 12:05:05 2012 +0200
    11.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Oct 01 16:37:22 2012 +0200
    11.3 @@ -181,9 +181,9 @@
    11.4    private val highlight_include =
    11.5      Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
    11.6        Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
    11.7 -      Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
    11.8 -      Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
    11.9 -      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
   11.10 +      Isabelle_Markup.PATH, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.FREE,
   11.11 +      Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE,
   11.12 +      Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
   11.13  
   11.14    def highlight(range: Text.Range): Option[Text.Info[Color]] =
   11.15    {
   11.16 @@ -299,8 +299,8 @@
   11.17        Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
   11.18  
   11.19    private val tooltip_elements =
   11.20 -    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
   11.21 -      Isabelle_Markup.PATH) ++ tooltips.keys
   11.22 +    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
   11.23 +      Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
   11.24  
   11.25    private def string_of_typing(kind: String, body: XML.Body): String =
   11.26      Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
   11.27 @@ -322,7 +322,8 @@
   11.28            if Path.is_ok(name) =>
   11.29              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   11.30              add(prev, r, (true, "file " + quote(jedit_file)))
   11.31 -          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
   11.32 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   11.33 +          if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
   11.34              add(prev, r, (true, string_of_typing("::", body)))
   11.35            case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
   11.36              add(prev, r, (false, string_of_typing("ML:", body)))