src/Pure/logic.ML
changeset 36767 d0095729e1f1
parent 35854 d452abc96459
child 36768 46be86127972
     1.1 --- a/src/Pure/logic.ML	Sun May 09 13:46:00 2010 +0200
     1.2 +++ b/src/Pure/logic.ML	Sun May 09 18:09:30 2010 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4    val name_arity: string * sort list * class -> string
     1.5    val mk_arities: arity -> term list
     1.6    val dest_arity: term -> string * sort list * class
     1.7 +  val unconstrain_allTs: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
     1.8    val protectC: term
     1.9    val protect: term -> term
    1.10    val unprotect: term -> term
    1.11 @@ -269,6 +270,42 @@
    1.12    in (t, Ss, c) end;
    1.13  
    1.14  
    1.15 +(* internalized sort constraints *)
    1.16 +
    1.17 +fun unconstrain_allTs shyps prop =
    1.18 +  let
    1.19 +    val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
    1.20 +    val extra = fold (Sorts.remove_sort o #2) present shyps;
    1.21 +
    1.22 +    val n = length present;
    1.23 +    val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
    1.24 +
    1.25 +    val present_map =
    1.26 +      map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
    1.27 +    val constraints_map =
    1.28 +      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
    1.29 +      map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
    1.30 +
    1.31 +    fun atyp_map T =
    1.32 +      (case AList.lookup (op =) present_map T of
    1.33 +        SOME U => U
    1.34 +      | NONE =>
    1.35 +          (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
    1.36 +            SOME U => U
    1.37 +          | NONE => raise TYPE ("Dangling type variable", [T], [])));
    1.38 +
    1.39 +    val constraints =
    1.40 +      maps (fn (_, T as TVar (ai, S)) =>
    1.41 +        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
    1.42 +        constraints_map;
    1.43 +
    1.44 +    val prop' =
    1.45 +      prop
    1.46 +      |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
    1.47 +      |> curry list_implies (map snd constraints);
    1.48 +  in ((atyp_map, constraints), prop') end;
    1.49 +
    1.50 +
    1.51  
    1.52  (** protected propositions and embedded terms **)
    1.53