diff --git a/src/compiler/compiler.ml b/src/compiler/compiler.ml index d05c2cdae..34afd8376 100644 --- a/src/compiler/compiler.ml +++ b/src/compiler/compiler.ml @@ -1503,15 +1503,15 @@ end = struct let check_and_spill_chr ~flags ~det_check_time ~time ~unknown ~type_abbrevs ~kinds ~types r = let unknown = time_this time (fun () -> Type_checker.check_chr_rule ~unknown ~type_abbrevs ~kinds ~types r) in + let guard = Option.map (Spilling.main ~type_abbrevs ~types) r.guard in + let new_goal = Option.map (fun ({ Ast.Chr.conclusion } as x) -> { x with conclusion = Spilling.main ~types ~type_abbrevs conclusion }) r.new_goal in if not flags.skip_det_checking then time_this det_check_time (fun () -> Option.iter (fun { Ast.Chr.conclusion } -> - Determinacy_checker.check_chr_guard_and_newgoal ~type_abbrevs ~types ~unknown ~guard:r.guard ~newgoal:conclusion) - r.new_goal); + Determinacy_checker.check_chr_guard_and_newgoal ~type_abbrevs ~types ~unknown ~guard ~newgoal:conclusion) + new_goal); if Option.fold ~none:false ~some:(fun x -> has_cut ~types x.Ast.Chr.conclusion) r.new_goal then error ~loc:r.loc "CHR new goals cannot contain cut"; - let guard = Option.map (Spilling.main ~type_abbrevs ~types) r.guard in - let new_goal = Option.map (fun ({ Ast.Chr.conclusion } as x) -> { x with conclusion = Spilling.main ~types ~type_abbrevs conclusion }) r.new_goal in unknown, { r with guard; new_goal } let check ~flags st ~base u : checked_compilation_unit = diff --git a/tests/sources/bug_419.elpi b/tests/sources/bug_419.elpi new file mode 100644 index 000000000..bf9a7223d --- /dev/null +++ b/tests/sources/bug_419.elpi @@ -0,0 +1,10 @@ +func f -> int. + +func zero -> int. +zero 0. + +constraint f { + rule (f X) <=> ({zero} = X). +} + +main. \ No newline at end of file diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml index ae701527a..3ec8c493f 100644 --- a/tests/suite/elpi_specific.ml +++ b/tests/suite/elpi_specific.ml @@ -175,6 +175,11 @@ let () = declare "spill2" ~description:"spilling 2 arguments" () +let () = declare "spill-chr" + ~source_elpi:"bug_419.elpi" + ~description:"spilling in chr" + () + let () = declare "spill_sigma" ~source_elpi:"spill_sigma.elpi" ~description:"spilling under sigma" @@ -586,4 +591,5 @@ let () = declare "macro_uv" ~source_elpi:"macro_uv.elpi" ~description:"refreshing of macro body" ~expectation:Success - () \ No newline at end of file + () +