pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
authorwenzelm
Thu Nov 10 22:32:10 2011 +0100 (2011-11-10)
changeset 4544541e641a870de
parent 45444 ac069060e08a
child 45446 d29d73117b73
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/term_position.ML
src/Pure/type.ML
src/Pure/type_infer_context.ML
src/Tools/jEdit/src/isabelle_markup.scala
     1.1 --- a/src/Pure/General/markup.ML	Thu Nov 10 17:47:25 2011 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Thu Nov 10 22:32:10 2011 +0100
     1.3 @@ -56,6 +56,7 @@
     1.4    val typN: string val typ: T
     1.5    val termN: string val term: T
     1.6    val propN: string val prop: T
     1.7 +  val typingN: string val typing: T
     1.8    val ML_keywordN: string val ML_keyword: T
     1.9    val ML_delimiterN: string val ML_delimiter: T
    1.10    val ML_tvarN: string val ML_tvar: T
    1.11 @@ -250,6 +251,8 @@
    1.12  val (termN, term) = markup_elem "term";
    1.13  val (propN, prop) = markup_elem "prop";
    1.14  
    1.15 +val (typingN, typing) = markup_elem "typing";
    1.16 +
    1.17  
    1.18  (* ML syntax *)
    1.19  
     2.1 --- a/src/Pure/General/markup.scala	Thu Nov 10 17:47:25 2011 +0100
     2.2 +++ b/src/Pure/General/markup.scala	Thu Nov 10 22:32:10 2011 +0100
     2.3 @@ -123,6 +123,8 @@
     2.4    val TERM = "term"
     2.5    val PROP = "prop"
     2.6  
     2.7 +  val TYPING = "typing"
     2.8 +
     2.9    val ATTRIBUTE = "attribute"
    2.10    val METHOD = "method"
    2.11  
     3.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 17:47:25 2011 +0100
     3.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 22:32:10 2011 +0100
     3.3 @@ -213,11 +213,11 @@
     3.4  
     3.5          fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
     3.6                (case Term_Position.decode_position typ of
     3.7 -                SOME p => decode (p :: ps) qs bs t
     3.8 +                SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
     3.9                | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
    3.10            | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
    3.11                (case Term_Position.decode_position typ of
    3.12 -                SOME q => decode ps (q :: qs) bs t
    3.13 +                SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
    3.14                | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
    3.15            | decode _ qs bs (Abs (x, T, t)) =
    3.16                let
    3.17 @@ -794,7 +794,7 @@
    3.18  val apply_typ_uncheck = check fst true;
    3.19  val apply_term_uncheck = check snd true;
    3.20  
    3.21 -fun prepare_types ctxt tys =
    3.22 +fun prepare_sorts ctxt tys =
    3.23    let
    3.24      fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
    3.25      val env =
    3.26 @@ -813,14 +813,26 @@
    3.27  in
    3.28  
    3.29  fun check_typs ctxt =
    3.30 -  prepare_types ctxt #>
    3.31 +  prepare_sorts ctxt #>
    3.32    apply_typ_check ctxt #>
    3.33    Term_Sharing.typs (Proof_Context.theory_of ctxt);
    3.34  
    3.35 -fun check_terms ctxt =
    3.36 -  Term.burrow_types (prepare_types ctxt) #>
    3.37 -  apply_term_check ctxt #>
    3.38 -  Term_Sharing.terms (Proof_Context.theory_of ctxt);
    3.39 +fun check_terms ctxt raw_ts =
    3.40 +  let
    3.41 +    val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts;
    3.42 +    val tys = map (Logic.mk_type o snd) ps;
    3.43 +    val (ts', tys') =
    3.44 +      Term.burrow_types (prepare_sorts ctxt) ts @ tys
    3.45 +      |> apply_term_check ctxt
    3.46 +      |> chop (length ts);
    3.47 +    val _ =
    3.48 +      map2 (fn (pos, _) => fn ty =>
    3.49 +        if Position.is_reported pos then
    3.50 +          Markup.markup (Position.markup pos Markup.typing)
    3.51 +            (Syntax.string_of_typ ctxt (Logic.dest_type ty))
    3.52 +        else "") ps tys'
    3.53 +      |> implode |> Output.report
    3.54 +  in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
    3.55  
    3.56  fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
    3.57  
     4.1 --- a/src/Pure/Syntax/term_position.ML	Thu Nov 10 17:47:25 2011 +0100
     4.2 +++ b/src/Pure/Syntax/term_position.ML	Thu Nov 10 22:32:10 2011 +0100
     4.3 @@ -9,7 +9,8 @@
     4.4    val pretty: Position.T -> Pretty.T
     4.5    val encode: Position.T -> string
     4.6    val decode: string -> Position.T option
     4.7 -  val decode_position: term -> Position.T option
     4.8 +  val decode_position: term -> (Position.T * typ) option
     4.9 +  val decode_positionT: typ -> Position.T option
    4.10    val is_position: term -> bool
    4.11    val strip_positions: term -> term
    4.12  end;
    4.13 @@ -39,9 +40,15 @@
    4.14  
    4.15  (* positions within parse trees *)
    4.16  
    4.17 -fun decode_position (Free (x, _)) = decode x
    4.18 +fun decode_position (Free (x, _)) =
    4.19 +      (case decode x of
    4.20 +        SOME pos => SOME (pos, TFree (x, dummyS))
    4.21 +      | NONE => NONE)
    4.22    | decode_position _ = NONE;
    4.23  
    4.24 +fun decode_positionT (TFree (x, _)) = decode x
    4.25 +  | decode_positionT _ = NONE;
    4.26 +
    4.27  val is_position = is_some o decode_position;
    4.28  
    4.29  fun strip_positions ((t as Const (c, _)) $ u $ v) =
     5.1 --- a/src/Pure/type.ML	Thu Nov 10 17:47:25 2011 +0100
     5.2 +++ b/src/Pure/type.ML	Thu Nov 10 22:32:10 2011 +0100
     5.3 @@ -10,6 +10,7 @@
     5.4    (*constraints*)
     5.5    val mark_polymorphic: typ -> typ
     5.6    val constraint: typ -> term -> term
     5.7 +  val constraint_type: Proof.context -> typ -> typ
     5.8    val strip_constraints: term -> term
     5.9    val appl_error: Proof.context -> term -> typ -> term -> typ -> string
    5.10    (*type signatures and certified types*)
    5.11 @@ -110,6 +111,10 @@
    5.12    if T = dummyT then t
    5.13    else Const ("_type_constraint_", T --> T) $ t;
    5.14  
    5.15 +fun constraint_type ctxt T =
    5.16 +  let fun err () = error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    5.17 +  in (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()) end;
    5.18 +
    5.19  fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t
    5.20    | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u
    5.21    | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
     6.1 --- a/src/Pure/type_infer_context.ML	Thu Nov 10 17:47:25 2011 +0100
     6.2 +++ b/src/Pure/type_infer_context.ML	Thu Nov 10 22:32:10 2011 +0100
     6.3 @@ -7,6 +7,7 @@
     6.4  signature TYPE_INFER_CONTEXT =
     6.5  sig
     6.6    val const_sorts: bool Config.T
     6.7 +  val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
     6.8    val prepare: Proof.context -> term list -> int * term list
     6.9    val infer_types: Proof.context -> term list -> term list
    6.10  end;
    6.11 @@ -82,9 +83,7 @@
    6.12  
    6.13      fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
    6.14            let
    6.15 -            fun err () =
    6.16 -              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    6.17 -            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
    6.18 +            val A = Type.constraint_type ctxt T;
    6.19              val (A', ps_idx') = prepare_typ A ps_idx;
    6.20              val (t', ps_idx'') = prepare t ps_idx';
    6.21            in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
    6.22 @@ -115,6 +114,55 @@
    6.23    in (tm', (vparams', params', idx'')) end;
    6.24  
    6.25  
    6.26 +(* prepare_positions *)
    6.27 +
    6.28 +fun prepare_positions ctxt tms =
    6.29 +  let
    6.30 +    val visible = Context_Position.is_visible ctxt;
    6.31 +
    6.32 +    fun prepareT (Type (a, Ts)) ps_idx =
    6.33 +          let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx
    6.34 +          in (Type (a, Ts'), ps_idx') end
    6.35 +      | prepareT T (ps, idx) =
    6.36 +          (case Term_Position.decode_positionT T of
    6.37 +            SOME pos =>
    6.38 +              if visible then
    6.39 +                let val U = Type_Infer.mk_param idx []
    6.40 +                in (U, ((pos, U) :: ps, idx + 1)) end
    6.41 +              else (dummyT, (ps, idx))
    6.42 +          | NONE => (T, (ps, idx)));
    6.43 +
    6.44 +    fun prepare (Const ("_type_constraint_", T)) ps_idx =
    6.45 +          let
    6.46 +            val A = Type.constraint_type ctxt T;
    6.47 +            val (A', ps_idx') = prepareT A ps_idx;
    6.48 +          in (Const ("_type_constraint_", A' --> A'), ps_idx') end
    6.49 +      | prepare (Const (c, T)) ps_idx =
    6.50 +          let val (T', ps_idx') = prepareT T ps_idx
    6.51 +          in (Const (c, T'), ps_idx') end
    6.52 +      | prepare (Free (x, T)) ps_idx =
    6.53 +          let val (T', ps_idx') = prepareT T ps_idx
    6.54 +          in (Free (x, T'), ps_idx') end
    6.55 +      | prepare (Var (xi, T)) ps_idx =
    6.56 +          let val (T', ps_idx') = prepareT T ps_idx
    6.57 +          in (Var (xi, T'), ps_idx') end
    6.58 +      | prepare (t as Bound _) ps_idx = (t, ps_idx)
    6.59 +      | prepare (Abs (x, T, t)) ps_idx =
    6.60 +          let
    6.61 +            val (T', ps_idx') = prepareT T ps_idx;
    6.62 +            val (t', ps_idx'') = prepare t ps_idx';
    6.63 +          in (Abs (x, T', t'), ps_idx'') end
    6.64 +      | prepare (t $ u) ps_idx =
    6.65 +          let
    6.66 +            val (t', ps_idx') = prepare t ps_idx;
    6.67 +            val (u', ps_idx'') = prepare u ps_idx';
    6.68 +          in (t' $ u', ps_idx'') end;
    6.69 +
    6.70 +    val idx = Type_Infer.param_maxidx_of tms + 1;
    6.71 +    val (tms', (ps, _)) = fold_map prepare tms ([], idx);
    6.72 +  in (tms', ps) end;
    6.73 +
    6.74 +
    6.75  
    6.76  (** order-sorted unification of types **)
    6.77  
     7.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Nov 10 17:47:25 2011 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Thu Nov 10 22:32:10 2011 +0100
     7.3 @@ -179,12 +179,15 @@
     7.4        Markup.ML_SOURCE -> "ML source",
     7.5        Markup.DOC_SOURCE -> "document source")
     7.6  
     7.7 +  private def string_of_typing(kind: String, body: XML.Body): String =
     7.8 +    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
     7.9 +      margin = Isabelle.Int_Property("tooltip-margin"))
    7.10 +
    7.11    val tooltip: Markup_Tree.Select[String] =
    7.12    {
    7.13      case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
    7.14 -    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    7.15 -      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
    7.16 -        margin = Isabelle.Int_Property("tooltip-margin"))
    7.17 +    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
    7.18 +    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
    7.19      case Text.Info(_, XML.Elem(Markup(name, _), _))
    7.20      if tooltips.isDefinedAt(name) => tooltips(name)
    7.21    }