Merge pull request #210 from LPCIC/HO-API

HO api

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`

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
 
@@ -806,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
 
@@ -877,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 "<pred1>"); 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 "<pred2>"); 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 "<pred3>"); 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
@@ -993,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

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 *)
@@ -556,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
@@ -574,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
@@ -637,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,

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,14 @@ 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 +910,14 @@ 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 +958,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 +1005,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 +1051,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.