Revert "bugfix"

This reverts commit 45aa4f0. This commit tries to include the removal of unit but introduce a infinite loop.
Drup · Dec 23, 2023 · 225ba67 · 225ba67
1 parent aa3eaaf
commit 225ba67
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 88 deletions.
diff --git a/lib/package/FromLibIndex.ml b/lib/package/FromLibIndex.ml
diff --git a/lib/package/FromLibIndex.mli b/lib/package/FromLibIndex.mli
diff --git a/lib/unification/AC.ml b/lib/unification/AC.ml
@@ -14,7 +14,6 @@ module System : sig
   val make : ACTerm.problem list -> t
 
   type dioph_solution
-  val pp_solution : dioph_solution Fmt.t
   val get_solution : dioph_solution -> int -> int
 
   val solve : t -> dioph_solution Iter.t
@@ -97,7 +96,6 @@ end = struct
     { nb_atom ; assoc_pure ; first_var ; system }
 
   type dioph_solution = int array
-  let pp_solution = Fmt.Dump.array Fmt.int
   let get_solution = Array.get
 
   let solve { first_var ; system ; _ } : dioph_solution Iter.t =
@@ -210,7 +208,7 @@ end = struct
         let sol = solutions.(i) in
         (* assert (Array.length sol = Array.length vars) ; *)
         let symb = symbols.(i) in
-        Logs.debug (fun m -> m "Checking %i:%a for subset %a@." i Pure.pp symb Bitv.pp subset) ;
+        (* log (fun m -> m "Checking %i:%a for subset %a@." i Pure.pp symb Bitv.pp subset) ; *)
         for j = 0 to Array.length vars - 1 do
           match vars.(j) with
           | Pure.Constant _ | Pure.FrozenVar _ -> ()
@@ -219,9 +217,9 @@ end = struct
             Variable.HMap.add_list unifiers var (multiplicity, symb)
         done;
     done;
-    Logs.debug (fun m -> m "Unif: %a@." Fmt.(iter_bindings ~sep:(any" | ") Variable.HMap.iter @@
-       pair ~sep:(any" -> ") Variable.pp @@ list ~sep:(any",@ ") @@ pair int Pure.pp ) unifiers
-    ) ;
+    (* log (fun m -> m "Unif: %a@." Fmt.(iter_bindings ~sep:(unit" | ") Variable.HMap.iter @@ *)
+    (*    pair ~sep:(unit" -> ") Variable.pp @@ list ~sep:(unit",@ ") @@ pair int Pure.pp ) unifiers *)
+    (* ) ; *)
     let buffer = CCVector.create_with ~capacity:10 Pure.dummy in
     fun k ->
       Variable.HMap.iter
@@ -236,11 +234,11 @@ end = struct
       (seq_solutions:System.dioph_solution Iter.t) : _ Iter.t =
     let stack_solutions = CCVector.create () in
     let bitvars = extract_solutions stack_solutions nb_atom seq_solutions in
-    Fmt.epr "@[Bitvars: %a@]@." (Fmt.Dump.array Bitv.pp) bitvars;
-    Fmt.epr "@[<v2>Sol stack:@ %a@]@."
-      (CCVector.pp System.pp_solution) stack_solutions;
+    (* Fmt.epr "@[Bitvars: %a@]@," (Fmt.Dump.array Bitv.pp) bitvars;
+     * Fmt.epr "@[<v2>Sol stack:@ %a@]@,"
+     *   (CCVector.pp @@ Fmt.Dump.array Fmt.int) stack_solutions; *)
     let symbols = symbols_of_solutions env system stack_solutions in
-    Fmt.epr "@[Symbols: %a@]@." (Fmt.Dump.array @@ Pure.pp) symbols;
+    (* Fmt.epr "@[Symbols: %a@]@," (Fmt.Dump.array @@ Pure.pp namefmt) symbols; *)
     let subsets = iterate_subsets (Array.length symbols) system bitvars in
     Iter.map
       (unifier_of_subset assoc_pure stack_solutions symbols)

diff --git a/lib/unification/Unification.ml b/lib/unification/Unification.ml
@@ -110,7 +110,6 @@ let rec process_stack env (stack : Stack.t) : return =
 and insert_rec env stack (t1 : Type.t) (t2 : Type.t) : return =
   match (t1, t2) with
   | _ when t1 == t2 -> process_stack env stack
-  | Var v, t | t, Var v -> insert_var env stack v t
   (* Decomposition rule
      (s₁,...,sₙ) p ≡ (t₁,...,tₙ) p  --> ∀i, sᵢ ≡ tᵢ
      when p is a type constructor.
@@ -138,22 +137,13 @@ and insert_rec env stack (t1 : Type.t) (t2 : Type.t) : return =
       let stack, pure_t = variable_abstraction_all env stack t in
       Env.push_tuple env pure_s pure_t;
       process_stack env stack
-  | s, Tuple t ->
-      let stack, pure_s = variable_abstraction env stack s in
-      let stack, pure_t = variable_abstraction_all env stack t in
-      Env.push_tuple env [|pure_s|] pure_t;
-      process_stack env stack
-  | Tuple s, t ->
-      let stack, pure_s = variable_abstraction_all env stack s in
-      let stack, pure_t = variable_abstraction env stack t in
-      Env.push_tuple env pure_s [|pure_t|];
-      process_stack env stack
+  | Var v, t | t, Var v -> insert_var env stack v t
   (* Clash rule
      Terms are incompatible
   *)
   | Constr _, Constr _ (* if same constructor, already checked above *)
-  | ( (Constr _ | Arrow _ | Other _ | FrozenVar _),
-      (Constr _ | Arrow _ | Other _ | FrozenVar _) ) ->
+  | ( (Constr _ | Tuple _ | Arrow _ | Other _ | FrozenVar _),
+      (Constr _ | Tuple _ | Arrow _ | Other _ | FrozenVar _) ) ->
       FailUnif (t1, t2)
 
 (* Repeated application of VA on an array of subexpressions. *)