From 1b08a68af1d5e767797ff9c34e967c13bc0fa012 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Apr 2020 22:04:49 +0200 Subject: [PATCH] fix query type --- src/.ppcache/API.ml | 211 ++++++++++++++++------------- src/.ppcache/API.mli | 66 ++++----- src/.ppcache/compiler.ml | 58 ++++---- src/.ppcache/compiler.mli | 8 +- src/.ppcache/data.ml | 55 ++++++-- src/.ppcache/runtime_trace_off.ml | 98 +++++++------- src/.ppcache/runtime_trace_off.mli | 6 +- src/.ppcache/runtime_trace_on.ml | 98 +++++++------- src/.ppcache/runtime_trace_on.mli | 6 +- src/API.ml | 151 +++++++++++---------- src/API.mli | 53 ++++---- src/builtin.ml | 38 ++++-- src/compiler.ml | 39 +++--- src/compiler.mli | 2 +- src/data.ml | 45 ++++-- src/runtime.ml | 46 ++++--- src/runtime.mli | 2 +- 17 files changed, 559 insertions(+), 423 deletions(-) diff --git a/src/.ppcache/API.ml b/src/.ppcache/API.ml index ceb4b7bf2..add18dbb2 100644 --- a/src/.ppcache/API.ml +++ b/src/.ppcache/API.ml @@ -1,4 +1,4 @@ -(*09dd92d029bc5129509dbb9e46c435ff8be4de41 *src/API.ml --cookie elpi_trace="false"*) +(*3945de0aacc72f43356fcba834b89bc2bd5836f5 *src/API.ml --cookie elpi_trace="false"*) #1 "src/API.ml" module type Runtime = module type of Runtime_trace_off let r = ref ((module Runtime_trace_off) : (module Runtime)) @@ -204,10 +204,103 @@ module Conversion = fun s -> fun x -> t.readback ~depth ((new ctx) h#raw) c s x) } end +module OpaqueData = + struct + include Util.CData + include ED.C + type name = string + type doc = string + type 'a declaration = + { + name: name ; + cname: name ; + doc: doc ; + pp: Format.formatter -> 'a -> unit ; + compare: 'a -> 'a -> int ; + hash: 'a -> int ; + hconsed: bool ; + constants: (name * 'a) list } + type 'a cdata_with_constants = + ('a cdata * name * (string * 'a) ED.Constants.Map.t * doc) + let rest ({ cin; name = c }, name, constants_map, doc) = + ((Conversion.TyName name), (fun fmt -> fun x -> pp fmt (cin x)), + (fun fmt -> + fun () -> + let module R = (val !r) in + let open R in + if doc <> "" + then + (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); + Format.fprintf fmt "@\n"); + Format.fprintf fmt + "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; + ED.Constants.Map.iter + (fun _ -> + fun (c, _) -> + Format.fprintf fmt "@[type %s %s.@]@\n" c name) + constants_map)) + let embed ({ cin;_}, _, _, _) = + (); + (fun ~depth:_ -> + fun _ -> + fun _ -> + fun state -> fun x -> (state, (ED.Term.CData (cin x)), [])) + let readback ({ isc; cout;_}, name, constants_map, _) = + (); + (fun ~depth -> + fun _ -> + fun _ -> + fun state -> + fun t -> + let module R = (val !r) in + let open R in + match R.deref_head ~depth t with + | ED.Term.CData c when isc c -> (state, (cout c), []) + | ED.Term.Const i as t when i < 0 -> + (try + (state, + (snd @@ (ED.Constants.Map.find i constants_map)), + []) + with + | Not_found -> + raise + (Conversion.TypeErr + ((Conversion.TyName name), depth, t))) + | t -> + raise + (Conversion.TypeErr + ((Conversion.TyName name), depth, t))) + let declare { name; cname; doc; pp; compare; hash; hconsed; constants } = + let cdata = + declare + { + data_compare = compare; + data_pp = pp; + data_hash = hash; + data_name = cname; + data_hconsed = hconsed + } in + (cdata, name, + (List.fold_right + (fun (n, v) -> + ED.Constants.Map.add + (ED.Global_symbols.declare_global_symbol n) (n, v)) constants + ED.Constants.Map.empty), doc) + let build_conversion x = + let (ty, pp, pp_doc) = rest x in + { + Conversion.ty = ty; + pp; + pp_doc; + embed = (embed x); + readback = (readback x) + } + end module RawOpaqueData = struct include Util.CData include ED.C + let cdata (c, _, _, _) = c let { cin = of_char; isc = is_char; cout = to_char } as char = declare { @@ -244,88 +337,6 @@ module RawOpaqueData = data_hconsed = false } let of_in_stream x = ED.mkCData (of_in_stream x) - type name = string - type doc = string - type 'a declaration = - { - name: name ; - doc: doc ; - pp: Format.formatter -> 'a -> unit ; - compare: 'a -> 'a -> int ; - hash: 'a -> int ; - hconsed: bool ; - constants: (name * 'a) list } - let conversion_of_cdata ~name ?(doc= "") ~constants_map - { cin; isc; cout; name = c } = - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try - (state, (snd @@ (ED.Constants.Map.find i constants_map)), - []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - ED.Constants.Map.iter - (fun _ -> - fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants_map in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> pp fmt (cin x)) - } - let declare { name; doc; pp; compare; hash; hconsed; constants } = - let cdata = - declare - { - data_compare = compare; - data_pp = pp; - data_hash = hash; - data_name = name; - data_hconsed = hconsed - } in - (cdata, - (List.fold_right - (fun (n, v) -> - ED.Constants.Map.add - (ED.Global_symbols.declare_global_symbol n) (n, v)) constants - ED.Constants.Map.empty), doc) - let declare_cdata (cd, constants_map, doc) = - conversion_of_cdata ~name:(cd.Util.CData.name) ~doc ~constants_map cd - end -module OpaqueData = - struct - type name = string - type doc = string - type 'a declaration = 'a RawOpaqueData.declaration = - { - name: name ; - doc: doc ; - pp: Format.formatter -> 'a -> unit ; - compare: 'a -> 'a -> int ; - hash: 'a -> int ; - hconsed: bool ; - constants: (name * 'a) list } - let declare x = - (x |> RawOpaqueData.declare) |> RawOpaqueData.declare_cdata end module Elpi = struct @@ -1181,20 +1192,28 @@ module BuiltInPredicate = module Query = struct type name = string - type 'f arguments = 'f ED.Query.arguments = - | N: unit arguments - | D: ('a, Conversion.ctx) Conversion.t * 'a * 'x arguments -> 'x - arguments - | Q: ('a, Conversion.ctx) Conversion.t * name * 'x arguments -> ('a * - 'x) arguments - type 'x t = - | Query of { - predicate: name ; - arguments: 'x arguments } - let compile (state, p) loc (Query { predicate; arguments }) = + type ('f, 'c) arguments = ('f, 'c) ED.Query.arguments = + | N: (unit, 'c) arguments + | D: ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments + -> ('x, 'c) arguments + | Q: ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) + arguments -> (('a * 'x), 'c) arguments + type 'c obj_builder = Data.state -> 'c constraint 'c = #Conversion.ctx + type _ t = + | Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx) + Conversion.context * 'c obj_builder -> 'x t + and ('a, 'x, 'c) query_contents = + { + context: 'a list ; + predicate: string ; + arguments: ('x, 'c) arguments } + let compile (state, p) loc (Query + ({ predicate; arguments; context }, cc, obj)) = let (state, predicate) = Compiler.Symbols.allocate_global_symbol_str state predicate in - let q = ED.Query.Query { predicate; arguments } in + let q = + let open ED.Query in + Query ({ predicate; arguments; context }, cc, obj) in Compiler.query_of_data state p loc q end module State = @@ -1210,6 +1229,8 @@ module RawQuery = struct let mk_Arg = Compiler.mk_Arg let is_Arg = Compiler.is_Arg + type 'a query_readback = + Data.term Data.StrMap.t -> Data.constraints -> State.t -> 'a let compile (state, p) f = Compiler.query_of_term state p f end module Quotation = diff --git a/src/.ppcache/API.mli b/src/.ppcache/API.mli index 2549891bc..78d96292d 100644 --- a/src/.ppcache/API.mli +++ b/src/.ppcache/API.mli @@ -1,4 +1,4 @@ -(*262f7f42585df543898448e5ff436973e6f64995 *src/API.mli --cookie elpi_trace="false"*) +(*17cbedc324e731e950a3163806e4dddda4081e81 *src/API.mli --cookie elpi_trace="false"*) #1 "src/API.mli" [@@@ocaml.text " This module is the API for clients of the Elpi library. "] [@@@ocaml.text @@ -215,6 +215,7 @@ sig type 'a declaration = { name: name ; + cname: name ; doc: doc ; pp: Format.formatter -> 'a -> unit ; compare: 'a -> 'a -> int ; @@ -222,7 +223,15 @@ sig hconsed: bool ; constants: (name * 'a) list }[@@ocaml.doc " The [eq] function is used by unification. Limitation: unification of\n * two cdata cannot alter the constraint store. This can be lifted in the\n * future if there is user request.\n *\n * If the hconsed is true, then the [readback] function is\n * automatically hashcons the data using the [eq] and [hash] functions.\n "] - val declare : 'a declaration -> ('a, 'c) Conversion.t + type 'a cdata_with_constants + val declare : 'a declaration -> 'a cdata_with_constants + val build_conversion : 'a cdata_with_constants -> ('a, 'c) Conversion.t + val embed : 'a cdata_with_constants -> ('a, 'c) Conversion.embedding + val readback : 'a cdata_with_constants -> ('a, 'c) Conversion.readback + val rest : + 'a cdata_with_constants -> + (Conversion.ty_ast * (Format.formatter -> 'a -> unit) * + (Format.formatter -> unit -> unit)) end[@@ocaml.doc " Declare data from the host application that is opaque (no syntax), like\n int but not like list or pair "] module AlgebraicData : @@ -350,16 +359,21 @@ end[@@ocaml.doc module Query : sig type name = string - type _ arguments = - | N: unit arguments - | D: ('a, Conversion.ctx) Conversion.t * 'a * 'x arguments -> 'x - arguments - | Q: ('a, Conversion.ctx) Conversion.t * name * 'x arguments -> ('a * 'x) - arguments - type 'x t = - | Query of { - predicate: name ; - arguments: 'x arguments } + type (_, _) arguments = + | N: (unit, 'c) arguments + | D: ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments + -> ('x, 'c) arguments + | Q: ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) arguments + -> (('a * 'x), 'c) arguments + type 'c obj_builder = Data.state -> 'c constraint 'c = #Conversion.ctx + type _ t = + | Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx) + Conversion.context * 'c obj_builder -> 'x t + and ('a, 'x, 'c) query_contents = + { + context: 'a list ; + predicate: string ; + arguments: ('x, 'c) arguments } val compile : Compile.program -> Ast.Loc.t -> 'a t -> 'a Compile.query end[@@ocaml.doc " Commodity module to build a simple query\n and extract the output from the solution found by Elpi.\n\n Example: \"foo data Output\" where [data] has type [t] ([a] is [t Conversion.t])\n and [Output] has type [v] ([b] is a [v Conversion.t]) can be described as:\n{[\n\n let q : (v * unit) t = Query {\n predicate = \"foo\";\n arguments = D(a, data,\n Q(b, \"Output\",\n N))\n }\n\n ]}\n\n Then [compile q] can be used to obtain the compiled query such that the\n resulting solution has a fied output of type [(v * unit)]. Example:\n{[\n\n Query.compile q |> Compile.link |> Execute.once |> function\n | Execute.Success { output } -> output\n | _ -> ...\n\n ]} "] @@ -503,30 +517,15 @@ sig end module RawOpaqueData : sig - type name = string - type doc = string type t - type 'a declaration = 'a OpaqueData.declaration = - { - name: name ; - doc: doc ; - pp: Format.formatter -> 'a -> unit ; - compare: 'a -> 'a -> int ; - hash: 'a -> int ; - hconsed: bool ; - constants: (name * 'a) list }[@@ocaml.doc - " If the data_hconsed is true, then the [cin] function below will\n automatically hashcons the data using the [eq] and [hash] functions. "] type 'a cdata = private { cin: 'a -> t ; isc: t -> bool ; cout: t -> 'a ; - name: string } - val declare : - 'a declaration -> ('a cdata * (name * 'a) Data.Constants.Map.t * string) - val declare_cdata : - ('a cdata * (name * 'a) Data.Constants.Map.t * string) -> - ('a, 'c) Conversion.t + name: string }[@@ocaml.doc + " If the data_hconsed is true, then the [cin] function below will\n automatically hashcons the data using the [eq] and [hash] functions. "] + val cdata : 'a OpaqueData.cdata_with_constants -> 'a cdata val pp : Format.formatter -> t -> unit val show : t -> string val equal : t -> t -> bool @@ -622,13 +621,16 @@ sig Data.state -> name:string -> args:Data.term list -> (Data.state * Data.term) val is_Arg : Data.state -> Data.term -> bool + type 'a query_readback = + Data.term Data.StrMap.t -> Data.constraints -> State.t -> 'a val compile : Compile.program -> (depth:int -> Data.hyps -> Data.constraints -> - Data.state -> (Data.state * (Ast.Loc.t * Data.term))) - -> unit Compile.query + Data.state -> + (Data.state * (Ast.Loc.t * Data.term) * 'a query_readback)) + -> 'a Compile.query end[@@ocaml.doc " This module lets one generate a query by providing a RawData.term directly "] module Quotation : diff --git a/src/.ppcache/compiler.ml b/src/.ppcache/compiler.ml index 2fcc25de2..aeaad9199 100644 --- a/src/.ppcache/compiler.ml +++ b/src/.ppcache/compiler.ml @@ -1,4 +1,4 @@ -(*460c62986d53adb8c20297ac71da3ae5b3c7414a *src/compiler.ml *) +(*456a86c1e7ead6322ffd1d9e45fcecda7099e3ac *src/compiler.ml *) #1 "src/compiler.ml" open Util module F = Ast.Func @@ -1238,7 +1238,7 @@ module WithMain = chr: (constant list * prechr_rule list) list ; initial_depth: int ; query: preterm ; - query_arguments: 'a Query.arguments [@opaque ]; + query_readback: 'a query_readback [@opaque ]; initial_goal: term ; assignments: term StrMap.t ; compiler_state: State.t }[@@deriving show] @@ -1385,10 +1385,10 @@ module WithMain = Ppx_deriving_runtime_proxy.Format.fprintf fmt "@]"); Ppx_deriving_runtime_proxy.Format.fprintf fmt ";@ "; Ppx_deriving_runtime_proxy.Format.fprintf fmt "@[%s =@ " - "query_arguments"; + "query_readback"; ((fun _ -> Ppx_deriving_runtime_proxy.Format.pp_print_string fmt - "")) x.query_arguments; + "")) x.query_readback; Ppx_deriving_runtime_proxy.Format.fprintf fmt "@]"); Ppx_deriving_runtime_proxy.Format.fprintf fmt ";@ "; Ppx_deriving_runtime_proxy.Format.fprintf fmt "@[%s =@ " @@ -1651,12 +1651,14 @@ module ToDBL : val query_preterm_of_ast : depth:int -> macro_declaration -> - State.t -> (Loc.t * Ast.Term.t) -> (State.t * preterm) + State.t -> + (Loc.t * Ast.Term.t) -> (State.t * preterm * unit query_readback) val query_preterm_of_function : depth:int -> macro_declaration -> State.t -> - (State.t -> (State.t * (Loc.t * term))) -> (State.t * preterm) + (State.t -> (State.t * (Loc.t * term) * 'a query_readback)) -> + (State.t * preterm * 'a query_readback) val lp : quotation val is_Arg : State.t -> term -> bool val fresh_Arg : @@ -1911,12 +1913,13 @@ module ToDBL : let query_preterm_of_function ~depth macros state f = assert (is_empty_amap (get_argmap state)); (let state = set_mtm state (Some { macros }) in - let (state, (loc, term)) = f state in - let amap = get_argmap state in (state, { amap; term; loc })) + let (state, (loc, term), readback) = f state in + let amap = get_argmap state in (state, { amap; term; loc }, readback)) let query_preterm_of_ast ~depth macros state (loc, t) = assert (is_empty_amap (get_argmap state)); (let (state, term) = preterm_of_ast loc ~depth macros state t in - let amap = get_argmap state in (state, { term; amap; loc })) + let amap = get_argmap state in + (state, { term; amap; loc }, (fun _ -> fun _ -> fun _ -> ()))) open Ast.Structured let check_no_overlap_macros _ _ = () let compile_macro m { Ast.Macro.loc = loc; name = n; body } = @@ -2938,7 +2941,7 @@ let query_of_ast compiler_state assembled_program t = let type_abbrevs = assembled_program.Assembled.type_abbrevs in let modes = assembled_program.Assembled.modes in let active_macros = assembled_program.Assembled.toplevel_macros in - let (state, query) = + let (state, query, query_readback) = ToDBL.query_preterm_of_ast ~depth:initial_depth active_macros compiler_state t in let query = @@ -2958,7 +2961,7 @@ let query_of_ast compiler_state assembled_program t = chr = (assembled_program.Assembled.chr); initial_depth; query; - query_arguments = Query.N; + query_readback; initial_goal; assignments; compiler_state = (state |> (uvbodies_of_assignments assignments)) @@ -2969,7 +2972,7 @@ let query_of_term compiler_state assembled_program f = let type_abbrevs = assembled_program.Assembled.type_abbrevs in let modes = assembled_program.Assembled.modes in let active_macros = assembled_program.Assembled.toplevel_macros in - let (state, query) = + let (state, query, query_readback) = ToDBL.query_preterm_of_function ~depth:initial_depth active_macros compiler_state (f ~depth:initial_depth [] []) in let query_env = Array.make (query.amap).nargs D.dummy in @@ -2987,22 +2990,20 @@ let query_of_term compiler_state assembled_program f = chr = (assembled_program.Assembled.chr); initial_depth; query; - query_arguments = Query.N; + query_readback; initial_goal; assignments; compiler_state = (state |> (uvbodies_of_assignments assignments)) } -let query_of_data state p loc (Query.Query { arguments } as descr) = - let query = - query_of_term state p - (fun ~depth -> - fun hyps -> - fun constraints -> - fun state -> - let (state, term) = - R.embed_query ~mk_Arg ~depth hyps constraints state descr in - (state, (loc, term))) in - { query with query_arguments = arguments } +let query_of_data state p loc qdescr = + query_of_term state p + (fun ~depth -> + fun hyps -> + fun constraints -> + fun state -> + let ((state, term), query_readback) = + R.embed_query ~mk_Arg ~depth hyps constraints state qdescr in + (state, (loc, term), query_readback)) module Compiler : sig val run : 'a query -> 'a executable end = struct let compile_chr depth state @@ -3075,7 +3076,7 @@ module Compiler : sig val run : 'a query -> 'a executable end = with | Not_found -> () let run { WithMain.types = types; modes; clauses; chr; initial_depth; - initial_goal; assignments; compiler_state = state; query_arguments } + initial_goal; assignments; compiler_state = state; query_readback } = let flags = State.get compiler_flags state in check_all_builtin_are_typed state types; @@ -3140,7 +3141,7 @@ module Compiler : sig val run : 'a query -> 'a executable end = initial_goal; initial_runtime_state = (State.end_compilation state); assignments; - query_arguments; + query_readback; symbol_table; builtins })) @@ -3319,7 +3320,7 @@ let term_of_ast ~depth state t = ToDBL.temporary_compilation_at_runtime (fun s -> fun x -> - let (s, x) = ToDBL.query_preterm_of_ast ~depth F.Map.empty s x in + let (s, x, _) = ToDBL.query_preterm_of_ast ~depth F.Map.empty s x in let (s, t) = stack_term_of_preterm ~depth s x in (s, (t, ((x.amap).nargs)))) state t in let env = Array.make nargs D.dummy in @@ -3375,6 +3376,7 @@ let static_check ~exec ~checker:(state, program) (checkc, (R.list_to_lp_list p), [q; R.list_to_lp_list tlist; - R.list_to_lp_list talist]))))) in + R.list_to_lp_list talist]))), + ((fun _ -> fun _ -> fun _ -> ())))) in let executable = optimize_query query in (exec executable) <> Failure diff --git a/src/.ppcache/compiler.mli b/src/.ppcache/compiler.mli index e377c5e76..0d66ec6c2 100644 --- a/src/.ppcache/compiler.mli +++ b/src/.ppcache/compiler.mli @@ -1,4 +1,4 @@ -(*236a6f802b725b0b7125f292daff8dfa43fe4334 *src/compiler.mli *) +(*8c0a98148744e29da0e681c9346f03a04ce14386 *src/compiler.mli *) #1 "src/compiler.mli" open Util open Data @@ -23,8 +23,10 @@ val query_of_term : State.t -> program -> (depth:int -> - hyps -> constraints -> State.t -> (State.t * (Loc.t * term))) - -> unit query + hyps -> + constraints -> + State.t -> (State.t * (Loc.t * term) * 'a query_readback)) + -> 'a query val query_of_data : State.t -> program -> Loc.t -> 'a Query.t -> 'a query val optimize_query : 'a query -> 'a executable val term_of_ast : diff --git a/src/.ppcache/data.ml b/src/.ppcache/data.ml index 0cf9acfbc..2011450b1 100644 --- a/src/.ppcache/data.ml +++ b/src/.ppcache/data.ml @@ -1,4 +1,4 @@ -(*9e41ed19c2304eae433f81858bfaabcd5701c359 *src/data.ml *) +(*d1ab878a9994ecb249bc95701570d498a788a5b4 *src/data.ml *) #1 "src/data.ml" module Fmt = Format module F = Ast.Func @@ -1527,6 +1527,13 @@ module Conversion = depth:int -> hyps -> constraints -> State.t -> (State.t * 'ctx * extra_goals) constraint 'ctx = #ctx + type ('a, 'ctx) context_builder = + depth:int -> + constraints -> + 'a list -> + State.t -> + (State.t * term ctx_entry Constants.Map.t * 'ctx * extra_goals) + constraint 'ctx = #ctx type dummy = unit let dummy = { @@ -1551,6 +1558,26 @@ module Conversion = let build_raw_ctx h s = (new ctx) h let in_raw_ctx : ctx ctx_readback = fun ~depth:_ -> fun h -> fun c -> fun s -> (s, (build_raw_ctx h s), []) + let context_builder { conv; to_key; push; init } obj_builder hyps = + (let do1 ~depth csts a m st = + let k = to_key ~depth a in + let st = push ~depth st k { depth; entry = a } in + let (st, a, gls) = conv.embed ~depth hyps csts st (depth, a) in + (st, (Constants.Map.add depth { depth; entry = a } m), gls) in + fun ~depth -> + fun csts -> + fun items -> + fun st -> + let st = init st in + let (st, m, glsl_rev, _) = + List.fold_left + (fun (st, m, gls, depth) -> + fun a -> + let (st, m, g) = do1 ~depth csts a m st in + (st, m, (g :: gls), (depth + 1))) + (st, Constants.Map.empty, [], depth) items in + (st, m, (obj_builder st), (List.concat (List.rev glsl_rev))) : + ('a, 'h) context_builder) end let while_compiling = State.declare ~name:"elpi:compiling" ~pp:(fun fmt -> fun _ -> ()) @@ -2105,16 +2132,21 @@ module BuiltInPredicate = module Query = struct type name = string - type 'x arguments = - | N: unit arguments - | D: ('a, Conversion.ctx) Conversion.t * 'a * 'x arguments -> 'x - arguments - | Q: ('a, Conversion.ctx) Conversion.t * name * 'x arguments -> ('a * - 'x) arguments - type 'x t = - | Query of { + type ('x, 'c) arguments = + | N: (unit, 'c) arguments + | D: ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments + -> ('x, 'c) arguments + | Q: ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) + arguments -> (('a * 'x), 'c) arguments + type 'c obj_builder = State.t -> 'c constraint 'c = #Conversion.ctx + type _ t = + | Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx) + Conversion.context * 'c obj_builder -> 'x t + and ('a, 'x, 'c) query_contents = + { + context: 'a list ; predicate: constant ; - arguments: 'x arguments } + arguments: ('x, 'c) arguments } end type symbol_table = { @@ -2154,6 +2186,7 @@ let rec pp_symbol_table : and show_symbol_table : symbol_table -> Ppx_deriving_runtime_proxy.string = fun x -> Ppx_deriving_runtime_proxy.Format.asprintf "%a" pp_symbol_table x [@@ocaml.warning "-32"] +type 'a query_readback = term StrMap.t -> constraints -> State.t -> 'a type 'a executable = { compiled_program: prolog_prog ; @@ -2164,7 +2197,7 @@ type 'a executable = symbol_table: symbol_table ; builtins: BuiltInPredicate.builtin_table ; assignments: term Util.StrMap.t ; - query_arguments: 'a Query.arguments } + query_readback: 'a query_readback } type pp_ctx = { uv_names: (string Util.PtrMap.t * int) ref ; diff --git a/src/.ppcache/runtime_trace_off.ml b/src/.ppcache/runtime_trace_off.ml index dac471efd..ff24e298e 100644 --- a/src/.ppcache/runtime_trace_off.ml +++ b/src/.ppcache/runtime_trace_off.ml @@ -1,4 +1,4 @@ -(*2cc741ee440ad7cd56532d0c52810aad119f1795 *src/runtime_trace_off.ml --cookie elpi_trace="false"*) +(*3a434c451cdabf1a722d3fd2ed37b08e1240c2f9 *src/runtime_trace_off.ml --cookie elpi_trace="false"*) #1 "src/runtime_trace_off.ml" module Fmt = Format module F = Ast.Func @@ -1792,68 +1792,70 @@ module FFI = aux ffi ctx constraints ~compute ~reduce data 1 state [] in (state, (gls_ctx @ gls)) end -let rec embed_query_aux : type a. - mk_Arg:(State.t -> name:string -> args:term list -> (State.t * term)) -> +let embed_query_args ctx ~mk_Arg = + let rec aux : type a. depth:int -> predicate:constant -> term list -> term list -> - hyps -> - constraints -> State.t -> a Query.arguments -> (State.t * term) - = - fun ~mk_Arg -> + constraints -> + State.t -> (a, 'ctx) Query.arguments -> (State.t * term) + = fun ~depth -> fun ~predicate -> fun gls -> fun args -> - fun hyps -> - fun constraints -> - fun state -> - fun descr -> - match descr with - | Data.Query.D (d, x, rest) -> - let (state, x, glsx) = - d.Conversion.embed ~depth - ((new Conversion.ctx) hyps) constraints state x in - embed_query_aux ~mk_Arg ~depth ~predicate - (gls @ glsx) (x :: args) hyps constraints state - rest - | Data.Query.Q (d, name, rest) -> - let (state, x) = mk_Arg state ~name ~args:[] in - embed_query_aux ~mk_Arg ~depth ~predicate gls (x :: - args) hyps constraints state rest - | Data.Query.N -> - let args = List.rev args in - (state, - ((match gls with - | [] -> C.mkAppL predicate args - | gls -> - C.mkAppL Global_symbols.andc - (gls @ [C.mkAppL predicate args])))) -let embed_query ~mk_Arg ~depth hyps constraints state (Query.Query - { predicate; arguments }) = - embed_query_aux ~mk_Arg ~depth ~predicate [] [] hyps constraints state - arguments + fun constraints -> + fun state -> + fun descr -> + match descr with + | Data.Query.D (d, x, rest) -> + let (state, x, glsx) = + d.Conversion.embed ~depth ctx constraints state x in + aux ~depth ~predicate (gls @ glsx) (x :: args) + constraints state rest + | Data.Query.Q (d, name, rest) -> + let (state, x) = mk_Arg state ~name ~args:[] in + aux ~depth ~predicate gls (x :: args) constraints state + rest + | Data.Query.N -> + let args = List.rev args in + (state, + ((match gls with + | [] -> C.mkAppL predicate args + | gls -> + C.mkAppL Global_symbols.andc + (gls @ [C.mkAppL predicate args])))) in + aux let rec query_solution_aux : type a. - a Query.arguments -> term StrMap.t -> hyps -> constraints -> State.t -> a = + (a, 'ctx) Query.arguments -> + term StrMap.t -> 'ctx -> constraints -> State.t -> a + = fun args -> fun assignments -> - fun hyps -> + fun ctx -> fun constraints -> fun state -> match args with | Data.Query.N -> () | Data.Query.D (_, _, args) -> - query_solution_aux args assignments hyps constraints state + query_solution_aux args assignments ctx constraints state | Data.Query.Q (d, name, args) -> let x = StrMap.find name assignments in let (state, x, _gls) = - d.Conversion.readback ~depth:0 ((new Conversion.ctx) hyps) - constraints state x in + d.Conversion.readback ~depth:0 ctx constraints state x in (x, - (query_solution_aux args assignments hyps constraints state)) -let output arguments assignments hyps constraints state = - query_solution_aux arguments assignments hyps constraints state + (query_solution_aux args assignments ctx constraints state)) +let output ctx arguments assignments constraints state = + query_solution_aux arguments assignments ctx constraints state +let embed_query ~mk_Arg ~depth hyps constraints state (Query.Query + ({ Query.context = context; predicate; arguments }, cc, builder)) = + let ctx_builder = + Data.Conversion.context_builder cc builder ((new Conversion.ctx) hyps) in + let (state, ctx_entries, ctx, gls) = + ctx_builder ~depth constraints context state in + ((embed_query_args ctx ~mk_Arg ~depth ~predicate gls [] constraints state + arguments), (output ctx arguments)) module Indexing = struct let mustbevariablec = min_int @@ -2686,7 +2688,7 @@ module Constraints : (let open State in ((init ()) |> (end_goal_compilation StrMap.empty)) |> end_compilation); - query_arguments = Query.N; + query_readback = (fun _ -> fun _ -> fun _ -> ()); symbol_table = (!C.table); builtins = (!FFI.builtins) } in @@ -3125,13 +3127,13 @@ open Mainloop let mk_outcome search get_cs assignments = try let alts = search () in - let (syn_csts, state, qargs, pp_ctx) = get_cs () in + let (syn_csts, state, readback_output, pp_ctx) = get_cs () in let solution = { assignments; constraints = syn_csts; state; - output = (output qargs assignments [] syn_csts state); + output = (readback_output assignments syn_csts state); pp_ctx } in ((Success solution), alts) @@ -3144,7 +3146,7 @@ let execute_once ?max_steps ?delay_outside_fragment exec = (mk_outcome search (fun () -> ((get CS.Ugly.delayed), ((get CS.state) |> State.end_execution), - (exec.query_arguments), + (exec.query_readback), { Data.uv_names = (ref (get Pp.uv_names)); table = (get C.table) })) exec.assignments)) let execute_loop ?delay_outside_fragment exec ~more ~pp = @@ -3157,7 +3159,7 @@ let execute_loop ?delay_outside_fragment exec ~more ~pp = mk_outcome f (fun () -> ((get CS.Ugly.delayed), ((get CS.state) |> State.end_execution), - (exec.query_arguments), + (exec.query_readback), { Data.uv_names = (ref (get Pp.uv_names)); table = (get C.table) })) exec.assignments in let time1 = Unix.gettimeofday () in k := alts; pp (time1 -. time0) o in diff --git a/src/.ppcache/runtime_trace_off.mli b/src/.ppcache/runtime_trace_off.mli index e39fcf18d..1d471db5e 100644 --- a/src/.ppcache/runtime_trace_off.mli +++ b/src/.ppcache/runtime_trace_off.mli @@ -1,4 +1,4 @@ -(*bf694777406dbb3b773e763e67beda1d5c6d725f *src/runtime_trace_off.mli --cookie elpi_trace="false"*) +(*dbd414a954857bee083d74bb49562a268062675f *src/runtime_trace_off.mli --cookie elpi_trace="false"*) #1 "src/runtime_trace_off.mli" open Util open Data @@ -19,7 +19,9 @@ val pp_stuck_goal : ?pp_ctx:pp_ctx -> Fmt.formatter -> stuck_goal -> unit val embed_query : mk_Arg:(State.t -> name:string -> args:term list -> (State.t * term)) -> depth:int -> - hyps -> constraints -> State.t -> 'a Query.t -> (State.t * term) + hyps -> + constraints -> + State.t -> 'a Query.t -> ((State.t * term) * 'a query_readback) val execute_once : ?max_steps:int -> ?delay_outside_fragment:bool -> 'a executable -> 'a outcome diff --git a/src/.ppcache/runtime_trace_on.ml b/src/.ppcache/runtime_trace_on.ml index 53b717613..2c0752478 100644 --- a/src/.ppcache/runtime_trace_on.ml +++ b/src/.ppcache/runtime_trace_on.ml @@ -1,4 +1,4 @@ -(*2cc741ee440ad7cd56532d0c52810aad119f1795 *src/runtime_trace_on.ml --cookie elpi_trace="true"*) +(*3a434c451cdabf1a722d3fd2ed37b08e1240c2f9 *src/runtime_trace_on.ml --cookie elpi_trace="true"*) #1 "src/runtime_trace_on.ml" module Fmt = Format module F = Ast.Func @@ -2283,68 +2283,70 @@ module FFI = aux ffi ctx constraints ~compute ~reduce data 1 state [] in (state, (gls_ctx @ gls)) end -let rec embed_query_aux : type a. - mk_Arg:(State.t -> name:string -> args:term list -> (State.t * term)) -> +let embed_query_args ctx ~mk_Arg = + let rec aux : type a. depth:int -> predicate:constant -> term list -> term list -> - hyps -> - constraints -> State.t -> a Query.arguments -> (State.t * term) - = - fun ~mk_Arg -> + constraints -> + State.t -> (a, 'ctx) Query.arguments -> (State.t * term) + = fun ~depth -> fun ~predicate -> fun gls -> fun args -> - fun hyps -> - fun constraints -> - fun state -> - fun descr -> - match descr with - | Data.Query.D (d, x, rest) -> - let (state, x, glsx) = - d.Conversion.embed ~depth - ((new Conversion.ctx) hyps) constraints state x in - embed_query_aux ~mk_Arg ~depth ~predicate - (gls @ glsx) (x :: args) hyps constraints state - rest - | Data.Query.Q (d, name, rest) -> - let (state, x) = mk_Arg state ~name ~args:[] in - embed_query_aux ~mk_Arg ~depth ~predicate gls (x :: - args) hyps constraints state rest - | Data.Query.N -> - let args = List.rev args in - (state, - ((match gls with - | [] -> C.mkAppL predicate args - | gls -> - C.mkAppL Global_symbols.andc - (gls @ [C.mkAppL predicate args])))) -let embed_query ~mk_Arg ~depth hyps constraints state (Query.Query - { predicate; arguments }) = - embed_query_aux ~mk_Arg ~depth ~predicate [] [] hyps constraints state - arguments + fun constraints -> + fun state -> + fun descr -> + match descr with + | Data.Query.D (d, x, rest) -> + let (state, x, glsx) = + d.Conversion.embed ~depth ctx constraints state x in + aux ~depth ~predicate (gls @ glsx) (x :: args) + constraints state rest + | Data.Query.Q (d, name, rest) -> + let (state, x) = mk_Arg state ~name ~args:[] in + aux ~depth ~predicate gls (x :: args) constraints state + rest + | Data.Query.N -> + let args = List.rev args in + (state, + ((match gls with + | [] -> C.mkAppL predicate args + | gls -> + C.mkAppL Global_symbols.andc + (gls @ [C.mkAppL predicate args])))) in + aux let rec query_solution_aux : type a. - a Query.arguments -> term StrMap.t -> hyps -> constraints -> State.t -> a = + (a, 'ctx) Query.arguments -> + term StrMap.t -> 'ctx -> constraints -> State.t -> a + = fun args -> fun assignments -> - fun hyps -> + fun ctx -> fun constraints -> fun state -> match args with | Data.Query.N -> () | Data.Query.D (_, _, args) -> - query_solution_aux args assignments hyps constraints state + query_solution_aux args assignments ctx constraints state | Data.Query.Q (d, name, args) -> let x = StrMap.find name assignments in let (state, x, _gls) = - d.Conversion.readback ~depth:0 ((new Conversion.ctx) hyps) - constraints state x in + d.Conversion.readback ~depth:0 ctx constraints state x in (x, - (query_solution_aux args assignments hyps constraints state)) -let output arguments assignments hyps constraints state = - query_solution_aux arguments assignments hyps constraints state + (query_solution_aux args assignments ctx constraints state)) +let output ctx arguments assignments constraints state = + query_solution_aux arguments assignments ctx constraints state +let embed_query ~mk_Arg ~depth hyps constraints state (Query.Query + ({ Query.context = context; predicate; arguments }, cc, builder)) = + let ctx_builder = + Data.Conversion.context_builder cc builder ((new Conversion.ctx) hyps) in + let (state, ctx_entries, ctx, gls) = + ctx_builder ~depth constraints context state in + ((embed_query_args ctx ~mk_Arg ~depth ~predicate gls [] constraints state + arguments), (output ctx arguments)) module Indexing = struct let mustbevariablec = min_int @@ -3377,7 +3379,7 @@ module Constraints : (let open State in ((init ()) |> (end_goal_compilation StrMap.empty)) |> end_compilation); - query_arguments = Query.N; + query_readback = (fun _ -> fun _ -> fun _ -> ()); symbol_table = (!C.table); builtins = (!FFI.builtins) } in @@ -4214,13 +4216,13 @@ open Mainloop let mk_outcome search get_cs assignments = try let alts = search () in - let (syn_csts, state, qargs, pp_ctx) = get_cs () in + let (syn_csts, state, readback_output, pp_ctx) = get_cs () in let solution = { assignments; constraints = syn_csts; state; - output = (output qargs assignments [] syn_csts state); + output = (readback_output assignments syn_csts state); pp_ctx } in ((Success solution), alts) @@ -4233,7 +4235,7 @@ let execute_once ?max_steps ?delay_outside_fragment exec = (mk_outcome search (fun () -> ((get CS.Ugly.delayed), ((get CS.state) |> State.end_execution), - (exec.query_arguments), + (exec.query_readback), { Data.uv_names = (ref (get Pp.uv_names)); table = (get C.table) })) exec.assignments)) let execute_loop ?delay_outside_fragment exec ~more ~pp = @@ -4246,7 +4248,7 @@ let execute_loop ?delay_outside_fragment exec ~more ~pp = mk_outcome f (fun () -> ((get CS.Ugly.delayed), ((get CS.state) |> State.end_execution), - (exec.query_arguments), + (exec.query_readback), { Data.uv_names = (ref (get Pp.uv_names)); table = (get C.table) })) exec.assignments in let time1 = Unix.gettimeofday () in k := alts; pp (time1 -. time0) o in diff --git a/src/.ppcache/runtime_trace_on.mli b/src/.ppcache/runtime_trace_on.mli index 275e4f32e..3b5372e13 100644 --- a/src/.ppcache/runtime_trace_on.mli +++ b/src/.ppcache/runtime_trace_on.mli @@ -1,4 +1,4 @@ -(*bf694777406dbb3b773e763e67beda1d5c6d725f *src/runtime_trace_on.mli --cookie elpi_trace="true"*) +(*dbd414a954857bee083d74bb49562a268062675f *src/runtime_trace_on.mli --cookie elpi_trace="true"*) #1 "src/runtime_trace_on.mli" open Util open Data @@ -19,7 +19,9 @@ val pp_stuck_goal : ?pp_ctx:pp_ctx -> Fmt.formatter -> stuck_goal -> unit val embed_query : mk_Arg:(State.t -> name:string -> args:term list -> (State.t * term)) -> depth:int -> - hyps -> constraints -> State.t -> 'a Query.t -> (State.t * term) + hyps -> + constraints -> + State.t -> 'a Query.t -> ((State.t * term) * 'a query_readback) val execute_once : ?max_steps:int -> ?delay_outside_fragment:bool -> 'a executable -> 'a outcome diff --git a/src/API.ml b/src/API.ml index 99310c734..4d20c8055 100644 --- a/src/API.ml +++ b/src/API.ml @@ -214,42 +214,16 @@ module Conversion = struct end -module RawOpaqueData = struct +module OpaqueData = struct include Util.CData include ED.C - let { cin = of_char; isc = is_char; cout = to_char } as char = declare { - data_compare = Pervasives.compare; - data_pp = (fun fmt c -> Format.fprintf fmt "%c" c); - data_hash = Hashtbl.hash; - data_name = "char"; - data_hconsed = false; - } - let of_char x = ED.mkCData (of_char x) - - let { cin = of_out_stream; isc = is_out_stream; cout = to_out_stream } as out_stream = declare { - data_compare = (fun (_,s1) (_,s2) -> String.compare s1 s2); - data_pp = (fun fmt (_,d) -> Format.fprintf fmt "" d); - data_hash = (fun (x,_) -> Hashtbl.hash x); - data_name = "out_stream"; - data_hconsed = false; - } - let of_out_stream x = ED.mkCData (of_out_stream x) - - let { cin = of_in_stream; isc = is_in_stream; cout = to_in_stream } as in_stream = declare { - data_compare = (fun (_,s1) (_,s2) -> String.compare s1 s2); - data_pp = (fun fmt (_,d) -> Format.fprintf fmt "" d); - data_hash = (fun (x,_) -> Hashtbl.hash x); - data_name = "in_stream"; - data_hconsed = false; - } - let of_in_stream x = ED.mkCData (of_in_stream x) - type name = string type doc = string type 'a declaration = { name : name; + cname : name; doc : doc; pp : Format.formatter -> 'a -> unit; compare : 'a -> 'a -> int; @@ -258,21 +232,13 @@ module RawOpaqueData = struct constants : (name * 'a) list; (* global constants of that type, eg "std_in" *) } - let conversion_of_cdata ~name ?(doc="") ~constants_map - { cin; isc; cout; name=c } - = - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = - state, ED.Term.CData (cin x), [] in - let readback ~depth _ _ state t = - let module R = (val !r) in let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> state, cout c, [] - | ED.Term.Const i as t when i < 0 -> - begin try state, snd @@ ED.Constants.Map.find i constants_map, [] - with Not_found -> raise (Conversion.TypeErr(ty,depth,t)) end - | t -> raise (Conversion.TypeErr(ty,depth,t)) in - let pp_doc fmt () = + type 'a cdata_with_constants = + 'a cdata * name * (string * 'a) ED.Constants.Map.t * doc + + let rest ({ cin; name=c; },name,constants_map,doc) = + Conversion.TyName name, + (fun fmt x -> pp fmt (cin x)), + fun fmt () -> let module R = (val !r) in let open R in if doc <> "" then begin ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); @@ -282,44 +248,77 @@ module RawOpaqueData = struct ED.Constants.Map.iter (fun _ (c,_) -> Format.fprintf fmt "@[type %s %s.@]@\n" c name) constants_map - in - { Conversion.embed; readback; ty; pp_doc; pp = (fun fmt x -> pp fmt (cin x)) } - let declare { name; doc; pp; compare; hash; hconsed; constants; } = + let embed ({ cin; _ },_,_,_) = (); fun ~depth:_ _ _ state x -> + state, ED.Term.CData (cin x), [] + let readback ({ isc; cout; _ },name,constants_map,_)= (); fun ~depth _ _ state t -> + let module R = (val !r) in let open R in + match R.deref_head ~depth t with + | ED.Term.CData c when isc c -> state, cout c, [] + | ED.Term.Const i as t when i < 0 -> + begin try state, snd @@ ED.Constants.Map.find i constants_map, [] + with Not_found -> raise (Conversion.TypeErr(Conversion.TyName name,depth,t)) end + | t -> raise (Conversion.TypeErr(Conversion.TyName name,depth,t)) + + let declare { name; cname; doc; pp; compare; hash; hconsed; constants; } = let cdata = declare { data_compare = compare; data_pp = pp; data_hash = hash; - data_name = name; + data_name = cname; data_hconsed = hconsed; } in - cdata, + cdata, name, List.fold_right (fun (n,v) -> ED.Constants.Map.add (ED.Global_symbols.declare_global_symbol n) (n,v)) constants ED.Constants.Map.empty, doc - let declare_cdata (cd,constants_map,doc) = - conversion_of_cdata ~name:cd.Util.CData.name ~doc ~constants_map cd + let build_conversion x = + let ty, pp, pp_doc = rest x in + { + Conversion.ty; + pp; + pp_doc; + embed = embed x; + readback = readback x; + } end -module OpaqueData = struct +module RawOpaqueData = struct + include Util.CData + include ED.C - type name = string - type doc = string + let cdata (c,_,_,_) = c - type 'a declaration = 'a RawOpaqueData.declaration = { - name : name; - doc : doc; - pp : Format.formatter -> 'a -> unit; - compare : 'a -> 'a -> int; - hash : 'a -> int; - hconsed : bool; - constants : (name * 'a) list; (* global constants of that type, eg "std_in" *) - } + let { cin = of_char; isc = is_char; cout = to_char } as char = declare { + data_compare = Pervasives.compare; + data_pp = (fun fmt c -> Format.fprintf fmt "%c" c); + data_hash = Hashtbl.hash; + data_name = "char"; + data_hconsed = false; + } + let of_char x = ED.mkCData (of_char x) + + let { cin = of_out_stream; isc = is_out_stream; cout = to_out_stream } as out_stream = declare { + data_compare = (fun (_,s1) (_,s2) -> String.compare s1 s2); + data_pp = (fun fmt (_,d) -> Format.fprintf fmt "" d); + data_hash = (fun (x,_) -> Hashtbl.hash x); + data_name = "out_stream"; + data_hconsed = false; + } + let of_out_stream x = ED.mkCData (of_out_stream x) + + let { cin = of_in_stream; isc = is_in_stream; cout = to_in_stream } as in_stream = declare { + data_compare = (fun (_,s1) (_,s2) -> String.compare s1 s2); + data_pp = (fun fmt (_,d) -> Format.fprintf fmt "" d); + data_hash = (fun (x,_) -> Hashtbl.hash x); + data_name = "in_stream"; + data_hconsed = false; + } + let of_in_stream x = ED.mkCData (of_in_stream x) - let declare x = x |> RawOpaqueData.declare |> RawOpaqueData.declare_cdata end @@ -890,17 +889,25 @@ end module Query = struct type name = string - type 'f arguments = 'f ED.Query.arguments = - | N : unit arguments - | D : ('a,Conversion.ctx) Conversion.t * 'a * 'x arguments -> 'x arguments - | Q : ('a,Conversion.ctx) Conversion.t * name * 'x arguments -> ('a * 'x) arguments - - type 'x t = Query of { predicate : name; arguments : 'x arguments } + type ('f,'c) arguments = ('f,'c) ED.Query.arguments = + | N : (unit,'c) arguments + | D : ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x,'c) arguments -> ('x,'c) arguments + | Q : ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x,'c) arguments -> ('a * 'x,'c) arguments + + type 'c obj_builder = Data.state -> 'c + constraint 'c = #Conversion.ctx + + type _ t = Query : ('a,'x,'c) query_contents * ('a,'k,Conversion.ctx) Conversion.context * 'c obj_builder -> 'x t + and ('a,'x,'c) query_contents = { + context : 'a list; + predicate : string; + arguments : ('x,'c) arguments; + } - let compile (state,p) loc (Query { predicate; arguments }) = + let compile (state,p) loc (Query({ predicate; arguments; context }, cc, obj)) = let state, predicate = Compiler.Symbols.allocate_global_symbol_str state predicate in - let q = ED.Query.Query{ predicate; arguments } in + let q = ED.Query.(Query({ predicate; arguments;context },cc, obj)) in Compiler.query_of_data state p loc q end @@ -921,6 +928,8 @@ end module RawQuery = struct let mk_Arg = Compiler.mk_Arg let is_Arg = Compiler.is_Arg + type 'a query_readback = + Data.term Data.StrMap.t -> Data.constraints -> State.t -> 'a let compile (state,p) f = Compiler.query_of_term state p f end diff --git a/src/API.mli b/src/API.mli index afa6ed9ac..1a7b68bd9 100644 --- a/src/API.mli +++ b/src/API.mli @@ -316,6 +316,7 @@ module OpaqueData : sig *) type 'a declaration = { name : name; + cname : name; doc : doc; pp : Format.formatter -> 'a -> unit; compare : 'a -> 'a -> int; @@ -324,7 +325,16 @@ module OpaqueData : sig constants : (name * 'a) list; (* global constants of that type, eg "std_in" *) } - val declare : 'a declaration -> ('a, 'c) Conversion.t + type 'a cdata_with_constants + + val declare : 'a declaration -> 'a cdata_with_constants + val build_conversion : 'a cdata_with_constants -> ('a,'c) Conversion.t + + (* To circumvent value restriction you have assemble a Conversion.t by hand *) + val embed : 'a cdata_with_constants -> ('a,'c) Conversion.embedding + val readback : 'a cdata_with_constants -> ('a,'c) Conversion.readback + val rest : 'a cdata_with_constants -> + Conversion.ty_ast * (Format.formatter -> 'a -> unit) * (Format.formatter -> unit -> unit) end @@ -628,12 +638,20 @@ end module Query : sig type name = string - type _ arguments = - | N : unit arguments - | D : ('a,Conversion.ctx) Conversion.t * 'a * 'x arguments -> 'x arguments - | Q : ('a,Conversion.ctx) Conversion.t * name * 'x arguments -> ('a * 'x) arguments + type (_,_) arguments = + | N : (unit, 'c) arguments + | D : ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments -> ('x, 'c) arguments + | Q : ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) arguments -> ('a * 'x, 'c) arguments - type 'x t = Query of { predicate : name; arguments : 'x arguments } + type 'c obj_builder = Data.state -> 'c + constraint 'c = #Conversion.ctx + + type _ t = Query : ('a,'x,'c) query_contents * ('a,'k,Conversion.ctx) Conversion.context * 'c obj_builder -> 'x t + and ('a,'x,'c) query_contents = { + context : 'a list; + predicate : string; + arguments : ('x,'c) arguments; + } val compile : Compile.program -> Ast.Loc.t -> 'a t -> 'a Compile.query @@ -892,23 +910,10 @@ end (** Low level module for OpaqueData *) module RawOpaqueData : sig - type name = string - type doc = string - type t (** If the data_hconsed is true, then the [cin] function below will automatically hashcons the data using the [eq] and [hash] functions. *) - type 'a declaration = 'a OpaqueData.declaration = { - name : name; - doc : doc; - pp : Format.formatter -> 'a -> unit; - compare : 'a -> 'a -> int; - hash : 'a -> int; - hconsed : bool; - constants : (name * 'a) list; (* global constants of that type, eg "std_in" *) - } - type 'a cdata = private { cin : 'a -> t; isc : t -> bool; @@ -916,8 +921,7 @@ module RawOpaqueData : sig name : string; } - val declare : 'a declaration -> 'a cdata * (name * 'a) Data.Constants.Map.t * string - val declare_cdata : 'a cdata * (name * 'a) Data.Constants.Map.t * string -> ('a,'c) Conversion.t + val cdata : 'a OpaqueData.cdata_with_constants -> 'a cdata val pp : Format.formatter -> t -> unit val show : t -> string @@ -1064,9 +1068,12 @@ module RawQuery : sig (* Args are parameters of the query (e.g. capital letters). *) val is_Arg : Data.state -> Data.term -> bool + type 'a query_readback = Data.term Data.StrMap.t -> Data.constraints -> State.t -> 'a + val compile : - Compile.program -> (depth:int -> Data.hyps -> Data.constraints -> Data.state -> Data.state * (Ast.Loc.t * Data.term)) -> - unit Compile.query + Compile.program -> + (depth:int -> Data.hyps -> Data.constraints -> Data.state -> Data.state * (Ast.Loc.t * Data.term) * 'a query_readback) -> + 'a Compile.query end diff --git a/src/builtin.ml b/src/builtin.ml index 26d197448..3aa8c58d1 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -917,10 +917,11 @@ let ctype = AlgebraicData.declare { constructors = [ K("ctype","",A(BuiltInData.string,N),B (fun x -> x), M (fun ~ok ~ko x -> ok x)) ] -} - -let safe = OpaqueData.declare { +} + +let safe_wc = OpaqueData.declare { OpaqueData.name = "safe"; + cname = "safe"; pp = (fun fmt (id,l) -> Format.fprintf fmt "[safe %d: %a]" id (RawPp.list (fun fmt (t,d) -> RawPp.term d fmt t) ";") !l); @@ -930,6 +931,13 @@ let safe = OpaqueData.declare { doc = "Holds data across bracktracking; can only contain closed terms"; constants = []; } +let ty, pp, pp_doc = OpaqueData.rest safe_wc +let safe : 'c. ('a, #Conversion.ctx as 'c) Conversion.t = +{ + Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed safe_wc ~depth); + readback = (fun ~depth -> OpaqueData.readback safe_wc ~depth); +} let safeno = ref 0 @@ -1161,8 +1169,9 @@ let elpi_stdlib_src = let open BuiltIn in let open BuiltInData in [ let ocaml_set ~name (type a) (alpha : (a,Conversion.ctx) Conversion.t) (module Set : Util.Set.S with type elt = a) = -let set = OpaqueData.declare { +let set_wc = OpaqueData.declare { OpaqueData.name; + cname = name; doc = ""; pp = (fun fmt m -> Format.fprintf fmt "%a" Set.pp m ); compare = (fun m1 m2 -> Set.compare m1 m2); @@ -1170,8 +1179,12 @@ let set = OpaqueData.declare { hconsed = false; constants = []; } in - -let set = { set with Conversion.ty = Conversion.(TyName name) } in +let ty, pp, pp_doc = OpaqueData.rest set_wc in +let set : (Set.t, #Conversion.ctx as 'c) Conversion.t = { + Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed set_wc ~depth); + readback = (fun ~depth -> OpaqueData.readback set_wc ~depth); +} in let open BuiltIn in let open BuiltInData in let open Conversion in @@ -1267,8 +1280,9 @@ let ocaml_map ~name (type a) let closed_A = BuiltInData.closed "A" in -let map = OpaqueData.declare { +let map_wc = OpaqueData.declare { OpaqueData.name; + cname = name; doc = ""; pp = (fun fmt m -> Format.fprintf fmt "%a" (Map.pp closed_A.pp) m ); compare = (fun m1 m2 -> Map.compare Pervasives.compare m1 m2); @@ -1276,9 +1290,13 @@ let map = OpaqueData.declare { hconsed = false; constants = []; } in - -let map a = { map with - Conversion.ty = Conversion.(TyApp(name,TyName a,[])) } in +let ty, pp, pp_doc = OpaqueData.rest map_wc in +let map a = { + Conversion.ty = Conversion.(TyApp(name,TyName a,[])); + pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed map_wc ~depth); + readback = (fun ~depth -> OpaqueData.readback map_wc ~depth); +} in let open BuiltIn in let open BuiltInData in let open Conversion in diff --git a/src/compiler.ml b/src/compiler.ml index c870077f0..8d09b4bca 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -446,7 +446,7 @@ type 'a query = { chr : (constant list * prechr_rule list) list; initial_depth : int; query : preterm; - query_arguments : 'a Query.arguments [@opaque]; + query_readback : 'a query_readback [@opaque]; (* We pre-compile the query to ease the API *) initial_goal : term; assignments : term StrMap.t; compiler_state : State.t; @@ -709,11 +709,11 @@ module ToDBL : sig (* Exported to compile the query *) val query_preterm_of_ast : depth:int -> macro_declaration -> State.t -> - Loc.t * Ast.Term.t -> State.t * preterm + Loc.t * Ast.Term.t -> State.t * preterm * unit query_readback val query_preterm_of_function : depth:int -> macro_declaration -> State.t -> - (State.t -> State.t * (Loc.t * term)) -> - State.t * preterm + (State.t -> State.t * (Loc.t * term) * 'a query_readback) -> + State.t * preterm * 'a query_readback (* Exported for quations *) val lp : quotation @@ -1003,15 +1003,15 @@ let preterms_of_ast ?on_type loc ~depth macros state f t = let query_preterm_of_function ~depth macros state f = assert(is_empty_amap (get_argmap state)); let state = set_mtm state (Some { macros }) in - let state, (loc, term) = f state in + let state, (loc, term), readback = f state in let amap = get_argmap state in - state, { amap; term; loc } + state, { amap; term; loc }, readback let query_preterm_of_ast ~depth macros state (loc, t) = assert(is_empty_amap (get_argmap state)); let state, term = preterm_of_ast loc ~depth macros state t in let amap = get_argmap state in - state, { term; amap; loc } + state, { term; amap; loc }, fun _ _ _ -> () ;; open Ast.Structured @@ -1976,7 +1976,7 @@ let query_of_ast compiler_state assembled_program t = let type_abbrevs = assembled_program.Assembled.type_abbrevs in let modes = assembled_program.Assembled.modes in let active_macros = assembled_program.Assembled.toplevel_macros in - let state, query = + let state, query, query_readback = ToDBL.query_preterm_of_ast ~depth:initial_depth active_macros compiler_state t in let query = Spill.spill_preterm state types (fun c -> C.Map.find c modes) query in let query_env = Array.make query.amap.nargs D.dummy in @@ -1993,7 +1993,7 @@ let query_of_ast compiler_state assembled_program t = chr = assembled_program.Assembled.chr; initial_depth; query; - query_arguments = Query.N; + query_readback; initial_goal; assignments; compiler_state = state |> (uvbodies_of_assignments assignments); @@ -2005,7 +2005,7 @@ let query_of_term compiler_state assembled_program f = let type_abbrevs = assembled_program.Assembled.type_abbrevs in let modes = assembled_program.Assembled.modes in let active_macros = assembled_program.Assembled.toplevel_macros in - let state, query = + let state, query, query_readback = ToDBL.query_preterm_of_function ~depth:initial_depth active_macros compiler_state (f ~depth:initial_depth [] []) in @@ -2023,18 +2023,17 @@ let query_of_term compiler_state assembled_program f = chr = assembled_program.Assembled.chr; initial_depth; query; - query_arguments = Query.N; + query_readback; initial_goal; assignments; compiler_state = state |> (uvbodies_of_assignments assignments); } -let query_of_data state p loc (Query.Query { arguments } as descr) = - let query = query_of_term state p (fun ~depth hyps constraints state -> - let state, term = R.embed_query ~mk_Arg ~depth hyps constraints state descr in - state, (loc, term)) in - { query with query_arguments = arguments } +let query_of_data state p loc qdescr = + query_of_term state p (fun ~depth hyps constraints state -> + let (state, term), query_readback = R.embed_query ~mk_Arg ~depth hyps constraints state qdescr in + state, (loc, term), query_readback) module Compiler : sig @@ -2118,7 +2117,7 @@ let run initial_goal; assignments; compiler_state = state; - query_arguments; + query_readback; } = let flags = State.get compiler_flags state in @@ -2172,7 +2171,7 @@ let run initial_goal; initial_runtime_state = State.end_compilation state; assignments; - query_arguments; + query_readback; symbol_table; builtins; } @@ -2366,7 +2365,7 @@ let term_of_ast ~depth state t = if State.get D.while_compiling state then anomaly ("term_of_ast cannot be used at compilation time"); let state, (t,nargs) = ToDBL.temporary_compilation_at_runtime (fun s x -> - let s, x = ToDBL.query_preterm_of_ast ~depth F.Map.empty s x in + let s, x, _ = ToDBL.query_preterm_of_ast ~depth F.Map.empty s x in let s, t = stack_term_of_preterm ~depth s x in s, (t, x.amap.nargs) ) state t in @@ -2397,7 +2396,7 @@ let static_check ~exec ~checker:(state,program) let query = query_of_term state program (fun ~depth hyps constraints state -> assert(depth=0); - state, (loc,App(checkc,R.list_to_lp_list p,[q;R.list_to_lp_list tlist;R.list_to_lp_list talist]))) in + state, (loc,App(checkc,R.list_to_lp_list p,[q;R.list_to_lp_list tlist;R.list_to_lp_list talist])), (fun _ _ _ -> ())) in let executable = optimize_query query in exec executable <> Failure ;; diff --git a/src/compiler.mli b/src/compiler.mli index e44ae6360..159aea148 100644 --- a/src/compiler.mli +++ b/src/compiler.mli @@ -27,7 +27,7 @@ val assemble_units : header:compilation_unit -> compilation_unit list -> State.t val query_of_ast : State.t -> program -> Ast.Goal.t -> unit query val query_of_term : - State.t -> program -> (depth:int -> hyps -> constraints -> State.t -> State.t * (Loc.t * term)) -> unit query + State.t -> program -> (depth:int -> hyps -> constraints -> State.t -> State.t * (Loc.t * term) * 'a query_readback) -> 'a query val query_of_data : State.t -> program -> Loc.t -> 'a Query.t -> 'a query val optimize_query : 'a query -> 'a executable diff --git a/src/data.ml b/src/data.ml index f0c042f0f..5b6062b7e 100644 --- a/src/data.ml +++ b/src/data.ml @@ -596,6 +596,11 @@ let rec show_ty_ast ?(outer=true) = function depth:int -> hyps -> constraints -> State.t -> State.t * 'ctx * extra_goals constraint 'ctx = #ctx + type ('a,'ctx) context_builder = + depth:int -> constraints -> 'a list -> State.t -> + State.t * term ctx_entry Constants.Map.t * 'ctx * extra_goals + constraint 'ctx = #ctx + type dummy = unit let dummy = { @@ -620,6 +625,21 @@ let rec show_ty_ast ?(outer=true) = function let in_raw_ctx : ctx ctx_readback = fun ~depth:_ h c s -> s, build_raw_ctx h s, [] + let context_builder { conv; to_key; push; init } obj_builder hyps : ('a,'h) context_builder = + let do1 ~depth csts a m st = + let k = to_key ~depth a in + let st = push ~depth st k { depth; entry = a } in + let st, a, gls = conv.embed ~depth hyps csts st (depth,a) in + st, Constants.Map.add depth { depth; entry = a } m, gls in + fun ~depth csts items st -> + let st = init st in + let st, m, glsl_rev, _ = + List.fold_left (fun (st, m, gls, depth) a -> + let st, m, g = do1 ~depth csts a m st in + st, m, g :: gls, depth+1) + (st, Constants.Map.empty, [], depth) items in + st, m, obj_builder st, List.concat (List.rev glsl_rev) + end let while_compiling = State.declare ~name:"elpi:compiling" @@ -1036,13 +1056,20 @@ end module Query = struct type name = string - type 'x arguments = - | N : unit arguments - | D : ('a,Conversion.ctx) Conversion.t * 'a * 'x arguments -> 'x arguments - | Q : ('a,Conversion.ctx) Conversion.t * name * 'x arguments -> ('a * 'x) arguments - - type 'x t = - | Query of { predicate : constant; arguments : 'x arguments } + type ('x,'c) arguments = + | N : (unit, 'c) arguments + | D : ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments -> ('x, 'c) arguments + | Q : ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) arguments -> ('a * 'x, 'c) arguments + + type 'c obj_builder = State.t -> 'c + constraint 'c = #Conversion.ctx + + type _ t = Query : ('a,'x,'c) query_contents * ('a,'k,Conversion.ctx) Conversion.context * 'c obj_builder -> 'x t + and ('a,'x,'c) query_contents = { + context : 'a list; + predicate : constant; + arguments : ('x,'c) arguments; + } end @@ -1053,6 +1080,8 @@ type symbol_table = { } [@@deriving show] +type 'a query_readback = term StrMap.t -> constraints -> State.t -> 'a + type 'a executable = { (* the lambda-Prolog program: an indexed list of clauses *) compiled_program : prolog_prog; @@ -1071,7 +1100,7 @@ type 'a executable = { (* solution *) assignments : term Util.StrMap.t; (* type of the query, reified *) - query_arguments: 'a Query.arguments; + query_readback : 'a query_readback; } type pp_ctx = { diff --git a/src/runtime.ml b/src/runtime.ml index 19ee800d3..bcb8e5a33 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -1968,38 +1968,44 @@ let call (Data.BuiltInPredicate.Pred(bname,ffi,in_ctx,compute)) ~depth hyps cons end -let rec embed_query_aux : type a. mk_Arg:(State.t -> name:string -> args:term list -> State.t * term) -> depth:int -> predicate:constant -> term list -> term list -> hyps -> constraints -> State.t -> a Query.arguments -> State.t * term - = fun ~mk_Arg ~depth ~predicate gls args hyps constraints state descr -> +let embed_query_args ctx ~mk_Arg = + let rec aux : type a. depth:int -> predicate:constant -> term list -> term list -> constraints -> State.t -> (a,'ctx) Query.arguments -> State.t * term + = fun ~depth ~predicate gls args constraints state descr -> match descr with | Data.Query.D(d,x,rest) -> - let state, x, glsx = d.Conversion.embed ~depth (new Conversion.ctx hyps) constraints state x in - embed_query_aux ~mk_Arg ~depth ~predicate (gls @ glsx) (x :: args) hyps constraints state rest + let state, x, glsx = d.Conversion.embed ~depth ctx constraints state x in + aux ~depth ~predicate (gls @ glsx) (x :: args) constraints state rest | Data.Query.Q(d,name,rest) -> let state, x = mk_Arg state ~name ~args:[] in - embed_query_aux ~mk_Arg ~depth ~predicate gls (x :: args) hyps constraints state rest + aux ~depth ~predicate gls (x :: args) constraints state rest | Data.Query.N -> let args = List.rev args in state, match gls with | [] -> C.mkAppL predicate args | gls -> C.mkAppL Global_symbols.andc (gls @ [C.mkAppL predicate args]) + in + aux ;; -let embed_query ~mk_Arg ~depth hyps constraints state (Query.Query { predicate; arguments }) = - embed_query_aux ~mk_Arg ~depth ~predicate [] [] hyps constraints state arguments - -let rec query_solution_aux : type a. a Query.arguments -> term StrMap.t -> hyps -> constraints -> State.t -> a - = fun args assignments hyps constraints state -> +let rec query_solution_aux : type a. (a,'ctx) Query.arguments -> term StrMap.t -> 'ctx -> constraints -> State.t -> a + = fun args assignments ctx constraints state -> match args with | Data.Query.N -> () - | Data.Query.D(_,_,args) -> query_solution_aux args assignments hyps constraints state + | Data.Query.D(_,_,args) -> query_solution_aux args assignments ctx constraints state | Data.Query.Q(d,name,args) -> let x = StrMap.find name assignments in - let state, x, _gls = d.Conversion.readback ~depth:0 (new Conversion.ctx hyps) constraints state x in - x, query_solution_aux args assignments hyps constraints state + let state, x, _gls = d.Conversion.readback ~depth:0 ctx constraints state x in + x, query_solution_aux args assignments ctx constraints state + +let output ctx arguments assignments constraints state = + query_solution_aux arguments assignments ctx constraints state -let output arguments assignments hyps constraints state = - query_solution_aux arguments assignments hyps constraints state +let embed_query ~mk_Arg ~depth hyps constraints state (Query.Query ({ Query.context; predicate; arguments },cc,builder)) = + let ctx_builder = Data.Conversion.context_builder cc builder (new Conversion.ctx hyps) in + let state, ctx_entries, ctx, gls = ctx_builder ~depth constraints context state in + embed_query_args ctx ~mk_Arg ~depth ~predicate gls [] constraints state arguments, + output ctx arguments (****************************************************************************** Indexing @@ -2945,7 +2951,7 @@ let try_fire_rule (gid[@trace]) rule (constraints as orig_constraints) = assignments = StrMap.empty; initial_depth = max_depth; initial_runtime_state = State.(init () |> end_goal_compilation StrMap.empty |> end_compilation); - query_arguments = Query.N; + query_readback = (fun _ _ _ -> ()); symbol_table = !C.table; builtins = !FFI.builtins; } in @@ -3378,12 +3384,12 @@ open Mainloop let mk_outcome search get_cs assignments = try let alts = search () in - let syn_csts, state, qargs, pp_ctx = get_cs () in + let syn_csts, state, readback_output, pp_ctx = get_cs () in let solution = { assignments; constraints = syn_csts; state; - output = output qargs assignments [] syn_csts state; + output = readback_output assignments syn_csts state; pp_ctx = pp_ctx; } in Success solution, alts @@ -3394,7 +3400,7 @@ let mk_outcome search get_cs assignments = let execute_once ?max_steps ?delay_outside_fragment exec = auxsg := []; let { search; get } = make_runtime ?max_steps ?delay_outside_fragment exec in - 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) + fst (mk_outcome search (fun () -> get CS.Ugly.delayed, get CS.state |> State.end_execution, exec.query_readback, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments) ;; let execute_loop ?delay_outside_fragment exec ~more ~pp = @@ -3402,7 +3408,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 in + let o, alts = mk_outcome f (fun () -> get CS.Ugly.delayed, get CS.state |> State.end_execution, exec.query_readback, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments in let time1 = Unix.gettimeofday() in k := alts; pp (time1 -. time0) o in diff --git a/src/runtime.mli b/src/runtime.mli index 0f997d989..a86805692 100644 --- a/src/runtime.mli +++ b/src/runtime.mli @@ -23,7 +23,7 @@ val embed_query : mk_Arg:(State.t -> name:string -> args:term list -> State.t * term) -> depth:int -> hyps -> constraints -> - State.t -> 'a Query.t -> State.t * term + State.t -> 'a Query.t -> (State.t * term) * 'a query_readback (* Interpreter API *) val execute_once :