Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Revert "bugfix" #24

Merged
merged 1 commit into from
Dec 23, 2023
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Revert "bugfix"
This reverts commit 45aa4f0.
This commit tries to include the removal of unit but introduce a
infinite loop.
  • Loading branch information
FardaleM committed Dec 23, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 225ba6753196068893aceef42a303263f64af568
53 changes: 0 additions & 53 deletions lib/package/FromLibIndex.ml

This file was deleted.

12 changes: 0 additions & 12 deletions lib/package/FromLibIndex.mli

This file was deleted.

18 changes: 8 additions & 10 deletions lib/unification/AC.ml
Original file line number Diff line number Diff line change
@@ -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)
16 changes: 3 additions & 13 deletions lib/unification/Unification.ml
Original file line number Diff line number Diff line change
@@ -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. *)
Loading