From 3c3b96e877dcb121d17da282dc4ca0caadda72b2 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 19 Jun 2014 17:53:33 +0200 Subject: Very buggy disjunction domain ! --- abstract/abs_domain.ml | 308 ++++++++++++++++++++++++++++++++++++++++++-- abstract/abs_interp.ml | 37 ++---- abstract/formula_printer.ml | 2 +- abstract/nonrelational.ml | 2 +- abstract/transform.ml | 63 +++++++-- frontend/ast_util.ml | 1 - frontend/typing.ml | 71 ++++++---- libs/util.ml | 6 + 8 files changed, 418 insertions(+), 72 deletions(-) diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index a7f5455..a30713a 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -4,6 +4,11 @@ open Num_domain open Typing open Util +type disjunct_policy = + | DAlways + | DNever + | DSometimes + module type ENVIRONMENT_DOMAIN = sig type t type itv @@ -21,6 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig val forgetvar : t -> id -> t val var_itv : t -> id -> itv + val set_disjunct : t -> id -> disjunct_policy -> t (* set_theoretic operations *) val join : t -> t -> t (* union *) @@ -33,7 +39,7 @@ module type ENVIRONMENT_DOMAIN = sig (* abstract operations *) val apply_f : t -> bool_expr -> t val apply_cl : t -> conslist -> t - val assign : t -> (id * num_expr) list -> t + val assign : t -> (id * id) list -> t (* pretty-printing *) val print_vars : Format.formatter -> t -> id list -> unit @@ -42,19 +48,13 @@ module type ENVIRONMENT_DOMAIN = sig end -module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct - - type enum_valuation = (string * string) list - - module VMapKey = struct - type t = enum_valuation VarMap.t - let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b)) - end - module VMap = Mapext.Make(VMapKey) +module D_ignore_enum (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = +struct type t = ND.t type itv = ND.itv + let init = ND.init let bottom = ND.bottom let vbottom = ND.vbottom @@ -66,6 +66,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let forgetvar = ND.forgetvar let var_itv = ND.var_itv + let set_disjunct x _ _ = x let join = ND.join let meet = ND.meet @@ -88,10 +89,295 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let apply_f x f = apply_cl x (conslist_of_f f) - let assign = ND.assign + let assign x v = ND.assign x (List.map (fun (id, id2) -> id, NIdent id2) v) let print_vars = ND.print_vars let print_all = ND.print_all let print_itv = ND.print_itv +end + +module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct + + module Valuation = struct + type t = string VarMap.t + let compare = VarMap.compare Pervasives.compare + + let subset a b = + VarMap.for_all + (fun id v -> + try v = VarMap.find id b + with Not_found -> true) + a + + let print fmt x = + let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x) in + let s = List.sort Pervasives.compare b in + let rec bl = function + | [] -> [] + | (v, id)::q -> + begin match bl q with + | (vv, ids)::q when vv = v -> (v, id::ids)::q + | r -> (v, [id])::r + end + in + let sbl = bl s in + Format.fprintf fmt "@[{ "; + List.iteri + (fun j (v, ids) -> + if j > 0 then Format.fprintf fmt "@ "; + Format.fprintf fmt "@["; + List.iteri + (fun i id -> + if i > 0 then Format.fprintf fmt ",@ "; + Format.fprintf fmt "%a" Formula_printer.print_id id) + ids; + Format.fprintf fmt " = %s@]" v) + sbl; + Format.fprintf fmt " }@]" + + end + module VMap = Mapext.Make(Valuation) + + type t = { + nvars : (id * bool) list; + evars : (id * string list) list; + nd_init : ND.t; + nd_bottom : ND.t; + value : ND.t VMap.t; + disj_v : id list; + nodisj_v : id list; + } + type itv = + | IN of ND.itv VMap.t + | IE of SSet.t + + + let init = { + nvars = []; evars = []; disj_v = []; nodisj_v = []; + nd_init = ND.init; + nd_bottom = ND.bottom; + value = VMap.singleton VarMap.empty ND.init; + } + let bottom = { + nvars = []; evars = []; disj_v = []; nodisj_v = []; + nd_init = ND.init; + nd_bottom = ND.bottom; + value = VMap.empty; + } + let vbottom x = { x with value = VMap.empty } + + let is_bot x = VMap.is_empty x.value || VMap.for_all (fun _ v -> ND.is_bot v) x.value + + let strict value = + VMap.filter (fun _ v -> not (ND.is_bot v)) value + + let add_case x (enum, num) = + let value = x.value in + let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in + let v = + if VMap.exists (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) value || ND.is_bot num then + value + else + try VMap.add enum (ND.join num (VMap.find enum value)) value + with Not_found -> VMap.add enum num value + in { x with value = v } + + let addvar x id ty = match ty with + | TInt | TReal -> + let is_real = (ty = TReal) in + { x with + nvars = (id, is_real)::(x.nvars); + nd_init = ND.addvar x.nd_init id is_real; + nd_bottom = ND.addvar x.nd_bottom id is_real; + value = VMap.map (fun v -> ND.addvar v id is_real) x.value + } + | TEnum options -> + { x with + evars = (id, options)::x.evars + } + + let vars x = + List.map (fun (id, r) -> id, if r then TReal else TInt) x.nvars @ + List.map (fun (id, o) -> id, TEnum o) x.evars + + let forgetvar x id = + if List.mem_assoc id x.evars then + VMap.fold + (fun enum num value -> + let enum' = VarMap.remove id enum in + add_case value (enum', num)) + x.value + { x with value = VMap.empty } + else + { x with value = strict @@ VMap.map (fun v -> ND.forgetvar v id) x.value } + + let rmvar x id = + if List.mem_assoc id x.evars then + let y = forgetvar x id in + { y with + evars = List.remove_assoc id x.evars } + else + { x with + nvars = List.remove_assoc id x.nvars; + value = strict @@ VMap.map (fun v -> ND.rmvar v id) x.value } + + let var_itv x id = + if List.mem_assoc id x.nvars + then IN (VMap.map (fun v -> ND.var_itv v id) x.value) + else not_implemented "var_itv for enum variable" + + let set_disjunct x id p = + { x with + disj_v = (if p = DAlways then id::x.disj_v + else List.filter ((<>) id) x.disj_v); + nodisj_v = (if p = DNever then id::x.nodisj_v + else List.filter ((<>) id) x.nodisj_v); + } + + let join x y = + VMap.fold + (fun enum num value -> add_case value (enum, num)) + x.value + y + let meet x y = not_implemented "meet for enum+num domain" + let widen x y = + { x with + value = VMap.merge + (fun _ a b -> match a, b with + | None, Some a -> Some a + | Some a, None -> Some a + | Some a, Some b -> Some (ND.widen a b) + | _ -> assert false) + x.value y.value } + + (* Some cases of subset/equality not detected *) + let subset a b = + VMap.for_all + (fun enum num -> + VMap.exists + (fun enum_b num_b -> + Valuation.subset enum enum_b && ND.subset num num_b) + b.value) + a.value + let eq a b = subset a b && subset b a + + (* Constraints ! *) + let apply_ec x (op, a, b) = + VMap.fold + (fun enum num value -> + match a, b with + | EItem x, EItem y -> + if (x = y && op = E_EQ) || (x <> y && op = E_NE) + then add_case value (enum, num) + else value + | EItem u, EIdent i | EIdent i, EItem u -> + begin try let y = VarMap.find i enum in + if (u = y && op = E_EQ) || (u <> y && op = E_NE) + then add_case value (enum, num) + else value + with Not_found -> + if op = E_EQ + then add_case value (VarMap.add i u enum, num) + else (* MAKE A DISJUNCTION *) + List.fold_left + (fun value item -> + add_case value (VarMap.add i item enum, num)) + value + (List.filter ((<>) u) (List.assoc i x.evars)) + end + | EIdent i, EIdent j -> + begin + try let x = VarMap.find i enum in + try let y = VarMap.find j enum in + if (x = y && op = E_EQ) || (x <> y && op = E_NE) + then add_case value (enum, num) + else value + with Not_found (* J not found *) -> + add_case value (VarMap.add j x enum, num) + with Not_found (* I not found *) -> + try let y = VarMap.find j enum in + add_case value (VarMap.add i y enum, num) + with Not_found (* J not found *) -> + if op = E_EQ + then (* MAKE A DISJUNCTION ! *) + List.fold_left + (fun value item -> + let enum = VarMap.add i item enum in + let enum = VarMap.add j item enum in + add_case value (enum, num)) + value + (List.assoc i x.evars) + else + add_case value (enum, num) + end) + x.value + { x with value = VMap.empty } + + let apply_ecl x cons = + let f x = List.fold_left apply_ec x cons in + fix eq f x + + + let apply_ncl x econs = + { x with value = strict @@ VMap.map (fun x -> ND.apply_ncl x econs) x.value } + + let rec apply_cl x (econs, ncons, rest) = match rest with + | CLTrue -> + let y = apply_ecl x econs in + let z = apply_ncl y ncons in + z + | CLFalse -> vbottom x + | CLAnd(a, b) -> + let y = apply_cl x (econs, ncons, a) in + apply_cl y (econs, ncons, b) + | CLOr((eca, ca, ra), (ecb, cb, rb)) -> + let y = apply_cl x (econs@eca, ncons@ca, ra) in + let z = apply_cl x (econs@ecb, ncons@cb, rb) in + join y z + + let apply_f x f = apply_cl x (conslist_of_f f) + + let assign x e = + let ee, ne = List.partition (fun (id, id2) -> List.mem_assoc id x.evars) e in + let ne_e = List.map (fun (id, id2) -> id, NIdent id2) ne in + + VMap.fold + (fun enum0 num value -> + let enum = List.fold_left + (fun enum (id, id2) -> + try let y = VarMap.find id2 enum0 in + VarMap.add id y enum + with Not_found -> + VarMap.remove id enum) + enum0 ee + in + add_case value (enum, ND.assign num ne_e)) + x.value + { x with value = VMap.empty } + + let print_all fmt x = + Format.fprintf fmt "@["; + VMap.iter + (fun enum num -> + Format.fprintf fmt "@[{ %a ∧@ %a }@]@ " + Valuation.print enum ND.print_all num) + x.value; + Format.fprintf fmt "@]" + + let print_vars fmt x idl = print_all fmt x (* TODO *) + + let print_itv fmt = function + | IN x -> + Format.fprintf fmt "@["; + VMap.iter + (fun enum i -> + Format.fprintf fmt "%a when %a@ " + ND.print_itv i Valuation.print enum) + x; + Format.fprintf fmt "@]" + | IE x -> + Format.fprintf fmt "@[{ "; + SSet.iter (fun x -> Format.fprintf fmt "%s@ " x) x; + Format.fprintf fmt "}@]" end diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 7950144..7a53134 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -52,6 +52,7 @@ end = struct guarantees; Format.printf "@."; + let env = E.set_disjunct env "/exit" DNever in let env = E.apply_f env init_f in let cl = Formula.conslist_of_f f in @@ -72,7 +73,7 @@ end = struct let tr_assigns = List.fold_left (fun q (_, id, _) -> if id.[0] = 'N' then - (String.sub id 1 (String.length id - 1), NIdent id)::q + (String.sub id 1 (String.length id - 1), id)::q else q) [] vars @@ -95,14 +96,10 @@ end = struct (* loop : st -> env -> env -> env *) - let loop st pnew stay = + let loop st acc0 = - Format.printf "Loop @[%a@]@.New @[%a@]@.Stay @[%a@]@." - Formula_printer.print_conslist st.cl - E.print_all pnew E.print_all stay; - - let add_stay = cycle st st.cl pnew in - let acc0 = E.join stay add_stay in + Format.printf "Loop @[%a@]@.@." + Formula_printer.print_conslist st.cl; let fsharp cl i = Format.printf "Acc @[%a@]@." E.print_all i; @@ -121,7 +118,7 @@ end = struct let x = iter 0 acc0 in let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *) - let z = E.apply_cl y st.cl in + let z = E.apply_cl y st.cl in (* no more guarantee *) y, z (* @@ -130,20 +127,14 @@ end = struct let do_prog widen_delay rp = let st = init_state widen_delay rp in - let pnew = st.env in - let pnew_c = E.apply_cl pnew st.cl in - - let stay, stay_c = loop st pnew (E.vbottom pnew) in - - Format.printf "@.@[New %a@]@.@." - E.print_all pnew_c; - Format.printf "@[Stay %a@]@.@." - E.print_all stay_c; - - let final = E.join pnew_c stay_c in + let final, final_c = loop st st.env in - Format.printf "@[Final %a@]@.@." + Format.printf "@[F %a@]@.@." E.print_all final; + (* + Format.printf "@[F' %a@]@.@." + E.print_all final_c; + *) let check_guarantee (id, f) = let cl = Formula.conslist_of_f f in @@ -162,9 +153,9 @@ end = struct end; if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin - Format.printf "Probes:@["; + Format.printf "Probes: @["; List.iter (fun (p, id, _) -> - if p then Format.printf " %a ∊ %a@ " + if p then Format.printf "%a ∊ %a@ " Formula_printer.print_id id E.print_itv (E.var_itv final id)) st.rp.all_vars; diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 44f2d39..0c7d65e 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -59,7 +59,7 @@ let rec print_num_expr fmt e = match e with (* Enumeated expressions *) let print_enum_expr fmt = function - | EIdent id -> Format.fprintf fmt "%s" id + | EIdent id -> print_id fmt id | EItem x -> Format.fprintf fmt "%s" x let str_of_enum_op = function diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 492b547..bbdc875 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -188,7 +188,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct match env with | Bot -> Format.fprintf fmt "⊥" | Env env -> - Format.fprintf fmt "@[{ "; let l = List.map (fun id -> (get_var env id, id)) ids in let s = List.sort Pervasives.compare l in let rec bl = function @@ -201,6 +200,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | _::q -> bl q in let sbl = bl s in + Format.fprintf fmt "@[{ "; List.iteri (fun j (v, ids) -> if j > 0 then Format.fprintf fmt "@ "; diff --git a/abstract/transform.ml b/abstract/transform.ml index 708456e..64fd8d8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -70,11 +70,19 @@ let rec f_of_neexpr td (node, prefix) where expr = | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> - f_or - (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) - (sub where a)) - (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) - (sub where b)) + if List.mem (node^"/") td.rp.init_scope + then + f_or + (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true)) + (sub where a)) + (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false)) + (sub where b)) + else + f_or + (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (sub where a)) + (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (sub where b)) (* other *) | AST_if(c, a, b) -> f_or @@ -261,12 +269,33 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in let time_incr_eq = if active then - BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) + f_and + (if not (List.mem (node^"/") td.rp.no_time_scope) + then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), + NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) + else BConst true) + (f_and + (if List.mem (node^"/") td.rp.act_scope + then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_true) + else BConst true) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) + else BConst true)) else - BRel(AST_EQ, - NIdent("N"^node^"/"^prefix^"time"), - NIdent(node^"/"^prefix^"time")) + f_and + (if not (List.mem (node^"/") td.rp.no_time_scope) + then BRel(AST_EQ, + NIdent("N"^node^"/"^prefix^"time"), + NIdent(node^"/"^prefix^"time")) + else BConst true) + (f_and + (if List.mem (node^"/") td.rp.act_scope + then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_false) + else BConst true) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) + (EIdent (node^"/"^prefix^"init")) + else BConst true)) in List.fold_left f_and time_incr_eq @@ -306,9 +335,17 @@ let rec init_f_of_scope rp (node, prefix, eqs) = | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton" in let time_eq = - BRel(AST_EQ, - NIdent(node^"/"^prefix^"time"), - NIntConst 0) + f_and + (if not (List.mem (node^"/") rp.no_time_scope) + then + BRel(AST_EQ, + NIdent(node^"/"^prefix^"time"), + NIntConst 0) + else BConst true) + (if List.mem (node^"/") rp.init_scope + then + f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true) + else BConst true) in List.fold_left f_and time_eq (List.map do_eq eqs) diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml index b3393a7..d229f2f 100644 --- a/frontend/ast_util.ml +++ b/frontend/ast_util.ml @@ -6,7 +6,6 @@ open Util let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v) let no_variable e = error ("No such variable: " ^ e) let type_error e = error ("Type error: " ^ e) -let not_implemented e = error ("Not implemented: " ^ e) let invalid_arity e = error ("Invalid arity (" ^ e ^ ")") (* Utility : find declaration of a const / a node *) diff --git a/frontend/typing.ml b/frontend/typing.ml index 1545a38..a4abfe0 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -30,11 +30,16 @@ type var = bool * id * typ type scope = id * id * eqn ext list type rooted_prog = { - p : prog; - root_node : node_decl; - root_scope : scope; - all_vars : var list; - const_vars : var list; + p : prog; + + no_time_scope : id list; (* scopes in which not to introduce time variable *) + act_scope : id list; (* scopes in which to introduce act variable *) + init_scope : id list; (* scopes in which to introduce init variable *) + + root_node : node_decl; + root_scope : scope; + all_vars : var list; + const_vars : var list; } (* Typing *) @@ -120,14 +125,14 @@ let node_vars p f nid = - pre variables are not prefixed by scope - next values for variables are prefixed by capital N *) -let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars = +let rec extract_all_vars rp (node, prefix, eqs) n_vars = let vars_of_expr e = List.flatten (List.map (fun (f, id, eqs, args) -> - let nv = node_vars p f (node^"/"^id) in - nv @ extract_all_vars p (node^"/"^id, "", eqs) nv const_vars) - (extract_instances p e)) + let nv = node_vars rp.p f (node^"/"^id) in + nv @ extract_all_vars rp (node^"/"^id, "", eqs) nv) + (extract_instances rp.p e)) @ List.flatten (List.map @@ -135,7 +140,7 @@ let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars = let vd = List.mapi (fun i t -> false, id^"."^(string_of_int i), t) - (type_expr_vl p n_vars const_vars node expr) + (type_expr_vl rp.p n_vars rp.const_vars node expr) in vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd)) (extract_pre e)) @@ -147,36 +152,58 @@ let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars = | AST_activate_body b -> let bvars = vars_in_node node b.act_locals in bvars @ - extract_all_vars p + extract_all_vars rp (node, b.act_id^".", b.body) (bvars@n_vars) - const_vars | AST_activate_if(c, a, b) -> vars_of_expr c @ do_branch a @ do_branch b in do_branch b | AST_automaton _ -> not_implemented "extract_all vars automaton" in - (false, node^"/"^prefix^"time", TInt):: - (false, "N"^node^"/"^prefix^"time", TInt):: - (List.flatten (List.map vars_of_eq eqs)) + let v = List.flatten (List.map vars_of_eq eqs) in + let v = + if not (List.mem (node^"/") rp.no_time_scope) + then + (false, node^"/"^prefix^"time", TInt):: + (false, "N"^node^"/"^prefix^"time", TInt)::v + else v in + let v = + if List.mem (node^"/") rp.act_scope + then (false, node^"/"^prefix^"act", bool_type)::v + else v in + let v = + if List.mem (node^"/") rp.init_scope + then + (false, node^"/"^prefix^"init", bool_type):: + (false, "N"^node^"/"^prefix^"init", bool_type)::v + else v in + v (* root_prog : prog -> id -> rooted_prog *) let root_prog p root = - let (n, _) = find_node_decl p root in - let root_scope = ("", "", n.body) in + let (root_node, _) = find_node_decl p root in + let root_scope = ("", "", root_node.body) in let const_vars = List.map (fun (cd, _) -> (false, cd.c_name, t_of_ast_t cd.typ)) (extract_const_decls p) in - let root_vars = vars_in_node "" (decls_of_node n) in - - { p; root_scope; root_node = n; - const_vars = const_vars; - all_vars = root_vars @ extract_all_vars p root_scope root_vars const_vars } + let root_vars = vars_in_node "" (decls_of_node root_node) in + + let rp = { + p; root_scope; root_node; + + no_time_scope = ["/"]; + act_scope = []; + init_scope = ["/"]; + + const_vars; + all_vars = [] } in + + { rp with all_vars = root_vars @ extract_all_vars rp root_scope root_vars } diff --git a/libs/util.ml b/libs/util.ml index 6931ed9..01b0c5c 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -25,6 +25,8 @@ let loc_error l f x = | NoLocError e -> raise (LocError([l], e)) | LocError(q, e) -> raise (LocError(l::q, e)) +let not_implemented e = error ("Not implemented: " ^ e) + (* Varmaps *) module VarMap = Mapext.Make(String) @@ -33,6 +35,10 @@ let disjoint_union k a b = match a, b with | None, Some y -> Some y | _ -> error ("Duplicate name in disjoint union: " ^ k) +module SSet = Set.Make(String) + +(* Fixpoint *) + let rec fix equal f s = let fs = f s in if equal fs s -- cgit v1.2.3