From 67e3e8965c9788e5b1db8fe0cbf04e2d3d71319b Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 31 Jan 2024 11:28:16 +0100 Subject: [PATCH] wip --- .nix/coq-overlays/coq-elpi/default.nix | 4 +++- .nix/ocaml-overlays/elpi/default.nix | 3 ++- coq-builtin.elpi | 5 +++++ elpi/coq-HOAS.elpi | 5 +++++ src/coq_elpi_HOAS.ml | 9 +++++++++ src/coq_elpi_HOAS.mli | 1 + src/coq_elpi_builtins.ml | 24 +++++++++++++++--------- 7 files changed, 40 insertions(+), 11 deletions(-) diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix index 6c564594c..58749edd7 100644 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ b/.nix/coq-overlays/coq-elpi/default.nix @@ -9,6 +9,8 @@ with builtins; with lib; let { case = "8.15"; out = { version = "1.16.5"; };} { case = "8.16"; out = { version = "1.16.5"; };} ] {} ); + dot-merlin-reader = coq.ocamlPackages.dot-merlin-reader; + dune = coq.ocamlPackages.dune_3; in mkCoqDerivation { pname = "elpi"; repo = "coq-elpi"; @@ -53,7 +55,7 @@ in mkCoqDerivation { releaseRev = v: "v${v}"; mlPlugin = true; - propagatedBuildInputs = [ elpi ]; + propagatedBuildInputs = [ elpi dot-merlin-reader dune ]; meta = { description = "Coq plugin embedding ELPI."; diff --git a/.nix/ocaml-overlays/elpi/default.nix b/.nix/ocaml-overlays/elpi/default.nix index bca9d8c90..d7f45921d 100644 --- a/.nix/ocaml-overlays/elpi/default.nix +++ b/.nix/ocaml-overlays/elpi/default.nix @@ -1,6 +1,7 @@ { lib , buildDunePackage, camlp5 , ocaml +, ocaml-lsp , menhir, menhirLib , stdlib-shims , re, perl, ncurses @@ -34,7 +35,7 @@ buildDunePackage rec { buildInputs = [ perl ncurses ] ++ optional (versionAtLeast version "1.15" || version == "dev") menhir; - propagatedBuildInputs = [ re stdlib-shims ] + propagatedBuildInputs = [ re stdlib-shims ocaml-lsp ] ++ (if versionAtLeast version "1.15" || version == "dev" then [ menhirLib ] else [ camlp5 ] ) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 84dce8854..d869f9797 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -354,6 +354,11 @@ typeabbrev opaque? bool. macro @opaque! :- tt. macro @transparent! :- ff. macro @global! :- get-option "coq:locality" "global". macro @local! :- get-option "coq:locality" "local". +macro @keep-alg-univs! :- + get-option "coq:algunivs" "keep-algunivs". +macro @purge-alg-univs! :- + get-option "coq:algunivs" "purge-algunivs". + macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions macro @reversible! :- get-option "coq:reversible" tt. % coercions diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 0265992bf..f143085c5 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -339,6 +339,11 @@ typeabbrev opaque? bool. macro @opaque! :- tt. macro @transparent! :- ff. macro @global! :- get-option "coq:locality" "global". macro @local! :- get-option "coq:locality" "local". +macro @keep-alg-univs! :- + get-option "coq:algunivs" "keep-algunivs". +macro @purge-alg-univs! :- + get-option "coq:algunivs" "purge-algunivs". + macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions macro @reversible! :- get-option "coq:reversible" tt. % coercions diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 7d997a02d..e1cbc73ff 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -344,6 +344,7 @@ type options = { reversible : bool option; keepunivs : bool option; redflags : CClosure.RedFlags.reds option; + algunivs : bool option; } let default_options () = { @@ -363,6 +364,7 @@ let default_options () = { reversible = None; keepunivs = None; redflags = None; + algunivs = None; } type 'a coq_context = { @@ -1105,6 +1107,12 @@ let get_options ~depth hyps state = let _, rd, gl = reduction_flags.Elpi.API.Conversion.readback ~depth state t in assert (gl = []); Some rd in + let keeping_algebraic_universes s = + if s = Some "default" then None + else if s = Some "keep-alguniv" then Some true + else if s = Some "purge-alguniv" then Some false + else if s = None then None + else err Pp.(str"Unknown algebraic universes attribute: " ++ str (Option.get s)) in { hoas_holes = begin match get_bool_option "HOAS:holes" with @@ -1126,6 +1134,7 @@ let get_options ~depth hyps state = reversible = get_bool_option "coq:reversible"; keepunivs = get_bool_option "coq:keepunivs"; redflags = get_redflags_option (); + algunivs = keeping_algebraic_universes @@ get_string_option "coq:algunivs"; } let mk_coq_context ~options state = diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index e9350aaf0..3c74388a5 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -47,6 +47,7 @@ type options = { reversible : bool option; keepunivs : bool option; redflags : CClosure.RedFlags.reds option; + algunivs : bool option; } type 'a coq_context = { diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 25e72f8df..8ae262373 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2173,29 +2173,35 @@ phase unnecessary.|}; MLCode(Pred("coq.sort.leq", InOut(B.ioarg_flex sort, "S1", InOut(B.ioarg_flex sort, "S2", - Full(unit_ctx, "constrains S1 <= S2"))), - (fun u1 u2 ~depth _ _ state -> + Full(global, "constrains S1 <= S2"))), + (fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.leq" + (fun state -> match u1, u2 with | Data u1, Data u2 -> if Sorts.equal u1 u2 then state, !: u1 +! u2,[] else - (* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *) - add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[] - | _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))), + let state, u2 = if true (* options.algunivs != Some true *) + then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) + else state, u2 in + add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[] + | _ -> err Pp.(str"coq.sort.leq: called with _ as argument")))), DocAbove); MLCode(Pred("coq.sort.eq", InOut(B.ioarg_flex sort, "S1", InOut(B.ioarg_flex sort, "S2", - Full(unit_ctx, "constrains S1 = S2"))), - (fun u1 u2 ~depth _ _ state -> + Full(global, "constrains S1 = S2"))), + (fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.eq" + (fun state -> match u1, u2 with | Data u1, Data u2 -> if Sorts.equal u1 u2 then state, !: u1 +! u2,[] else - (* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *) + let state, u2 = if true (* options.algunivs != Some true *) + then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) + else state, u2 in add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, [] - | _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))), + | _ -> err Pp.(str"coq.sort.eq: called with _ as argument")))), DocAbove); MLCode(Pred("coq.sort.sup",