Changeset 16099


Ignore:
Timestamp:
12/03/08 15:26:22 (6 years ago)
Author:
hritcu
Message:

Updated alpha.ml (partial)

Location:
src
Files:
14 edited

Legend:

Unmodified
Added
Removed
  • src/cg/genalpha.ml

    r14830 r16099  
    2121let generateRule recusive (pattern,args) =  
    2222    pattern ^ "-> " ^  
    23     if List.length args = 0 then "bf" else 
    24     "tupleatl [" ^ String.concat ";" (List.map (fun a -> recusive^" "^a^" bf") args) ^ "]" 
     23    if List.length args = 0 then "String_set.empty" else 
     24    "list_union [" ^ String.concat ";" (List.map (fun a -> recusive^" "^ a) args) ^ "]" 
    2525 
    2626let gen config str =  
    2727    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    2828    "(*<Types>*)", (String.concat "\r\n" (List.map (fun tcons -> generateRule "free_type" (genPatternT "\t| T" tcons)) config.type_constructors)); 
    29     "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.constructors)); 
    30     "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.constructors)); 
    31     "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.destr_types)); 
    32     "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.destr_types)); 
     29    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_term" (genPatternICA "\t| " cons)) config.constructors)); 
     30    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_stmt" (genPatternS "\t| " cons)) config.constructors)); 
     31    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_term" (genPatternICA "\t| " cons)) config.destr_types)); 
     32    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_stmt" (genPatternS "\t| " cons)) config.destr_types)); 
    3333    ] 
  • src/default.config

    r16094 r16099  
    4848                        -> (match get_env vk gamma' with 
    4949                        TVerKey(tstar) ->  
    50                                 if (intersection xy (snd (free_type tstar ([],[])))) = []  
     50                                if (intersection xy (free_type tstar)) = []  
    5151                                                && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma')))) then 
    5252                                        (if not (kind_immediately tstar Kpub (ffalse::(gamma@gamma'))) then 
     
    6565                        -> (match get_env vm gamma' with 
    6666                        TPubEnc(tstar) ->  
    67                                 if intersection xy (snd(free_type tstar ([],[]))) = [] 
     67                                if intersection xy (free_type tstar) = [] 
    6868                                && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma')))) 
    6969                                && (not (kind_immediately tstar Kpub (ffalse::(gamma@gamma')))) then 
  • src/martin-try.config

    r15762 r16099  
    4646                        -> (match get_env vk gamma' with 
    4747                        TVerKey(tstar) ->  
    48                                 if (intersection xy (snd (free_type tstar ([],[])))) = []  
     48                                if (intersection xy (free_type tstar)) = []  
    4949                                                && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma'))) 
    5050                                                        || kind_immediately tstar Kpub (ffalse::(gamma@gamma'))) then 
     
    6060                        -> (match get_env vm gamma' with 
    6161                        TPubEnc(tstar) ->  
    62                                 if intersection xy (snd(free_type tstar ([],[]))) = [] 
     62                                if intersection xy (free_type tstar) = [] 
    6363                                && (not (kind_immediately tstar Ktnt (ffalse::(gamma@gamma')))) 
    6464                                && (not (kind_immediately tstar Kpub (ffalse::(gamma@gamma')))) then 
  • src/martin.config

    r15762 r16099  
    4646                        -> (match get_env vk gamma' with 
    4747                        TVerKey(tstar) ->  
    48                                 if (intersection xy (snd (free_type tstar ([],[])))) = []  
     48                                if (intersection xy (free_type tstar)) = []  
    4949                                                && (not (kind_immediately tstar Ktnt (gamma@gamma'))) then 
    5050                                        (if not (kind_immediately tstar Kpub (gamma@gamma')) then 
     
    6363                        -> (match get_env vm gamma' with 
    6464                        TPubEnc(tstar) ->  
    65                                 if intersection xy (snd(free_type tstar ([],[]))) = [] 
     65                                if intersection xy (free_type tstar) = [] 
    6666                                && (not (kind_immediately tstar Ktnt (gamma@gamma'))) 
    6767                                && (not (kind_immediately tstar Kpub (gamma@gamma'))) then 
  • src/martin2.config

    r15830 r16099  
    4646                        -> (match get_env vk gamma' with 
    4747                        TVerKey(tstar) ->  
    48                                 if (intersection xy (snd (free_type tstar ([],[])))) = [] 
     48                                if (intersection xy (free_type tstar)) = [] 
    4949                                                && (subtype_immediately (get_env vm gamma') (TSigned tstar) (gamma@gamma')) then 
    5050                                                (Logmanager.log "Weak \"check(vm,vk) = vn\" case\n" ~loglevel:3; 
  • src/typechecker/alpha.ml

    r15908 r16099  
    1717open Spasssyntax 
    1818open Syntax 
     19 
     20module String_set = Set.Make (String) 
    1921 
    2022let used_name_list : string list ref = ref []  
     
    5860        get_fresh_name n [n] 
    5961 
    60 let tupleat (a, b) (c, d) = (a @ c, b @ d) 
    61 let tupleatl l = List.fold_left tupleat ([],[]) l 
    6262 
    63 (* 
    64 let rec rename_types f t = match t with 
    65         TCh of t' -> rename_types f t' 
    66         | TOk s -> rename_spass f s 
    67         |  
    68 *) 
    69 let add_symbols_bound sl bound = List.fold_left (fun a b ->  
    70         match b with 
    71         S_Symbol(S_Sym_Ident x) -> x :: a 
    72         | _ -> raise (Invalid_argument "add_symbols_bound: got a non-string in identifier list for quantifier")) bound sl 
    7363 
    74 let remove_from_list x f2free = List.fold_left  
    75         (fun a b -> if String.compare x b = 0 then a else b :: a) [] f2free 
    7664 
    77 let rec free_spass c ((bound, free) as bf) = match c with 
    78         S_Term(_, sl, st) -> free_spass st (add_symbols_bound sl bound, free) 
    79         | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> tupleat a (free_spass b bf)) bf sl 
    80         | S_Symbol(S_Sym_Ident s) -> if (List.exists (create_pred s) bound) || (s = "ok") then 
     65 
     66 
     67 
     68 
     69 
     70let slist2set sl = List.fold_left (fun a b ->  
     71                match b with 
     72                S_Symbol(S_Sym_Ident x) -> String_set.add x a 
     73                | _ -> raise (Invalid_argument "slist2set: got a non-string in identifier list for quantifier") 
     74        ) String_set.empty sl 
     75 
     76let list2set xs = List.fold_left (fun a b -> String_set.add b a) String_set.empty xs 
     77 
     78let list_union list = List.fold_left String_set.union String_set.empty list 
     79 
     80let rec free_spass c = match c with 
     81        | S_Term(_, sl, st) -> String_set.diff (free_spass st) (slist2set sl) 
     82        | S_Symbol_Term(_, sl) -> List.fold_left (fun a b -> String_set.union a (free_spass b)) String_set.empty sl 
     83        | S_Symbol(S_Sym_Ident s) -> if (s = "ok") then String_set.empty else String_set.singleton s 
    8184                (* this is a hack, but I found no cleaner way to stop ok to be considered free *) 
    8285                (* we would need to do this for all zeroary function symbols we add to spass *) 
    83                 bf else (bound, s :: free) 
    84         | S_Symbol _ -> bf 
     86        | S_Symbol _ -> String_set.empty 
    8587 
    86 and free_type ty bf = match ty with 
    87         TUn -> bf 
    88         | TPrivate -> bf 
    89         | TSecret -> bf 
    90         | TUntainted -> bf 
    91         | TCh ty2 -> free_type ty2 bf  
    92         | TOk sp -> free_spass sp bf 
    93         | TPair(Ident(x), t1, t2) ->  
    94                 let f1 = free_type t1 bf in 
    95                 let f2bound, f2free = free_type t2 bf in 
    96                 tupleat f1 (x :: f2bound, remove_from_list x f2free) 
    97         | TZKProof(_, _, _, t1) -> free_type t1 bf 
    98         | TStm t1 -> free_type t1 bf 
    99         | TVar _ -> bf 
     88and free_type ty = match ty with 
     89        | TUn -> String_set.empty 
     90        | TCh t -> free_type t  
     91        | TPair(x, t1, t2) -> 
     92                (String_set.union (free_type t1) (String_set.remove x (free_type t2)))            
     93        | TZKProof(_, _, _, yts, c) -> 
     94                let free_ts = List.fold_left (fun a (y,t) -> String_set.union a (free_type t)) String_set.empty yts in 
     95                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) *) 
     96                String_set.union free_ts free_c  
     97        | TStm (yts, c) -> 
     98                let free_ts = List.fold_left (fun a (y,t) -> String_set.union a (free_type t)) String_set.empty yts in 
     99                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) *) 
     100                String_set.union free_ts free_c 
     101        | TVar _ -> String_set.empty 
    100102(*>>blindSig>>*) 
    101         | TBlind t1 -> free_type t1 bf 
    102         | TBlindSigKey t1 -> free_type t1 bf 
    103         | TBlindVerKey t1 -> free_type t1 bf 
    104         | TBlindSigned t1 -> free_type t1 bf 
    105         | TBlinder t1 -> free_type t1 bf 
     103        | TBlind t1 -> free_type t1 
     104        | TBlindSigKey t1 -> free_type t1 
     105        | TBlindVerKey t1 -> free_type t1 
     106        | TBlindSigned t1 -> free_type t1 
     107        | TBlinder t1 -> free_type t1 
    106108(*<<blindSig<<*) 
    107         | TTop -> bf 
     109        | TTop -> String_set.empty 
     110        | TAnd (t1,t2) -> String_set.union (free_type t1) (free_type t2) 
     111        | TOr (t1,t2) -> String_set.union (free_type t1) (free_type t2) 
     112        | TRefine(x,t1,c) -> String_set.union (free_type t1) (String_set.remove x (free_spass c)) 
    108113(*<Types>*) 
    109114 
    110 and free_destr g bf = match g with 
    111         Fst m -> free_m' m bf 
    112         | Snd m -> free_m' m bf 
    113         | Eq (m, n) -> tupleat (free_m' m bf) (free_m' n bf) 
    114         | And (m, n) -> tupleat (free_m' m bf) (free_m' n bf) 
    115         | Or (m, n) -> tupleat (free_m' m bf) (free_m' n bf) 
    116         | Public(_, _, m) -> free_m' m bf 
    117         | Ver (_, _, _, _, m, l) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_m' m bf) l 
    118         | Exercise  m -> free_m' m bf 
     115and free_destr g = match g with 
     116        | Eq (m, n) -> String_set.union (free_term m) (free_term n) 
     117        | And (m, n) -> String_set.union (free_term m) (free_term n) 
     118        | Or (m, n) -> String_set.union (free_term m) (free_term n) 
     119        | Public(_, _, m) -> free_term m 
     120        | Ver (_, _, _, _, m, l) -> List.fold_left (fun a b -> String_set.union (free_term b) a) (free_term m) l 
    119121(*>>blindSig>>*) 
    120         | Unblind(t, m, n, o) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_type t bf) [m; n; o] 
    121         | Bcheck(t, m, n) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_type t bf) [m; n] 
     122        | Unblind(t, m, n, o) -> List.fold_left (fun a b -> String_set.union (free_term b) a) (free_type t) [m; n; o] 
     123        | Bcheck(t, m, n) -> List.fold_left (fun a b -> String_set.union (free_term b) a) (free_type t) [m; n] 
    122124(*<<blindSig<<*) 
    123         | Id m -> free_m' m bf 
    124125(*<Destructors>*) 
    125126 
    126 and free_constr f ((bound, free) as bf) = match f with 
    127         Pair(m, _, n, _) -> tupleat (free_m' m bf) (free_m' n bf) 
    128         | Ok ty -> free_type ty bf 
    129         | True -> bf 
    130         | Zk (_, _, _, tl) ->  
    131                 List.fold_left (fun a b -> tupleat a (free_m' b bf)) bf tl 
     127and free_constr f = match f with 
     128        | Ok -> String_set.empty 
     129        | True -> String_set.empty 
     130        | Zk (_, _, _, tl) -> List.fold_left (fun a b -> String_set.union a (free_term b)) String_set.empty tl 
    132131(*>>blindSig>>*) 
    133         | Blind(m, n) -> tupleat (free_m' m bf) (free_m' n bf) 
    134         | Bvk(m) -> free_m' m bf 
    135         | Bsign(t, m, n) -> tupleat (free_type t bf) (tupleat (free_m' m bf) (free_m' n bf)) 
     132        | Blind(m, n) -> String_set.union (free_term m) (free_term n) 
     133        | Bvk(m) -> free_term m 
     134        | Bsign(t, m, n) -> String_set.union (free_type t) (String_set.union (free_term m) (free_term n)) 
    136135(*<<blindSig<<*) 
    137136(*<Constructors>*) 
    138137 
    139 and free_m' m (bound, free) = match m with 
    140         Ident n -> if List.exists (create_pred n) bound then 
    141                 (bound, free) else (bound, n :: free) 
    142         | F f -> free_constr f (bound, free) 
     138and free_term m = match m with 
     139        Ident n -> String_set.singleton n 
     140        | Pair(n, m, ot) -> (match ot with 
     141                | Some t -> String_set.union (String_set.union (free_term m) (free_term n)) (free_type t)  
     142                | None -> String_set.union (free_term m) (free_term n)) 
     143        | F (f, ot) -> (match ot with 
     144                        | Some t -> String_set.union (free_constr f) (free_type t) 
     145                        | None -> free_constr f) 
    143146 
    144 let free_m m = free_m' m ([], []) 
    145  
    146 let rec free_sdestr sd bf = match sd with 
    147         SFst m -> free_s' m bf 
    148         | SSnd m -> free_s' m bf 
    149         | SEq (m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    150         | SAnd (m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    151         | SOr (m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    152         | SPublic(_, _, m) -> free_s' m bf 
    153         | SExercise  m -> free_s' m bf 
     147let rec free_sdestr sd = match sd with 
     148        | SEq (m, n) -> String_set.union (free_stmt m) (free_stmt n) 
     149        | SAnd (m, n) -> String_set.union (free_stmt m) (free_stmt n) 
     150        | SOr (m, n) -> String_set.union (free_stmt m) (free_stmt n) 
     151        | SPublic(_, _, m) -> free_stmt m 
    154152(*>>blindSig>>*) 
    155         | SUnblind(m, n, o) -> List.fold_left (fun a b -> tupleat (free_s' b bf) a) ([],[]) [m; n; o] 
    156         | SBcheck(m, n) -> List.fold_left (fun a b -> tupleat (free_s' b bf) a) ([],[]) [m; n] 
     153        | SUnblind(m, n, o) -> List.fold_left (fun a b -> String_set.union (free_stmt b) a) String_set.empty [m; n; o] 
     154        | SBcheck(m, n) -> List.fold_left (fun a b -> String_set.union (free_stmt b) a) String_set.empty [m; n] 
    157155(*<<blindSig<<*) 
    158         | SId m -> free_s' m bf 
    159156(*<SDestructors>*) 
    160157 
    161 and free_sconstr sc ((bound, free) as bf) = match sc with 
    162         SPair(m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    163         | SOk -> ([], []) 
    164         | STrue -> bf 
     158and free_sconstr sc = match sc with 
     159        | SOk -> String_set.empty 
     160        | STrue -> String_set.empty 
    165161        | SZk (_, _, _, tl) ->  
    166                 List.fold_left (fun a b -> tupleat a (free_s' b bf)) bf tl 
     162                List.fold_left (fun a b -> String_set.union a (free_stmt b)) String_set.empty tl 
    167163(*>>blindSig>>*) 
    168         | SBlind(m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    169         | SBvk(m) -> free_s' m bf 
    170         | SBsign(m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
     164        | SBlind(m, n) -> String_set.union (free_stmt m) (free_stmt n) 
     165        | SBvk(m) -> free_stmt m 
     166        | SBsign(m, n) -> String_set.union (free_stmt m) (free_stmt n) 
    171167(*<<blindSig<<*) 
    172168(*<SConstructors>*) 
    173169 
    174 and free_s' s (bound, free) = match s with 
    175         SIdent n -> if List.exists (create_pred n) bound then 
    176                 (bound, free) else (bound, n :: free) 
    177         | SAlpha _ -> (bound, free) 
    178         | SBeta _ -> (bound, free) 
    179         | SConstr sc -> free_sconstr sc (bound, free) 
    180         | SDestr sd -> free_sdestr sd (bound, free) 
    181  
    182 let free_s s = free_s' s ([], []) 
     170and free_stmt s = match s with 
     171        | SIdent n -> String_set.singleton n 
     172        | SAlpha _ -> String_set.empty 
     173        | SBeta _ -> String_set.empty 
     174        | SPair(m, n) -> String_set.union (free_stmt m) (free_stmt n) 
     175        | SConstr sc -> free_sconstr sc 
     176        | SDestr sd -> free_sdestr sd 
  • src/typechecker/ckind.ml

    r15908 r16099  
    5252and con_gen_kind_type t f typename =  
    5353        if well_formed f && 
    54         subset (kft t) (dom f) then [] else 
     54        String_set.subset (free_type t) (list2set (dom f)) then [] else 
    5555        raise (Invalid_argument (typename^"gamma not well-formed or free not a subset of dom gamma")) 
    5656 
    5757and con_gen_kind_zk_tnt t1 f = 
    58         if well_formed f && subset (kft t1) (dom f) then [] else 
     58        if well_formed f && String_set.subset (free_type t1) (list2set (dom f)) then [] else 
    5959        raise (Invalid_argument "con_gen_kind_zk_tnt: gamma not well-formed or free not a subset of dom gamma") 
    6060 
     
    7373        | TZKProof(_, _, _, t1), _ -> ckind t1 l f 
    7474(*>>blindSig>>*) 
    75         | TBlind t, _ -> if well_formed f && subset (kft t) (dom f) then 
     75        | TBlind t, _ -> if well_formed f && String_set.subset (free_type t1) (list2set (dom f)) then 
    7676                        [] 
    7777                else 
    7878                        raise (Invalid_argument "ckind: ckind-blind: gamma not well-formed or free not subset of dom gamma") 
    7979        | TBlinder t, _ -> ckind t Kpub f @ ckind t Ktnt f 
    80         | TBlindSigned t, _ -> if well_formed f && subset (kft t) (dom f) then 
     80        | TBlindSigned t, _ -> if well_formed f && String_set.subset (free_type t) (list2set (dom f)) then 
    8181                        [] 
    8282                else 
    8383                        raise (Invalid_argument "ckind: ckind-blindsigned: gamma not well-formed or free not subset of dom gamma") 
    84         | TBlindVerKey t, Kpub -> if well_formed f && subset (kft t) (dom f) then 
     84        | TBlindVerKey t, Kpub -> if well_formed f && String_set.subset (free_type t) (list2set (dom f)) then 
    8585                        [] 
    8686                else 
  • src/typechecker/compile.ml

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

    r16094 r16099  
    2323open Spasssyntax 
    2424 
    25 (* to get rid of the let _, free = stuff... Kinding Free Types*) 
    26 let kft t = let _, free = free_type t ([], []) in free 
    27  
    2825let rec kind' t l f foo = match t, l with 
    2926        TUn, _ -> well_formed f 
     
    3936        | TZKProof(_, _, _, t), _ -> kind' t l f foo 
    4037(*>>blindSig>>*) 
    41         | TBlind t, _ -> well_formed f && subset (kft t) (dom f) 
     38        | TBlind t, _ -> well_formed f && String_set.subset (free_type t) (list2set (dom f)) 
    4239        | TBlinder t, _ -> kind' t Kpub f foo && kind' t Ktnt f foo 
    43         | TBlindSigned t, _ -> well_formed f && subset (kft t) (dom f) 
    44         | TBlindVerKey t, Kpub -> well_formed f && subset (kft t) (dom f) 
     40        | TBlindSigned t, _ -> well_formed f && String_set.subset (free_type t) (list2set (dom f)) 
     41        | TBlindVerKey t, Kpub -> well_formed f && String_set.subset (free_type t) (list2set (dom f)) 
    4542        | TBlindVerKey t, Ktnt -> kind' t Ktnt f foo 
    4643        | TBlindSigKey t, _ -> kind' t Ktnt f foo 
  • src/typechecker/print.ml

    r16094 r16099  
    5050        TUn -> Printf.bprintf b "Un" 
    5151        | TCh x -> (Printf.bprintf b "Ch("; print_type_b b x; Printf.bprintf b ")") 
    52         | 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 ")") 
     52        | 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 ")") 
    5353        | TZKProof(n,m,s,ts,c) -> (Printf.bprintf b "ZKProof(*%d,%d,%s*)(" n m s; 
    5454                List.iter (fun (x,t) -> Printf.bprintf b "%s" (x ^ ": "); print_type_b b t; Printf.bprintf b " ") ts; 
  • src/typechecker/subtype.ml

    r16094 r16099  
    3535                                subtype' (rename_type x fresh_name t2) (rename_type y fresh_name u2)  
    3636                                        (EBind(fresh_name, t1) :: f) foo 
    37                         | TOk c1, TOk c2 -> let _, free = free_spass c1 ([], []) in 
    38                                 if well_formed f && subset free (dom f) then 
     37                        | TOk c1, TOk c2 ->  
     38                                if well_formed f && String_set.subset (free_spass c1) (list2set (dom f)) then 
    3939                                (foo ((EFormula c1) :: f) c2) 
    4040                                else false 
     
    7373                | TPair(Ident(x), t1, t2), TPair(Ident(y), u1, u2) ->  
    7474                                (* x and y should be equal, if not rename them to be *) 
    75                                 let _, f1 = free_type t1 ([], []) in 
    76                                 let _, f2 = free_type t2 ([], []) in 
    77                                 let fresh = get_fresh_name x (f1 @ f2) in 
     75                                let fresh = get_fresh_name x (String_set.union (free_type t1) (free_type t2)) in 
    7876                                S_Symbol_Term (S_Or,  
    7977                                        [S_Symbol_Term (S_And, [sub t1 u1; 
  • src/typechecker/syntax.ml

    r16094 r16099  
    2626        | TCh of types 
    2727(*      | TOk of spass -- can be defined as syntax sugar *) 
    28         | TPair of term * types * types 
     28        | TPair of string * types * types 
    2929        | TZKProof of int * int * string * (string * types) list  * spass 
    3030        | TStm of (string * types) list * spass 
  • src/typechecker/typeterm.ml

    r15908 r16099  
    126126(*>>blindSig>>*) 
    127127        | Unblind(TPair(_, TBlind(tvar), _), _, _, _) -> TSigned(tvar) 
    128         | Bcheck(TPair(Ident z, TBlind(tvar), TOk c), _, _) -> let _, free = 
    129                 free_spass c ([], []) in 
    130                 let x = get_fresh_name "x" free in 
    131                 let y = get_fresh_name "y" free in 
     128        | Bcheck(TPair(Ident z, TBlind(tvar), TOk c), _, _) -> 
     129                let x = get_fresh_name "x" (free_spass c) in 
     130                let y = get_fresh_name "y" (free_spass c) in 
    132131                TPair(Ident x, tvar, TOk(Spasssyntax.S_Term(Spasssyntax.S_Exists,  
    133132                        [S_Symbol(Spasssyntax.S_Sym_Ident y)], replace_formula z (F(Blind(Ident x, Ident y))) c))) 
  • src/typechecker/unify.ml

    r16094 r16099  
    9595        | _ -> raise (Invalid_argument "make_unique: got types that are no variables")) tvarlist 
    9696 
    97 let rec con_gen_ok_plus f c c' = let _, free = free_spass c ([], []) in 
    98         if well_formed f && subset free (dom f)  
     97let rec con_gen_ok_plus f c c' = 
     98        if well_formed f && String_set.subset (free_spass c) (list2set (dom f))  
    9999        then [FCons(c :: formulas f, c')] 
    100100        else raise (Invalid_argument "con_gen_ok_plus: not well_formed or not subset") 
    101101 
    102 and con_gen_ok_minus f c c' = let _, free = free_spass c ([], []) in 
    103         if well_formed f && subset free (dom f)  
     102and con_gen_ok_minus f c c' = 
     103        if well_formed f && String_set.subset (free_spass c) (list2set (dom f))  
    104104        then [FCons(c' :: formulas f, c)] 
    105105        else raise (Invalid_argument "con_gen_ok_minus: not well_formed or not subset") 
Note: See TracChangeset for help on using the changeset viewer.