cleanup/document API change for -delay-problems-outside-pattern-fragment

bench/jobs/elpi/ko/elpi_only_llam.elpi

@@ -0,0 +1 @@
+../../../sources/elpi/elpi_only_llam.elpi

bench/sources/elpi/elpi_only_llam.elpi

@@ -0,0 +1 @@
+main :- p (F X) F X => p (f x) f x.

src/elpi_API.ml

@@ -101,7 +101,7 @@ module Compile = struct
   let static_check header ?checker ?flags p =
     let module R = (val !r) in let open R in
     let checker = Elpi_util.option_map List.flatten checker in
-    Elpi_compiler.static_check header ~exec:execute_once ?checker ?flags p
+    Elpi_compiler.static_check header ~exec:(execute_once ~delay_outside_fragment:false) ?checker ?flags p
 
   module StrSet = Elpi_util.StrSet
 

src/elpi_API.mli

@@ -140,8 +140,12 @@ module Execute : sig
 
   type outcome = Success of Data.solution | Failure | NoMoreSteps
 
-  (* Returns the first solution, if any, within the optional steps bound *)
-  val once : ?max_steps:int -> ?delay_outside_fragment:bool -> Compile.executable -> outcome
+  (* Returns the first solution, if any, within the optional steps bound.
+   * Setting delay_outside_fragment (false by default) results in unification
+   * outside the pattern fragment to be delayed (behavior of Teyjus), rather
+   * than abort the execution (default behavior) *)
+  val once : ?max_steps:int -> ?delay_outside_fragment:bool ->
+    Compile.executable -> outcome
 
   (** Prolog's REPL.
     [pp] is called on all solutions.

src/elpi_compiler.ml

@@ -1462,7 +1462,7 @@ let quote_syntax { Query.clauses; query_loc; query } =
 let default_checker () = Elpi_parser.parse_program ["elpi-checker.elpi"]
 
 let static_check header
-  ?(exec=execute_once) ?(checker=default_checker ()) ?(flags=default_flags)
+  ?(exec=execute_once ~delay_outside_fragment:false) ?(checker=default_checker ()) ?(flags=default_flags)
   ({ Query.types } as q)
 =
   let p,q = quote_syntax q in

src/elpi_compiler.mli

@@ -41,7 +41,7 @@ val quote_syntax : query -> term list * term
 
 (* false means a type error was found *)
 val static_check : Elpi_ast.decl list -> (* header *)
-  ?exec:(?max_steps:int -> ?delay_outside_fragment:bool -> executable -> outcome) ->
+  ?exec:(?max_steps:int -> executable -> outcome) ->
   ?checker:Elpi_ast.decl list ->
   ?flags:flags ->
   query -> bool

src/elpi_runtime.ml

@@ -1281,6 +1281,11 @@ let rec list_to_lp_list = function
 ;;
 
 let delay_hard_unif_problems = Fork.new_local false
+let error_msg_hard_unif =
+  "Unification problem outside the pattern fragment. "^
+  "Pass -delay-problems-outside-pattern-fragment (elpi command line utility) "^
+  "or set delay_outside_fragment to true (Elpi_API) in order to delay "^
+  "(deprecated, for Teyjus compatibility)."
 
 let rec unif matching depth adepth a bdepth b e =
    [%trace "unif" ("@[<hov 2>^%d:%a@ =%d%s= ^%d:%a@]%!"
@@ -1447,7 +1452,7 @@ let rec unif matching depth adepth a bdepth b e =
          | Some r' -> if r==r' then [r] else [r;r'] in
        CS.declare_new { kind; blockers };
        true
-       end else error "Unification problem outside the pattern fragment. Use -delay-problems-outside-pattern-fragment."
+       end else error error_msg_hard_unif
    | AppUVar({ rest = _ :: _ },_,_), (AppUVar ({ rest = [] },_,_) | UVar ({ rest = [] },_,_)) -> unif matching depth bdepth b adepth a e
    | AppUVar (r, lvl,args), other when not matching ->
        let is_llam, args = is_llam lvl args adepth bdepth depth true e in
@@ -1459,7 +1464,7 @@ let rec unif matching depth adepth a bdepth b e =
        let blockers = match is_flex (bdepth+depth) other with | None -> [r] | Some r' -> [r;r'] in
        CS.declare_new { kind; blockers };
        true
-       end else error "Unification problem outside the pattern fragment. Use -delay-problems-outside-pattern-fragment."
+       end else error error_msg_hard_unif
    | other, AppUVar (r, lvl,args) ->
        let is_llam, args = is_llam lvl args adepth bdepth depth false e in
        if is_llam then
@@ -1473,7 +1478,7 @@ let rec unif matching depth adepth a bdepth b e =
          | Some r' -> if r==r' then [r] else [r;r'] in
        CS.declare_new { kind; blockers };
        true
-       end else error "Unification problem outside the pattern fragment. Use -delay-problems-outside-pattern-fragment."
+       end else error error_msg_hard_unif
 
    (* recursion *)
    | App (c1,x2,xs), App (c2,y2,ys) ->