Skip to content

Commit

Permalink
a way to get poly opaque data and algebraic data
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Apr 30, 2020
1 parent c1b497c commit 338db60
Show file tree
Hide file tree
Showing 8 changed files with 132 additions and 2,278 deletions.
1,430 changes: 0 additions & 1,430 deletions src/.ppcache/API.ml
View file

This file was deleted.

724 changes: 0 additions & 724 deletions src/.ppcache/API.mli
View file

This file was deleted.

42 changes: 23 additions & 19 deletions src/.ppcache/data.ml
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(*d1ab878a9994ecb249bc95701570d498a788a5b4 *src/data.ml *)
(*7f2ba7fa31dccc0775a96d5831ee46cdbb09241c *src/data.ml *)
#1 "src/data.ml"
module Fmt = Format
module F = Ast.Func
Expand Down Expand Up @@ -1669,8 +1669,10 @@ module BuiltInPredicate =
| S: ('bs, 'b, 'ms, 'm, 'self, 'ctx) constructor_arguments ->
('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self,
'ctx) constructor_arguments
| C: (('self, 'ctx) Conversion.t -> ('a, 'ctx) Conversion.t) *
('bs, 'b, 'ms, 'm, 'self, 'ctx) constructor_arguments ->
| C:
(('self, Conversion.ctx) Conversion.t ->
('a, Conversion.ctx) Conversion.t)
* ('bs, 'b, 'ms, 'm, 'self, 'ctx) constructor_arguments ->
('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'ctx)
constructor_arguments
type ('t, 'h) constructor =
Expand Down Expand Up @@ -1704,16 +1706,17 @@ module BuiltInPredicate =
('t, 'h) compiled_constructor Constants.Map.t
let buildk ~mkConst kname =
function | [] -> mkConst kname | x::xs -> mkApp kname x xs
let rec readback_args : type a m t h.
let rec readback_args : type a m t.
look:(depth:int -> term -> term) ->
Conversion.ty_ast ->
depth:int ->
h ->
#Conversion.ctx ->
constraints ->
State.t ->
extra_goals list ->
term ->
(a, m, t, h) compiled_constructor_arguments ->
(a, m, t, Conversion.ctx)
compiled_constructor_arguments ->
a -> term list -> (State.t * t * extra_goals)
=
fun ~look ->
Expand Down Expand Up @@ -1743,15 +1746,15 @@ module BuiltInPredicate =
readback_args ~look ty ~depth hyps
constraints state (gls :: extra) origin
rest (convert x) xs
and readback : type t h.
and readback : type t.
mkinterval:(int -> int -> int -> term list) ->
look:(depth:int -> term -> term) ->
alloc:(?name:string -> State.t -> (State.t * 'uk)) ->
mkUnifVar:('uk -> args:term list -> State.t -> term) ->
Conversion.ty_ast ->
(t, h) compiled_adt ->
(t, Conversion.ctx) compiled_adt ->
depth:int ->
h ->
#Conversion.ctx ->
constraints ->
State.t -> term -> (State.t * t * extra_goals)
=
Expand Down Expand Up @@ -1801,15 +1804,16 @@ module BuiltInPredicate =
with
| Not_found ->
raise (Conversion.TypeErr (ty, depth, t))
and adt_embed_args : type m a t h.
and adt_embed_args : type m a t.
mkConst:(int -> term) ->
Conversion.ty_ast ->
(t, h) compiled_adt ->
(t, Conversion.ctx) compiled_adt ->
constant ->
depth:int ->
h ->
#Conversion.ctx ->
constraints ->
(a, m, t, h) compiled_constructor_arguments ->
(a, m, t, Conversion.ctx)
compiled_constructor_arguments ->
(State.t -> (State.t * term * extra_goals)) list ->
m
=
Expand Down Expand Up @@ -1841,13 +1845,13 @@ module BuiltInPredicate =
((fun state ->
d.embed ~depth hyps constraints
state x) :: acc))
and embed : type a h.
and embed : type a.
mkConst:(int -> term) ->
Conversion.ty_ast ->
(Format.formatter -> a -> unit) ->
(a, h) compiled_adt ->
(a, Conversion.ctx) compiled_adt ->
depth:int ->
h ->
#Conversion.ctx ->
constraints ->
State.t -> a -> (State.t * term * extra_goals)
=
Expand Down Expand Up @@ -1875,9 +1879,9 @@ module BuiltInPredicate =
matcher ~ok ~ko:(aux rest) t state in
aux bindings state
let rec compile_arguments : type b bs m ms t.
(bs, b, ms, m, t, 'h) constructor_arguments ->
(t, #Conversion.ctx as 'h) Conversion.t ->
(bs, ms, t, 'h) compiled_constructor_arguments
(bs, b, ms, m, t, Conversion.ctx) constructor_arguments ->
(t, #Conversion.ctx) Conversion.t ->
(bs, ms, t, Conversion.ctx) compiled_constructor_arguments
=
fun arg ->
fun self ->
Expand Down
114 changes: 52 additions & 62 deletions src/API.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -260,28 +260,24 @@ module OpaqueData = struct
with Not_found -> raise (Conversion.TypeErr(Conversion.TyName name,depth,t)) end
| t -> raise (Conversion.TypeErr(Conversion.TyName name,depth,t))

let declare_cdata cdata name doc constants =
let cd_w_consts =
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 in
let ty, pp, pp_doc = rest cd_w_consts in
ty, pp, pp_doc, cd_w_consts

let declare { name; cname; doc; pp; compare; hash; hconsed; constants; } =
let cdata = declare {
let c = 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;
pp;
pp_doc;
embed = embed x;
readback = readback x;
}
} in
declare_cdata c name doc constants

end

Expand Down Expand Up @@ -618,53 +614,47 @@ end

module BuiltInData = struct

let[@elpi.template] inline_data = fun name doc cdata constants constants_map ->
let { Util.CData.cin; isc; cout; name=c } = cdata in
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, 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 () =
let module R = (val !r) in let open R in
if doc <> "" then begin
ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc);
Format.fprintf fmt "@\n";
end;
Format.fprintf fmt "@[<hov 2>typeabbrev %s (ctype \"%s\").@]@\n@\n" name c;
List.iter (fun (c,_) ->
Format.fprintf fmt "@[<hov 2>type %s %s.@]@\n" c name)
constants in
{ Conversion.embed; readback; ty; pp_doc; pp = (fun fmt x -> Util.CData.pp fmt (cin x)) }

let int : 'h. (int, 'h) Conversion.t = [%elpi.template inline_data "int" "" ED.C.int [] ED.Constants.Map.empty]
let float : 'h. (float, 'h) Conversion.t = [%elpi.template inline_data "float" "" ED.C.float [] ED.Constants.Map.empty]
let string : 'h. (string, 'h) Conversion.t = [%elpi.template inline_data "string" "" ED.C.string [] ED.Constants.Map.empty]
let loc : 'h. (Util.Loc.t, 'h) Conversion.t = [%elpi.template inline_data "loc" "" ED.C.loc [] ED.Constants.Map.empty]
let char : 'h. (char, 'h) Conversion.t = [%elpi.template inline_data "char" "an octect" RawOpaqueData.char [] ED.Constants.Map.empty]

let in_stream_constants = ["std_in",(stdin,"stdin")]
let in_stream_cmap = List.fold_left (fun m (c,v) ->
let c = ED.Global_symbols.declare_global_symbol c in
ED.Constants.Map.add c v m)
ED.Constants.Map.empty in_stream_constants

let in_stream : 'h. (in_channel * string, 'h) Conversion.t = [%elpi.template inline_data "in_stream" "" RawOpaqueData.in_stream in_stream_constants in_stream_cmap]

let out_stream_constants = ["std_out",(stdout,"stdout");"std_err",(stderr,"stderr")]
let out_stream_cmap = List.fold_left (fun m (c,v) ->
let c = ED.Global_symbols.declare_global_symbol c in
ED.Constants.Map.add c v m)
ED.Constants.Map.empty out_stream_constants

let out_stream : 'h. (out_channel * string, 'h) Conversion.t = [%elpi.template inline_data "out_stream" "" RawOpaqueData.out_stream out_stream_constants out_stream_cmap]
let ty, pp, pp_doc, int = OpaqueData.declare_cdata RawOpaqueData.int "int" "" []
let int : 'h. (int, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed int ~depth);
readback = (fun ~depth -> OpaqueData.readback int ~depth);
}

let ty, pp, pp_doc, float = OpaqueData.declare_cdata RawOpaqueData.float "float" "" []
let float : 'h. (float, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed float ~depth);
readback = (fun ~depth -> OpaqueData.readback float ~depth);
}

let ty, pp, pp_doc, string = OpaqueData.declare_cdata RawOpaqueData.string "string" "" []
let string : 'h. (string, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed string ~depth);
readback = (fun ~depth -> OpaqueData.readback string ~depth);
}

let ty, pp, pp_doc, loc = OpaqueData.declare_cdata RawOpaqueData.loc "loc" "" []
let loc : 'h. (Util.Loc.t, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed loc ~depth);
readback = (fun ~depth -> OpaqueData.readback loc ~depth);
}

let ty, pp, pp_doc, char = OpaqueData.declare_cdata RawOpaqueData.char "char" "an octect" []
let char : 'h. (char, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed char ~depth);
readback = (fun ~depth -> OpaqueData.readback char ~depth);
}

let ty, pp, pp_doc, in_stream = OpaqueData.declare_cdata RawOpaqueData.in_stream "in_stream" "" ["std_in",(stdin,"stdin")]
let in_stream : 'h. (in_channel * string, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed in_stream ~depth);
readback = (fun ~depth -> OpaqueData.readback in_stream ~depth);
}

let ty, pp, pp_doc, out_stream = OpaqueData.declare_cdata RawOpaqueData.out_stream "out_stream" "" ["std_out",(stdout,"stdout");"std_err",(stderr,"stderr")]
let out_stream : 'h. (out_channel * string, 'h) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed out_stream ~depth);
readback = (fun ~depth -> OpaqueData.readback out_stream ~depth);
}

let poly ty =
let embed ~depth:_ _ _ state x = state, x, [] in
Expand Down
40 changes: 31 additions & 9 deletions src/API.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -327,14 +327,26 @@ module OpaqueData : sig

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 declare : 'a declaration ->
Conversion.ty_ast * (Format.formatter -> 'a -> unit) * (Format.formatter -> unit -> unit) * 'a cdata_with_constants

(* To circumvent value restriction you have assemble a Conversion.t by hand *)
(** To circumvent value restriction you have assemble a Conversion.t by
hand. Example (top level of a module):
let ty, pp, pp_doc, name = declare {
name = "name";
cname = "Names.Name.t";
doc = "Name hints";
pp = ...
}
let name : 'c. (Names.Name.t, #ctx as 'c) t= { ty; pp; pp_doc;
embed = (fun ~depth -> embed name ~depth);
readback = (fun ~depth -> readback name ~depth);
}
*)
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

Expand Down Expand Up @@ -403,7 +415,7 @@ module AlgebraicData : sig
| S : ('bs,'b, 'ms, 'm, 'self, 'c) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'c) constructor_arguments
(* An argument of type `T 'self` for a constainer `T`, like a `list 'self`.
`S args` above is a shortcut for `C(fun x -> x, args)` *)
| C : (('self,'c) Conversion.t -> ('a,'c) Conversion.t) * ('bs,'b,'ms,'m,'self, 'c) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms,'a -> 'm, 'self, 'c) constructor_arguments
| C : (('self,Conversion.ctx) Conversion.t -> ('a,Conversion.ctx) Conversion.t) * ('bs,'b,'ms,'m,'self, 'c) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms,'a -> 'm, 'self, 'c) constructor_arguments

type ('t,'c) constructor =
K : name * doc *
Expand All @@ -420,7 +432,17 @@ module AlgebraicData : sig
}
constraint 'c = #Conversion.ctx

val declare : ('t,'c) declaration -> ('t,'c) Conversion.t
(** In order to obtain a quantification over the context one can do
as follows:
let { ty; pp; pp_doc; embed; readback } = declare { ... }
let foo : 'c. (foo, #ctx as 'c) t = { ty; pp; pp_doc;
embed = (fun ~depth (c : #ctx) -> embed ~depth (c :> ctx));
readback = (fun ~depth (c : #ctx) -> readback ~depth (c :> ctx));
}
*)
val declare : ('t,Conversion.ctx) declaration -> ('t,Conversion.ctx) Conversion.t

end

Expand Down Expand Up @@ -795,8 +817,8 @@ module BuiltInData : sig
val string : (string, 'c) Conversion.t
val list : ('a, 'c) Conversion.t -> ('a list, 'c) Conversion.t
val loc : (Ast.Loc.t, 'c) Conversion.t
val bool : (bool, 'c) Conversion.t
val char : (char, 'c) Conversion.t
val bool : (bool, 'c) Conversion.t
val char : (char, 'c) Conversion.t
(* The string is the "file name" *)
val in_stream : (in_channel * string, 'c) Conversion.t
val out_stream : (out_channel * string, 'c) Conversion.t
Expand Down
28 changes: 11 additions & 17 deletions src/builtin.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -919,7 +919,7 @@ let ctype = AlgebraicData.declare {
]
}

let safe_wc = OpaqueData.declare {
let ty, pp, pp_doc, safe = OpaqueData.declare {
OpaqueData.name = "safe";
cname = "safe";
pp = (fun fmt (id,l) ->
Expand All @@ -931,12 +931,9 @@ let safe_wc = 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 safe : 'c. ('a, #Conversion.ctx as 'c) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed safe ~depth);
readback = (fun ~depth -> OpaqueData.readback safe ~depth);
}

let safeno = ref 0
Expand Down Expand Up @@ -1169,7 +1166,7 @@ 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_wc = OpaqueData.declare {
let ty, pp, pp_doc, set = OpaqueData.declare {
OpaqueData.name;
cname = name;
doc = "";
Expand All @@ -1179,11 +1176,9 @@ let set_wc = OpaqueData.declare {
hconsed = false;
constants = [];
} 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);
let set : (Set.t, #Conversion.ctx as 'c) Conversion.t = { Conversion.ty; pp; pp_doc;
embed = (fun ~depth -> OpaqueData.embed set ~depth);
readback = (fun ~depth -> OpaqueData.readback set ~depth);
} in

let open BuiltIn in let open BuiltInData in let open Conversion in
Expand Down Expand Up @@ -1280,7 +1275,7 @@ let ocaml_map ~name (type a)

let closed_A = BuiltInData.closed "A" in

let map_wc = OpaqueData.declare {
let ty, pp, pp_doc, map = OpaqueData.declare {
OpaqueData.name;
cname = name;
doc = "";
Expand All @@ -1290,12 +1285,11 @@ let map_wc = OpaqueData.declare {
hconsed = false;
constants = [];
} 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);
embed = (fun ~depth -> OpaqueData.embed map ~depth);
readback = (fun ~depth -> OpaqueData.readback map ~depth);
} in

let open BuiltIn in let open BuiltInData in let open Conversion in
Expand Down
Loading

0 comments on commit 338db60

Please sign in to comment.