Changeset 16099

Timestamp:

12/03/08 15:26:22 (4 years ago)

Author:

hritcu

Message:

Updated alpha.ml (partial)

Location:

src

Files:

• cg/genalpha.ml (modified) (1 diff)
• default.config (modified) (2 diffs)
• martin-try.config (modified) (2 diffs)
• martin.config (modified) (2 diffs)
• martin2.config (modified) (1 diff)
• typechecker/alpha.ml (modified) (2 diffs)
• typechecker/ckind.ml (modified) (2 diffs)
• typechecker/compile.ml (modified) (1 diff)
• typechecker/kinding.ml (modified) (2 diffs)
• typechecker/print.ml (modified) (1 diff)
• typechecker/subtype.ml (modified) (2 diffs)
• typechecker/syntax.ml (modified) (1 diff)
• typechecker/typeterm.ml (modified) (1 diff)
• typechecker/unify.ml (modified) (1 diff)

src/cg/genalpha.ml

@@ -21 +21 @@
 let generateRule recusive (pattern,args) = 
     pattern ^ "-> " ^ 
-    if List.length args = 0 then "bf" else
-    "tupleatl [" ^ String.concat ";" (List.map (fun a -> recusive^" "^a^" bf") args) ^ "]"
+    if List.length args = 0 then "String_set.empty" else
+    "list_union [" ^ String.concat ";" (List.map (fun a -> recusive^" "^ a) args) ^ "]"
 
 let gen config str = 
     List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [
     "(*<Types>*)", (String.concat "\r\n" (List.map (fun tcons -> generateRule "free_type" (genPatternT "\t| T" tcons)) config.type_constructors));
-    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.constructors));
-    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.constructors));
-    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.destr_types));
-    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.destr_types));
+    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_term" (genPatternICA "\t| " cons)) config.constructors));
+    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_stmt" (genPatternS "\t| " cons)) config.constructors));
+    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_term" (genPatternICA "\t| " cons)) config.destr_types));
+    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_stmt" (genPatternS "\t| " cons)) config.destr_types));
     ]

src/default.config

@@ -48 +48 @@
                         -> (match get_env vk gamma' with
                         TVerKey(tstar) -> 
-                                if (intersection xy (snd (free_type tstar ([],[])))) = [] 
+                                if (intersection xy (free_type tstar)) = [] 
                                                 && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma')))) then
                                         (if not (kind_immediately tstar Kpub (ffalse::(gamma@gamma'))) then
@@ -65 +65 @@
                         -> (match get_env vm gamma' with
                         TPubEnc(tstar) -> 
-                                if intersection xy (snd(free_type tstar ([],[]))) = []
+                                if intersection xy (free_type tstar) = []
                                 && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma'))))
                                 && (not (kind_immediately tstar Kpub (ffalse::(gamma@gamma')))) then

src/martin-try.config

@@ -46 +46 @@
                         -> (match get_env vk gamma' with
                         TVerKey(tstar) -> 
-                                if (intersection xy (snd (free_type tstar ([],[])))) = [] 
+                                if (intersection xy (free_type tstar)) = [] 
                                                 && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma')))
                                                         || kind_immediately tstar Kpub (ffalse::(gamma@gamma'))) then
@@ -60 +60 @@
                         -> (match get_env vm gamma' with
                         TPubEnc(tstar) -> 
-                                if intersection xy (snd(free_type tstar ([],[]))) = []
+                                if intersection xy (free_type tstar) = []
                                 && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma'))))
                                 && (not (kind_immediately tstar Kpub (ffalse::(gamma@gamma')))) then

src/martin.config

@@ -46 +46 @@
                         -> (match get_env vk gamma' with
                         TVerKey(tstar) -> 
-                                if (intersection xy (snd (free_type tstar ([],[])))) = [] 
+                                if (intersection xy (free_type tstar)) = [] 
                                                 && (not (kind_immediately tstar Ktnt (gamma@gamma'))) then
                                         (if not (kind_immediately tstar Kpub (gamma@gamma')) then
@@ -63 +63 @@
                         -> (match get_env vm gamma' with
                         TPubEnc(tstar) -> 
-                                if intersection xy (snd(free_type tstar ([],[]))) = []
+                                if intersection xy (free_type tstar) = []
                                 && (not (kind_immediately tstar Ktnt (gamma@gamma')))
                                 && (not (kind_immediately tstar Kpub (gamma@gamma'))) then

src/martin2.config

@@ -46 +46 @@
                         -> (match get_env vk gamma' with
                         TVerKey(tstar) -> 
-                                if (intersection xy (snd (free_type tstar ([],[])))) = []
+                                if (intersection xy (free_type tstar)) = []
                                                 && (subtype_immediately (get_env vm gamma') (TSigned tstar) (gamma@gamma')) then
                                                 (Logmanager.log "Weak \"check(vm,vk) = vn\" case\n" ~loglevel:3;

src/typechecker/alpha.ml

@@ -17 +17 @@
 open Spasssyntax
 open Syntax
+
+module String_set = Set.Make (String)
 
 let used_name_list : string list ref = ref [] 
@@ -58 +60 @@
         get_fresh_name n [n]
 
-let tupleat (a, b) (c, d) = (a @ c, b @ d)
-let tupleatl l = List.fold_left tupleat ([],[]) l
 
-(*
-let rec rename_types f t = match t with
-        TCh of t' -> rename_types f t'
-        | TOk s -> rename_spass f s
-        | 
-*)
-let add_symbols_bound sl bound = List.fold_left (fun a b -> 
-        match b with
-        S_Symbol(S_Sym_Ident x) -> x :: a
-        | _ -> raise (Invalid_argument "add_symbols_bound: got a non-string in identifier list for quantifier")) bound sl
 
-let remove_from_list x f2free = List.fold_left 
-        (fun a b -> if String.compare x b = 0 then a else b :: a) [] f2free
 
-let rec free_spass c ((bound, free) as bf) = match c with
-        S_Term(_, sl, st) -> free_spass st (add_symbols_bound sl bound, free)
-        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> tupleat a (free_spass b bf)) bf sl
-        | S_Symbol(S_Sym_Ident s) -> if (List.exists (create_pred s) bound) || (s = "ok") then
+
+
+
+
+
+let slist2set sl = List.fold_left (fun a b -> 
+                match b with
+                S_Symbol(S_Sym_Ident x) -> String_set.add x a
+                | _ -> raise (Invalid_argument "slist2set: got a non-string in identifier list for quantifier")
+        ) String_set.empty sl
+
+let list2set xs = List.fold_left (fun a b -> String_set.add b a) String_set.empty xs
+
+let list_union list = List.fold_left String_set.union String_set.empty list
+
+let rec free_spass c = match c with
+        | S_Term(_, sl, st) -> String_set.diff (free_spass st) (slist2set sl)
+        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (free_spass b)) String_set.empty sl
+        | S_Symbol(S_Sym_Ident s) -> if (s = "ok") then String_set.empty else String_set.singleton s
                 (* this is a hack, but I found no cleaner way to stop ok to be considered free *)
                 (* we would need to do this for all zeroary function symbols we add to spass *)
-                bf else (bound, s :: free)
-        | S_Symbol _ -> bf
+        | S_Symbol _ -> String_set.empty
 
-and free_type ty bf = match ty with
-        TUn -> bf
-        | TPrivate -> bf
-        | TSecret -> bf
-        | TUntainted -> bf
-        | TCh ty2 -> free_type ty2 bf 
-        | TOk sp -> free_spass sp bf
-        | TPair(Ident(x), t1, t2) -> 
-                let f1 = free_type t1 bf in
-                let f2bound, f2free = free_type t2 bf in
-                tupleat f1 (x :: f2bound, remove_from_list x f2free)
-        | TZKProof(_, _, _, t1) -> free_type t1 bf
-        | TStm t1 -> free_type t1 bf
-        | TVar _ -> bf
+and free_type ty = match ty with
+        | TUn -> String_set.empty
+        | TCh t -> free_type t 
+        | TPair(x, t1, t2) ->
+                (String_set.union (free_type t1) (String_set.remove x (free_type t2)))           
+        | TZKProof(_, _, _, yts, c) ->
+                let free_ts = List.fold_left (fun a (y,t) -> String_set.union a (free_type t)) String_set.empty yts in
+                let free_c = String_set.diff (free_spass c) (list2set (List.map (fun (y,t) -> y) yts)) in (* Alternative: list2set (match List.split yts with ys, _ -> ys) *)
+                String_set.union free_ts free_c 
+        | TStm (yts, c) ->
+                let free_ts = List.fold_left (fun a (y,t) -> String_set.union a (free_type t)) String_set.empty yts in
+                let free_c = String_set.diff (free_spass c) (list2set (List.map (fun (y,t) -> y) yts)) in (* Alternative: list2set (match List.split yts with ys, _ -> ys) *)
+                String_set.union free_ts free_c
+        | TVar _ -> String_set.empty
 (*>>blindSig>>*)
-        | TBlind t1 -> free_type t1 bf
-        | TBlindSigKey t1 -> free_type t1 bf
-        | TBlindVerKey t1 -> free_type t1 bf
-        | TBlindSigned t1 -> free_type t1 bf
-        | TBlinder t1 -> free_type t1 bf
+        | TBlind t1 -> free_type t1
+        | TBlindSigKey t1 -> free_type t1
+        | TBlindVerKey t1 -> free_type t1
+        | TBlindSigned t1 -> free_type t1
+        | TBlinder t1 -> free_type t1
 (*<<blindSig<<*)
-        | TTop -> bf
+        | TTop -> String_set.empty
+        | TAnd (t1,t2) -> String_set.union (free_type t1) (free_type t2)
+        | TOr (t1,t2) -> String_set.union (free_type t1) (free_type t2)
+        | TRefine(x,t1,c) -> String_set.union (free_type t1) (String_set.remove x (free_spass c))
 (*<Types>*)
 
-and free_destr g bf = match g with
-        Fst m -> free_m' m bf
-        | Snd m -> free_m' m bf
-        | Eq (m, n) -> tupleat (free_m' m bf) (free_m' n bf)
-        | And (m, n) -> tupleat (free_m' m bf) (free_m' n bf)
-        | Or (m, n) -> tupleat (free_m' m bf) (free_m' n bf)
-        | Public(_, _, m) -> free_m' m bf
-        | Ver (_, _, _, _, m, l) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_m' m bf) l
-        | Exercise  m -> free_m' m bf
+and free_destr g = match g with
+        | Eq (m, n) -> String_set.union (free_term m) (free_term n)
+        | And (m, n) -> String_set.union (free_term m) (free_term n)
+        | Or (m, n) -> String_set.union (free_term m) (free_term n)
+        | Public(_, _, m) -> free_term m
+        | Ver (_, _, _, _, m, l) -> List.fold_left (fun a b -> String_set.union (free_term b) a) (free_term m) l
 (*>>blindSig>>*)
-        | Unblind(t, m, n, o) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_type t bf) [m; n; o]
-        | Bcheck(t, m, n) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_type t bf) [m; n]
+        | Unblind(t, m, n, o) -> List.fold_left (fun a b -> String_set.union (free_term b) a) (free_type t) [m; n; o]
+        | Bcheck(t, m, n) -> List.fold_left (fun a b -> String_set.union (free_term b) a) (free_type t) [m; n]
 (*<<blindSig<<*)
-        | Id m -> free_m' m bf
 (*<Destructors>*)
 
-and free_constr f ((bound, free) as bf) = match f with
-        Pair(m, _, n, _) -> tupleat (free_m' m bf) (free_m' n bf)
-        | Ok ty -> free_type ty bf
-        | True -> bf
-        | Zk (_, _, _, tl) -> 
-                List.fold_left (fun a b -> tupleat a (free_m' b bf)) bf tl
+and free_constr f = match f with
+        | Ok -> String_set.empty
+        | True -> String_set.empty
+        | Zk (_, _, _, tl) -> List.fold_left (fun a b -> String_set.union a (free_term b)) String_set.empty tl
 (*>>blindSig>>*)
-        | Blind(m, n) -> tupleat (free_m' m bf) (free_m' n bf)
-        | Bvk(m) -> free_m' m bf
-        | Bsign(t, m, n) -> tupleat (free_type t bf) (tupleat (free_m' m bf) (free_m' n bf))
+        | Blind(m, n) -> String_set.union (free_term m) (free_term n)
+        | Bvk(m) -> free_term m
+        | Bsign(t, m, n) -> String_set.union (free_type t) (String_set.union (free_term m) (free_term n))
 (*<<blindSig<<*)
 (*<Constructors>*)
 
-and free_m' m (bound, free) = match m with
-        Ident n -> if List.exists (create_pred n) bound then
-                (bound, free) else (bound, n :: free)
-        | F f -> free_constr f (bound, free)
+and free_term m = match m with
+        Ident n -> String_set.singleton n
+        | Pair(n, m, ot) -> (match ot with
+                | Some t -> String_set.union (String_set.union (free_term m) (free_term n)) (free_type t) 
+                | None -> String_set.union (free_term m) (free_term n))
+        | F (f, ot) -> (match ot with
+                        | Some t -> String_set.union (free_constr f) (free_type t)
+                        | None -> free_constr f)
 
-let free_m m = free_m' m ([], [])
-
-let rec free_sdestr sd bf = match sd with
-        SFst m -> free_s' m bf
-        | SSnd m -> free_s' m bf
-        | SEq (m, n) -> tupleat (free_s' m bf) (free_s' n bf)
-        | SAnd (m, n) -> tupleat (free_s' m bf) (free_s' n bf)
-        | SOr (m, n) -> tupleat (free_s' m bf) (free_s' n bf)
-        | SPublic(_, _, m) -> free_s' m bf
-        | SExercise  m -> free_s' m bf
+let rec free_sdestr sd = match sd with
+        | SEq (m, n) -> String_set.union (free_stmt m) (free_stmt n)
+        | SAnd (m, n) -> String_set.union (free_stmt m) (free_stmt n)
+        | SOr (m, n) -> String_set.union (free_stmt m) (free_stmt n)
+        | SPublic(_, _, m) -> free_stmt m
 (*>>blindSig>>*)
-        | SUnblind(m, n, o) -> List.fold_left (fun a b -> tupleat (free_s' b bf) a) ([],[]) [m; n; o]
-        | SBcheck(m, n) -> List.fold_left (fun a b -> tupleat (free_s' b bf) a) ([],[]) [m; n]
+        | SUnblind(m, n, o) -> List.fold_left (fun a b -> String_set.union (free_stmt b) a) String_set.empty [m; n; o]
+        | SBcheck(m, n) -> List.fold_left (fun a b -> String_set.union (free_stmt b) a) String_set.empty [m; n]
 (*<<blindSig<<*)
-        | SId m -> free_s' m bf
 (*<SDestructors>*)
 
-and free_sconstr sc ((bound, free) as bf) = match sc with
-        SPair(m, n) -> tupleat (free_s' m bf) (free_s' n bf)
-        | SOk -> ([], [])
-        | STrue -> bf
+and free_sconstr sc = match sc with
+        | SOk -> String_set.empty
+        | STrue -> String_set.empty
         | SZk (_, _, _, tl) -> 
-                List.fold_left (fun a b -> tupleat a (free_s' b bf)) bf tl
+                List.fold_left (fun a b -> String_set.union a (free_stmt b)) String_set.empty tl
 (*>>blindSig>>*)
-        | SBlind(m, n) -> tupleat (free_s' m bf) (free_s' n bf)
-        | SBvk(m) -> free_s' m bf
-        | SBsign(m, n) -> tupleat (free_s' m bf) (free_s' n bf)
+        | SBlind(m, n) -> String_set.union (free_stmt m) (free_stmt n)
+        | SBvk(m) -> free_stmt m
+        | SBsign(m, n) -> String_set.union (free_stmt m) (free_stmt n)
 (*<<blindSig<<*)
 (*<SConstructors>*)
 
-and free_s' s (bound, free) = match s with
-        SIdent n -> if List.exists (create_pred n) bound then
-                (bound, free) else (bound, n :: free)
-        | SAlpha _ -> (bound, free)
-        | SBeta _ -> (bound, free)
-        | SConstr sc -> free_sconstr sc (bound, free)
-        | SDestr sd -> free_sdestr sd (bound, free)
-
-let free_s s = free_s' s ([], [])
+and free_stmt s = match s with
+        | SIdent n -> String_set.singleton n
+        | SAlpha _ -> String_set.empty
+        | SBeta _ -> String_set.empty
+        | SPair(m, n) -> String_set.union (free_stmt m) (free_stmt n)
+        | SConstr sc -> free_sconstr sc
+        | SDestr sd -> free_sdestr sd

src/typechecker/ckind.ml

@@ -52 +52 @@
 and con_gen_kind_type t f typename = 
         if well_formed f &&
-        subset (kft t) (dom f) then [] else
+        String_set.subset (free_type t) (list2set (dom f)) then [] else
         raise (Invalid_argument (typename^"gamma not well-formed or free not a subset of dom gamma"))
 
 and con_gen_kind_zk_tnt t1 f =
-        if well_formed f && subset (kft t1) (dom f) then [] else
+        if well_formed f && String_set.subset (free_type t1) (list2set (dom f)) then [] else
         raise (Invalid_argument "con_gen_kind_zk_tnt: gamma not well-formed or free not a subset of dom gamma")
 
@@ -73 +73 @@
         | TZKProof(_, _, _, t1), _ -> ckind t1 l f
 (*>>blindSig>>*)
-        | TBlind t, _ -> if well_formed f && subset (kft t) (dom f) then
+        | TBlind t, _ -> if well_formed f && String_set.subset (free_type t1) (list2set (dom f)) then
                         []
                 else
                         raise (Invalid_argument "ckind: ckind-blind: gamma not well-formed or free not subset of dom gamma")
         | TBlinder t, _ -> ckind t Kpub f @ ckind t Ktnt f
-        | TBlindSigned t, _ -> if well_formed f && subset (kft t) (dom f) then
+        | TBlindSigned t, _ -> if well_formed f && String_set.subset (free_type t) (list2set (dom f)) then
                         []
                 else
                         raise (Invalid_argument "ckind: ckind-blindsigned: gamma not well-formed or free not subset of dom gamma")
-        | TBlindVerKey t, Kpub -> if well_formed f && subset (kft t) (dom f) then
+        | TBlindVerKey t, Kpub -> if well_formed f && String_set.subset (free_type t) (list2set (dom f)) then
                         []
                 else

src/typechecker/compile.ml

@@ -181 +181 @@
                 | SDestr(SEq(SIdent(vn), SDestr(SBcheck(SIdent vm, SIdent vk))))
                         -> (match get_env vk gamma' with
-                        TBlindVerKey(TPair(Ident z, TBlind t1, TOk c')) -> 
-                                let _, free = free_spass c' ([], []) in
-                                let y = get_fresh_name "y" free in
+                        TBlindVerKey(TPair(Ident z, TBlind t1, TOk c')) ->
+                                (* TODO this is probably bogus since get_fresh_name should get bound not free as the second argument *) 
+                                let y = get_fresh_name "y" (free_spass c') in
                                 if (not (kind_immediately t1 Ktnt (ffalse::(gamma @ gamma')))) && (not (kind_immediately t1 Kpub (ffalse::(gamma @ gamma')))) then
                                         List.fold_left (fun a b -> update_gamma a b) (EFormula(c) :: 

src/typechecker/kinding.ml

@@ -23 +23 @@
 open Spasssyntax
 
-(* to get rid of the let _, free = stuff... Kinding Free Types*)
-let kft t = let _, free = free_type t ([], []) in free
-
 let rec kind' t l f foo = match t, l with
         TUn, _ -> well_formed f
@@ -39 +36 @@
         | TZKProof(_, _, _, t), _ -> kind' t l f foo
 (*>>blindSig>>*)
-        | TBlind t, _ -> well_formed f && subset (kft t) (dom f)
+        | TBlind t, _ -> well_formed f && String_set.subset (free_type t) (list2set (dom f))
         | TBlinder t, _ -> kind' t Kpub f foo && kind' t Ktnt f foo
-        | TBlindSigned t, _ -> well_formed f && subset (kft t) (dom f)
-        | TBlindVerKey t, Kpub -> well_formed f && subset (kft t) (dom f)
+        | TBlindSigned t, _ -> well_formed f && String_set.subset (free_type t) (list2set (dom f))
+        | TBlindVerKey t, Kpub -> well_formed f && String_set.subset (free_type t) (list2set (dom f))
         | TBlindVerKey t, Ktnt -> kind' t Ktnt f foo
         | TBlindSigKey t, _ -> kind' t Ktnt f foo

src/typechecker/print.ml

@@ -50 +50 @@
         TUn -> Printf.bprintf b "Un"
         | TCh x -> (Printf.bprintf b "Ch("; print_type_b b x; Printf.bprintf b ")")
-        | TPair (x, t1, t2) -> (Printf.bprintf b "Pair("; print_term_b b x; Printf.bprintf b " : "; print_type_b b t1; Printf.bprintf b ", "; print_type_b b t2; Printf.bprintf b ")")
+        | TPair (x, t1, t2) -> (Printf.bprintf b "Pair(%s:" x; print_type_b b t1; Printf.bprintf b ", "; print_type_b b t2; Printf.bprintf b ")")
         | TZKProof(n,m,s,ts,c) -> (Printf.bprintf b "ZKProof(*%d,%d,%s*)(" n m s;
                 List.iter (fun (x,t) -> Printf.bprintf b "%s" (x ^ ": "); print_type_b b t; Printf.bprintf b " ") ts;

src/typechecker/subtype.ml

@@ -35 +35 @@
                                 subtype' (rename_type x fresh_name t2) (rename_type y fresh_name u2) 
                                         (EBind(fresh_name, t1) :: f) foo
-                        | TOk c1, TOk c2 -> let _, free = free_spass c1 ([], []) in
-                                if well_formed f && subset free (dom f) then
+                        | TOk c1, TOk c2 -> 
+                                if well_formed f && String_set.subset (free_spass c1) (list2set (dom f)) then
                                 (foo ((EFormula c1) :: f) c2)
                                 else false
@@ -73 +73 @@
                 | TPair(Ident(x), t1, t2), TPair(Ident(y), u1, u2) -> 
                                 (* x and y should be equal, if not rename them to be *)
-                                let _, f1 = free_type t1 ([], []) in
-                                let _, f2 = free_type t2 ([], []) in
-                                let fresh = get_fresh_name x (f1 @ f2) in
+                                let fresh = get_fresh_name x (String_set.union (free_type t1) (free_type t2)) in
                                 S_Symbol_Term (S_Or, 
                                         [S_Symbol_Term (S_And, [sub t1 u1;

src/typechecker/syntax.ml

@@ -26 +26 @@
         | TCh of types
 (*      | TOk of spass -- can be defined as syntax sugar *)
-        | TPair of term * types * types
+        | TPair of string * types * types
         | TZKProof of int * int * string * (string * types) list  * spass
         | TStm of (string * types) list * spass

src/typechecker/typeterm.ml

@@ -126 +126 @@
 (*>>blindSig>>*)
         | Unblind(TPair(_, TBlind(tvar), _), _, _, _) -> TSigned(tvar)
-        | Bcheck(TPair(Ident z, TBlind(tvar), TOk c), _, _) -> let _, free =
-                free_spass c ([], []) in
-                let x = get_fresh_name "x" free in
-                let y = get_fresh_name "y" free in
+        | Bcheck(TPair(Ident z, TBlind(tvar), TOk c), _, _) ->
+                let x = get_fresh_name "x" (free_spass c) in
+                let y = get_fresh_name "y" (free_spass c) in
                 TPair(Ident x, tvar, TOk(Spasssyntax.S_Term(Spasssyntax.S_Exists, 
                         [S_Symbol(Spasssyntax.S_Sym_Ident y)], replace_formula z (F(Blind(Ident x, Ident y))) c)))

src/typechecker/unify.ml

@@ -95 +95 @@
         | _ -> raise (Invalid_argument "make_unique: got types that are no variables")) tvarlist
 
-let rec con_gen_ok_plus f c c' = let _, free = free_spass c ([], []) in
-        if well_formed f && subset free (dom f) 
+let rec con_gen_ok_plus f c c' =
+        if well_formed f && String_set.subset (free_spass c) (list2set (dom f)) 
         then [FCons(c :: formulas f, c')]
         else raise (Invalid_argument "con_gen_ok_plus: not well_formed or not subset")
 
-and con_gen_ok_minus f c c' = let _, free = free_spass c ([], []) in
-        if well_formed f && subset free (dom f) 
+and con_gen_ok_minus f c c' =
+        if well_formed f && String_set.subset (free_spass c) (list2set (dom f)) 
         then [FCons(c' :: formulas f, c)]
         else raise (Invalid_argument "con_gen_ok_minus: not well_formed or not subset")