From 91d448d069680935df3048cc74805046f13f4830 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Nov 2023 13:29:36 +0100 Subject: [PATCH 1/4] API: solution relocation --- src/API.ml | 22 ++++++++++++++++++---- src/API.mli | 1 + src/compiler.ml | 17 +++++++++-------- src/data.ml | 1 + src/runtime.ml | 13 +++++++------ src/runtime.mli | 1 + 6 files changed, 37 insertions(+), 18 deletions(-) diff --git a/src/API.ml b/src/API.ml index cda06a5c5..9c2cde548 100644 --- a/src/API.ml +++ b/src/API.ml @@ -137,12 +137,13 @@ module Data = struct type state = Data.State.t type pretty_printer_context = ED.pp_ctx module StrMap = Util.StrMap - type 'a solution = 'a Data.solution = { + type 'a solution = { assignments : term StrMap.t; constraints : constraints; state : state; output : 'a; pp_ctx : pretty_printer_context; + relocate_assignment_to_runtime : target:state -> depth:int -> string -> (term, string) Stdlib.Result.t } type hyp = Data.clause_src = { hdepth : int; @@ -187,14 +188,27 @@ module Compile = struct end module Execute = struct - type 'a outcome = 'a ED.outcome = + type 'a outcome = Success of 'a Data.solution | Failure | NoMoreSteps + + let map_outcome full_deref hmove = function + | ED.Failure -> Failure + | ED.NoMoreSteps -> NoMoreSteps + | ED.Success { ED.assignments; constraints; state; output; pp_ctx; state_for_relocation = (idepth,from); } -> + Success { assignments; constraints; state; output; pp_ctx; + relocate_assignment_to_runtime = (fun ~target ~depth s -> + Compiler.relocate_closed_term ~from + (Util.StrMap.find s assignments |> full_deref ~depth:idepth) ~to_:target + |> Stdlib.Result.map (hmove ?avoid:None ~from:depth ~to_:depth) + ); + } + let once ?max_steps ?delay_outside_fragment p = let module R = (val !r) in - R.execute_once ?max_steps ?delay_outside_fragment p + map_outcome R.full_deref R.hmove @@ R.execute_once ?max_steps ?delay_outside_fragment p let loop ?delay_outside_fragment p ~more ~pp = let module R = (val !r) in - R.execute_loop ?delay_outside_fragment p ~more ~pp + R.execute_loop ?delay_outside_fragment p ~more ~pp:(fun t o -> pp t (map_outcome R.full_deref R.hmove o)) end diff --git a/src/API.mli b/src/API.mli index 2d91dcb51..d0e0030a8 100644 --- a/src/API.mli +++ b/src/API.mli @@ -157,6 +157,7 @@ module Data : sig state : state; output : 'a; pp_ctx : pretty_printer_context; + relocate_assignment_to_runtime : target:state -> depth:int -> string -> (term, string) Stdlib.Result.t } (* Hypothetical context *) diff --git a/src/compiler.ml b/src/compiler.ml index f3f69ae54..4b1cd985f 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -129,7 +129,7 @@ let table = D.State.declare ~goal_compilation_begins:(fun x -> x) ~goal_compilation_is_over:(fun ~args:_ x -> Some x) ~compilation_is_over:(fun x -> Some { x with frozen = true }) (* to implement read_term and relocate_closed_term *) - ~execution_is_over:(fun x -> Some x) (* to implement relocate_closed_term *) + ~execution_is_over:(fun _ -> None) ~init:(fun () -> { ast2ct = F.Map.empty; last_global = D.Global_symbols.table.last_global; @@ -2057,13 +2057,14 @@ let rec constants_of acc = function | D.AppUVar _ | D.UVar _ -> anomaly "relocate_closed_term: not a closed term" | D.Nil | D.Discard | D.CData _ -> acc -let relocate_closed_term ~from ~to_ t = - let table = State.get Symbols.table from in - let alive = constants_of C.Set.empty t in - let table = Symbols.prune table ~alive in - let base = State.update Symbols.table to_ Symbols.lock in - Stdlib.Result.bind (Symbols.build_shift ~lock_base:true ~flags:default_flags ~base table) - (fun (base, shift) -> Stdlib.Result.Ok (Flatten.relocate_term to_ shift t)) + let relocate_closed_term ~from = + let table = State.get Symbols.table from in + fun ~to_ t -> + let alive = constants_of C.Set.empty t in + let table = Symbols.prune table ~alive in + let base = State.update Symbols.table to_ Symbols.lock in + Stdlib.Result.bind (Symbols.build_shift ~lock_base:true ~flags:default_flags ~base table) + (fun (base, shift) -> Stdlib.Result.Ok (Flatten.relocate_term to_ shift t)) let w_symbol_table s f x = let table = Symbols.compile_table @@ State.get Symbols.table s in diff --git a/src/data.ml b/src/data.ml index d7b14a89f..721d2d3a2 100644 --- a/src/data.ml +++ b/src/data.ml @@ -1343,6 +1343,7 @@ type 'a solution = { state : State.t; output : 'a; pp_ctx : pp_ctx; + state_for_relocation : int * State.t; } type 'a outcome = Success of 'a solution | Failure | NoMoreSteps diff --git a/src/runtime.ml b/src/runtime.ml index 0a2eb2409..11c1f3d66 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -3988,14 +3988,14 @@ open Mainloop let mk_outcome search get_cs assignments depth = try let alts = search () in - let syn_csts, state, qargs, pp_ctx = get_cs () in - let assignments = StrMap.map (fun x -> full_deref ~adepth:0 empty_env ~depth x) assignments in + let syn_csts, reloc_state, final_state, qargs, pp_ctx = get_cs () in let solution = { assignments; constraints = syn_csts; - state; - output = output qargs assignments state; + state = final_state; + output = output qargs assignments final_state; pp_ctx = pp_ctx; + state_for_relocation = reloc_state; } in Success solution, alts with @@ -4005,7 +4005,7 @@ let mk_outcome search get_cs assignments depth = let execute_once ?max_steps ?delay_outside_fragment exec = let { search; get } = make_runtime ?max_steps ?delay_outside_fragment exec in try - let result = fst (mk_outcome search (fun () -> get CS.Ugly.delayed, get CS.state |> State.end_execution, exec.query_arguments, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments exec.initial_depth) in + let result = fst (mk_outcome search (fun () -> get CS.Ugly.delayed, (exec.initial_depth,get CS.state), get CS.state |> State.end_execution, exec.query_arguments, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments exec.initial_depth) in [%end_trace "execute_once" ~rid]; result with e -> @@ -4019,7 +4019,7 @@ let execute_loop ?delay_outside_fragment exec ~more ~pp = let k = ref noalts in let do_with_infos f = let time0 = Unix.gettimeofday() in - let o, alts = mk_outcome f (fun () -> get CS.Ugly.delayed, get CS.state |> State.end_execution, exec.query_arguments, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments exec.initial_depth in + let o, alts = mk_outcome f (fun () -> get CS.Ugly.delayed, (exec.initial_depth,get CS.state), get CS.state |> State.end_execution, exec.query_arguments, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments exec.initial_depth in let time1 = Unix.gettimeofday() in k := alts; pp (time1 -. time0) o in @@ -4039,6 +4039,7 @@ let is_flex = HO.is_flex let deref_uv = HO.deref_uv let deref_appuv = HO.deref_appuv let deref_head = HO.deref_head +let full_deref = HO.full_deref ~adepth:0 empty_env let eta_contract_flex = HO.eta_contract_flex let make_runtime = Mainloop.make_runtime let lp_list_to_list = Clausify.lp_list_to_list diff --git a/src/runtime.mli b/src/runtime.mli index a2bc367ab..5d6be243a 100644 --- a/src/runtime.mli +++ b/src/runtime.mli @@ -76,3 +76,4 @@ val clausify1 : mode Constants.Map.t -> (* for caching it in the clause *) nargs:int -> depth:int -> term -> (constant * clause) * clause_src * int +val full_deref : depth:int -> term -> term From 1c4120b02daa8a2abc29cd7e2b760eaea2218fba Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Nov 2023 13:03:40 +0100 Subject: [PATCH 2/4] API: ho functions --- src/API.ml | 85 +++++++++++++++++++++++++++++++++-- src/API.mli | 48 ++++++++++++++++++++ src/builtin.elpi | 53 ++++++++++++++++++++++ src/builtin.ml | 56 +++++++++++++++++++++++ src/data.ml | 2 + src/runtime.ml | 19 ++++++-- tests/sources/map_ho.elpi | 4 ++ tests/sources/set_ho.elpi | 10 +++++ tests/suite/performance_FO.ml | 9 ++++ 9 files changed, 279 insertions(+), 7 deletions(-) create mode 100644 tests/sources/map_ho.elpi create mode 100644 tests/sources/set_ho.elpi diff --git a/src/API.ml b/src/API.ml index 9c2cde548..8363316bd 100644 --- a/src/API.ml +++ b/src/API.ml @@ -820,6 +820,8 @@ module AlgebraicData = struct end module BuiltInPredicate = struct + type once = depth:int -> Data.term -> Data.state -> Data.state + include ED.BuiltInPredicate exception No_clause = ED.No_clause @@ -891,6 +893,84 @@ module BuiltInPredicate = struct let (+?) a b = a, b end + + let beta ~depth t args = + let module R = (val !r) in let open R in + deref_appuv ~from:depth ~to_:depth ?avoid:None args t + + module HOAdaptors = struct + + type 'a pred1 = Data.term * 'a Conversion.t + type ('a,'b) pred2 = Data.term * 'a Conversion.t * 'b Conversion.t + type ('a,'b,'c) pred3 = Data.term * 'a Conversion.t * 'b Conversion.t * 'c Conversion.t + + let pred1_ty x = Conversion.TyApp("->",x.Conversion.ty,[Conversion.TyName"prop"]) + let pred1 x = { Conversion.ty = pred1_ty x; readback = (fun ~depth state e -> state,(e,x),[]); embed = (fun ~depth state (x,_) -> state,x,[]); pp = (fun fmt (x,_) -> Format.fprintf fmt ""); pp_doc = (fun fmt () -> ()) } + let pred2_ty x y = Conversion.(TyApp("->",x.Conversion.ty,[TyApp("->",y.Conversion.ty,[Conversion.TyName"prop"])])) + let pred2 x y = { Conversion.ty = pred2_ty x y; readback = (fun ~depth state e -> state,(e,x,y),[]); embed = (fun ~depth state (x,_,_) -> state,x,[]); pp = (fun fmt (x,_,_) -> Format.fprintf fmt ""); pp_doc = (fun fmt () -> ()) } + let pred3_ty x y z = Conversion.(TyApp("->",x.Conversion.ty,[TyApp("->",y.Conversion.ty,[TyApp("->",z.Conversion.ty,[Conversion.TyName"prop"])])])) + let pred3 x y z = { Conversion.ty = pred3_ty x y z; readback = (fun ~depth state e -> state,(e,x,y,z),[]); embed = (fun ~depth state (x,_,_,_) -> state,x,[]); pp = (fun fmt (x,_,_,_) -> Format.fprintf fmt ""); pp_doc = (fun fmt () -> ()) } + + + let filter1 ~once ~depth ~filter (f,c1) m state = + let gls = ref [] in + let st = ref state in + let m = filter (fun x -> + try + let state, x, gls0 = c1.Conversion.embed ~depth !st x in + gls := gls0 :: !gls; + let state = once ~depth (beta ~depth f [x]) state in + st := state; + true + with No_clause -> false) m in + !st, m, List.concat @@ List.rev !gls + let filter2 ~once ~depth ~filter (f,c1,c2) m state = + let gls = ref [] in + let st = ref state in + let m = filter (fun x y -> + try + let state, x, gls0 = c1.Conversion.embed ~depth !st x in + let state, y, gls1 = c2.Conversion.embed ~depth state y in + gls := gls1 :: gls0 :: !gls; + let state = once ~depth (beta ~depth f [x;y]) state in + st := state; + true + with No_clause -> false) m in + !st, m, List.concat @@ List.rev !gls + + let map1 ~once ~depth ~map (f,c1,c2) m state = + let gls = ref [] in + let st = ref state in + let m = map (fun x -> + let state, x, gls0 = c1.Conversion.embed ~depth !st x in + let state, y = FlexibleData.Elpi.make state in + let y = RawData.mkUnifVar y ~args:(List.init depth RawData.mkConst) state in + gls := gls0 :: !gls; + let state = once ~depth (beta ~depth f [x;y]) state in + let state, y, gls1 = c2.Conversion.readback ~depth state y in + st := state; + y + ) m in + !st, m, List.concat @@ List.rev !gls + + let map2 ~once ~depth ~map (f,c1,c2,c3) m state = + let gls = ref [] in + let st = ref state in + let m = map (fun x y -> + let state, x, gls0 = c1.Conversion.embed ~depth !st x in + let state, y, gls1 = c2.Conversion.embed ~depth state y in + let state, z = FlexibleData.Elpi.make state in + let z = RawData.mkUnifVar z ~args:(List.init depth RawData.mkConst) state in + gls := gls1 :: gls0 :: !gls; + let state = once ~depth (beta ~depth f [x;y;z]) state in + let state, z, gls1 = c3.Conversion.readback ~depth state z in + st := state; + z + ) m in + !st, m, List.concat @@ List.rev !gls + + end + end module BuiltIn = struct @@ -1007,9 +1087,8 @@ module Utils = struct let move ~from ~to_ t = let module R = (val !r) in let open R in hmove ~from ~to_ ?avoid:None t - let beta ~depth t args = - let module R = (val !r) in let open R in - deref_appuv ~from:depth ~to_:depth ?avoid:None args t + + let beta = BuiltInPredicate.beta let error = Util.error let type_error = Util.type_error diff --git a/src/API.mli b/src/API.mli index d0e0030a8..cb1b7c842 100644 --- a/src/API.mli +++ b/src/API.mli @@ -557,6 +557,8 @@ module BuiltInPredicate : sig type 'a oarg = Keep | Discard type 'a ioarg = private Data of 'a | NoData + type once + type ('function_type, 'inernal_outtype_in, 'internal_hyps, 'internal_constraints) ffi = (* Arguemnts that are translated independently of the program context *) | In : 't Conversion.t * doc * ('i, 'o,'h,'c) ffi -> ('t -> 'i,'o,'h,'c) ffi @@ -575,6 +577,7 @@ module BuiltInPredicate : sig context readback function *) | Read : ('h,'c) ContextualConversion.ctx_readback * doc -> (depth:int -> 'h -> 'c -> Data.state -> 'o, 'o,'h,'c) ffi | Full : ('h,'c) ContextualConversion.ctx_readback * doc -> (depth:int -> 'h -> 'c -> Data.state -> Data.state * 'o * Conversion.extra_goals, 'o,'h,'c) ffi + | FullHO : ('h,'c) ContextualConversion.ctx_readback * doc -> (once:once -> depth:int -> 'h -> 'c -> Data.state -> Data.state * 'o * Conversion.extra_goals, 'o,'h,'c) ffi | VariadicIn : ('h,'c) ContextualConversion.ctx_readback * ('t,'h,'c) ContextualConversion.t * doc -> ('t list -> depth:int -> 'h -> 'c -> Data.state -> Data.state * 'o, 'o,'h,'c) ffi | VariadicOut : ('h,'c) ContextualConversion.ctx_readback * ('t,'h,'c) ContextualConversion.t * doc -> ('t oarg list -> depth:int -> 'h -> 'c -> Data.state -> Data.state * ('o * 't option list option), 'o,'h,'c) ffi | VariadicInOut : ('h,'c) ContextualConversion.ctx_readback * ('t ioarg,'h,'c) ContextualConversion.t * doc -> ('t ioarg list -> depth:int -> 'h -> 'c -> Data.state -> Data.state * ('o * 't option list option), 'o,'h,'c) ffi @@ -638,6 +641,51 @@ module BuiltInPredicate : sig end + (** Adaptors for standard HO functions *) + module HOAdaptors : sig + + type 'a pred1 + type ('a,'b) pred2 + type ('a,'b,'c) pred3 + + val pred1 : 'a Conversion.t -> 'a pred1 Conversion.t + val pred2 : 'a Conversion.t -> 'b Conversion.t -> ('a,'b) pred2 Conversion.t + val pred3 : 'a Conversion.t -> 'b Conversion.t -> 'c Conversion.t -> ('a,'b,'c) pred3 Conversion.t + + val filter1 : + once:once -> depth:int -> + filter:(('a -> bool) -> 's -> 's) -> + 'a pred1 -> + 's -> + Data.state -> + Data.state * 's * Conversion.extra_goals + + val filter2 : + once:once -> depth:int -> + filter:(('a -> 'b -> bool) -> 's -> 's) -> + ('a,'b) pred2 -> + 's -> + Data.state -> + Data.state * 's * Conversion.extra_goals + + val map1 : + once:once -> depth:int -> + map:(('a -> 'c) -> 's -> 's) -> + ('a,'c) pred2 -> + 's -> + Data.state -> + Data.state * 's * Conversion.extra_goals + + val map2 : + once:once -> depth:int -> + map:(('a -> 'b -> 'c) -> 's -> 's) -> + ('a,'b,'c) pred3 -> + 's -> + Data.state -> + Data.state * 's * Conversion.extra_goals + + end + end (** Setup.init takes a list of declarations of data types and predicates, diff --git a/src/builtin.elpi b/src/builtin.elpi index 1a6fbc50e..5b281660f 100644 --- a/src/builtin.elpi +++ b/src/builtin.elpi @@ -846,6 +846,16 @@ external pred std.string.map.find i:string, i:std.string.map A, o:A. external pred std.string.map.bindings i:std.string.map A, o:list (pair string A). +% [std.string.map.filter M F M1] Filter M w.r.t. the predicate F +external pred std.string.map.filter i:std.string.map A, + i:(string -> (A -> prop)), + o:std.string.map A. + +% [std.string.map.map M F M1] Map M w.r.t. the predicate F +external pred std.string.map.map i:std.string.map A, + i:(string -> (A -> (B -> prop))), + o:std.string.map B. + % CAVEAT: the type parameter of std.int.map must be a closed term kind std.int.map type -> type. @@ -869,6 +879,15 @@ external pred std.int.map.find i:int, i:std.int.map A, o:A. % [std.int.map.bindings M L] L is M transformed into an associative list external pred std.int.map.bindings i:std.int.map A, o:list (pair int A). +% [std.int.map.filter M F M1] Filter M w.r.t. the predicate F +external pred std.int.map.filter i:std.int.map A, i:(int -> (A -> prop)), + o:std.int.map A. + +% [std.int.map.map M F M1] Map M w.r.t. the predicate F +external pred std.int.map.map i:std.int.map A, + i:(int -> (A -> (B -> prop))), + o:std.int.map B. + % CAVEAT: the type parameter of std.loc.map must be a closed term kind std.loc.map type -> type. @@ -892,6 +911,15 @@ external pred std.loc.map.find i:loc, i:std.loc.map A, o:A. % [std.loc.map.bindings M L] L is M transformed into an associative list external pred std.loc.map.bindings i:std.loc.map A, o:list (pair loc A). +% [std.loc.map.filter M F M1] Filter M w.r.t. the predicate F +external pred std.loc.map.filter i:std.loc.map A, i:(loc -> (A -> prop)), + o:std.loc.map A. + +% [std.loc.map.map M F M1] Map M w.r.t. the predicate F +external pred std.loc.map.map i:std.loc.map A, + i:(loc -> (A -> (B -> prop))), + o:std.loc.map B. + kind std.string.set type. % [std.string.set.empty A] The empty set @@ -932,6 +960,15 @@ external pred std.string.set.elements i:std.string.set, o:list string. % [std.string.set.cardinal M N] N is the number of elements of M external pred std.string.set.cardinal i:std.string.set, o:int. +% [std.string.set.filter M F M1] Filter M w.r.t. the predicate F +external pred std.string.set.filter i:std.string.set, i:(string -> prop), + o:std.string.set. + +% [std.string.set.map M F M1] Map M w.r.t. the predicate F +external pred std.string.set.map i:std.string.set, + i:(string -> (string -> prop)), + o:std.string.set. + kind std.int.set type. % [std.int.set.empty A] The empty set @@ -970,6 +1007,14 @@ external pred std.int.set.elements i:std.int.set, o:list int. % [std.int.set.cardinal M N] N is the number of elements of M external pred std.int.set.cardinal i:std.int.set, o:int. +% [std.int.set.filter M F M1] Filter M w.r.t. the predicate F +external pred std.int.set.filter i:std.int.set, i:(int -> prop), + o:std.int.set. + +% [std.int.set.map M F M1] Map M w.r.t. the predicate F +external pred std.int.set.map i:std.int.set, i:(int -> (int -> prop)), + o:std.int.set. + kind std.loc.set type. % [std.loc.set.empty A] The empty set @@ -1008,6 +1053,14 @@ external pred std.loc.set.elements i:std.loc.set, o:list loc. % [std.loc.set.cardinal M N] N is the number of elements of M external pred std.loc.set.cardinal i:std.loc.set, o:int. +% [std.loc.set.filter M F M1] Filter M w.r.t. the predicate F +external pred std.loc.set.filter i:std.loc.set, i:(loc -> prop), + o:std.loc.set. + +% [std.loc.set.map M F M1] Map M w.r.t. the predicate F +external pred std.loc.set.map i:std.loc.set, i:(loc -> (loc -> prop)), + o:std.loc.set. + #line 0 "builtin_map.elpi" kind std.map type -> type -> type. type std.map std.map.private.map K V -> (K -> K -> cmp -> prop) -> std.map K V. diff --git a/src/builtin.ml b/src/builtin.ml index 978edb5ea..9750a9ba6 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1372,6 +1372,34 @@ set, Easy "N is the number of elements of M")), (fun m _ ~depth -> !: (Set.cardinal m))), DocAbove); + + MLCode(Pred(name^".filter", + In(set,"M", + In(HOAdaptors.pred1 alpha,"F", + Out(set,"M1", + FullHO(ContextualConversion.unit_ctx, "Filter M w.r.t. the predicate F")))), + (fun m f _ ~once ~depth _ _ state -> + + let state, m, gls = HOAdaptors.filter1 ~once ~depth ~filter:Set.filter f m state in + + state, !: m, gls + )), + DocAbove); + + MLCode(Pred(name^".map", + In(set,"M", + In(HOAdaptors.pred2 alpha alpha,"F", + Out(set,"M1", + FullHO(ContextualConversion.unit_ctx, "Map M w.r.t. the predicate F")))), + (fun m f _ ~once ~depth _ _ state -> + + let state, m, gls = HOAdaptors.map1 ~once ~depth ~map:Set.map f m state in + + state, !: m, gls + )), + DocAbove); + + ] ;; let ocaml_set ~name c m = snd (ocaml_set_conv ~name c m) @@ -1380,6 +1408,7 @@ let ocaml_map ~name (type a) (alpha : a Conversion.t) (module Map : Util.Map.S with type key = a) = let closed_A = BuiltInData.closed "A" in +let closed_B = BuiltInData.closed "B" in let map = OpaqueData.declare { OpaqueData.name; @@ -1448,6 +1477,33 @@ let open BuiltIn in let open BuiltInData in (fun m _ ~depth -> !: (Map.bindings m))), DocAbove); + MLCode(Pred(name^".filter", + In(map "A","M", + In(HOAdaptors.pred2 alpha closed_A,"F", + Out(map "A","M1", + FullHO(ContextualConversion.unit_ctx, "Filter M w.r.t. the predicate F")))), + (fun m f _ ~once ~depth _ _ state -> + + let state, m, gls = HOAdaptors.filter2 ~once ~depth ~filter:Map.filter f m state in + + state, !: m, gls + )), + DocAbove); + + MLCode(Pred(name^".map", + In(map "A","M", + In(HOAdaptors.pred3 alpha closed_A closed_B,"F", + Out(map "B","M1", + FullHO(ContextualConversion.unit_ctx, "Map M w.r.t. the predicate F")))), + (fun m f _ ~once ~depth _ _ state -> + + let state, m, gls = HOAdaptors.map2 ~once ~depth ~map:Map.mapi f m state in + + state, !: m, gls + )), + DocAbove); + + ] ;; diff --git a/src/data.ml b/src/data.ml index 721d2d3a2..77b4ff63a 100644 --- a/src/data.ml +++ b/src/data.ml @@ -902,6 +902,7 @@ type ('function_type, 'inernal_outtype_in, 'internal_hyps, 'internal_constraints | Easy : doc -> (depth:int -> 'o, 'o,unit,unit) ffi | Read : ('h,'c) ContextualConversion.ctx_readback * doc -> (depth:int -> 'h -> 'c -> State.t -> 'o, 'o,'h,'c) ffi | Full : ('h,'c) ContextualConversion.ctx_readback * doc -> (depth:int -> 'h -> 'c -> State.t -> State.t * 'o * Conversion.extra_goals, 'o,'h,'c) ffi + | FullHO : ('h,'c) ContextualConversion.ctx_readback * doc -> (once:(depth:int -> term -> State.t -> State.t) -> depth:int -> 'h -> 'c -> State.t -> State.t * 'o * Conversion.extra_goals, 'o,'h,'c) ffi | VariadicIn : ('h,'c) ContextualConversion.ctx_readback * ('t,'h,'c) ContextualConversion.t * doc -> ('t list -> depth:int -> 'h -> 'c -> State.t -> State.t * 'o, 'o,'h,'c) ffi | VariadicOut : ('h,'c) ContextualConversion.ctx_readback * ('t,'h,'c) ContextualConversion.t * doc -> ('t oarg list -> depth:int -> 'h -> 'c -> State.t -> State.t * ('o * 't option list option), 'o,'h,'c) ffi | VariadicInOut : ('h,'c) ContextualConversion.ctx_readback * ('t ioarg,'h,'c) ContextualConversion.t * doc -> ('t ioarg list -> depth:int -> 'h -> 'c -> State.t -> State.t * ('o * 't option list option), 'o,'h,'c) ffi @@ -1265,6 +1266,7 @@ let document_pred fmt docspec name ffi = | Read (_,s) -> pp_pred fmt docspec name s args | Easy s -> pp_pred fmt docspec name s args | Full (_,s) -> pp_pred fmt docspec name s args + | FullHO (_,s) -> pp_pred fmt docspec name s args | VariadicIn( _,{ ContextualConversion.ty }, s) -> pp_variadictype fmt name s (Conversion.show_ty_ast ty) args | VariadicOut( _,{ ContextualConversion.ty }, s) -> pp_variadictype fmt name s (Conversion.show_ty_ast ty) args | VariadicInOut( _,{ ContextualConversion.ty }, s) -> pp_variadictype fmt name s (Conversion.show_ty_ast ty) args diff --git a/src/runtime.ml b/src/runtime.ml index 11c1f3d66..2ccfc64d3 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2135,7 +2135,7 @@ let map_acc f s l = in aux [] [] s l -let call (Data.BuiltInPredicate.Pred(bname,ffi,compute)) ~depth hyps constraints state data = +let call (Data.BuiltInPredicate.Pred(bname,ffi,compute)) ~once ~depth hyps constraints state data = let rec aux : type i o h c. (i,o,h,c) Data.BuiltInPredicate.ffi -> h -> c -> compute:i -> reduce:(State.t -> o -> State.t * Conversion.extra_goals) -> term list -> int -> State.t -> Conversion.extra_goals list -> State.t * Conversion.extra_goals = @@ -2153,6 +2153,10 @@ let call (Data.BuiltInPredicate.Pred(bname,ffi,compute)) ~depth hyps constraints let state, result, gls = wrap_type_err bname 0 (compute ~depth ctx constraints) state in let state, l = reduce state result in state, List.(concat (rev extra)) @ gls @ List.rev l + | Data.BuiltInPredicate.FullHO _, [] -> + let state, result, gls = wrap_type_err bname 0 (compute ~once ~depth ctx constraints) state in + let state, l = reduce state result in + state, List.(concat (rev extra)) @ gls @ List.rev l | Data.BuiltInPredicate.VariadicIn(_,{ ContextualConversion.readback }, _), data -> let state, i, gls = map_acc (in_of_termC ~depth readback n bname ctx constraints) state data in @@ -2222,6 +2226,7 @@ let call (Data.BuiltInPredicate.Pred(bname,ffi,compute)) ~depth hyps constraints in let rec aux_ctx : type i o h c. (i,o,h,c) Data.BuiltInPredicate.ffi -> (h,c) ContextualConversion.ctx_readback = function + | Data.BuiltInPredicate.FullHO(f,_) -> f | Data.BuiltInPredicate.Full(f,_) -> f | Data.BuiltInPredicate.Read(f,_) -> f | Data.BuiltInPredicate.VariadicIn(f,_,_) -> f @@ -2995,6 +3000,7 @@ module Constraints : sig (* out of place *) val exect_builtin_predicate : + once:(depth:int -> term -> State.t -> State.t) -> constant -> depth:int -> prolog_prog -> (UUID.t[@trace]) -> term list -> term list end = struct (* {{{ *) @@ -3284,7 +3290,7 @@ let declare_constraint ~depth prog (gid[@trace]) args = ~depth prog ~goal:g (gid[@trace]) ~on:keys | None -> delay_goal ~depth prog ~goal:g (gid[@trace]) ~on:keys -let exect_builtin_predicate c ~depth idx (gid[@trace]) args = +let exect_builtin_predicate ~once c ~depth idx (gid[@trace]) args = if c == Global_symbols.declare_constraintc then begin declare_constraint ~depth idx (gid[@trace]) args; [] end else if c == Global_symbols.print_constraintsc then begin @@ -3297,7 +3303,7 @@ let exect_builtin_predicate c ~depth idx (gid[@trace]) args = anomaly ("no built-in predicated named " ^ C.show c) in let constraints = !CS.Ugly.delayed in let state = !CS.state in - let state, gs = FFI.call b ~depth (local_prog idx) constraints state args in + let state, gs = FFI.call b ~once ~depth (local_prog idx) constraints state args in let state, gs = State.get Data.Conversion.extra_goals_postprocessing state gs state in CS.state := state; List.map Data.Conversion.term_of_extra_goal gs @@ -3706,7 +3712,12 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses]; [%tcall backchain depth p (k, x, xs, gs) (gid[@trace]) next alts cutto_alts clauses] | Builtin(c, args) -> [%spy "user:rule" ~rid ~gid pp_string "builtin"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (C.show c)]; - begin match Constraints.exect_builtin_predicate c ~depth p (gid[@trace]) args with + let once ~depth g state = + CS.state := state; + let { depth; program; goal; gid = gid [@trace] } = (make_subgoal[@inlined]) (gid[@trace]) ~depth p g in + let _alts = run depth program goal (gid[@trace]) [] FNil noalts noalts in + !CS.state in + begin match Constraints.exect_builtin_predicate ~once c ~depth p (gid[@trace]) args with | gs' -> [%spy "user:rule:builtin" ~rid ~gid pp_string "success"]; (match List.map (fun g -> (make_subgoal[@inlined]) (gid[@trace]) ~depth p g) gs' @ gs with diff --git a/tests/sources/map_ho.elpi b/tests/sources/map_ho.elpi new file mode 100644 index 000000000..3b6a3ed09 --- /dev/null +++ b/tests/sources/map_ho.elpi @@ -0,0 +1,4 @@ +main :- + std.fold {std.iota 9} {std.int.map.empty} (i\std.int.map.add i (x\x)) S, + std.int.map.map S (x\f\r\ pi _\ r = f x) S1, + print S1. \ No newline at end of file diff --git a/tests/sources/set_ho.elpi b/tests/sources/set_ho.elpi new file mode 100644 index 000000000..99bca742e --- /dev/null +++ b/tests/sources/set_ho.elpi @@ -0,0 +1,10 @@ +main :- + std.fold {std.iota 999999} {std.int.set.empty} std.int.set.add S, + std.time (std.int.set.filter S (x\0 is x mod 123) S1) T1, + std.int.set.cardinal S1 N, + std.time (std.filter {std.int.set.elements S} (x\0 is x mod 123) L, std.fold L {std.int.set.empty} std.int.set.add S2) T2, + std.int.set.cardinal S2 M, + std.assert! (N = M) "wrong card filter", + print T1 " < " T2, + std.int.set.map S1 (_\r\ r = 1) S3, + std.assert! (std.int.set.cardinal S3 1) "wrong card map". \ No newline at end of file diff --git a/tests/suite/performance_FO.ml b/tests/suite/performance_FO.ml index 1963cf106..1d588bfc8 100644 --- a/tests/suite/performance_FO.ml +++ b/tests/suite/performance_FO.ml @@ -74,11 +74,20 @@ let () = declare "map (builtin list)" ~source_elpi:"map_list_opt.elpi" ~description:"stdlib map reference" () +let () = declare "map_ho" + ~source_elpi:"map_ho.elpi" + ~description:"stdlib map HO" + () let () = declare "set" ~source_elpi:"set.elpi" ~description:"stdlib set" () +let () = declare "set_ho" + ~source_elpi:"set_ho.elpi" + ~description:"stdlib set HO" + () + let () = declare "dt" ~source_elpi:"dt.elpi" From 58b38ba6054eb5fe281a11318d226ead7d4fd424 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Nov 2023 13:16:33 +0100 Subject: [PATCH 3/4] changelog --- CHANGES.md | 2 ++ src/builtin.elpi | 26 ++++++++++++-------------- src/builtin.ml | 1 - src/data.ml | 24 +++++++++++++++++++++--- tests/sources/set_ho.elpi | 2 +- 5 files changed, 36 insertions(+), 19 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 7dea45984..f8ad5526b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,8 @@ API: query is run, even if the query is given as an ast. - New `Utils.relocate_closed_term` to move a term from one runtime to another (experimental) + - New `BuiltInPredicate.FullHO` for higher order external predicates + - New `BuiltInPredicate.HOAdaptors` for `map` and `filter` like HO predicates Library: - New `std.fold-right` diff --git a/src/builtin.elpi b/src/builtin.elpi index 5b281660f..91d68ad4e 100644 --- a/src/builtin.elpi +++ b/src/builtin.elpi @@ -848,12 +848,12 @@ external pred std.string.map.bindings i:std.string.map A, % [std.string.map.filter M F M1] Filter M w.r.t. the predicate F external pred std.string.map.filter i:std.string.map A, - i:(string -> (A -> prop)), + i:string -> A -> prop, o:std.string.map A. % [std.string.map.map M F M1] Map M w.r.t. the predicate F external pred std.string.map.map i:std.string.map A, - i:(string -> (A -> (B -> prop))), + i:string -> A -> B -> prop, o:std.string.map B. % CAVEAT: the type parameter of std.int.map must be a closed term @@ -880,12 +880,11 @@ external pred std.int.map.find i:int, i:std.int.map A, o:A. external pred std.int.map.bindings i:std.int.map A, o:list (pair int A). % [std.int.map.filter M F M1] Filter M w.r.t. the predicate F -external pred std.int.map.filter i:std.int.map A, i:(int -> (A -> prop)), +external pred std.int.map.filter i:std.int.map A, i:int -> A -> prop, o:std.int.map A. % [std.int.map.map M F M1] Map M w.r.t. the predicate F -external pred std.int.map.map i:std.int.map A, - i:(int -> (A -> (B -> prop))), +external pred std.int.map.map i:std.int.map A, i:int -> A -> B -> prop, o:std.int.map B. % CAVEAT: the type parameter of std.loc.map must be a closed term @@ -912,12 +911,11 @@ external pred std.loc.map.find i:loc, i:std.loc.map A, o:A. external pred std.loc.map.bindings i:std.loc.map A, o:list (pair loc A). % [std.loc.map.filter M F M1] Filter M w.r.t. the predicate F -external pred std.loc.map.filter i:std.loc.map A, i:(loc -> (A -> prop)), +external pred std.loc.map.filter i:std.loc.map A, i:loc -> A -> prop, o:std.loc.map A. % [std.loc.map.map M F M1] Map M w.r.t. the predicate F -external pred std.loc.map.map i:std.loc.map A, - i:(loc -> (A -> (B -> prop))), +external pred std.loc.map.map i:std.loc.map A, i:loc -> A -> B -> prop, o:std.loc.map B. kind std.string.set type. @@ -961,12 +959,12 @@ external pred std.string.set.elements i:std.string.set, o:list string. external pred std.string.set.cardinal i:std.string.set, o:int. % [std.string.set.filter M F M1] Filter M w.r.t. the predicate F -external pred std.string.set.filter i:std.string.set, i:(string -> prop), +external pred std.string.set.filter i:std.string.set, i:string -> prop, o:std.string.set. % [std.string.set.map M F M1] Map M w.r.t. the predicate F external pred std.string.set.map i:std.string.set, - i:(string -> (string -> prop)), + i:string -> string -> prop, o:std.string.set. kind std.int.set type. @@ -1008,11 +1006,11 @@ external pred std.int.set.elements i:std.int.set, o:list int. external pred std.int.set.cardinal i:std.int.set, o:int. % [std.int.set.filter M F M1] Filter M w.r.t. the predicate F -external pred std.int.set.filter i:std.int.set, i:(int -> prop), +external pred std.int.set.filter i:std.int.set, i:int -> prop, o:std.int.set. % [std.int.set.map M F M1] Map M w.r.t. the predicate F -external pred std.int.set.map i:std.int.set, i:(int -> (int -> prop)), +external pred std.int.set.map i:std.int.set, i:int -> int -> prop, o:std.int.set. kind std.loc.set type. @@ -1054,11 +1052,11 @@ external pred std.loc.set.elements i:std.loc.set, o:list loc. external pred std.loc.set.cardinal i:std.loc.set, o:int. % [std.loc.set.filter M F M1] Filter M w.r.t. the predicate F -external pred std.loc.set.filter i:std.loc.set, i:(loc -> prop), +external pred std.loc.set.filter i:std.loc.set, i:loc -> prop, o:std.loc.set. % [std.loc.set.map M F M1] Map M w.r.t. the predicate F -external pred std.loc.set.map i:std.loc.set, i:(loc -> (loc -> prop)), +external pred std.loc.set.map i:std.loc.set, i:loc -> loc -> prop, o:std.loc.set. #line 0 "builtin_map.elpi" diff --git a/src/builtin.ml b/src/builtin.ml index 9750a9ba6..6a1310a56 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1503,7 +1503,6 @@ let open BuiltIn in let open BuiltInData in )), DocAbove); - ] ;; diff --git a/src/data.ml b/src/data.ml index 77b4ff63a..d632ff9ef 100644 --- a/src/data.ml +++ b/src/data.ml @@ -713,11 +713,29 @@ module Conversion = struct exception TypeErr of ty_ast * int * term (* a type error at data conversion time *) -let rec show_ty_ast ?(outer=true) = function +type prec_level = + | Arrow + | AppArg + +let need_par x y = + match x,y with + | Some AppArg, Arrow -> true + | Some AppArg, AppArg -> true + | Some Arrow, Arrow -> true + | Some Arrow, AppArg -> false + | None, _ -> false + +let with_par p1 p2 s = if need_par p1 p2 then "("^s^")" else s + +let rec show_ty_ast ?prec = function | TyName s -> s + | TyApp ("->",src,[tgt]) -> + let src = show_ty_ast ~prec:Arrow src in + let tgt = show_ty_ast tgt in + with_par prec Arrow (src ^" -> "^ tgt) | TyApp (s,x,xs) -> - let t = String.concat " " (s :: List.map (show_ty_ast ~outer:false) (x::xs)) in - if outer then t else "("^t^")" + let t = String.concat " " (s :: List.map (show_ty_ast ~prec:AppArg) (x::xs)) in + with_par prec AppArg t let term_of_extra_goal = function | Unify(a,b) -> Builtin(Global_symbols.eqc,[a;b]) diff --git a/tests/sources/set_ho.elpi b/tests/sources/set_ho.elpi index 99bca742e..cbe7048ef 100644 --- a/tests/sources/set_ho.elpi +++ b/tests/sources/set_ho.elpi @@ -1,5 +1,5 @@ main :- - std.fold {std.iota 999999} {std.int.set.empty} std.int.set.add S, + std.fold {std.iota 99999} {std.int.set.empty} std.int.set.add S, std.time (std.int.set.filter S (x\0 is x mod 123) S1) T1, std.int.set.cardinal S1 N, std.time (std.filter {std.int.set.elements S} (x\0 is x mod 123) L, std.fold L {std.int.set.empty} std.int.set.add S2) T2, From 9c300cceaccfd13ae6a810aae2656aee685b6a13 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Nov 2023 09:52:07 +0100 Subject: [PATCH 4/4] fix test --- tests/sources/trace_chr.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/sources/trace_chr.json b/tests/sources/trace_chr.json index 49377dfae..51da5305f 100644 --- a/tests/sources/trace_chr.json +++ b/tests/sources/trace_chr.json @@ -96,7 +96,7 @@ {"step" : 13,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X1"]} {"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]} {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 2, column 3, character 25:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]} -{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--484 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--496 []"]} {"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]} {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]} {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]} @@ -104,7 +104,7 @@ {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["fail"]} {"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:rule-failed","payload" : []} {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 3, column 3, character 71:"," \\ (even A0) (odd A0) | (odd (s z)) <=> (fail)"]} -{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--485 []"]} +{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--497 []"]} {"step" : 0,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]} {"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]} {"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}