Skip to content

Commit

Permalink
fix query type
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Apr 29, 2020
1 parent e0efada commit b84e164
Show file tree
Hide file tree
Showing 17 changed files with 546 additions and 423 deletions.
208 changes: 113 additions & 95 deletions src/.ppcache/API.ml
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(*09dd92d029bc5129509dbb9e46c435ff8be4de41 *src/API.ml --cookie elpi_trace="false"*)
(*332b22a78600ccb50a6a5a1271c10ce168f491b0 *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))
Expand Down Expand Up @@ -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
"@[<hov 2>typeabbrev %s (ctype \"%s\").@]@\n@\n" name c;
ED.Constants.Map.iter
(fun _ ->
fun (c, _) ->
Format.fprintf fmt "@[<hov 2>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
{
Expand Down Expand Up @@ -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
"@[<hov 2>typeabbrev %s (ctype \"%s\").@]@\n@\n" name c;
ED.Constants.Map.iter
(fun _ ->
fun (c, _) ->
Format.fprintf fmt "@[<hov 2>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
Expand Down Expand Up @@ -1181,20 +1192,25 @@ 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 _ t =
| Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx)
Conversion.context * (Data.state -> #Conversion.ctx as 'c) -> '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 = ED.Query.Query ({ predicate; arguments; context }, cc, obj) in
Compiler.query_of_data state p loc q
end
module State =
Expand All @@ -1210,6 +1226,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 =
Expand Down
65 changes: 33 additions & 32 deletions src/.ppcache/API.mli
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(*262f7f42585df543898448e5ff436973e6f64995 *src/API.mli --cookie elpi_trace="false"*)
(*1a1a1714a91ce24bd6b8d55bb21f552675762a09 *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
Expand Down Expand Up @@ -215,14 +215,23 @@ sig
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 }[@@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 :
Expand Down Expand Up @@ -350,16 +359,20 @@ 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 _ t =
| Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx)
Conversion.context * (Data.state -> #Conversion.ctx as 'c) -> '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 ]} "]
Expand Down Expand Up @@ -503,30 +516,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
Expand Down Expand Up @@ -622,13 +620,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 :
Expand Down
Loading

0 comments on commit b84e164

Please sign in to comment.