Merge pull request #104 from LPCIC/builtin-findall

Builtin findall

CHANGES.md

@@ -1,3 +1,11 @@
+# v1.13.6 (June 2021)
+
+- API:
+  - Fix `std.findall` is now calling a builtin which is able to produce
+    solutions which contain eigenvariables and uvars as well.
+  - `loc` is now printed using `/` as a path separator also on Windows
+  - `loc.fields` to project a `loc` into the file, line, etc...
+
 # v1.13.5 (May 2021)
 
 - API:

src/ast.ml

@@ -265,10 +265,7 @@ let { CData.cin = in_string; isc = is_string; cout = out_string } as cstring =
 let { CData.cin = in_loc; isc = is_loc; cout = out_loc } as cloc =
   CData.(declare {
     data_name = "Loc.t";
-    data_pp = (fun f x ->
-      let bname = x.Loc.source_name in
-      let line_no = x.Loc.line in
-      Fmt.fprintf f "File %S, line %d:" bname line_no);
+    data_pp = Util.Loc.pp;
     data_compare = Pervasives.compare;
     data_hash = Hashtbl.hash;
     data_hconsed = false;

src/builtin.elpi

@@ -359,6 +359,10 @@ external pred quote_syntax i:string, i:string, o:list A, o:A.
 typeabbrev loc (ctype "Loc.t").
 
 
+% [loc.fields Loc File StartChar StopChar Line LineStartsAtChar] Decomposes
+% a loc into its fields
+external pred loc.fields i:loc, o:string, o:int, o:int, o:int, o:int.
+
 % == Regular Expressions =====================================
 
 % [rex.match Rex Subject] checks if Subject matches Rex. Matching is based
@@ -458,6 +462,14 @@ primitive? X S :- is_cdata X (ctype S).
 % of N are guaranteed to be incresing.
 external pred new_int o:int.
 
+% [findall_solution P L] finds all the solved instances of P and puts them
+% in L
+% in the order in which they are found. Instances can contain
+% eigenvariables
+% and unification variables.
+
+external pred findall_solutions i:prop, o:list prop.
+
 % Holds data across bracktracking; can only contain closed terms
 typeabbrev safe (ctype "safe").
 
@@ -776,11 +788,8 @@ max N M N :- N >= M, !.
 max _ M M.
 
 % [findall P L] L is the list [P1,P2,P3..] where each Pi is a solution to P.
-% Solutions must be closed (no unification variables nor eigenvariables).
 pred findall i:prop, o:list prop.
-findall P L :- new_safe F, findall.aux P F, open_safe F L.
-findall.aux P F :- P, stash_in_safe F P, fail.
-findall.aux _ _.
+findall P L :- findall_solutions P L.
 
 }
 

src/builtin.ml

@@ -823,6 +823,18 @@ counter C N :- trace.counter C N.|};
 
   MLData loc;
 
+  MLCode(Pred("loc.fields",
+    In(loc, "Loc",
+    Out(string, "File",
+    Out(int, "StartChar",
+    Out(int, "StopChar",
+    Out(int, "Line",
+    Out(int, "LineStartsAtChar",
+    Easy "Decomposes a loc into its fields")))))),
+  (fun { source_name; source_start; source_stop; line; line_starts_at; } _ _ _ _ _ ~depth:_ ->
+     !: source_name +! source_start +! source_stop +! line +! line_starts_at )),
+  DocAbove);
+
   LPDoc "== Regular Expressions =====================================";
 
   MLCode(Pred("rex.match",
@@ -1110,6 +1122,11 @@ X == Y :- same_term X Y.
       !: !fresh_int)),
   DocAbove);
 
+  LPDoc  {|[findall_solution P L] finds all the solved instances of P and puts them in L
+in the order in which they are found. Instances can contain eigenvariables
+and unification variables.|};
+  LPCode "external pred findall_solutions i:prop, o:list prop.";
+
   MLData safe;
 
    MLCode(Pred("new_safe",

src/builtin_stdlib.elpi

@@ -279,10 +279,7 @@ max N M N :- N >= M, !.
 max _ M M.
 
 % [findall P L] L is the list [P1,P2,P3..] where each Pi is a solution to P.
-% Solutions must be closed (no unification variables nor eigenvariables).
 pred findall i:prop, o:list prop.
-findall P L :- new_safe F, findall.aux P F, open_safe F L.
-findall.aux P F :- P, stash_in_safe F P, fail.
-findall.aux _ _.
+findall P L :- findall_solutions P L.
 
 }

src/compiler.ml

@@ -312,6 +312,7 @@ let is_declared_str state x =
   || x == Symbols.(show state D.Global_symbols.declare_constraintc)
   || x == Symbols.(show state D.Global_symbols.print_constraintsc)
   || x == Symbols.(show state D.Global_symbols.cutc)
+  || x == Symbols.(show state D.Global_symbols.findall_solutionsc)
 ;;
 
 let is_declared state x =
@@ -320,6 +321,7 @@ let is_declared state x =
   || x == D.Global_symbols.declare_constraintc
   || x == D.Global_symbols.print_constraintsc
   || x == D.Global_symbols.cutc
+  || x == D.Global_symbols.findall_solutionsc
 ;;
 
 end

src/data.ml

@@ -402,6 +402,7 @@ module Global_symbols : sig
 
   val declare_constraintc : constant
   val print_constraintsc  : constant
+  val findall_solutionsc  : constant
 
 end = struct
 
@@ -470,6 +471,7 @@ let variadic            = declare_global_symbol "variadic"
 let declare_constraintc = declare_global_symbol "declare_constraint"
 let cutc                = declare_global_symbol_for_builtin F.(show cutf)
 let print_constraintsc  = declare_global_symbol_for_builtin "print_constraints"
+let findall_solutionsc  = declare_global_symbol_for_builtin "findall_solutions"
 
 end
 

src/runtime.ml

@@ -1850,10 +1850,13 @@ let type_err ~depth bname n ty t =
   type_error begin
     "builtin " ^ bname ^ ": " ^
     (if n = 0 then "" else string_of_int n ^ "th argument: ") ^
-    "expected " ^ ty ^ ": got " ^
+    "expected " ^ ty ^ " got" ^
     match t with
     | None -> "_"
-    | Some t -> Format.asprintf "%a" (Pp.uppterm depth [] 0 empty_env) t
+    | Some t ->
+       match t with
+       | CData c -> Format.asprintf " %s: %a" (CData.name c) (Pp.uppterm depth [] 0 empty_env) t
+       | _ -> Format.asprintf ":%a" (Pp.uppterm depth [] 0 empty_env) t
   end
 
 let wrap_type_err bname n f x =
@@ -3021,7 +3024,7 @@ let try_fire_rule (gid[@trace]) rule (constraints as orig_constraints) =
     try
       let _ = search () in
       if get CS.Ugly.delayed <> [] then
-        error "propagation rules must declare constraint(s)"
+        error "propagation rules must not declare constraint(s)"
     with No_clause -> raise NoMatch in
 
   let result = try
@@ -3214,6 +3217,8 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
     match g with
     | Builtin(c,[]) when c == Global_symbols.cutc -> [%spy "user:rule" ~rid ~gid pp_string "cut"];
        [%tcall cut (gid[@trace]) gs next alts lvl]
+    | Builtin(c,[q;sol]) when c == Global_symbols.findall_solutionsc -> [%spy "user:rule" ~rid ~gid pp_string "findall"];
+       [%tcall findall depth p q sol (gid[@trace]) gs next alts lvl]
     | App(c, g, gs') when c == Global_symbols.andc -> [%spy "user:rule" ~rid ~gid pp_string "and"];
        let gs' = List.map (fun x -> (make_subgoal[@inlined]) ~depth (gid[@trace]) p x) gs' in
        let gid[@trace] = make_subgoal_id gid ((depth,g)[@trace]) in
@@ -3334,6 +3339,53 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
     | [] -> pop_andl alts next lvl
     | { depth; program; goal; gid = gid [@trace] } :: gs -> run depth program goal (gid[@trace]) gs next alts lvl
 
+  and findall depth p g s (gid[@trace]) gs next alts lvl =
+    let avoid = oref C.dummy in (* to force a copy *)
+    let copy = move ~adepth:depth ~from:depth ~to_:depth empty_env ~avoid in
+    let g = copy g in (* so that Discard becomes a variable *)
+    [%trace "findall" ~rid ("@[<hov 2>query: %a@]" (uppterm depth [] 0 empty_env) g) begin
+    let executable = {
+      (* same program *)
+      compiled_program = p; 
+      (* no meta meta level *)
+      chr = CHR.empty;
+      initial_goal = g;
+      assignments = StrMap.empty;
+      initial_depth = depth;
+      initial_runtime_state = State.(init () |> State.begin_goal_compilation |> end_goal_compilation StrMap.empty |> end_compilation);
+      query_arguments = Query.N;
+      symbol_table = !C.table;
+      builtins = !FFI.builtins;
+    } in
+    let { search; next_solution; destroy; get; _ } = !do_make_runtime executable in
+    let solutions = ref [] in
+    let add_sol () =
+      if get CS.Ugly.delayed <> [] then
+        error "findall search must not declare constraint(s)";
+      let sol = copy g in
+      [%spy "findall solution:" ~rid ~gid (ppterm depth [] 0 empty_env) g];
+      solutions := sol :: !solutions in
+    let alternatives = ref noalts in
+    try
+      alternatives := search ();
+      add_sol ();
+      while true do
+        alternatives := next_solution !alternatives;
+        add_sol ();
+      done;
+      raise No_clause
+    with No_clause ->
+      destroy ();
+      let solutions = list_to_lp_list (List.rev !solutions) in
+      [%spy "findall solutions:" ~rid ~gid (ppterm depth [] 0 empty_env) solutions];
+      match unif ~matching:false (gid[@trace]) depth empty_env depth s solutions with
+      | false -> [%tcall next_alt alts]
+      | true ->
+        begin match gs with
+        | [] -> [%tcall pop_andl alts next lvl]
+        | { depth ; program; goal; gid = gid [@trace] } :: gs -> [%tcall run depth program goal (gid[@trace]) gs next alts lvl] end
+    end]
+
   and pop_andl alts next lvl =
    match next with
     | FNil ->

src/util.ml

@@ -133,13 +133,13 @@ module Loc = struct
   =
     let source =
      if source_name = "" then ""
-     else source_name ^ ", " in
+     else "File \"" ^ source_name ^ "\", " in
     let chars = Printf.sprintf "characters %d-%d" source_start source_stop in
     let pos =
       if line = -1 then chars
-      else Printf.sprintf "%s, line %d, column %d"
-             chars line (source_stop - line_starts_at) in
-    source ^ pos
+      else Printf.sprintf "line %d, column %d, %s"
+             line (source_stop - line_starts_at) chars in
+    Re.(Str.global_replace (Str.regexp_string "\\") "/" source) ^ pos ^ ":"
 
   let pp fmt l = Fmt.fprintf fmt "%s" (to_string l)
   let show l = to_string l

tests/sources/findall.elpi

@@ -3,4 +3,35 @@ p 1 1.
 p 1 2.
 p 2 2.
 
-main :- std.findall (p A B) [p 1 1, p 1 2, p 2 2].
+test1 :- std.findall (p A B) [p 1 1, p 1 2, p 2 2].
+test2 :- std.findall (p _ _) [p X 1, p 1 2, p 2 2], not(var X).
+test3 :-
+  pi q\
+    q 1 1 =>
+    q 1 2 =>
+    q 2 2 =>
+      (std.findall (q _ _) [q X 2, q 1 2, q 1 1], not (var X)).
+
+
+test4 :-
+  pi q\
+    q 1 A =>
+    q 2 A =>
+      (std.findall (q _ _) [q 2 X, q 1 Y], not(same_var X Y)).
+% this is super tricky but hard to implement differently.
+% q _ _ -> q A^1 B^1
+% q A^1 B^1 == q 1 X0 --restrict--> X0 := X1,  A1 := _\X1
+% when we backtrack the "restriction" on X0 is lost
+
+test5 :-
+  pi q\
+    q 1 A =>
+    q 2 A =>
+      (std.findall (q _ Z) [q 2 X, q 1 Y], same_var X Y).
+% this works because there is no restriction
+
+main :- test1, print 1,
+        test2, print 2,
+        test3, print 3,
+        test4, print 4,
+        test5, print 5.