From 8f04ed22e72a311b1dc957577fa4c2c795860c73 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Jun 2021 15:53:10 +0200 Subject: [PATCH 1/3] loc: print / as a separator on windows as well --- src/ast.ml | 5 +---- src/util.ml | 8 ++++---- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index 290aa28e7..a6dca6c4d 100644 --- a/src/ast.ml +++ b/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; diff --git a/src/util.ml b/src/util.ml index 4c23a71f4..a39f06693 100644 --- a/src/util.ml +++ b/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 From 51ba6547b332426b6c54c3b382ccf21b1943adb0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Jun 2021 17:11:40 +0200 Subject: [PATCH 2/3] builtin findall --- CHANGES.md | 7 ++++++ src/builtin.elpi | 13 +++++++--- src/builtin.ml | 5 ++++ src/builtin_stdlib.elpi | 5 +--- src/compiler.ml | 2 ++ src/data.ml | 2 ++ src/runtime.ml | 51 +++++++++++++++++++++++++++++++++++++- tests/sources/findall.elpi | 33 +++++++++++++++++++++++- 8 files changed, 108 insertions(+), 10 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 258bf7da9..4d8151f8d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,10 @@ +# 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 + # v1.13.5 (May 2021) - API: diff --git a/src/builtin.elpi b/src/builtin.elpi index dcc7196af..9c57fdd79 100644 --- a/src/builtin.elpi +++ b/src/builtin.elpi @@ -458,6 +458,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 +784,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. } diff --git a/src/builtin.ml b/src/builtin.ml index 47ce4dbc0..5274a122f 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1110,6 +1110,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", diff --git a/src/builtin_stdlib.elpi b/src/builtin_stdlib.elpi index 3c29a26dd..f5eb21ec9 100644 --- a/src/builtin_stdlib.elpi +++ b/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. } \ No newline at end of file diff --git a/src/compiler.ml b/src/compiler.ml index 8144b3fef..8a6475618 100644 --- a/src/compiler.ml +++ b/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 diff --git a/src/data.ml b/src/data.ml index 9347075a3..123141aca 100644 --- a/src/data.ml +++ b/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 diff --git a/src/runtime.ml b/src/runtime.ml index e9bf5c6e7..b4c7010d5 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -3021,7 +3021,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 +3214,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 +3336,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 ("@[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 -> diff --git a/tests/sources/findall.elpi b/tests/sources/findall.elpi index cadeb4f60..2bc02d7f0 100644 --- a/tests/sources/findall.elpi +++ b/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]. \ No newline at end of file +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. \ No newline at end of file From e51e114d1b70361fe9afb89a76ae2223c7f76e4a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 16 Jun 2021 14:55:14 +0200 Subject: [PATCH 3/3] builtin loc.fields --- CHANGES.md | 1 + src/builtin.elpi | 4 ++++ src/builtin.ml | 12 ++++++++++++ src/runtime.ml | 7 +++++-- 4 files changed, 22 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 4d8151f8d..2f2b293f8 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,6 +4,7 @@ - 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) diff --git a/src/builtin.elpi b/src/builtin.elpi index 9c57fdd79..65ed4561b 100644 --- a/src/builtin.elpi +++ b/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 diff --git a/src/builtin.ml b/src/builtin.ml index 5274a122f..72c9c17c6 100644 --- a/src/builtin.ml +++ b/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", diff --git a/src/runtime.ml b/src/runtime.ml index b4c7010d5..5b4b57286 100644 --- a/src/runtime.ml +++ b/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 =