From 6d20b0165b419430d237baea620e3cdcd6157f49 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 May 2023 13:47:22 +0200 Subject: [PATCH] wip --- ocaml-elpi/main_ocaml_elpi_rewriter.ml | 33 +- ocaml-elpi/ocaml_ast_for_elpi.ml | 18 +- ocaml-elpi/tests/dune.inc | 2 +- ocaml-elpi/tests/gen_dune.ml | 4 +- ocaml-elpi/tests/test_swap.elpi | 2 +- ppx_elpi/ppx_elpi.ml | 122 ++-- ppx_elpi/tests/dune.inc | 23 + ppx_elpi/tests/test_container.expected.elpi | 16 + ppx_elpi/tests/test_container.expected.ml | 0 ppx_elpi/tests/test_container.ml | 34 + ppx_elpi/tests/test_double_contextual.ml | 14 +- ppx_elpi/tests/test_mutual_contextual.ml | 684 +------------------- ppx_elpi/tests/test_poly_adt.expected.elpi | 2 +- ppx_elpi/tests/test_poly_adt.ml | 14 +- ppx_elpi/tests/test_poly_alias.ml | 4 +- ppx_elpi/tests/test_simple_contextual.ml | 22 +- ppx_elpi/tests/test_two_layers_context.ml | 27 +- src/API.ml | 176 ++++- src/API.mli | 60 +- src/builtin.ml | 137 +++- src/builtin.mli | 22 +- src/compiler.ml | 14 +- src/data.ml | 9 +- src/runtime.ml | 46 +- 24 files changed, 595 insertions(+), 890 deletions(-) create mode 100644 ppx_elpi/tests/test_container.expected.elpi create mode 100644 ppx_elpi/tests/test_container.expected.ml create mode 100644 ppx_elpi/tests/test_container.ml diff --git a/ocaml-elpi/main_ocaml_elpi_rewriter.ml b/ocaml-elpi/main_ocaml_elpi_rewriter.ml index aa94c86f0..a6e8ff199 100644 --- a/ocaml-elpi/main_ocaml_elpi_rewriter.ml +++ b/ocaml-elpi/main_ocaml_elpi_rewriter.ml @@ -57,7 +57,7 @@ ocaml-elpi.ppx: no program specified. Supported options: let query = let open Query in compile program (Ast.Loc.initial "ppx") @@ - Query { predicate = "map.structure"; arguments = D(structure,s,(Q(structure,"Result",N))) } in + CQuery ("map.structure", DC(structure,s,(QC(structure,"Result",NC))),new ctx_for_structure [],RawData.no_constraints) in if !typecheck then begin if not @@ Compile.static_check ~checker:Elpi.Builtin.(default_checker ()) query then begin exit 1 @@ -77,13 +77,16 @@ let erase_loc = object inherit [State.t] Ast_traverse.fold_map method! location _ (st : State.t) = Ocaml_ast_for_elpi.dummy_location, st + method! location_stack l (st : State.t) = [], st end ;; let expression_quotation ~depth state _loc s = let e = Ppxlib.Parse.expression (Lexing.from_string s) in let e, state = erase_loc#expression e state in - let state, x, gls = (expression).Conversion.embed ~depth state e in + let ctx = new ctx_for_expression [] state in + let csts = RawData.no_constraints in + let state, x, gls = (expression).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x @@ -93,7 +96,9 @@ let () = Quotation.set_default_quotation expression_quotation let pattern_quotation ~depth state _loc s = let e = Ppxlib.Parse.pattern (Lexing.from_string s) in let e, state = erase_loc#pattern e state in - let state, x, gls = (pattern).Conversion.embed ~depth state e in + let ctx = new ctx_for_pattern [] state in + let csts = RawData.no_constraints in + let state, x, gls = (pattern).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x @@ -102,7 +107,9 @@ let () = Quotation.register_named_quotation ~name:"pat" pattern_quotation let type_quotation ~depth state _loc s = let e = Ppxlib.Parse.core_type (Lexing.from_string s) in let e, state = erase_loc#core_type e state in - let state, x, gls = (core_type).Conversion.embed ~depth state e in + let ctx = new ctx_for_core_type [] state in + let csts = RawData.no_constraints in + let state, x, gls = (core_type).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x @@ -113,7 +120,9 @@ let stri_quotation ~depth state _loc s = match e with | Ptop_def [e] -> let e, state = erase_loc#structure_item e state in - let state, x, gls = (structure_item).Conversion.embed ~depth state e in + let ctx = new ctx_for_structure_item [] state in + let csts = RawData.no_constraints in + let state, x, gls = (structure_item).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x | Ptop_def _ -> @@ -128,7 +137,9 @@ let sigi_quotation ~depth state _loc s = match e with | [e] -> let e, state = erase_loc#signature_item e state in - let state, x, gls = (signature_item).Conversion.embed ~depth state e in + let ctx = new ctx_for_signature_item [] state in + let csts = RawData.no_constraints in + let state, x, gls = (signature_item).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x | _ -> @@ -139,7 +150,9 @@ let () = Quotation.register_named_quotation ~name:"sigi" stri_quotation let structure_quotation ~depth state _loc s = let e = Ppxlib.Parse.implementation (Lexing.from_string s) in let e, state = erase_loc#structure e state in - let state, x, gls = (structure).Conversion.embed ~depth state e in + let ctx = new ctx_for_structure [] state in + let csts = RawData.no_constraints in + let state, x, gls = (structure).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x @@ -148,7 +161,9 @@ let () = Quotation.register_named_quotation ~name:"str" structure_quotation let signature_quotation ~depth state _loc s = let e = Ppxlib.Parse.interface (Lexing.from_string s) in let e, state = erase_loc#signature e state in - let state, x, gls = (signature).Conversion.embed ~depth state e in + let ctx = new ctx_for_signature [] state in + let csts = RawData.no_constraints in + let state, x, gls = (signature).ContextualConversion.embed ~depth ctx csts state e in assert(gls = []); state, x @@ -166,7 +181,7 @@ let arg_typecheck t = match Driver.Cookies.get t "typecheck" Ast_pattern.(__) with | Some _ -> typecheck := true | _ -> () - + let arg_debug t = match Driver.Cookies.get t "debug" Ast_pattern.(__) with | Some _ -> debug := true diff --git a/ocaml-elpi/ocaml_ast_for_elpi.ml b/ocaml-elpi/ocaml_ast_for_elpi.ml index 43c552ab4..7816c5414 100644 --- a/ocaml-elpi/ocaml_ast_for_elpi.ml +++ b/ocaml-elpi/ocaml_ast_for_elpi.ml @@ -31,23 +31,23 @@ let dummy_location = loc_ghost = false } -let maybe_override_embed default = fun ~depth st e -> +let maybe_override_embed default = fun ~depth h c st e -> let open Parsetree in match e with | ({ Location.txt = ("e"|"p"|"t"|"m"|"i"); _ }, PStr [{ pstr_desc = Pstr_eval ({ pexp_desc = Parsetree.Pexp_constant (Pconst_string(s,_,_)); pexp_loc = loc; _ },[]) ; _}]) -> let loc = elpi_loc_of_location loc in let st, x = Elpi.API.Quotation.lp ~depth st loc s in st, x, [] - | e -> default ~depth st e + | e -> default ~depth h c st e -let maybe_override_embed2 default = fun ~depth st e a -> +let maybe_override_embed2 default = fun ~depth h c st e a -> let open Parsetree in match e with | ({ Location.txt = ("e"|"p"|"t"|"m"|"i"); _ }, PStr [{ pstr_desc = Pstr_eval ({ pexp_desc = Parsetree.Pexp_constant (Pconst_string(s,_,_)); pexp_loc = loc; _ },[]) ; _}]) -> let loc = elpi_loc_of_location loc in let st, x = Elpi.API.Quotation.lp ~depth st loc s in st, x, [] - | _ -> default ~depth st e a + | _ -> default ~depth h c st e a module Warnings = struct include Warnings @@ -109,16 +109,16 @@ and location = Location.t = { loc_start: position; loc_end: position; loc_ghost: bool; -} [@@elpi.embed fun default ~depth st start end_ ghost -> +} [@@elpi.embed fun default ~depth h c st start end_ ghost -> if ghost = false && start = dummy_position && end_ = dummy_position then let st, v = Elpi.API.FlexibleData.Elpi.make st in st, Elpi.API.RawData.mkUnifVar v ~args: [] st, [] else - default ~depth st start end_ ghost ] - [@@elpi.default_constructor_readback fun default ~depth st t -> + default ~depth h c st start end_ ghost ] + [@@elpi.default_constructor_readback fun default ~depth h c st t -> match Elpi.API.RawData.look ~depth t with | Elpi.API.RawData.UnifVar _ -> st, dummy_location, [] - | _ -> default ~depth st t] + | _ -> default ~depth h c st t] and location_stack = location list @@ -1111,7 +1111,5 @@ and directive_argument_desc = Parsetree.directive_argument_desc = | Pdir_bool of bool [@@deriving show, elpi { declaration = parsetree_declaration; mapper = parsetree_mapper }] - - let parsetree_declaration = !parsetree_declaration let parsetree_mapper = !parsetree_mapper diff --git a/ocaml-elpi/tests/dune.inc b/ocaml-elpi/tests/dune.inc index 624a88f47..e8d18fdcf 100644 --- a/ocaml-elpi/tests/dune.inc +++ b/ocaml-elpi/tests/dune.inc @@ -1,7 +1,7 @@ (rule (targets test_swap.actual.ml) - (deps (:pp pp.exe) (:input test_swap.ml) ../ocaml_ast.elpi) + (deps (:pp pp.exe) (:input test_swap.ml) ../ocaml_ast.elpi test_swap.elpi) (action (run ./%{pp} --impl %{input} --cookie "program=\"test_swap.elpi\"" -o %{targets}))) (rule diff --git a/ocaml-elpi/tests/gen_dune.ml b/ocaml-elpi/tests/gen_dune.ml index 31c8e10b5..7025fe2a6 100644 --- a/ocaml-elpi/tests/gen_dune.ml +++ b/ocaml-elpi/tests/gen_dune.ml @@ -5,7 +5,7 @@ let output_stanzas filename = Printf.printf {| (rule (targets %s.actual.ml) - (deps (:pp pp.exe) (:input %s.ml) ../ocaml_ast.elpi) + (deps (:pp pp.exe) (:input %s.ml) ../ocaml_ast.elpi %s.elpi) (action (run ./%%{pp} --impl %%{input} --cookie "program=\"%s.elpi\"" -o %%{targets}))) (rule @@ -18,7 +18,7 @@ let output_stanzas filename = (preprocess (pps ocaml-elpi.ppx -- --cookie "program=\"ocaml-elpi/tests/%s.elpi\""))) |} - base base base base base base base base + base base base base base base base base base let is_test filename = Filename.check_suffix filename ".ml" && diff --git a/ocaml-elpi/tests/test_swap.elpi b/ocaml-elpi/tests/test_swap.elpi index 04201207a..c9e7a750c 100644 --- a/ocaml-elpi/tests/test_swap.elpi +++ b/ocaml-elpi/tests/test_swap.elpi @@ -1,3 +1,3 @@ + map.value-binding (value-binding {{:pat ( [%e "P1"], [%e "P2" ] ) }} E X L) (value-binding {{:pat ( [%e "P2"], [%e "P1" ] ) }} E X L) :- !. - diff --git a/ppx_elpi/ppx_elpi.ml b/ppx_elpi/ppx_elpi.ml index 77b0bf4e0..ad80beb86 100644 --- a/ppx_elpi/ppx_elpi.ml +++ b/ppx_elpi/ppx_elpi.ml @@ -305,9 +305,9 @@ let is_HO = function HO _ -> true | _ -> false let ctx_index_ty (module B : Ast_builder.S) = let open B in FO { - readback = [%expr Elpi.API.BuiltInData.nominal.Elpi.API.ContextualConversion.readback ]; - embed = [%expr Elpi.API.BuiltInData.nominal.Elpi.API.ContextualConversion.embed ]; - ty_ast = [%expr Elpi.API.BuiltInData.nominal.Elpi.API.ContextualConversion.ty ]; + readback = [%expr Elpi.API.BuiltInContextualData.nominal.Elpi.API.ContextualConversion.readback ]; + embed = [%expr Elpi.API.BuiltInContextualData.nominal.Elpi.API.ContextualConversion.embed ]; + ty_ast = [%expr Elpi.API.BuiltInContextualData.nominal.Elpi.API.ContextualConversion.ty ]; ty = [%type: Elpi.API.Data.constant ]; key = false; } @@ -432,7 +432,7 @@ let rec embed_k (module B : Ast_builder.S) c all_kargs all_tmp kargs tmp tys n = [%expr elpi__state, Elpi.API.RawData.mkAppL [%e c] [%e elist @@ List.map evar @@ List.map fst all_kargs], List.concat [%e elist all_tmp] ] | (px,ex) :: xs, y :: ys, (FO { embed = t; _ }) :: ts -> [%expr let elpi__state, [%p pvar px], [%p pvar y] = - [%e t] ~depth: elpi__depth elpi__state [%e ex] in + [%e t] ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state [%e ex] in [%e embed_k (module B) c all_kargs all_tmp xs ys ts (n+1)]] | (px,ex) :: xs, y :: ys, HO{ build_ctx = f; embed = t; ctx = ctx_name; _ } :: ts -> let xtmp = fresh () in @@ -445,7 +445,7 @@ let rec embed_k (module B : Ast_builder.S) c all_kargs all_tmp kargs tmp tys n = let elpi__ctx_entry = { Elpi.API.ContextualConversion.entry = elpi__ctx_entry; depth = elpi__depth } in let elpi__state = [%e elpi_push ] ~depth: (elpi__depth + 1) elpi__state elpi__ctx_key elpi__ctx_entry in let elpi__state, [%p pvar xtmp], [%p pvar y] = - [%e t] ~depth: (elpi__depth + 1) elpi__state [%e ex] in + [%e t] ~depth: (elpi__depth + 1) elpi__hyps elpi__constraints elpi__state [%e ex] in let [%p pvar px] = Elpi.API.RawData.mkLam [%e evar xtmp] in let elpi__state = [%e elpi_pop ] ~depth: (elpi__depth + 1) elpi__state elpi__ctx_key in [%e embed_k (module B) c all_kargs all_tmp xs ys ts (n+1)]] @@ -471,7 +471,7 @@ let abstract_standard_branch_embed (module B : Ast_builder.S) l e = let open B i | [] -> e | x::xs -> [%expr fun [%p pvar x] -> [%e aux xs]] in - [%expr fun ~depth: elpi__depth elpi__state -> [%e aux l ]] + [%expr fun ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state -> [%e aux l ]] let embed_branch (module B : Ast_builder.S) is_pred = function | Skip { constructor_name; has_args } -> error_constructor_not_supported (module B) (constructor_name,has_args) @@ -491,14 +491,14 @@ let embed_branch (module B : Ast_builder.S) is_pred = function ~rhs:begin match embed with | Custom { ml; _ } -> eapply [%expr [%e ml] [%e abstract_standard_branch_embed (module B) pvl standard ] - ~depth: elpi__depth elpi__state] (List.map evar pvl) + ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state] (List.map evar pvl) | Standard -> standard | Name { get_key; ctx_name } -> embed_var (module B) ctx_name (List.map evar pvl) get_key end let embed (module B : Ast_builder.S) is_pred kl = let open B in - [%expr fun ~depth: elpi__depth elpi__state -> + [%expr fun ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state -> [%e pexp_function (List.map (embed_branch (module B) is_pred) kl) ]] let readback_k (module B : Ast_builder.S) c mk_k t ts = let open B in @@ -506,7 +506,7 @@ let readback_k (module B : Ast_builder.S) c mk_k t ts = let open B in match t with | FO { readback = t; _ } -> [%expr let elpi__state, [%p pvar p1], [%p pvar e1] = - [%e t] ~depth: elpi__depth elpi__state [%e x] in + [%e t] ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state [%e x] in [%e kont] ] | HO { build_ctx = f; readback = t; ctx = ctx_name; _ } -> let elpi_to_key = evar (elpi_to_key ctx_name) in @@ -520,7 +520,7 @@ let readback_k (module B : Ast_builder.S) c mk_k t ts = let open B in let elpi__state, [%p pvar p1], [%p pvar e1] = match Elpi.API.RawData.look ~depth: elpi__depth [%e x] with | Elpi.API.RawData.Lam elpi__bo -> - [%e t] ~depth: (elpi__depth + 1) elpi__state elpi__bo + [%e t] ~depth: (elpi__depth + 1) elpi__hyps elpi__constraints elpi__state elpi__bo | _ -> assert false in let elpi__state = [%e elpi_pop ] ~depth: elpi__depth elpi__state elpi__ctx_key in [%e kont]] in @@ -561,12 +561,12 @@ let readback_var (module B : Ast_builder.S) ctx_name constructor = let open B in ] let abstract_standard_branch_readback (module B : Ast_builder.S) pos e = let open B in - [%expr fun ~depth: elpi__depth elpi__state -> function + [%expr fun ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state -> function | [] -> [%e e ] | _ -> Elpi.API.Utils.error ~loc: [%e elpi_loc_of_position (module B) pos ] "standard branch readback takes 0 arguments"] let abstract_standard_branch_readback2 (module B : Ast_builder.S) pos e = let open B in - [%expr fun ~depth: elpi__depth elpi__state -> function + [%expr fun ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state -> function | elpi__x :: elpi__xs -> [%e e ] | [] -> Elpi.API.Utils.error ~loc: [%e elpi_loc_of_position (module B) pos ] "standard branch readback takes 1 argument or more"] @@ -594,17 +594,17 @@ let readback_branch (module B : Ast_builder.S) is_pred { constant; constructor; | Custom { ml; pos } -> case ~lhs:[%pat? Elpi.API.RawData.App (elpi__hd,elpi__x,elpi__xs)] ~guard:(Some [%expr elpi__hd == [%e constant]]) - ~rhs:([%expr [%e ml] [%e abstract_standard_branch_readback2 (module B) pos standard ] ~depth: elpi__depth elpi__state (elpi__x :: elpi__xs)]) + ~rhs:([%expr [%e ml] [%e abstract_standard_branch_readback2 (module B) pos standard ] ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state (elpi__x :: elpi__xs)]) | Name { ctx_name; _} -> assert(ts = []); case ~lhs:[%pat? Elpi.API.RawData.Const elpi__hd] ~guard:(Some [%expr elpi__hd >= 0]) ~rhs:(readback_var (module B) ctx_name constructor) let abstract_standard_default_readback (module B : Ast_builder.S) e = let open B in - [%expr fun ~depth: elpi__depth elpi__state elpi__x -> [%e e]] + [%expr fun ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state elpi__x -> [%e e]] let readback (module B : Ast_builder.S) name is_pred default_readback kl = let open B in - [%expr fun ~depth: elpi__depth elpi__state elpi__x -> + [%expr fun ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state elpi__x -> [%e pexp_match [%expr Elpi.API.RawData.look ~depth: elpi__depth elpi__x] (List.map (readback_branch (module B) is_pred) (drop_skip kl) @ [case ~guard:None ~lhs:[%pat? _ ] @@ -614,7 +614,7 @@ let readback (module B : Ast_builder.S) name is_pred default_readback kl = let o [%e estring name] (Elpi.API.RawPp.term elpi__depth) elpi__x) ] in match default_readback with | None -> standard - | Some e -> [%expr [%e e] [%e abstract_standard_default_readback (module B) standard ] ~depth: elpi__depth elpi__state elpi__x ] + | Some e -> [%expr [%e e] [%e abstract_standard_default_readback (module B) standard ] ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state elpi__x ] end])]] let ctx_entry_key (module B : Ast_builder.S) kl = let open B in @@ -721,17 +721,17 @@ let rec fmap f = function [] -> [] | x :: xs -> match f x with None -> fmap f xs let conversion_of (module B : Ast_builder.S) ty = let open B in let rec aux = function - | [%type: string] -> [%expr Elpi.API.BuiltInData.string] - | [%type: int] -> [%expr Elpi.API.BuiltInData.int] - | [%type: float] -> [%expr Elpi.API.BuiltInData.float] - | [%type: bool] -> [%expr Elpi.Builtin.bool] - | [%type: char] -> [%expr Elpi.Builtin.char] - | [%type: [%t? typ] list] -> [%expr Elpi.API.BuiltInData.list [%e aux typ ]] - | [%type: [%t? typ] option] -> [%expr Elpi.Builtin.option [%e aux typ ]] - | [%type: [%t? typ1] * [%t? typ2]] -> [%expr Elpi.Builtin.pair [%e aux typ1 ] [%e aux typ2 ]] - | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3]] -> [%expr Elpi.Builtin.triple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ]] - | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3] * [%t? typ4]] -> [%expr Elpi.Builtin.quadruple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ] [%e aux typ4 ]] - | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3] * [%t? typ4] * [%t? typ5]] -> [%expr Elpi.Builtin.quintuple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ] [%e aux typ4 ] [%e aux typ5 ]] + | [%type: string] -> [%expr Elpi.API.BuiltInContextualData.string] + | [%type: int] -> [%expr Elpi.API.BuiltInContextualData.int] + | [%type: float] -> [%expr Elpi.API.BuiltInContextualData.float] + | [%type: bool] -> [%expr Elpi.Builtin.PPX.bool] + | [%type: char] -> [%expr Elpi.Builtin.PPX.char] + | [%type: [%t? typ] list] -> [%expr Elpi.API.BuiltInContextualData.list [%e aux typ ]] + | [%type: [%t? typ] option] -> [%expr Elpi.Builtin.PPX.option [%e aux typ ]] + | [%type: [%t? typ1] * [%t? typ2]] -> [%expr Elpi.Builtin.PPX.pair [%e aux typ1 ] [%e aux typ2 ]] + | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3]] -> [%expr Elpi.Builtin.PPX.triple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ]] + | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3] * [%t? typ4]] -> [%expr Elpi.Builtin.PPX.quadruple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ] [%e aux typ4 ]] + | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3] * [%t? typ4] * [%t? typ5]] -> [%expr Elpi.Builtin.PPX.quintuple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ] [%e aux typ4 ] [%e aux typ5 ]] | { ptyp_desc = Ptyp_tuple _; _ } -> error ~loc "seriously? I don't have sixtuples at hand, file a bugreport" | { ptyp_desc = Ptyp_constr ({ txt = id; _ }, params); _ } -> let id = pexp_ident @@ Located.mk id in @@ -745,15 +745,11 @@ let is_parameter id = Re.(Str.string_match (Str.regexp_string param_prefix) id 0 let rec find_embed_of (module B : Ast_builder.S) current_mutrec_block ty = let open B in let rec aux ty = match ty with - | [%type: string] -> [%expr Elpi.API.BuiltInData.string.Elpi.API.ContextualConversion.embed] - | [%type: int] -> [%expr Elpi.API.BuiltInData.int.Elpi.API.ContextualConversion.embed] - | [%type: float] -> [%expr Elpi.API.BuiltInData.float.Elpi.API.ContextualConversion.embed] - | [%type: bool] -> [%expr Elpi.Builtin.bool.Elpi.API.ContextualConversion.embed] - | [%type: char] -> [%expr Elpi.Builtin.char.Elpi.API.ContextualConversion.embed] | [%type: [%t? typ] list] -> - [%expr ((fun embed ~depth s l -> - let s, l, eg = Elpi.API.Utils.map_acc (embed ~depth) s l in - s, Elpi.API.Utils.list_to_lp_list l, eg) [%e aux typ]) ] + [%expr (let embed = [%e aux typ] in + (fun ~depth h c s l -> + let s, l, eg = Elpi.API.Utils.map_acc (embed ~depth h c) s l in + s, Elpi.API.Utils.list_to_lp_list l, eg)) ] | [%type: [%t? typ] option] -> [%expr Elpi.Builtin.PPX.embed_option [%e aux typ ]] | [%type: [%t? typ1] * [%t? typ2]] -> [%expr Elpi.Builtin.PPX.embed_pair [%e aux typ1 ] [%e aux typ2 ]] | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3]] -> [%expr Elpi.Builtin.PPX.embed_triple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ]] @@ -764,20 +760,14 @@ let rec find_embed_of (module B : Ast_builder.S) current_mutrec_block ty = let eapply (evar (elpi_embed_name id)) (List.map (find_embed_of (module B) current_mutrec_block) params) | t -> [%expr [%e conversion_of (module B) t ].Elpi.API.ContextualConversion.embed ] in - aux ty + [%expr fun ~depth h c s t -> [%e aux ty ] ~depth h c s t ] let rec find_readback_of (module B : Ast_builder.S) current_mutrec_block ty = let open B in let rec aux ty = match ty with - | [%type: string] -> [%expr Elpi.API.BuiltInData.string.Elpi.API.ContextualConversion.readback] - | [%type: int] -> [%expr Elpi.API.BuiltInData.int.Elpi.API.ContextualConversion.readback] - | [%type: float] -> [%expr Elpi.API.BuiltInData.float.Elpi.API.ContextualConversion.readback] - | [%type: bool] -> [%expr Elpi.Builtin.bool.Elpi.API.ContextualConversion.readback] - | [%type: char] -> [%expr Elpi.Builtin.char.Elpi.API.ContextualConversion.readback] | [%type: [%t? typ] list] -> - [%expr ((fun readback ~depth s t -> - Elpi.API.Utils.map_acc (readback ~depth) s - (Elpi.API.Utils.lp_list_to_list ~depth t)) [%e aux typ])] + [%expr (let readback = [%e aux typ] in + (fun ~depth h c s t -> Elpi.API.Utils.map_acc (readback ~depth h c) s (Elpi.API.Utils.lp_list_to_list ~depth t)))] | [%type: [%t? typ] option] -> [%expr Elpi.Builtin.PPX.readback_option [%e aux typ ]] | [%type: [%t? typ1] * [%t? typ2]] -> [%expr Elpi.Builtin.PPX.readback_pair [%e aux typ1 ] [%e aux typ2 ]] | [%type: [%t? typ1] * [%t? typ2] * [%t? typ3]] -> [%expr Elpi.Builtin.PPX.readback_triple [%e aux typ1 ] [%e aux typ2 ] [%e aux typ3 ]] @@ -788,7 +778,7 @@ let rec find_readback_of (module B : Ast_builder.S) current_mutrec_block ty = l eapply (evar (elpi_readback_name id)) (List.map (find_readback_of (module B) current_mutrec_block) params) | t -> [%expr [%e conversion_of (module B) t ].Elpi.API.ContextualConversion.readback ] in - aux ty + [%expr fun ~depth h c s t -> [%e aux ty ] ~depth h c s t ] let rec find_ty_ast_of (module B : Ast_builder.S) current_mutrec_block ty = let open B in match ty with @@ -1084,10 +1074,10 @@ let conversion_type (module B : Ast_builder.S) name params is_pred all_ctx = let | [] -> let t = ptyp_constr (Located.lident name) (List.map ptyp_var params) in let t = if is_pred then ptyp_tuple [ [%type: Elpi.API.RawData.constant ] ;t] else t in - [%type: ([%t t ]) Elpi.API.ContextualConversion.t] - | t :: ts -> [%type: ([%t ptyp_var t ]) Elpi.API.ContextualConversion.t -> [%t aux ts]] + [%type: ([%t t ],[%t ctx_obj (module B) name is_pred all_ctx ] as 'c,'csts) Elpi.API.ContextualConversion.t] + | t :: ts -> [%type: ([%t ptyp_var t ],[%t ctx_obj (module B) name is_pred all_ctx ] as 'c,'csts) Elpi.API.ContextualConversion.t -> [%t aux ts]] in - quantify_ty_over_params (module B) (params @ ["c"]) (aux params) + quantify_ty_over_params (module B) (params @ ["c";"csts"]) (aux params) let readback_type (module B : Ast_builder.S) name params is_pred all_ctx = let open B in @@ -1096,9 +1086,9 @@ let readback_type (module B : Ast_builder.S) name params is_pred all_ctx = let o let t = ptyp_constr (Located.lident name) (List.map ptyp_var params) in let t = if is_pred then ptyp_tuple [ [%type: Elpi.API.RawData.constant ] ;t] else t in [%type: ([%t t ], [%t ctx_obj (module B) name is_pred all_ctx ] as 'c, 'csts) Elpi.API.ContextualConversion.readback] - | t :: ts -> [%type: ([%t ptyp_var t ]) Elpi.API.Conversion.readback -> [%t aux ts]] + | t :: ts -> [%type: ([%t ptyp_var t ], [%t ctx_obj (module B) name is_pred all_ctx ] as 'c, 'csts) Elpi.API.ContextualConversion.readback -> [%t aux ts]] in - quantify_ty_over_params (module B) (params @ ["c"]) (aux params) + quantify_ty_over_params (module B) (params @ ["c";"csts"]) (aux params) let embed_type (module B : Ast_builder.S) name params is_pred all_ctx = let open B in let rec aux = function @@ -1106,21 +1096,24 @@ let embed_type (module B : Ast_builder.S) name params is_pred all_ctx = let open let t = ptyp_constr (Located.lident name) (List.map ptyp_var params) in let t = if is_pred then ptyp_tuple [ [%type: Elpi.API.RawData.constant ] ;t] else t in [%type: ([%t t ],[%t ctx_obj (module B) name is_pred all_ctx ] as 'c, 'csts) Elpi.API.ContextualConversion.embedding] - | t :: ts -> [%type: ([%t ptyp_var t ]) Elpi.API.Conversion.embedding -> [%t aux ts]] + | t :: ts -> [%type: ([%t ptyp_var t ],[%t ctx_obj (module B) name is_pred all_ctx ] as 'c, 'csts) Elpi.API.ContextualConversion.embedding -> [%t aux ts]] in - quantify_ty_over_params (module B) (params @ ["c"]) (aux params) + quantify_ty_over_params (module B) (params @ ["c";"csts"]) (aux params) + +let lift_conversion (module B : Ast_builder.S) e = let open B in + [%expr + let { Elpi.API.Conversion.embed; readback; ty; pp_doc; pp } = [%e e ] in + let embed = (fun ~depth _ _ s t -> embed ~depth s t) in + let readback = (fun ~depth _ _ s t -> readback ~depth s t) in + { Elpi.API.ContextualConversion.embed; readback; ty; pp_doc; pp } + ] let coversion_for_opaque (module B : Ast_builder.S) elpi_name name = let open B in value_binding ~pat:(ppat_constraint (pvar name) (quantify_ty_over_params (module B) ["c"] [%type: ( [%t ptyp_constr (Located.lident name) []] , #Elpi.API.ContextualConversion.ctx as 'c, 'csts) Elpi.API.ContextualConversion.t])) - ~expr:[%expr - let { Elpi.API.Conversion.embed; readback; ty; pp_doc; pp } = [%e evar @@ elpi_cdata_name name ] in - let embed = (fun ~depth _ _ s t -> embed ~depth s t) in - let readback = (fun ~depth _ _ s t -> readback ~depth s t) in - { Elpi.API.ContextualConversion.embed; readback; ty; pp_doc; pp } - ] + ~expr:(lift_conversion (module B) (evar @@ elpi_cdata_name name)) (* let name = [%e elpi_name ] in @@ -1222,7 +1215,7 @@ let embed_for_tyd (module B : Ast_builder.S) same_mutrec_block all_ctx { name; p value_binding ~pat:(pvar (elpi_embed_name name)) ~expr:[%expr [%e evar name].Elpi.API.ContextualConversion.embed ] | Alias orig -> value_binding ~pat:(ppat_constraint (pvar (elpi_embed_name name)) (embed_type (module B) name params is_pred all_ctx)) - ~expr:(abstract_expr_over_params (module B) params elpi_embed_name @@ [%expr fun ~depth s t -> [%e find_embed_of (module B) same_mutrec_block orig] ~depth s t]) + ~expr:(abstract_expr_over_params (module B) params elpi_embed_name @@ find_embed_of (module B) same_mutrec_block orig) | Algebraic(csts,_) -> value_binding ~pat:(ppat_constraint (pvar (elpi_embed_name name)) (embed_type (module B) name params is_pred all_ctx)) ~expr:(abstract_expr_over_params (module B) params elpi_embed_name @@ embed (module B) is_pred csts) @@ -1234,7 +1227,7 @@ let readback_for_tyd (module B : Ast_builder.S) same_mutrec_block all_ctx { name value_binding ~pat:(pvar (elpi_readback_name name)) ~expr:[%expr [%e evar name].Elpi.API.ContextualConversion.readback ] | Alias orig -> value_binding ~pat:(ppat_constraint (pvar (elpi_readback_name name)) (readback_type (module B) name params is_pred all_ctx)) - ~expr:(abstract_expr_over_params (module B) params elpi_readback_name @@ [%expr fun ~depth s t -> [%e find_readback_of (module B) same_mutrec_block orig] ~depth s t]) + ~expr:(abstract_expr_over_params (module B) params elpi_readback_name @@ find_readback_of (module B) same_mutrec_block orig) | Algebraic(csts,def_readback) -> value_binding ~pat:(ppat_constraint (pvar (elpi_readback_name name)) (readback_type (module B) name params is_pred all_ctx)) ~expr:(abstract_expr_over_params (module B) params elpi_readback_name @@ readback (module B) name is_pred def_readback csts) @@ -1300,7 +1293,7 @@ let elpi_declaration_of_tyd (module B : Ast_builder.S) tyd = let open B in match tyd.type_decl with | Alias orig -> (if tyd.params = [] then (fun x -> x) - else pexp_let Nonrecursive (List.mapi (fun i x -> value_binding ~pat:(pvar x) ~expr:[%expr Elpi.API.BuiltInData.poly (Printf.sprintf "A%d" [%e eint i]) ]) tyd.params)) + else pexp_let Nonrecursive (List.mapi (fun i x -> value_binding ~pat:(pvar x) ~expr:(pexp_ident @@ Located.lident @@ Printf.sprintf "Elpi.API.BuiltInContextualData.polyA%d" i)) tyd.params)) [%expr Elpi.API.BuiltIn.LPCode ("typeabbrev " ^ [%e typeabbrev_for (module B) (estring tyd.elpi_name) tyd.params ] ^ " " ^ @@ -1310,8 +1303,8 @@ let elpi_declaration_of_tyd (module B : Ast_builder.S) tyd = let open B in if tyd.params = [] then evar tyd.name else error ~loc "opaque with params" ]] | Algebraic _ -> - let vars = List.mapi (fun i _ -> [%expr Elpi.API.BuiltInData.poly [%e estring @@ Printf.sprintf "A%d" i] ]) tyd.params in - [%expr Elpi.API.BuiltIn.MLData [%e + let vars = List.mapi (fun i _ -> pexp_ident @@ Located.lident @@ Printf.sprintf "Elpi.API.BuiltInContextualData.polyA%d" i) tyd.params in + [%expr Elpi.API.BuiltIn.MLDataC [%e if tyd.params = [] then evar tyd.name else eapply (evar tyd.name) vars]] in { decl = pstr_value Nonrecursive [value_binding ~pat:(pvar decl_name) ~expr:decl]; @@ -1395,7 +1388,8 @@ let extras_of_task (module B : Ast_builder.S) { types; names; context; ctx_names ~expr:(pmod_apply (pmod_ident (Located.mk (Longident.parse "Elpi.API.Utils.Map.Make"))) m)); pstr_value Nonrecursive [value_binding ~pat:(pvar (elpi_state_name name)) ~expr:[%expr Elpi.API.State.declare ~name:[%e estring elpi_name] ~pp:(fun fmt _ -> Format.fprintf fmt "TODO") - ~init:(fun () -> [%e initial_state (module B) name]); + ~init:(fun () -> [%e initial_state (module B) name]) + ~start:(fun x -> x); ]]; pstr_value Nonrecursive [value_binding ~pat:(pvar (elpi_to_key name)) ~expr:(ctx_entry_key (module B) csts)]; pstr_value Nonrecursive [value_binding ~pat:(pvar (elpi_is_ctx_entry_name name)) ~expr:(is_ctx_entry (module B) csts)]; diff --git a/ppx_elpi/tests/dune.inc b/ppx_elpi/tests/dune.inc index 2d576f448..9596cada7 100644 --- a/ppx_elpi/tests/dune.inc +++ b/ppx_elpi/tests/dune.inc @@ -22,6 +22,29 @@ (preprocess (pps elpi.ppx))) +(rule + (targets test_container.actual.ml) + (deps (:pp pp.exe) (:input test_container.ml)) + (action (run ./%{pp} -deriving-keep-w32 both --impl %{input} -o %{targets}))) + +(rule + (alias runtest) + (action (diff test_container.expected.ml test_container.actual.ml))) + +(rule + (alias runtest) + (action (diff test_container.expected.elpi test_container.actual.elpi))) + +(rule + (target test_container.actual.elpi) + (action (run ./test_container.exe %{target}))) + +(executable + (name test_container) + (modules test_container) + (preprocess (pps elpi.ppx))) + + (rule (targets test_double_contextual.actual.ml) (deps (:pp pp.exe) (:input test_double_contextual.ml)) diff --git a/ppx_elpi/tests/test_container.expected.elpi b/ppx_elpi/tests/test_container.expected.elpi new file mode 100644 index 000000000..24da75ab0 --- /dev/null +++ b/ppx_elpi/tests/test_container.expected.elpi @@ -0,0 +1,16 @@ + + +% loc +kind loc type -> type. +type loc int -> A0 -> loc A0. % loc + +% term +kind term type. +type a int -> term. % A +type b string -> bool -> term. % B + +typeabbrev x (pair (loc term) int). % x + + + + diff --git a/ppx_elpi/tests/test_container.expected.ml b/ppx_elpi/tests/test_container.expected.ml new file mode 100644 index 000000000..e69de29bb diff --git a/ppx_elpi/tests/test_container.ml b/ppx_elpi/tests/test_container.ml new file mode 100644 index 000000000..fc2b3a367 --- /dev/null +++ b/ppx_elpi/tests/test_container.ml @@ -0,0 +1,34 @@ +let declaration = ref [] + +let pp_loc _ _ _ = () + +type 'a loc = { + loc : int; + data : 'a; +} +[@@deriving elpi { declaration }] + +let pp_term _ _ = () +type term = + | A of int + | B of string * bool +[@@deriving elpi { declaration }] + +let pp_x _ _ = () +type x = term loc * int +[@@deriving elpi { declaration }] + +let xx : 'c 'csts. (x,'c,'csts) Elpi.API.ContextualConversion.t = x + +open Elpi.API + +let builtin = let open BuiltIn in + declare ~file_name:(Sys.argv.(1)) !declaration + +let main () = + let _elpi= Setup.init ~builtins:[builtin] () in + BuiltIn.document_file builtin; + exit 0 +;; + +main () \ No newline at end of file diff --git a/ppx_elpi/tests/test_double_contextual.ml b/ppx_elpi/tests/test_double_contextual.ml index f55051bd8..2a454244a 100644 --- a/ppx_elpi/tests/test_double_contextual.ml +++ b/ppx_elpi/tests/test_double_contextual.ml @@ -44,16 +44,16 @@ open Elpi.API open BuiltInPredicate open Notation -let term_to_string = Pred("term->string", - In(term,"T", - Out(BuiltInData.string,"S", - Read("what else"))),in_ctx_for_term, +let term_to_string = CPred("term->string",in_ctx_for_term, + CIn(term,"T", + COut(BuiltInContextualData.string,"S", + CRead("what else"))), fun (t : term) (_ety : string oarg) ~depth:_ c (_cst : Data.constraints) (_state : State.t) -> !: (Format.asprintf "@[%a@ ; %a@ |-@ %a@]@\n%!" - (RawData.Constants.Map.pp (Conversion.pp_ctx_entry pp_tctx)) c#tyctx - (RawData.Constants.Map.pp (Conversion.pp_ctx_entry pp_tctx)) c#tctx + (RawData.Constants.Map.pp (ContextualConversion.pp_ctx_entry pp_tctx)) c#tyctx + (RawData.Constants.Map.pp (ContextualConversion.pp_ctx_entry pp_tctx)) c#tctx term.pp t) ) @@ -68,7 +68,7 @@ let builtin2 = let open BuiltIn in declare ~file_name:(Sys.argv.(1)) !declaration let main () = - let _elpi, _ = Setup.init ~builtins:[builtin1;builtin2] ~basedir:"." [] in + let _elpi = Setup.init ~builtins:[builtin1;builtin2] () in BuiltIn.document_file builtin2; exit 0 ;; diff --git a/ppx_elpi/tests/test_mutual_contextual.ml b/ppx_elpi/tests/test_mutual_contextual.ml index 76cccfa3c..4b0d2a673 100644 --- a/ppx_elpi/tests/test_mutual_contextual.ml +++ b/ppx_elpi/tests/test_mutual_contextual.ml @@ -19,692 +19,20 @@ and tctx = | Entry of (string[@elpi.index]) * ty | TEentry of (string[@elpi.index]) * bool [@@elpi.index (module String)] -[@@deriving_inline elpi { declaration }] -[@@@warning "-26-27-32-39-60"] -let elpi_constant_type_term = "term" -let elpi_constant_type_termc = - Elpi.API.RawData.Constants.declare_global_symbol elpi_constant_type_term -let elpi_constant_constructor_term_Var = "var" -let elpi_constant_constructor_term_Varc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_term_Var -let elpi_constant_constructor_term_App = "app" -let elpi_constant_constructor_term_Appc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_term_App -let elpi_constant_constructor_term_Tapp = "tapp" -let elpi_constant_constructor_term_Tappc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_term_Tapp -let elpi_constant_constructor_term_Lam = "lam" -let elpi_constant_constructor_term_Lamc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_term_Lam -let elpi_constant_type_ty = "ty" -let elpi_constant_type_tyc = - Elpi.API.RawData.Constants.declare_global_symbol elpi_constant_type_ty -let elpi_constant_constructor_ty_TVar = "tvar" -let elpi_constant_constructor_ty_TVarc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_ty_TVar -let elpi_constant_constructor_ty_TIdx = "tidx" -let elpi_constant_constructor_ty_TIdxc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_ty_TIdx -let elpi_constant_constructor_ty_TAbs = "tabs" -let elpi_constant_constructor_ty_TAbsc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_ty_TAbs -let elpi_constant_type_tctx = "tctx" -let elpi_constant_type_tctxc = - Elpi.API.RawData.Constants.declare_global_symbol elpi_constant_type_tctx -let elpi_constant_constructor_tctx_Entry = "entry" -let elpi_constant_constructor_tctx_Entryc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_tctx_Entry -let elpi_constant_constructor_tctx_TEentry = "teentry" -let elpi_constant_constructor_tctx_TEentryc = - Elpi.API.RawData.Constants.declare_global_symbol - elpi_constant_constructor_tctx_TEentry -module Ctx_for_term = +[@@deriving elpi { declaration }] -ONLY ONE - - struct - class type t = - object - inherit Elpi.API.Conversion.ctx - inherit Ctx_for_tctx.t - method tctx : tctx Elpi.API.Conversion.ctx_field - end - end -module Ctx_for_ty = - struct - class type t = - object - inherit Elpi.API.Conversion.ctx - inherit Ctx_for_tctx.t - method tctx : tctx Elpi.API.Conversion.ctx_field - end - end -module Ctx_for_tctx = - struct - class type t = - object - inherit Elpi.API.Conversion.ctx - inherit Ctx_for_tctx.t - method tctx : tctx Elpi.API.Conversion.ctx_field - end - end -let rec elpi_embed_term : - 'c . (term, #Ctx_for_term.t as 'c) Elpi.API.Conversion.embedding = - fun ~depth:elpi__depth -> - fun elpi__hyps -> - fun elpi__constraints -> - fun elpi__state -> - function - | Var elpi__17 -> - let (elpi__ctx2dbl, _) = - Elpi.API.State.get elpi_tctx_state elpi__state in - let elpi__key = (fun x -> x) elpi__17 in - (if not (Elpi_tctx_Map.mem elpi__key elpi__ctx2dbl) - then Elpi.API.Utils.error "Unbound variable"; - (elpi__state, - (Elpi.API.RawData.mkBound - (Elpi_tctx_Map.find elpi__key elpi__ctx2dbl)), [])) - | App (elpi__20, elpi__21) -> - let (elpi__state, elpi__24, elpi__22) = - elpi_embed_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__20 in - let (elpi__state, elpi__25, elpi__23) = - elpi_embed_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__21 in - (elpi__state, - (Elpi.API.RawData.mkAppL elpi_constant_constructor_term_Appc - [elpi__24; elpi__25]), (List.concat [elpi__22; elpi__23])) - | Tapp (elpi__26, elpi__27) -> - let (elpi__state, elpi__30, elpi__28) = - elpi_embed_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__26 in - let (elpi__state, elpi__31, elpi__29) = - elpi_embed_ty ~depth:elpi__depth elpi__hyps elpi__constraints - elpi__state elpi__27 in - (elpi__state, - (Elpi.API.RawData.mkAppL elpi_constant_constructor_term_Tappc - [elpi__30; elpi__31]), (List.concat [elpi__28; elpi__29])) - | Lam (elpi__32, elpi__33, elpi__34) -> - let (elpi__state, elpi__38, elpi__35) = - elpi_embed_ty ~depth:elpi__depth elpi__hyps elpi__constraints - elpi__state elpi__32 in - let (elpi__state, elpi__39, elpi__36) = - Elpi.API.PPX.embed_string ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__33 in - let elpi__ctx_entry = - (fun b -> fun s -> Entry (s, b)) elpi__32 elpi__33 in - let elpi__ctx_key = - elpi_tctx_to_key ~depth:elpi__depth elpi__ctx_entry in - let elpi__ctx_entry = - { - Elpi.API.Conversion.entry = elpi__ctx_entry; - depth = elpi__depth - } in - let elpi__state = - elpi_push_tctx ~depth:(elpi__depth + 1) elpi__state - elpi__ctx_key elpi__ctx_entry in - let (elpi__state, elpi__41, elpi__37) = - elpi_embed_term ~depth:(elpi__depth + 1) elpi__hyps - elpi__constraints elpi__state elpi__34 in - let elpi__40 = Elpi.API.RawData.mkLam elpi__41 in - let elpi__state = - elpi_pop_tctx ~depth:(elpi__depth + 1) elpi__state - elpi__ctx_key in - (elpi__state, - (Elpi.API.RawData.mkAppL elpi_constant_constructor_term_Lamc - [elpi__38; elpi__39; elpi__40]), - (List.concat [elpi__35; elpi__36; elpi__37])) -and elpi_embed_ty : - 'c . (ty, #Ctx_for_ty.t as 'c) Elpi.API.Conversion.embedding = - fun ~depth:elpi__depth -> - fun elpi__hyps -> - fun elpi__constraints -> - fun elpi__state -> - function - | TVar elpi__54 -> - let (elpi__ctx2dbl, _) = - Elpi.API.State.get elpi_tctx_state elpi__state in - let elpi__key = (fun x -> x) elpi__54 in - (if not (Elpi_tctx_Map.mem elpi__key elpi__ctx2dbl) - then Elpi.API.Utils.error "Unbound variable"; - (elpi__state, - (Elpi.API.RawData.mkBound - (Elpi_tctx_Map.find elpi__key elpi__ctx2dbl)), [])) - | TIdx (elpi__57, elpi__58) -> - let (elpi__state, elpi__61, elpi__59) = - elpi_embed_ty ~depth:elpi__depth elpi__hyps elpi__constraints - elpi__state elpi__57 in - let (elpi__state, elpi__62, elpi__60) = - elpi_embed_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__58 in - (elpi__state, - (Elpi.API.RawData.mkAppL elpi_constant_constructor_ty_TIdxc - [elpi__61; elpi__62]), (List.concat [elpi__59; elpi__60])) - | TAbs (elpi__63, elpi__64, elpi__65) -> - let (elpi__state, elpi__69, elpi__66) = - Elpi.API.PPX.embed_string ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__63 in - let (elpi__state, elpi__70, elpi__67) = - Elpi.Builtin.PPX.embed_bool ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__64 in - let elpi__ctx_entry = - (fun s -> fun b -> TEntry (s, b)) elpi__63 elpi__64 in - let elpi__ctx_key = - elpi_tctx_to_key ~depth:elpi__depth elpi__ctx_entry in - let elpi__ctx_entry = - { - Elpi.API.Conversion.entry = elpi__ctx_entry; - depth = elpi__depth - } in - let elpi__state = - elpi_push_tctx ~depth:(elpi__depth + 1) elpi__state - elpi__ctx_key elpi__ctx_entry in - let (elpi__state, elpi__72, elpi__68) = - elpi_embed_ty ~depth:(elpi__depth + 1) elpi__hyps - elpi__constraints elpi__state elpi__65 in - let elpi__71 = Elpi.API.RawData.mkLam elpi__72 in - let elpi__state = - elpi_pop_tctx ~depth:(elpi__depth + 1) elpi__state - elpi__ctx_key in - (elpi__state, - (Elpi.API.RawData.mkAppL elpi_constant_constructor_ty_TAbsc - [elpi__69; elpi__70; elpi__71]), - (List.concat [elpi__66; elpi__67; elpi__68])) -and elpi_embed_tctx : - 'c . - ((Elpi.API.RawData.constant * tctx), #Ctx_for_tctx.t as 'c) - Elpi.API.Conversion.embedding - = - fun ~depth:elpi__depth -> - fun elpi__hyps -> - fun elpi__constraints -> - fun elpi__state -> - function - | (elpi__87, Entry (elpi__85, elpi__86)) -> - let (elpi__state, elpi__91, elpi__88) = - Elpi.API.BuiltInData.nominal.Elpi.API.Conversion.embed - ~depth:elpi__depth elpi__hyps elpi__constraints elpi__state - elpi__87 in - let (elpi__state, elpi__92, elpi__89) = - Elpi.API.PPX.embed_string ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__85 in - let (elpi__state, elpi__93, elpi__90) = - elpi_embed_ty ~depth:elpi__depth elpi__hyps elpi__constraints - elpi__state elpi__86 in - (elpi__state, - (Elpi.API.RawData.mkAppL - elpi_constant_constructor_tctx_Entryc - [elpi__91; elpi__92; elpi__93]), - (List.concat [elpi__88; elpi__89; elpi__90])) - | (elpi__96, TEentry (elpi__94, elpi__95)) -> - let (elpi__state, elpi__100, elpi__97) = - Elpi.API.BuiltInData.nominal.Elpi.API.Conversion.embed - ~depth:elpi__depth elpi__hyps elpi__constraints elpi__state - elpi__96 in - let (elpi__state, elpi__101, elpi__98) = - Elpi.API.PPX.embed_string ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__94 in - let (elpi__state, elpi__102, elpi__99) = - Elpi.Builtin.PPX.embed_bool ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__95 in - (elpi__state, - (Elpi.API.RawData.mkAppL - elpi_constant_constructor_tctx_TEentryc - [elpi__100; elpi__101; elpi__102]), - (List.concat [elpi__97; elpi__98; elpi__99])) -let rec elpi_readback_term : - 'c . (term, #Ctx_for_term.t as 'c) Elpi.API.Conversion.readback = - fun ~depth:elpi__depth -> - fun elpi__hyps -> - fun elpi__constraints -> - fun elpi__state -> - fun elpi__x -> - match Elpi.API.RawData.look ~depth:elpi__depth elpi__x with - | Elpi.API.RawData.Const elpi__hd when elpi__hd >= 0 -> - let (_, elpi__dbl2ctx) = - Elpi.API.State.get elpi_tctx_state elpi__state in - (if - not - (Elpi.API.RawData.Constants.Map.mem elpi__hd - elpi__dbl2ctx) - then - Elpi.API.Utils.error - (Format.asprintf "Unbound variable: %s in %a" - (Elpi.API.RawData.Constants.show elpi__hd) - (Elpi.API.RawData.Constants.Map.pp - (Elpi.API.Conversion.pp_ctx_entry pp_tctx)) - elpi__dbl2ctx); - (let { Elpi.API.Conversion.entry = elpi__entry; - depth = elpi__depth } - = - Elpi.API.RawData.Constants.Map.find elpi__hd - elpi__dbl2ctx in - (elpi__state, - (Var (elpi_tctx_to_key ~depth:elpi__depth elpi__entry)), - []))) - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_term_Appc -> - let (elpi__state, elpi__6, elpi__5) = - elpi_readback_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__x in - (match elpi__xs with - | elpi__3::[] -> - let (elpi__state, elpi__3, elpi__4) = - elpi_readback_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__3 in - (elpi__state, (App (elpi__6, elpi__3)), - (List.concat [elpi__5; elpi__4])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_term_Appc))) - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_term_Tappc -> - let (elpi__state, elpi__10, elpi__9) = - elpi_readback_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__x in - (match elpi__xs with - | elpi__7::[] -> - let (elpi__state, elpi__7, elpi__8) = - elpi_readback_ty ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__7 in - (elpi__state, (Tapp (elpi__10, elpi__7)), - (List.concat [elpi__9; elpi__8])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_term_Tappc))) - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_term_Lamc -> - let (elpi__state, elpi__16, elpi__15) = - elpi_readback_ty ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__x in - (match elpi__xs with - | elpi__11::elpi__12::[] -> - let (elpi__state, elpi__11, elpi__13) = - Elpi.API.PPX.readback_string ~depth:elpi__depth - elpi__hyps elpi__constraints elpi__state elpi__11 in - let elpi__ctx_entry = - (fun b -> fun s -> Entry (s, b)) elpi__16 elpi__11 in - let elpi__ctx_key = - elpi_tctx_to_key ~depth:elpi__depth elpi__ctx_entry in - let elpi__ctx_entry = - { - Elpi.API.Conversion.entry = elpi__ctx_entry; - depth = elpi__depth - } in - let elpi__state = - elpi_push_tctx ~depth:elpi__depth elpi__state - elpi__ctx_key elpi__ctx_entry in - let (elpi__state, elpi__12, elpi__14) = - match Elpi.API.RawData.look ~depth:elpi__depth - elpi__12 - with - | Elpi.API.RawData.Lam elpi__bo -> - elpi_readback_term ~depth:(elpi__depth + 1) - elpi__hyps elpi__constraints elpi__state - elpi__bo - | _ -> assert false in - let elpi__state = - elpi_pop_tctx ~depth:elpi__depth elpi__state - elpi__ctx_key in - (elpi__state, (Lam (elpi__16, elpi__11, elpi__12)), - (List.concat [elpi__15; elpi__13; elpi__14])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_term_Lamc))) - | _ -> - Elpi.API.Utils.type_error - (Format.asprintf "Not a constructor of type %s: %a" "term" - (Elpi.API.RawPp.term elpi__depth) elpi__x) -and elpi_readback_ty : - 'c . (ty, #Ctx_for_ty.t as 'c) Elpi.API.Conversion.readback = - fun ~depth:elpi__depth -> - fun elpi__hyps -> - fun elpi__constraints -> - fun elpi__state -> - fun elpi__x -> - match Elpi.API.RawData.look ~depth:elpi__depth elpi__x with - | Elpi.API.RawData.Const elpi__hd when elpi__hd >= 0 -> - let (_, elpi__dbl2ctx) = - Elpi.API.State.get elpi_tctx_state elpi__state in - (if - not - (Elpi.API.RawData.Constants.Map.mem elpi__hd - elpi__dbl2ctx) - then - Elpi.API.Utils.error - (Format.asprintf "Unbound variable: %s in %a" - (Elpi.API.RawData.Constants.show elpi__hd) - (Elpi.API.RawData.Constants.Map.pp - (Elpi.API.Conversion.pp_ctx_entry pp_tctx)) - elpi__dbl2ctx); - (let { Elpi.API.Conversion.entry = elpi__entry; - depth = elpi__depth } - = - Elpi.API.RawData.Constants.Map.find elpi__hd - elpi__dbl2ctx in - (elpi__state, - (TVar (elpi_tctx_to_key ~depth:elpi__depth elpi__entry)), - []))) - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_ty_TIdxc -> - let (elpi__state, elpi__47, elpi__46) = - elpi_readback_ty ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__x in - (match elpi__xs with - | elpi__44::[] -> - let (elpi__state, elpi__44, elpi__45) = - elpi_readback_term ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__44 in - (elpi__state, (TIdx (elpi__47, elpi__44)), - (List.concat [elpi__46; elpi__45])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_ty_TIdxc))) - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_ty_TAbsc -> - let (elpi__state, elpi__53, elpi__52) = - Elpi.API.PPX.readback_string ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__x in - (match elpi__xs with - | elpi__48::elpi__49::[] -> - let (elpi__state, elpi__48, elpi__50) = - Elpi.Builtin.PPX.readback_bool ~depth:elpi__depth - elpi__hyps elpi__constraints elpi__state elpi__48 in - let elpi__ctx_entry = - (fun s -> fun b -> TEntry (s, b)) elpi__53 elpi__48 in - let elpi__ctx_key = - elpi_tctx_to_key ~depth:elpi__depth elpi__ctx_entry in - let elpi__ctx_entry = - { - Elpi.API.Conversion.entry = elpi__ctx_entry; - depth = elpi__depth - } in - let elpi__state = - elpi_push_tctx ~depth:elpi__depth elpi__state - elpi__ctx_key elpi__ctx_entry in - let (elpi__state, elpi__49, elpi__51) = - match Elpi.API.RawData.look ~depth:elpi__depth - elpi__49 - with - | Elpi.API.RawData.Lam elpi__bo -> - elpi_readback_ty ~depth:(elpi__depth + 1) - elpi__hyps elpi__constraints elpi__state - elpi__bo - | _ -> assert false in - let elpi__state = - elpi_pop_tctx ~depth:elpi__depth elpi__state - elpi__ctx_key in - (elpi__state, (TAbs (elpi__53, elpi__48, elpi__49)), - (List.concat [elpi__52; elpi__50; elpi__51])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_ty_TAbsc))) - | _ -> - Elpi.API.Utils.type_error - (Format.asprintf "Not a constructor of type %s: %a" "ty" - (Elpi.API.RawPp.term elpi__depth) elpi__x) -and elpi_readback_tctx : - 'c . - ((Elpi.API.RawData.constant * tctx), #Ctx_for_tctx.t as 'c) - Elpi.API.Conversion.readback - = - fun ~depth:elpi__depth -> - fun elpi__hyps -> - fun elpi__constraints -> - fun elpi__state -> - fun elpi__x -> - match Elpi.API.RawData.look ~depth:elpi__depth elpi__x with - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_tctx_Entryc -> - let (elpi__state, elpi__78, elpi__77) = - Elpi.API.BuiltInData.nominal.Elpi.API.Conversion.readback - ~depth:elpi__depth elpi__hyps elpi__constraints - elpi__state elpi__x in - (match elpi__xs with - | elpi__73::elpi__74::[] -> - let (elpi__state, elpi__73, elpi__75) = - Elpi.API.PPX.readback_string ~depth:elpi__depth - elpi__hyps elpi__constraints elpi__state elpi__73 in - let (elpi__state, elpi__74, elpi__76) = - elpi_readback_ty ~depth:elpi__depth elpi__hyps - elpi__constraints elpi__state elpi__74 in - (elpi__state, (elpi__78, (Entry (elpi__73, elpi__74))), - (List.concat [elpi__77; elpi__75; elpi__76])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_tctx_Entryc))) - | Elpi.API.RawData.App (elpi__hd, elpi__x, elpi__xs) when - elpi__hd == elpi_constant_constructor_tctx_TEentryc -> - let (elpi__state, elpi__84, elpi__83) = - Elpi.API.BuiltInData.nominal.Elpi.API.Conversion.readback - ~depth:elpi__depth elpi__hyps elpi__constraints - elpi__state elpi__x in - (match elpi__xs with - | elpi__79::elpi__80::[] -> - let (elpi__state, elpi__79, elpi__81) = - Elpi.API.PPX.readback_string ~depth:elpi__depth - elpi__hyps elpi__constraints elpi__state elpi__79 in - let (elpi__state, elpi__80, elpi__82) = - Elpi.Builtin.PPX.readback_bool ~depth:elpi__depth - elpi__hyps elpi__constraints elpi__state elpi__80 in - (elpi__state, - (elpi__84, (TEentry (elpi__79, elpi__80))), - (List.concat [elpi__83; elpi__81; elpi__82])) - | _ -> - Elpi.API.Utils.type_error - ("Not enough arguments to constructor: " ^ - (Elpi.API.RawData.Constants.show - elpi_constant_constructor_tctx_TEentryc))) - | _ -> - Elpi.API.Utils.type_error - (Format.asprintf "Not a constructor of type %s: %a" "tctx" - (Elpi.API.RawPp.term elpi__depth) elpi__x) -let term : 'c . (term, #Ctx_for_term.t as 'c) Elpi.API.Conversion.t = - let kind = Elpi.API.Conversion.TyName "term" in - { - Elpi.API.Conversion.ty = kind; - pp_doc = - (fun fmt -> - fun () -> - Elpi.API.PPX.Doc.kind fmt kind ~doc:"term"; - (Elpi.API.PPX.Doc.constructor fmt ~ty:kind ~name:"app" ~doc:"App" - ~args:[Elpi.API.Conversion.TyName elpi_constant_type_term; - Elpi.API.Conversion.TyName elpi_constant_type_term]; - Elpi.API.PPX.Doc.constructor fmt ~ty:kind ~name:"tapp" - ~doc:"Tapp" - ~args:[Elpi.API.Conversion.TyName elpi_constant_type_term; - Elpi.API.Conversion.TyName elpi_constant_type_ty]); - Elpi.API.PPX.Doc.constructor fmt ~ty:kind ~name:"lam" ~doc:"Lam" - ~args:[Elpi.API.Conversion.TyName elpi_constant_type_ty; - Elpi.API.BuiltInData.string.Elpi.API.Conversion.ty; - Elpi.API.Conversion.TyApp - ("->", (Elpi.API.Conversion.TyName "term"), - [Elpi.API.Conversion.TyName elpi_constant_type_term])]); - pp = pp_term; - embed = elpi_embed_term; - readback = elpi_readback_term - } -let ty : 'c . (ty, #Ctx_for_ty.t as 'c) Elpi.API.Conversion.t = - let kind = Elpi.API.Conversion.TyName "ty" in - { - Elpi.API.Conversion.ty = kind; - pp_doc = - (fun fmt -> - fun () -> - Elpi.API.PPX.Doc.kind fmt kind ~doc:"ty"; - Elpi.API.PPX.Doc.constructor fmt ~ty:kind ~name:"tidx" ~doc:"TIdx" - ~args:[Elpi.API.Conversion.TyName elpi_constant_type_ty; - Elpi.API.Conversion.TyName elpi_constant_type_term]; - Elpi.API.PPX.Doc.constructor fmt ~ty:kind ~name:"tabs" ~doc:"TAbs" - ~args:[Elpi.API.BuiltInData.string.Elpi.API.Conversion.ty; - Elpi.Builtin.bool.Elpi.API.Conversion.ty; - Elpi.API.Conversion.TyApp - ("->", (Elpi.API.Conversion.TyName "ty"), - [Elpi.API.Conversion.TyName elpi_constant_type_ty])]); - pp = pp_ty; - embed = elpi_embed_ty; - readback = elpi_readback_ty - } -let tctx : - 'c . - ((Elpi.API.RawData.constant * tctx), #Ctx_for_tctx.t as 'c) - Elpi.API.Conversion.t - = - let kind = Elpi.API.Conversion.TyName "tctx" in - { - Elpi.API.Conversion.ty = kind; - pp_doc = - (fun fmt -> - fun () -> - Elpi.API.PPX.Doc.kind fmt kind ~doc:"tctx"; - Elpi.API.PPX.Doc.constructor fmt - ~ty:(Elpi.API.Conversion.TyName "prop") ~name:"entry" - ~doc:"Entry" - ~args:[Elpi.API.BuiltInData.nominal.Elpi.API.Conversion.ty; - Elpi.API.BuiltInData.string.Elpi.API.Conversion.ty; - Elpi.API.Conversion.TyName elpi_constant_type_ty]; - Elpi.API.PPX.Doc.constructor fmt - ~ty:(Elpi.API.Conversion.TyName "prop") ~name:"teentry" - ~doc:"TEentry" - ~args:[Elpi.API.BuiltInData.nominal.Elpi.API.Conversion.ty; - Elpi.API.BuiltInData.string.Elpi.API.Conversion.ty; - Elpi.Builtin.bool.Elpi.API.Conversion.ty]); - pp = (fun fmt -> fun (_, x) -> pp_tctx fmt x); - embed = elpi_embed_tctx; - readback = elpi_readback_tctx - } -let elpi_term = Elpi.API.BuiltIn.MLData term -let elpi_ty = Elpi.API.BuiltIn.MLData ty -let elpi_tctx = Elpi.API.BuiltIn.MLData tctx -class ctx_for_term (h : Elpi.API.Data.hyps) (s : Elpi.API.Data.state) - : Ctx_for_term.t = - object (_) - inherit ((Elpi.API.Conversion.ctx) h) - inherit ! ((ctx_for_tctx) h s) - method tctx = context_made_of_tctx.Elpi.API.Conversion.get s - end -let (in_ctx_for_term : Ctx_for_term.t Elpi.API.Conversion.ctx_readback) = - fun ~depth -> - fun h -> - fun c -> - fun s -> - let ctx = (new ctx_for_tctx) h s in - let (s, gls0) = - Elpi.API.PPX.readback_context ~depth context_made_of_tctx ctx h c - s in - (s, ((new ctx_for_term) h s), (List.concat [gls0])) -class ctx_for_ty (h : Elpi.API.Data.hyps) (s : Elpi.API.Data.state) - : Ctx_for_ty.t = - object (_) - inherit ((Elpi.API.Conversion.ctx) h) - inherit ! ((ctx_for_tctx) h s) - method tctx = context_made_of_tctx.Elpi.API.Conversion.get s - end -let (in_ctx_for_ty : Ctx_for_ty.t Elpi.API.Conversion.ctx_readback) = - fun ~depth -> - fun h -> - fun c -> - fun s -> - let ctx = (new ctx_for_tctx) h s in - let (s, gls0) = - Elpi.API.PPX.readback_context ~depth context_made_of_tctx ctx h c - s in - (s, ((new ctx_for_ty) h s), (List.concat [gls0])) -class ctx_for_tctx (h : Elpi.API.Data.hyps) (s : Elpi.API.Data.state) - : Ctx_for_tctx.t = - object (_) - inherit ((Elpi.API.Conversion.ctx) h) - inherit ! ((ctx_for_tctx) h s) - method tctx = context_made_of_tctx.Elpi.API.Conversion.get s - end -let (in_ctx_for_tctx : Ctx_for_tctx.t Elpi.API.Conversion.ctx_readback) = - fun ~depth -> - fun h -> - fun c -> - fun s -> - let ctx = (new ctx_for_tctx) h s in - let (s, gls0) = - Elpi.API.PPX.readback_context ~depth context_made_of_tctx ctx h c - s in - (s, ((new ctx_for_tctx) h s), (List.concat [gls0])) -let () = declaration := ((!declaration) @ [elpi_term; elpi_ty; elpi_tctx]) -[@@@end] +ONLY ONE open Elpi.API - -let in_ctx_for_term : ctx_for_term Conversion.ctx_readback = in_ctx_for_term - -let builtin = let open BuiltIn in - declare ~file_name:(Sys.argv.(1)) !declaration - -let main () = - let _elpi, _ = Setup.init ~builtins:[builtin] ~basedir:"." [] in - BuiltIn.document_file builtin; - exit 0 -;; - -main () -rsion.ctx_readback) = - fun ~depth -> - fun h -> - fun c -> - fun s -> - let ctx = (new ctx_for_tctx) h s in - let (s, gls0) = - Elpi.API.PPX.readback_context ~depth context_made_of_tctx ctx h c - s in - (s, ((new ctx_for_ty) h s), (List.concat [gls0])) -let _ = in_ctx_for_ty -class ctx_for_tctx (h : Elpi.API.Data.hyps) (s : Elpi.API.Data.state) - : Ctx_for_tctx.t = - object (_) - inherit ((Elpi.API.Conversion.ctx) h) - inherit ! ((ctx_for_tctx) h s) - method tctx = context_made_of_tctx.Elpi.API.Conversion.get s - end -let (in_ctx_for_tctx : Ctx_for_tctx.t Elpi.API.Conversion.ctx_readback) = - fun ~depth -> - fun h -> - fun c -> - fun s -> - let ctx = (new ctx_for_tctx) h s in - let (s, gls0) = - Elpi.API.PPX.readback_context ~depth context_made_of_tctx ctx h c - s in - (s, ((new ctx_for_tctx) h s), (List.concat [gls0])) -let _ = in_ctx_for_tctx -let () = declaration := ((!declaration) @ [elpi_term; elpi_ty; elpi_tctx]) -[@@@end] - -open Elpi.API - -let in_ctx_for_term : ctx_for_term Conversion.ctx_readback = in_ctx_for_term +open BuiltInPredicate +open Notation +let in_ctx_for_term : 'csts. (ctx_for_term, 'csts) ContextualConversion.ctx_readback = in_ctx_for_term let builtin = let open BuiltIn in declare ~file_name:(Sys.argv.(1)) !declaration let main () = - let _elpi, _ = Setup.init ~builtins:[builtin] ~basedir:"." [] in + let _elpi = Setup.init ~builtins:[builtin] () in BuiltIn.document_file builtin; exit 0 ;; diff --git a/ppx_elpi/tests/test_poly_adt.expected.elpi b/ppx_elpi/tests/test_poly_adt.expected.elpi index 35a727166..bf07da145 100644 --- a/ppx_elpi/tests/test_poly_adt.expected.elpi +++ b/ppx_elpi/tests/test_poly_adt.expected.elpi @@ -4,7 +4,7 @@ kind simple type -> type. type a simple A0. % A type b int -> simple A0. % B -type c A0 -> int -> simple A0. % C +type c list A0 -> int -> simple A0. % C diff --git a/ppx_elpi/tests/test_poly_adt.ml b/ppx_elpi/tests/test_poly_adt.ml index ad3dfc5ac..20ee5d106 100644 --- a/ppx_elpi/tests/test_poly_adt.ml +++ b/ppx_elpi/tests/test_poly_adt.ml @@ -1,13 +1,15 @@ let elpi_stuff = ref [] let pp_simple _ _ _ = () -type 'a simple = A | B of int | C of 'a * int +type 'a simple = A | B of int | C of 'a list * int [@@deriving elpi { declaration = elpi_stuff } ] -class type o = object inherit Elpi.API.Conversion.ctx method foobar : bool end +let t1 : 'a 'c 'csts. ('a, #Elpi.API.ContextualConversion.ctx as 'c, 'csts) Elpi.API.ContextualConversion.t -> ('a simple, #Elpi.API.ContextualConversion.ctx as 'c, 'csts) Elpi.API.ContextualConversion.t = simple -let _ : (int simple, o) Elpi.API.Conversion.t = simple Elpi.API.BuiltInData.int -let _ : (float simple, o) Elpi.API.Conversion.t = simple Elpi.API.BuiltInData.float +class type o = object inherit Elpi.API.ContextualConversion.ctx method foobar : bool end + +let t2 : (int simple, o, Elpi.API.Data.constraints) Elpi.API.ContextualConversion.t = simple Elpi.API.BuiltInContextualData.int +let t3 : (float simple, o, Elpi.API.Data.constraints) Elpi.API.ContextualConversion.t = simple Elpi.API.BuiltInContextualData.float open Elpi.API @@ -15,9 +17,9 @@ let builtin = let open BuiltIn in declare ~file_name:(Sys.argv.(1)) !elpi_stuff let main () = - let _elpi, _ = Setup.init ~builtins:[builtin] ~basedir:"." [] in + let _elpi = Setup.init ~builtins:[builtin] () in BuiltIn.document_file builtin; exit 0 ;; -main () \ No newline at end of file +main () diff --git a/ppx_elpi/tests/test_poly_alias.ml b/ppx_elpi/tests/test_poly_alias.ml index f539a0d7c..420234b25 100644 --- a/ppx_elpi/tests/test_poly_alias.ml +++ b/ppx_elpi/tests/test_poly_alias.ml @@ -6,13 +6,13 @@ type 'a simple = 'a * int open Elpi.API -let x : 'c. ('a, 'c) Conversion.t -> ('a simple, 'c)Conversion.t = simple +let x : 'a 'c 'csts. ('a, 'c,'csts) ContextualConversion.t -> ('a simple, 'c, 'csts) ContextualConversion.t = simple let builtin = let open BuiltIn in declare ~file_name:(Sys.argv.(1)) !elpi_stuff let main () = - let _elpi, _ = Setup.init ~builtins:[builtin] ~basedir:"." [] in + let _elpi = Setup.init ~builtins:[builtin] () in BuiltIn.document_file builtin; exit 0 ;; diff --git a/ppx_elpi/tests/test_simple_contextual.ml b/ppx_elpi/tests/test_simple_contextual.ml index 34e5f5658..a7a72cc45 100644 --- a/ppx_elpi/tests/test_simple_contextual.ml +++ b/ppx_elpi/tests/test_simple_contextual.ml @@ -11,9 +11,9 @@ type tctx = Entry of (string[@elpi.key]) * bool [@@elpi.index (module String)] [@@deriving elpi { declaration }] -let tctx : 'c. (int * tctx, 'c) Elpi.API.Conversion.t = tctx -let context_made_of_tctx : 'c. (tctx, string, #ctx_for_tctx as 'c) Elpi.API.Conversion.context = context_made_of_tctx -let in_ctx_for_tctx : ctx_for_tctx Elpi.API.Conversion.ctx_readback = in_ctx_for_tctx +let tctx : 'c 'csts. (int * tctx, 'c,'csts) Elpi.API.ContextualConversion.t = tctx +let context_made_of_tctx : 'c 'csts. (tctx, string, #ctx_for_tctx as 'c,'csts) Elpi.API.ContextualConversion.context = context_made_of_tctx +let in_ctx_for_tctx : (ctx_for_tctx,'csts) Elpi.API.ContextualConversion.ctx_readback = in_ctx_for_tctx let pp_term _ _ = () type term = @@ -22,22 +22,22 @@ type term = | Lam of bool * string * (term[@elpi.binder "term" tctx (fun b s -> Entry(s,b))]) [@@deriving elpi { declaration }] -let term : 'c. (term, #ctx_for_term as 'c) Elpi.API.Conversion.t = term -let in_ctx_for_term : ctx_for_term Elpi.API.Conversion.ctx_readback = in_ctx_for_term +let term : 'c 'csts. (term, #ctx_for_term as 'c, 'csts) Elpi.API.ContextualConversion.t = term +let in_ctx_for_term : (ctx_for_term, 'csts) Elpi.API.ContextualConversion.ctx_readback = in_ctx_for_term open Elpi.API open BuiltInPredicate open Notation -let term_to_string = Pred("term->string", - In(term,"T", - Out(BuiltInData.string,"S", - Read("what else"))),in_ctx_for_term, +let term_to_string = CPred("term->string",in_ctx_for_term, + CIn(term,"T", + COut(BuiltInContextualData.string,"S", + CRead("what else"))), fun (t : term) (_ety : string oarg) ~depth:_ c (_cst : Data.constraints) (_state : State.t) -> !: (Format.asprintf "@[%a@ |-@ %a@]@\n%!" - (RawData.Constants.Map.pp (Conversion.pp_ctx_entry pp_tctx)) c#tctx + (RawData.Constants.Map.pp (ContextualConversion.pp_ctx_entry pp_tctx)) c#tctx term.pp t) ) @@ -52,7 +52,7 @@ let builtin2 = let open BuiltIn in declare ~file_name:(Sys.argv.(1)) !declaration let main () = - let _elpi, _ = Setup.init ~builtins:[builtin1;builtin2] ~basedir:"." [] in + let _elpi = Setup.init ~builtins:[builtin1;builtin2] () in BuiltIn.document_file builtin2; exit 0 ;; diff --git a/ppx_elpi/tests/test_two_layers_context.ml b/ppx_elpi/tests/test_two_layers_context.ml index 4a316e2ce..ce8af52a4 100644 --- a/ppx_elpi/tests/test_two_layers_context.ml +++ b/ppx_elpi/tests/test_two_layers_context.ml @@ -18,15 +18,15 @@ type tye = | TArrow of tye * tye [@@deriving elpi { declaration } ] -let tye : 'a. (tye, #ctx_for_tye as 'a) Elpi.API.Conversion.t = tye - +let tye : 'a 'csts. (tye, #ctx_for_tye as 'a,'csts) Elpi.API.ContextualConversion.t = tye + let pp_ty _ _ = () type ty = | Mono of tye | Forall of string * bool * (ty[@elpi.binder "tye" tctx (fun s b -> TDecl(s,b))]) [@@deriving elpi ] -let ty : 'a. (ty, #ctx_for_ty as 'a) Elpi.API.Conversion.t = ty +let ty : 'a 'csts. (ty, #ctx_for_ty as 'a,'csts) Elpi.API.ContextualConversion.t = ty let pp_ctx _ _ = () type ctx = Decl of (string[@elpi.key]) * ty @@ -54,22 +54,22 @@ type term = | Cast(t,_) -> aux fmt t in aux ] -let term : 'a. (term, #ctx_for_term as 'a) Elpi.API.Conversion.t = term +let term : 'a 'csts. (term, #ctx_for_term as 'a,'csts) Elpi.API.ContextualConversion.t = term open Elpi.API open BuiltInPredicate open Notation -let term_to_string = Pred("term->string", - In(term,"T", - Out(BuiltInData.string,"S", - Read("what else"))), in_ctx_for_term, +let term_to_string = CPred("term->string",in_ctx_for_term, + CIn(term,"T", + COut(BuiltInContextualData.string,"S", + CRead("what else"))), fun (t : term) (_ety : string oarg) ~depth:_ c (_cst : Data.constraints) (_state : State.t) -> !: (Format.asprintf "@[%a@ %a@ |-@ %a@]@\n%!" - (RawData.Constants.Map.pp (Conversion.pp_ctx_entry pp_tctx)) c#tctx - (RawData.Constants.Map.pp (Conversion.pp_ctx_entry pp_ctx)) c#ctx + (RawData.Constants.Map.pp (ContextualConversion.pp_ctx_entry pp_tctx)) c#tctx + (RawData.Constants.Map.pp (ContextualConversion.pp_ctx_entry pp_ctx)) c#ctx term.pp t) ) @@ -91,14 +91,13 @@ main :- |} let main () = - let elpi, _ = Setup.init ~builtins:[builtin] ~basedir:"." [] in + let elpi = Setup.init ~builtins:[builtin] () in let out = open_out Sys.argv.(1) in let fmt = Format.formatter_of_out_channel out in Setup.set_err_formatter fmt; Setup.set_std_formatter fmt; - let program = Parse.program_from_stream ~elpi (Ast.Loc.initial "test") - Stream.(of_string program) in - let goal = Parse.goal (Ast.Loc.initial "test") "main." in + let program = Parse.program_from ~elpi ~loc:(Ast.Loc.initial "test") (Lexing.from_string program) in + let goal = Parse.goal ~elpi ~loc:(Ast.Loc.initial "test") ~text:"main." in let program = Compile.program ~elpi ~flags:Compile.default_flags [program] in let goal = Compile.query program goal in let exe = Compile.optimize goal in diff --git a/src/API.ml b/src/API.ml index 9e02bcb69..6c4e43394 100644 --- a/src/API.ml +++ b/src/API.ml @@ -398,6 +398,7 @@ module OpaqueData = struct end + module BuiltInData = struct let int = snd @@ RawOpaqueData.conversion_of_cdata ~name:"int" ~compare:(fun x y -> x - y) ~pp:(fun fmt x -> Util.CData.pp fmt (ED.C.int.Util.CData.cin x)) ED.C.int @@ -494,6 +495,113 @@ module BuiltInData = struct end +module BuiltInContextualData = struct + + let int : 'c 'csts. (int,'c,'csts) ContextualConversion.t = + let open ContextualConversion in + let it = BuiltInData.int in { + ty = it.Conversion.ty; pp = it.Conversion.pp; pp_doc = it.Conversion.pp_doc; + embed = (fun ~depth _ _ s x -> it.Conversion.embed ~depth s x); + readback = (fun ~depth _ _ s x -> it.Conversion.readback ~depth s x); + } + let float : 'c 'csts. (float,'c,'csts) ContextualConversion.t = + let open ContextualConversion in + let it = BuiltInData.float in { + ty = it.Conversion.ty; pp = it.Conversion.pp; pp_doc = it.Conversion.pp_doc; + embed = (fun ~depth _ _ s x -> it.Conversion.embed ~depth s x); + readback = (fun ~depth _ _ s x -> it.Conversion.readback ~depth s x); + } + let string : 'c 'csts. (string,'c,'csts) ContextualConversion.t = + let open ContextualConversion in + let it = BuiltInData.string in { + ty = it.Conversion.ty; pp = it.Conversion.pp; pp_doc = it.Conversion.pp_doc; + embed = (fun ~depth _ _ s x -> it.Conversion.embed ~depth s x); + readback = (fun ~depth _ _ s x -> it.Conversion.readback ~depth s x); + } + let loc : 'c 'csts. (Util.Loc.t,'c,'csts) ContextualConversion.t = + let open ContextualConversion in + let it = BuiltInData.loc in { + ty = it.Conversion.ty; pp = it.Conversion.pp; pp_doc = it.Conversion.pp_doc; + embed = (fun ~depth _ _ s x -> it.Conversion.embed ~depth s x); + readback = (fun ~depth _ _ s x -> it.Conversion.readback ~depth s x); + } + + + let polyA0 = + let embed ~depth:_ _ _ state x = state, x, [] in + let readback ~depth _ _ state t = state, t, [] in + { ContextualConversion.embed; readback; ty = Conversion.TyName "A0"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + pp_doc = (fun fmt () -> ()) } + let polyA1 = + let embed ~depth:_ _ _ state x = state, x, [] in + let readback ~depth _ _ state t = state, t, [] in + { ContextualConversion.embed; readback; ty = Conversion.TyName "A1"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + pp_doc = (fun fmt () -> ()) } + let polyA2 = + let embed ~depth:_ _ _ state x = state, x, [] in + let readback ~depth _ _ state t = state, t, [] in + { ContextualConversion.embed; readback; ty = Conversion.TyName "A2"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + pp_doc = (fun fmt () -> ()) } + let polyA3 = + let embed ~depth:_ _ _ state x = state, x, [] in + let readback ~depth _ _ state t = state, t, [] in + { ContextualConversion.embed; readback; ty = Conversion.TyName "A3"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + pp_doc = (fun fmt () -> ()) } + + let any = + let embed ~depth:_ _ _ state x = state, x, [] in + let readback ~depth _ _ state t = state, t, [] in + { ContextualConversion.embed; readback; ty = Conversion.TyName "any"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + pp_doc = (fun fmt () -> ()) } + + let map_acc f s l = + let rec aux acc extra s = function + | [] -> s, List.rev acc, List.(concat (rev extra)) + | x :: xs -> + let s, x, gls = f s x in + aux (x :: acc) (gls :: extra) s xs + in + aux [] [] s l + + let list d = + let embed ~depth h c s l = + let module R = (val !r) in let open R in + let s, l, eg = map_acc (d.ContextualConversion.embed ~depth h c) s l in + s, list_to_lp_list l, eg in + let readback ~depth h c s t = + let module R = (val !r) in let open R in + map_acc (d.ContextualConversion.readback ~depth h c) s + (lp_list_to_list ~depth t) + in + let pp fmt l = + Format.fprintf fmt "[%a]" (Util.pplist d.pp ~boxed:true "; ") l in + { ContextualConversion.embed; readback; + ty = TyApp ("list",d.ty,[]); + pp; + pp_doc = (fun fmt () -> ()) } + + let nominal = + let embed ~depth:_ _ _ state x = + let module R = (val !r) in + if x < 0 then Util.type_error "not a bound variable"; + state, R.mkConst x, [] in + let readback ~depth _ _ state t = + let module R = (val !r) in + match R.deref_head ~depth t with + | ED.Const i when i >= 0 -> state, i, [] + | _ -> Util.type_error "not a bound variable" in + { ContextualConversion.embed; readback; ty = TyName "nominal"; + pp = (fun fmt d -> Format.fprintf fmt "%d" d); + pp_doc = (fun fmt () -> ()) } + +end + + module Elpi = struct type t = Arg of string | Ref of ED.uvar_body @@ -649,17 +757,8 @@ module RawData = struct let of_term x = x - let of_hyp x = x - let of_hyps x = x - - type hyp = Data.hyp = { - hdepth : int; - hsrc : term - } - type hyps = hyp list - type suspended_goal = ED.suspended_goal = { - context : hyps; + context : Data.hyps; goal : int * term } @@ -903,17 +1002,30 @@ end module Query = struct type name = string - type 'f arguments = 'f ED.Query.arguments = + type 'a arguments = 'a ED.Query.arguments = | N : unit arguments | D : 'a Conversion.t * 'a * 'x arguments -> 'x arguments | Q : 'a Conversion.t * name * 'x arguments -> ('a * 'x) arguments - type 'x t = Query of { predicate : name; arguments : 'x arguments } + type ('a,'b,'c) carguments = ('a,'b,'c) ED.Query.carguments = + | NC : (unit,'c,'csts) carguments + | DC : ('a,'c,'csts) ContextualConversion.t * 'a * ('x,'c,'csts) carguments -> ('x,'c,'csts) carguments + | QC : ('a,'c,'csts) ContextualConversion.t * name * ('x,'c,'csts) carguments -> ('a * 'x,'c,'csts) carguments + + type 'x t = + | Query of { predicate : name; arguments : 'x arguments } + | CQuery : name * ('x,#ContextualConversion.ctx as 'c,'csts) carguments * (ED.State.t -> 'c) * 'csts -> 'x t + + let compile p loc = function + | Query { predicate; arguments } -> + let p, predicate = Compiler.lookup_query_predicate p predicate in + let q = ED.Query.Query{ predicate; arguments } in + Compiler.query_of_data p loc q + | CQuery(predicate, arguments, ctx, csts) -> + let p, predicate = Compiler.lookup_query_predicate p predicate in + let q = ED.Query.CQuery(predicate, arguments, ctx, csts) in + Compiler.query_of_data p loc q - let compile p loc (Query { predicate; arguments }) = - let p, predicate = Compiler.lookup_query_predicate p predicate in - let q = ED.Query.Query{ predicate; arguments } in - Compiler.query_of_data p loc q end module State = struct @@ -1083,4 +1195,36 @@ module PPX = struct let show_ty_ast = ED.Conversion.show_ty_ast end + + type context_description = + | C : ('a,'k,'c,'csts) ContextualConversion.context -> context_description + + let readback_context { ContextualConversion.conv; to_key; push; is_entry_for_nominal; init} ctx ~depth hyps constraints state = + let module CMap = RawData.Constants.Map in + let filtered_hyps = + List.fold_left (fun m hyp -> + match is_entry_for_nominal hyp with + | None -> m + | Some idx -> + if CMap.mem idx m then + Utils.type_error "more than one context entry for the same nominal"; + CMap.add idx hyp m) CMap.empty + hyps in + let rec aux state gls i = + if i = depth then state, List.concat (List.rev gls) + else + if not (CMap.mem i filtered_hyps) then aux state gls (i + 1) + else + let hyp = CMap.find i filtered_hyps in + let hyp_depth = hyp.Data.hdepth in + let state, (nominal, t), gls_t = + conv.ContextualConversion.readback + ~depth:hyp_depth ctx constraints state hyp.Data.hsrc in + assert (nominal = i); + let s = to_key ~depth:hyp_depth t in + let state = + push ~depth:i state s { ContextualConversion.entry = t; depth = hyp_depth } in + aux state (gls_t :: gls) (i + 1) in + let state = init state in + aux state [] 0 end diff --git a/src/API.mli b/src/API.mli index 87b8dfa5b..c43490007 100644 --- a/src/API.mli +++ b/src/API.mli @@ -148,7 +148,10 @@ module Data : sig } (* Hypothetical context *) - type hyp + type hyp = { + hdepth : int; + hsrc : term + } type hyps = hyp list type constant = int @@ -371,11 +374,6 @@ module ContextualConversion : sig (* cast *) val (!<) : ('a,ctx,unit) t -> 'a Conversion.t - (* morphisms *) - val (!>) : 'a Conversion.t -> ('a,#ctx as 'hyps,'constraints) t - val (!>>) : ('a Conversion.t -> 'b Conversion.t) -> ('a,'hyps,'constraints) t -> ('b,'hyps,'constraints) t - val (!>>>) : ('a Conversion.t -> 'b Conversion.t -> 'c Conversion.t) -> ('a,'hyps,'constraints) t -> ('b,'hyps,'constraints) t -> ('c,'hyps,'constraints) t - end @@ -401,6 +399,28 @@ module BuiltInData : sig end +module BuiltInContextualData : sig + + (** See {!module:Elpi.Builtin} for a few more *) + val int : (int,'c,'csts) ContextualConversion.t + val float : (float,'c,'csts) ContextualConversion.t + val string : (string,'c,'csts) ContextualConversion.t + val list : ('a,'c,'csts) ContextualConversion.t -> ('a list,'c,'csts) ContextualConversion.t + val loc : (Ast.Loc.t,'c,'csts) ContextualConversion.t + + (* poly "A" is what one would use for, say, [type eq A -> A -> prop] *) + val polyA0 : (Data.term,'c,'csts) ContextualConversion.t + val polyA1 : (Data.term,'c,'csts) ContextualConversion.t + val polyA2 : (Data.term,'c,'csts) ContextualConversion.t + val polyA3 : (Data.term,'c,'csts) ContextualConversion.t + + (* any is like poly "X" for X fresh *) + val any : (Data.term,'c,'csts) ContextualConversion.t + + val nominal : (Data.constant,'c,'csts) ContextualConversion.t + +end + (** Declare data from the host application that is opaque (no syntax), like int but not like list or pair *) module OpaqueData : sig @@ -750,8 +770,14 @@ module Query : sig | N : unit arguments | D : 'a Conversion.t * 'a * 'x arguments -> 'x arguments | Q : 'a Conversion.t * name * 'x arguments -> ('a * 'x) arguments + type (_,_,_) carguments = + | NC : (unit,'c,'csts) carguments + | DC : ('a,'c,'csts) ContextualConversion.t * 'a * ('x,'c,'csts) carguments -> ('x,'c,'csts) carguments + | QC : ('a,'c,'csts) ContextualConversion.t * name * ('x,'c,'csts) carguments -> ('a * 'x,'c,'csts) carguments - type 'x t = Query of { predicate : name; arguments : 'x arguments } + type 'x t = + | Query of { predicate : name; arguments : 'x arguments } + | CQuery : name * ('x,#ContextualConversion.ctx as 'c,'csts) carguments * (Data.state -> 'c) * 'csts -> 'x t val compile : Compile.program -> Ast.Loc.t -> 'a t -> 'a Compile.query @@ -1017,16 +1043,9 @@ module RawData : sig val mkConst : constant -> term (* no check, works for globals and bound *) val cmp_builtin : builtin -> builtin -> int - type hyp = { - hdepth : int; - hsrc : term - } - type hyps = hyp list - val of_hyp : Data.hyp -> hyp - val of_hyps : Data.hyp list -> hyps type suspended_goal = { - context : hyps; + context : Data.hyps; goal : int * term } val constraints : Data.constraints -> suspended_goal list @@ -1258,6 +1277,17 @@ module PPX : sig end + type context_description = + | C : ('a,'k,'c,'csts) ContextualConversion.context -> context_description + + val readback_context : + ('a,'k,'c,'csts) ContextualConversion.context -> + 'c -> + depth:int -> + Data.hyps -> + 'csts -> + Data.state -> Data.state * Conversion.extra_goals + end (**/**) diff --git a/src/builtin.ml b/src/builtin.ml index bbdc644f7..f8f80711a 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -248,6 +248,99 @@ let char : char Conversion.t = { } + +module PPX = struct + + let bool : (bool,'c,'csts) ContextualConversion.t = { + ty = TyName "bool"; + pp_doc = (fun fmt () -> Format.fprintf fmt "Char values: single character strings"); + pp = (fun fmt b -> Format.fprintf fmt "%b" b); + embed = (fun ~depth _ _ (st: State.t) c -> bool.embed ~depth st c); + readback = (fun ~depth _ _ st term -> bool.readback ~depth st term); + } + let char : (char,'c,'csts) ContextualConversion.t = { + ty = TyName "char"; + pp_doc = (fun fmt () -> Format.fprintf fmt "Char values: single character strings"); + pp = (fun fmt b -> Format.fprintf fmt "%c" b); + embed = (fun ~depth _ _ (st: State.t) (c: char) -> BuiltInData.string.embed ~depth st (String.make 1 c)); + readback = (fun ~depth _ _ st term -> + let st,name,goals = BuiltInData.string.readback ~depth st term in + st,name.[0],goals + ); + } + + let pair a b = let open AlgebraicData in declare { + ty = TyApp ("pair",a.ContextualConversion.ty,[b.ContextualConversion.ty]); + doc = "Pair: the constructor is pr, since ',' is for conjunction"; + pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_pair a.ContextualConversion.pp b.ContextualConversion.pp) o); + constructors = [ + K("pr","",CA(a,CA(b,N)), + B (fun a b -> (a,b)), + M (fun ~ok ~ko:_ -> function (a,b) -> ok a b)); + ] + } + + let triple a b c = let open AlgebraicData in declare { + ty = TyApp ("triple",a.ContextualConversion.ty,[b.ContextualConversion.ty;c.ContextualConversion.ty]); + doc = "Triple: the constructor is trpl, since ',' is for conjunction"; + pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_triple a.ContextualConversion.pp b.ContextualConversion.pp c.ContextualConversion.pp) o); + constructors = [ + K("trpl","",CA(a,CA(b,CA(c,N))), + B (fun a b c -> (a,b, c)), + M (fun ~ok ~ko:_ -> function (a,b,c) -> ok a b c)); + ] + } + + let quadruple a b c d = let open AlgebraicData in declare { + ty = TyApp ("quadruple",a.ContextualConversion.ty,[b.ContextualConversion.ty;c.ContextualConversion.ty;d.ContextualConversion.ty]); + doc = "Quadruple: the constructor is quadrpl, since ',' is for conjunction"; + pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_quadruple a.ContextualConversion.pp b.ContextualConversion.pp c.ContextualConversion.pp d.ContextualConversion.pp) o); + constructors = [ + K("quadrpl","",CA(a,CA(b,CA(c,CA(d,N)))), + B (fun a b c d -> (a,b,c,d)), + M (fun ~ok ~ko:_ -> function (a,b,c,d) -> ok a b c d)); + ] + } + + let option a = let open AlgebraicData in declare { + ty = TyApp("option",a.ContextualConversion.ty,[]); + doc = "The option type (aka Maybe)"; + pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_option a.ContextualConversion.pp) o); + constructors = [ + K("none","",N, + B None, + M (fun ~ok ~ko -> function None -> ok | _ -> ko ())); + K("some","",CA(a,N), + B (fun x -> Some x), + M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ())); + ] + } + + let hack embed = { + ContextualConversion.embed; + readback = (fun ~depth _ _ st x -> assert false); + ty = Conversion.TyName "hack"; + pp = (fun fmt x -> assert false); + pp_doc = (fun fmt x -> assert false); + } + let embed_option a = (option (hack a)).ContextualConversion.embed + let embed_pair a b = (pair (hack a) (hack b)).ContextualConversion.embed + let embed_triple a b c = (triple (hack a) (hack b) (hack c)).ContextualConversion.embed + let embed_quadruple a b c d = (quadruple (hack a) (hack b) (hack c) (hack d)).ContextualConversion.embed + + let hack readback = { + ContextualConversion.readback; + embed = (fun ~depth _ _ st x -> assert false); + ty = ContextualConversion.TyName "hack"; + pp = (fun fmt x -> assert false); + pp_doc = (fun fmt x -> assert false); + } + let readback_option a = (option (hack a)).ContextualConversion.readback + let readback_pair a b = (pair (hack a) (hack b)).ContextualConversion.readback + let readback_triple a b c = (triple (hack a) (hack b) (hack c)).ContextualConversion.readback + let readback_quadruple a b c d = (quadruple (hack a) (hack b) (hack c) (hack d)).ContextualConversion.readback +end + let pair a b = let open AlgebraicData in declare { ty = TyApp ("pair",a.Conversion.ty,[b.Conversion.ty]); doc = "Pair: the constructor is pr, since ',' is for conjunction"; @@ -295,33 +388,6 @@ let option a = let open AlgebraicData in declare { ] } |> ContextualConversion.(!<) -module PPX = struct - let hack embed = { - Conversion.embed; - readback = (fun ~depth st x -> assert false); - ty = Conversion.TyName "hack"; - pp = (fun fmt x -> assert false); - pp_doc = (fun fmt x -> assert false); - } - let embed_option a = (option (hack a)).Conversion.embed - let embed_pair a b = (pair (hack a) (hack b)).Conversion.embed - let embed_triple a b c = (triple (hack a) (hack b) (hack c)).Conversion.embed - let embed_quadruple a b c d = (quadruple (hack a) (hack b) (hack c) (hack d)).Conversion.embed - - let hack readback = { - Conversion.readback; - embed = (fun ~depth st x -> assert false); - ty = Conversion.TyName "hack"; - pp = (fun fmt x -> assert false); - pp_doc = (fun fmt x -> assert false); - } - let readback_option a = (option (hack a)).Conversion.readback - let readback_pair a b = (pair (hack a) (hack b)).Conversion.readback - let readback_triple a b c = (triple (hack a) (hack b) (hack c)).Conversion.readback - let readback_quadruple a b c d = (quadruple (hack a) (hack b) (hack c) (hack d)).Conversion.readback -end - - type diagnostic = OK | ERROR of string ioarg let mkOK = OK let mkERROR s = ERROR (mkData s) @@ -442,7 +508,22 @@ let unspecC data = let open API.ContextualConversion in let open API.RawData in let state, x, gls = data.readback ~depth hyps constraints state (kool t) in state, Given x, gls) } -let unspec d = API.ContextualConversion.(!<(unspecC (!> d))) +let unspec data = let open API.Conversion in let open API.RawData in { + ty = data.ty; + pp_doc = data.pp_doc; + pp = (fun fmt -> function + | Unspec -> Format.fprintf fmt "Unspec" + | Given x -> Format.fprintf fmt "Given %a" data.pp x); + embed = (fun ~depth state -> function + | Given x -> data.embed ~depth state x + | Unspec -> state, mkDiscard, []); + readback = (fun ~depth state x -> + match look ~depth x with + | UnifVar _ -> state, Unspec, [] + | t -> + let state, x, gls = data.readback ~depth state (kool t) in + state, Given x, gls) +} (** Core built-in ********************************************************* *) diff --git a/src/builtin.mli b/src/builtin.mli index 34ce8032c..7440b08cf 100644 --- a/src/builtin.mli +++ b/src/builtin.mli @@ -63,14 +63,20 @@ val bool : bool API.Conversion.t val char : char API.Conversion.t module PPX : sig - val embed_option : 'a API.Conversion.embedding -> ('a option) API.Conversion.embedding - val embed_pair : 'a API.Conversion.embedding -> 'b API.Conversion.embedding -> ('a * 'b) API.Conversion.embedding - val embed_triple : 'a API.Conversion.embedding -> 'b API.Conversion.embedding -> 'c API.Conversion.embedding -> ('a * 'b * 'c) API.Conversion.embedding - val embed_quadruple : 'a API.Conversion.embedding -> 'b API.Conversion.embedding -> 'c API.Conversion.embedding -> 'd API.Conversion.embedding -> ('a * 'b * 'c * 'd) API.Conversion.embedding - val readback_option : 'a API.Conversion.readback -> ('a option) API.Conversion.readback - val readback_pair : 'a API.Conversion.readback -> 'b API.Conversion.readback -> ('a * 'b) API.Conversion.readback - val readback_triple : 'a API.Conversion.readback -> 'b API.Conversion.readback -> 'c API.Conversion.readback -> ('a * 'b * 'c) API.Conversion.readback - val readback_quadruple : 'a API.Conversion.readback -> 'b API.Conversion.readback -> 'c API.Conversion.readback -> 'd API.Conversion.readback -> ('a * 'b * 'c * 'd) API.Conversion.readback + val embed_option : ('a, 'ctx, 'csts) API.ContextualConversion.embedding -> ('a option, 'ctx, 'csts) API.ContextualConversion.embedding + val embed_pair : ('a, 'ctx, 'csts) API.ContextualConversion.embedding -> ('b, 'ctx, 'csts) API.ContextualConversion.embedding -> ('a * 'b, 'ctx, 'csts) API.ContextualConversion.embedding + val embed_triple : ('a, 'ctx, 'csts) API.ContextualConversion.embedding -> ('b, 'ctx, 'csts) API.ContextualConversion.embedding -> ('c, 'ctx, 'csts) API.ContextualConversion.embedding -> ('a * 'b * 'c, 'ctx, 'csts) API.ContextualConversion.embedding + val embed_quadruple : ('a, 'ctx, 'csts) API.ContextualConversion.embedding -> ('b, 'ctx, 'csts) API.ContextualConversion.embedding -> ('c, 'ctx, 'csts) API.ContextualConversion.embedding -> ('d, 'ctx, 'csts) API.ContextualConversion.embedding -> ('a * 'b * 'c * 'd, 'ctx, 'csts) API.ContextualConversion.embedding + val readback_option : ('a, 'ctx, 'csts) API.ContextualConversion.readback -> ('a option, 'ctx, 'csts) API.ContextualConversion.readback + val readback_pair : ('a, 'ctx, 'csts) API.ContextualConversion.readback -> ('b, 'ctx, 'csts) API.ContextualConversion.readback -> ('a * 'b, 'ctx, 'csts) API.ContextualConversion.readback + val readback_triple : ('a, 'ctx, 'csts) API.ContextualConversion.readback -> ('b, 'ctx, 'csts) API.ContextualConversion.readback -> ('c, 'ctx, 'csts) API.ContextualConversion.readback -> ('a * 'b * 'c, 'ctx, 'csts) API.ContextualConversion.readback + val readback_quadruple : ('a, 'ctx, 'csts) API.ContextualConversion.readback -> ('b, 'ctx, 'csts) API.ContextualConversion.readback -> ('c, 'ctx, 'csts) API.ContextualConversion.readback -> ('d, 'ctx, 'csts) API.ContextualConversion.readback -> ('a * 'b * 'c * 'd, 'ctx, 'csts) API.ContextualConversion.readback + val option : ('a, 'ctx, 'csts) API.ContextualConversion.t -> ('a option, 'ctx, 'csts) API.ContextualConversion.t + val pair : ('a, 'ctx, 'csts) API.ContextualConversion.t -> ('b, 'ctx, 'csts) API.ContextualConversion.t -> ('a * 'b, 'ctx, 'csts) API.ContextualConversion.t + val triple : ('a, 'ctx, 'csts) API.ContextualConversion.t -> ('b, 'ctx, 'csts) API.ContextualConversion.t -> ('c, 'ctx, 'csts) API.ContextualConversion.t -> ('a * 'b * 'c, 'ctx, 'csts) API.ContextualConversion.t + val quadruple : ('a, 'ctx, 'csts) API.ContextualConversion.t -> ('b, 'ctx, 'csts) API.ContextualConversion.t -> ('c, 'ctx, 'csts) API.ContextualConversion.t -> ('d, 'ctx, 'csts) API.ContextualConversion.t -> ('a * 'b * 'c * 'd, 'ctx, 'csts) API.ContextualConversion.t + val bool : (bool, 'ctx, 'csts) API.ContextualConversion.t + val char : (char, 'ctx, 'csts) API.ContextualConversion.t end (* A standard way to make a predicate always succeed but still give errors *) diff --git a/src/compiler.ml b/src/compiler.ml index 264c242bc..181ec918f 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -529,7 +529,7 @@ type 'a query = { chr : (constant list * prechr_rule list) list; initial_depth : int; query : preterm; - query_arguments : 'a Query.arguments [@opaque]; + query_adt : 'a Query.t [@opaque]; (* We pre-compile the query to ease the API *) initial_goal : term; assignments : term StrMap.t; compiler_state : State.t; @@ -2200,7 +2200,7 @@ let query_of_ast (compiler_state, assembled_program) t = chr = assembled_program.Assembled.chr; initial_depth; query; - query_arguments = Query.N; + query_adt = Query.(Query {predicate=0;arguments=N}); initial_goal; assignments; compiler_state = state |> (uvbodies_of_assignments assignments); @@ -2231,18 +2231,18 @@ let query_of_term (compiler_state, assembled_program) f = chr = assembled_program.Assembled.chr; initial_depth; query; - query_arguments = Query.N; + query_adt = Query.(Query {predicate=0;arguments=N}); initial_goal; assignments; compiler_state = state |> (uvbodies_of_assignments assignments); } -let query_of_data (state, p) loc (Query.Query { arguments } as descr) = +let query_of_data (state, p) loc descr = let query = query_of_term (state, p) (fun ~depth state -> let state, term, gls = R.embed_query ~mk_Arg ~depth state descr in state, (loc, term), gls) in - { query with query_arguments = arguments } + { query with query_adt = descr } let lookup_query_predicate (state, p) pred = let state, pred = Symbols.allocate_global_symbol_str state pred in @@ -2335,7 +2335,7 @@ let run initial_goal; assignments; compiler_state = state; - query_arguments; + query_adt; } = check_all_builtin_are_typed state types; @@ -2391,7 +2391,7 @@ let run initial_goal; initial_runtime_state = State.end_compilation state; assignments; - query_arguments; + query_adt; symbol_table; builtins; } diff --git a/src/data.ml b/src/data.ml index c7d71c8b9..c29916bfa 100644 --- a/src/data.ml +++ b/src/data.ml @@ -734,7 +734,7 @@ module ContextualConversion = struct let in_raw_ctx : (ctx,'a) ctx_readback = fun ~depth:_ h c s -> s, build_raw_ctx h s, c,[] - let unit_ctx : (ctx,unit) ctx_readback = fun ~depth:_ h _ s -> s, build_raw_ctx h s, (), [] + let unit_ctx : (ctx,unit) ctx_readback = fun ~depth:_ h c s -> s, build_raw_ctx h s, (), [] let raw_ctx : (ctx,constraints) ctx_readback = fun ~depth:_ h c s -> s, build_raw_ctx h s, c, [] @@ -1244,9 +1244,14 @@ module Query = struct | N : unit arguments | D : 'a Conversion.t * 'a * 'x arguments -> 'x arguments | Q : 'a Conversion.t * name * 'x arguments -> ('a * 'x) arguments + type (_,_,_) carguments = + | NC : (unit,'c,'csts) carguments + | DC : ('a,'c,'csts) ContextualConversion.t * 'a * ('x,'c,'csts) carguments -> ('x,'c,'csts) carguments + | QC : ('a,'c,'csts) ContextualConversion.t * name * ('x,'c,'csts) carguments -> ('a * 'x,'c,'csts) carguments type 'x t = | Query of { predicate : constant; arguments : 'x arguments } + | CQuery : constant * ('x,#ContextualConversion.ctx as 'c,'csts) carguments * (State.t -> 'c) * 'csts -> 'x t end @@ -1275,7 +1280,7 @@ type 'a executable = { (* solution *) assignments : term Util.StrMap.t; (* type of the query, reified *) - query_arguments: 'a Query.arguments; + query_adt: 'a Query.t; } type pp_ctx = { diff --git a/src/runtime.ml b/src/runtime.ml index 3dd025d3b..d7f05e960 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2306,8 +2306,25 @@ let rec embed_query_aux : type a. mk_Arg:(State.t -> name:string -> args:term li state, C.mkAppL predicate args, gls ;; -let embed_query ~mk_Arg ~depth state (Query.Query { predicate; arguments }) = - embed_query_aux ~mk_Arg ~depth ~predicate [] [] state arguments +let rec embed_cquery_aux : type a csts. mk_Arg:(State.t -> name:string -> args:term list -> State.t * term) -> depth:int -> predicate:constant -> ctx:(#ContextualConversion.ctx as 'c) -> csts:csts -> Conversion.extra_goals -> term list -> State.t -> (a,'c,csts) Query.carguments -> State.t * term * Conversion.extra_goals + = fun ~mk_Arg ~depth ~predicate ~ctx ~csts gls args state descr -> + match descr with + | Data.Query.DC(d,x,rest) -> + let state, x, glsx = d.ContextualConversion.embed ~depth ctx csts state x in + embed_cquery_aux ~mk_Arg ~depth ~predicate ~ctx ~csts (gls @ glsx) (x :: args) state rest + | Data.Query.QC(d,name,rest) -> + let state, x = mk_Arg state ~name ~args:[] in + embed_cquery_aux ~mk_Arg ~depth ~predicate ~ctx ~csts gls (x :: args) state rest + | Data.Query.NC -> + let args = List.rev args in + state, C.mkAppL predicate args, gls +;; + +let embed_query ~mk_Arg ~depth state = function + | Query.Query { predicate; arguments } -> + embed_query_aux ~mk_Arg ~depth ~predicate [] [] state arguments + | Query.CQuery (predicate, arguments, ctx, csts) -> + embed_cquery_aux ~mk_Arg ~depth ~predicate ~ctx:(ctx state) ~csts [] [] state arguments let rec query_solution_aux : type a. a Query.arguments -> term StrMap.t -> State.t -> a = fun args assignments state -> @@ -2319,8 +2336,21 @@ let rec query_solution_aux : type a. a Query.arguments -> term StrMap.t -> State let state, x, _gls = d.Conversion.readback ~depth:0 state x in x, query_solution_aux args assignments state -let output arguments assignments state = - query_solution_aux arguments assignments state +let rec cquery_solution_aux : type a csts. (a,#ContextualConversion.ctx as 'c,csts) Query.carguments -> term StrMap.t -> State.t -> 'c -> csts -> a += fun args assignments state ctx csts -> + match args with + | Data.Query.NC -> () + | Data.Query.DC(_,_,args) -> cquery_solution_aux args assignments state ctx csts + | Data.Query.QC(d,name,args) -> + let x = StrMap.find name assignments in + let state, x, _gls = d.ContextualConversion.readback ~depth:0 ctx csts state x in + x, cquery_solution_aux args assignments state ctx csts + + +let output query assignments state = + match query with + | Query.Query { arguments; _ } -> query_solution_aux arguments assignments state + | Query.CQuery (_,arguments,c,csts) -> cquery_solution_aux arguments assignments state (c state) csts (****************************************************************************** Indexing @@ -3348,7 +3378,7 @@ let try_fire_rule (gid[@trace]) rule (constraints as orig_constraints) = assignments = StrMap.empty; initial_depth = max_depth; initial_runtime_state = State.(init () |> State.begin_goal_compilation |> end_goal_compilation StrMap.empty |> end_compilation); - query_arguments = Query.N; + query_adt = Query.(Query { predicate = 0; arguments = N } ); symbol_table = !C.table; builtins = !FFI.builtins; } in @@ -3745,7 +3775,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut assignments = StrMap.empty; initial_depth = depth; initial_runtime_state = State.(init () |> State.begin_goal_compilation |> end_goal_compilation StrMap.empty |> end_compilation); - query_arguments = Query.N; + query_adt = Query.(Query { predicate = 0; arguments = N }); symbol_table = !C.table; builtins = !FFI.builtins; } in @@ -3948,7 +3978,7 @@ let mk_outcome search get_cs assignments = let execute_once ?max_steps ?delay_outside_fragment exec = let { search; get } = make_runtime ?max_steps ?delay_outside_fragment exec in try - let result = fst (mk_outcome search (fun () -> get CS.Ugly.delayed, get CS.state |> State.end_execution, exec.query_arguments, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments) in + let result = fst (mk_outcome search (fun () -> get CS.Ugly.delayed, get CS.state |> State.end_execution, exec.query_adt, { Data.uv_names = ref (get Pp.uv_names); table = get C.table }) exec.assignments) in [%end_trace "execute_once" ~rid]; result with e -> @@ -3962,7 +3992,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_adt, { 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