From d7865f890667e633512abffd9ff384ae7b5157f4 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 22 Oct 2024 23:10:48 +0200 Subject: [PATCH] Fix bug #272 (forgot parens...) --- src/runtime.ml | 4 ++-- tests/sources/dt_bug272.elpi | 23 +++++++++++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) create mode 100644 tests/sources/dt_bug272.elpi diff --git a/src/runtime.ml b/src/runtime.ml index f1e45a9f..8d5557de 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2508,8 +2508,8 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar arg_mo (* up to the 30^th elemebt *) if h > 30 then (Path.emit path mkListEnd; update_current_min_depth path_depth) else - main ~safe ~depth a path_depth; - list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b + (main ~safe ~depth a path_depth; + list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b) (* These cases can come from terms like `[_ | _]`, `[_ | A]` ... *) | UVar _ | AppUVar _ | Arg _ | AppArg _ | Discard -> Path.emit path mkListTailVariable; update_current_min_depth path_depth diff --git a/tests/sources/dt_bug272.elpi b/tests/sources/dt_bug272.elpi new file mode 100644 index 00000000..ba127e69 --- /dev/null +++ b/tests/sources/dt_bug272.elpi @@ -0,0 +1,23 @@ +:index(1 1) +pred map2 i:list A, i:list B, i:(A -> B -> C -> o), o:list C. +map2 [] [] _ []. +map2 [A|As] [B|Bs] F [C|Cs] :- F A B C, map2 As Bs F Cs. + +pred any_list i:int, o:list int. +any_list 0 [] :- !. +any_list N [N|L] :- any_list {calc (N - 1)} L. + +pred any_pred i:int, i:int, o:int. +any_pred A B R :- R is A + B. + +pred test i:int, o:list int. +test N R :- any_list N L, map2 L L any_pred R. + +pred loop i:int, i:int. +loop N N :- !. +loop N M :- + test N _, + N1 is N + 1, + loop N1 M. + +main :- loop 1 100. \ No newline at end of file