src/Pure/type_infer_context.ML
changeset 45445 41e641a870de
parent 45429 fd58cbf8cae3
child 46873 7a73f181cbcf
     1.1 --- a/src/Pure/type_infer_context.ML	Thu Nov 10 17:47:25 2011 +0100
     1.2 +++ b/src/Pure/type_infer_context.ML	Thu Nov 10 22:32:10 2011 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  signature TYPE_INFER_CONTEXT =
     1.5  sig
     1.6    val const_sorts: bool Config.T
     1.7 +  val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
     1.8    val prepare: Proof.context -> term list -> int * term list
     1.9    val infer_types: Proof.context -> term list -> term list
    1.10  end;
    1.11 @@ -82,9 +83,7 @@
    1.12  
    1.13      fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
    1.14            let
    1.15 -            fun err () =
    1.16 -              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    1.17 -            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
    1.18 +            val A = Type.constraint_type ctxt T;
    1.19              val (A', ps_idx') = prepare_typ A ps_idx;
    1.20              val (t', ps_idx'') = prepare t ps_idx';
    1.21            in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
    1.22 @@ -115,6 +114,55 @@
    1.23    in (tm', (vparams', params', idx'')) end;
    1.24  
    1.25  
    1.26 +(* prepare_positions *)
    1.27 +
    1.28 +fun prepare_positions ctxt tms =
    1.29 +  let
    1.30 +    val visible = Context_Position.is_visible ctxt;
    1.31 +
    1.32 +    fun prepareT (Type (a, Ts)) ps_idx =
    1.33 +          let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx
    1.34 +          in (Type (a, Ts'), ps_idx') end
    1.35 +      | prepareT T (ps, idx) =
    1.36 +          (case Term_Position.decode_positionT T of
    1.37 +            SOME pos =>
    1.38 +              if visible then
    1.39 +                let val U = Type_Infer.mk_param idx []
    1.40 +                in (U, ((pos, U) :: ps, idx + 1)) end
    1.41 +              else (dummyT, (ps, idx))
    1.42 +          | NONE => (T, (ps, idx)));
    1.43 +
    1.44 +    fun prepare (Const ("_type_constraint_", T)) ps_idx =
    1.45 +          let
    1.46 +            val A = Type.constraint_type ctxt T;
    1.47 +            val (A', ps_idx') = prepareT A ps_idx;
    1.48 +          in (Const ("_type_constraint_", A' --> A'), ps_idx') end
    1.49 +      | prepare (Const (c, T)) ps_idx =
    1.50 +          let val (T', ps_idx') = prepareT T ps_idx
    1.51 +          in (Const (c, T'), ps_idx') end
    1.52 +      | prepare (Free (x, T)) ps_idx =
    1.53 +          let val (T', ps_idx') = prepareT T ps_idx
    1.54 +          in (Free (x, T'), ps_idx') end
    1.55 +      | prepare (Var (xi, T)) ps_idx =
    1.56 +          let val (T', ps_idx') = prepareT T ps_idx
    1.57 +          in (Var (xi, T'), ps_idx') end
    1.58 +      | prepare (t as Bound _) ps_idx = (t, ps_idx)
    1.59 +      | prepare (Abs (x, T, t)) ps_idx =
    1.60 +          let
    1.61 +            val (T', ps_idx') = prepareT T ps_idx;
    1.62 +            val (t', ps_idx'') = prepare t ps_idx';
    1.63 +          in (Abs (x, T', t'), ps_idx'') end
    1.64 +      | prepare (t $ u) ps_idx =
    1.65 +          let
    1.66 +            val (t', ps_idx') = prepare t ps_idx;
    1.67 +            val (u', ps_idx'') = prepare u ps_idx';
    1.68 +          in (t' $ u', ps_idx'') end;
    1.69 +
    1.70 +    val idx = Type_Infer.param_maxidx_of tms + 1;
    1.71 +    val (tms', (ps, _)) = fold_map prepare tms ([], idx);
    1.72 +  in (tms', ps) end;
    1.73 +
    1.74 +
    1.75  
    1.76  (** order-sorted unification of types **)
    1.77