diff options
| author | Gaëtan Gilbert | 2020-11-23 16:08:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-23 16:08:37 +0100 |
| commit | 60ed425ffc8bc30c11a3a8e542a9bfb0a0a06471 (patch) | |
| tree | 9ce750e090f593cc063ceed05ef97fcd5f5d5df2 /plugins/extraction | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
Fix comparison of extracted array literals
Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
let o = optims () in
let rec norm a =
let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
if eq_ml_ast a a' then a else norm a'
in norm a
~~~
the `eq_ml_ast` was always returning `false`.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 21ec80abbc..da4a50b674 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -399,7 +399,11 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2 | MLfloat f1, MLfloat f2 -> Float64.equal f1 f2 -| _, _ -> false +| MLparray (t1,def1), MLparray (t2, def2) -> Array.equal eq_ml_ast t1 t2 && eq_ml_ast def1 def2 +| (MLrel _|MLapp _|MLlam _|MLletin _|MLglob _|MLcons _ + |MLtuple _|MLcase _|MLfix _|MLexn _|MLdummy _|MLaxiom + | MLmagic _| MLuint _| MLfloat _|MLparray _), _ + -> false and eq_ml_pattern p1 p2 = match p1, p2 with | Pcons (gr1, p1), Pcons (gr2, p2) -> |