--- a/src/Pure/logic.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/logic.ML Mon Jul 29 11:09:37 2019 +0200
@@ -56,11 +56,13 @@
val mk_arities: arity -> term list
val mk_arity: string * sort list * class -> term
val dest_arity: term -> string * sort list * class
- val unconstrainT: sort list -> term ->
- {atyp_map: typ -> typ,
+ type unconstrain_context =
+ {present_map: (typ * typ) list,
+ extra_map: (sort * typ) list,
+ atyp_map: typ -> typ,
constraints: ((typ * class) * term) list,
- outer_constraints: (typ * class) list,
- prop: term}
+ outer_constraints: (typ * class) list};
+ val unconstrainT: sort list -> term -> unconstrain_context * term
val protectC: term
val protect: term -> term
val unprotect: term -> term
@@ -342,6 +344,13 @@
(* internalized sort constraints *)
+type unconstrain_context =
+ {present_map: (typ * typ) list,
+ extra_map: (sort * typ) list,
+ atyp_map: typ -> typ,
+ constraints: ((typ * class) * term) list,
+ outer_constraints: (typ * class) list};
+
fun unconstrainT shyps prop =
let
val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
@@ -352,37 +361,37 @@
val present_map =
map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
- val constraints_map =
- map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
+ val extra_map =
map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
fun atyp_map T =
(case AList.lookup (op =) present_map T of
SOME U => U
| NONE =>
- (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
+ (case AList.lookup (op =) extra_map (Type.sort_of_atyp T) of
SOME U => U
| NONE => raise TYPE ("Dangling type variable", [T], [])));
+ val constraints_map =
+ map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ extra_map;
val constraints =
- maps (fn (_, T as TVar (ai, S)) =>
- map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
- constraints_map;
+ constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
+ map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
val outer_constraints =
maps (fn (T, S) => map (pair T) S)
(present @ map (fn S => (TFree ("'dummy", S), S)) extra);
- val prop' =
- prop
+ val context =
+ {present_map = present_map,
+ extra_map = extra_map,
+ atyp_map = atyp_map,
+ constraints = constraints,
+ outer_constraints = outer_constraints};
+ val prop' = prop
|> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
|> curry list_implies (map snd constraints);
- in
- {atyp_map = atyp_map,
- constraints = constraints,
- outer_constraints = outer_constraints,
- prop = prop'}
- end;
+ in (context, prop') end;