API: reduction flags

Author: gares

Makefile.examples.coq

@@ -385,6 +385,8 @@ macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
 macro @inline-at! N :- get-option "coq:inline" (coq.inline.at N). % like Inline(N)
 macro @inline! N :- get-option "coq:inline" coq.inline.default. % like
 
+macro @redflags! F :- get-option "coq:redflags" F. % for whd & co
+
 % both arguments are strings eg "8.12.0" "use foo instead"
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).
@@ -1359,15 +1361,57 @@ external pred coq.elaborate-skeleton i:term, o:term, o:term, o:diagnostic.
 external pred coq.elaborate-ty-skeleton i:term, o:sort, o:term, 
                                         o:diagnostic.
 
+% -- Coq's reduction flags    ------------------------------------
+
+% Flags for lazy, cbv, ... reductions
+kind coq.redflag type.
+type coq.redflags.beta coq.redflag.
+type coq.redflags.delta coq.redflag.
+type coq.redflags.match coq.redflag.
+type coq.redflags.fix coq.redflag.
+type coq.redflags.cofix coq.redflag.
+type coq.redflags.zeta coq.redflag.
+type coq.redflags.const constant -> coq.redflag.
+
+% Set of flags for lazy, cbv, ... reductions
+typeabbrev coq.redflags (ctype "coq.redflags").
+
+type coq.redflags.all coq.redflags.
+type coq.redflags.allnolet coq.redflags.
+type coq.redflags.beta coq.redflags.
+type coq.redflags.betadeltazeta coq.redflags.
+type coq.redflags.betaiota coq.redflags.
+type coq.redflags.betaiotazeta coq.redflags.
+type coq.redflags.betazeta coq.redflags.
+type coq.redflags.delta coq.redflags.
+type coq.redflags.zeta coq.redflags.
+type coq.redflags.nored coq.redflags.
+
+% [coq.redflags.add Flags Options NewFlags] Updates reduction Flags by
+% adding Options
+external pred coq.redflags.add i:coq.redflags, i:list coq.redflag, 
+                               o:coq.redflags.
+
+% [coq.redflags.sub Flags Options NewFlags] Updates reduction Flags by
+% removing Options
+external pred coq.redflags.sub i:coq.redflags, i:list coq.redflag, 
+                               o:coq.redflags.
+
 % -- Coq's reduction machines ------------------------------------
 
-% [coq.reduction.lazy.whd_all T Tred] Puts T in weak head normal form
-external pred coq.reduction.lazy.whd_all i:term, o:term.
+% [coq.reduction.lazy.whd T Tred] Puts T in weak head normal form.
+% Supported attributes:
+% - @redflags! (default coq.redflags.all)
+external pred coq.reduction.lazy.whd i:term, o:term.
 
-% [coq.reduction.lazy.norm T Tred] Puts T in normal form
+% [coq.reduction.lazy.norm T Tred] Puts T in normal form.
+% Supported attributes:
+% - @redflags! (default coq.redflags.all)
 external pred coq.reduction.lazy.norm i:term, o:term.
 
-% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form
+% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form.
+% Supported attributes:
+% - @redflags! (default coq.redflags.all)
 external pred coq.reduction.cbv.norm i:term, o:term.
 
 % [coq.reduction.vm.norm T Ty Tred] Puts T in normal form. Its type Ty can
@@ -1397,6 +1441,12 @@ coq.reduction.vm.whd_all T TY R :-
   coq.reduction.vm.norm T TY R.
 
 
+
+pred coq.reduction.lazy.whd_all i:term, o:term.
+coq.reduction.lazy.whd_all X Y :-
+  @redflags! coq.redflags.all => coq.reduction.lazy.whd X Y.
+
+
 % -- Coq's conversion strategy tweaks --------------------------
 
 % Strategy for conversion test

Makefile.examples.coq.conf

@@ -370,6 +370,8 @@ macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
 macro @inline-at! N :- get-option "coq:inline" (coq.inline.at N). % like Inline(N)
 macro @inline! N :- get-option "coq:inline" coq.inline.default. % like
 
+macro @redflags! F :- get-option "coq:redflags" F. % for whd & co
+
 % both arguments are strings eg "8.12.0" "use foo instead"
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).

coq-builtin.elpi

@@ -342,6 +342,7 @@ type options = {
   nonuniform : bool option;
   reversible : bool option;
   keepunivs : bool option;
+  redflags : CClosure.RedFlags.reds option;
 }
 
 let default_options = {
@@ -360,6 +361,7 @@ let default_options = {
   nonuniform = None;
   reversible = None;
   keepunivs = None;
+  redflags = None;
 }
 
 type 'a coq_context = {
@@ -983,6 +985,27 @@ let module_inline_default = { module_inline_unspec with
      | state, Elpi.Builtin.Unspec, gls -> state,Declaremods.DefaultInline,gls)
 }
 
+let reduction_flags = let open API.OpaqueData in let open CClosure in declare {
+  name = "coq.redflags";
+  doc = "Set of flags for lazy, cbv, ... reductions";
+  pp = (fun fmt (x : RedFlags.reds) -> Format.fprintf fmt "TODO");
+  compare = Stdlib.compare;
+  hash = Hashtbl.hash;
+  hconsed = false;
+  constants = [
+    "coq.redflags.all",           all          ;
+    "coq.redflags.allnolet",      allnolet     ;
+    "coq.redflags.beta",          beta         ;
+    "coq.redflags.betadeltazeta", betadeltazeta;
+    "coq.redflags.betaiota",      betaiota     ;
+    "coq.redflags.betaiotazeta",  betaiotazeta ;
+    "coq.redflags.betazeta",      betazeta     ;
+    "coq.redflags.delta",         delta        ;
+    "coq.redflags.zeta",          zeta         ;
+    "coq.redflags.nored",         nored        ;
+];
+}
+
 let get_optionc   = E.Constants.declare_global_symbol "get-option"
 
 let get_options ~depth hyps state =
@@ -1074,6 +1097,13 @@ let get_options ~depth hyps state =
       assert (gl = []);
       NonCumulative ud
     in
+  let get_redflags_option () =
+    match API.Data.StrMap.find_opt "coq:redflags" map with
+    | None -> None
+    | Some (t,depth) ->
+      let _, rd, gl = reduction_flags.Elpi.API.Conversion.readback ~depth state t in
+      assert (gl = []);
+      Some rd in
   {
     hoas_holes =
       begin match get_bool_option "HOAS:holes" with
@@ -1094,6 +1124,7 @@ let get_options ~depth hyps state =
     nonuniform = get_bool_option "coq:nonuniform";
     reversible = get_bool_option "coq:reversible";
     keepunivs = get_bool_option "coq:keepunivs";
+    redflags = get_redflags_option ();
   }
 
 let mk_coq_context ~options state =

elpi/coq-HOAS.elpi

@@ -46,6 +46,7 @@ type options = {
   nonuniform : bool option;
   reversible : bool option;
   keepunivs : bool option;
+  redflags : CClosure.RedFlags.reds option;
 }
 
 type 'a coq_context = {
@@ -228,6 +229,7 @@ val in_coq_modpath : depth:int -> term -> Names.ModPath.t
 val modpath : Names.ModPath.t Conversion.t
 val modtypath : Names.ModPath.t Conversion.t
 val module_inline_default : Declaremods.inline Conversion.t
+val reduction_flags : CClosure.RedFlags.reds Conversion.t
 
 val in_elpi_module : depth:int -> State.t -> Declarations.module_body -> GlobRef.t list
 val in_elpi_module_type : Declarations.module_type_body -> string list

src/coq_elpi_HOAS.ml

@@ -587,6 +587,35 @@ let conversion_strategy = let open API.AlgebraicData in let open Conv_oracle in
   ]
 } |> CConv.(!<)
 
+let reduction_kind = let open API.AlgebraicData in let open CClosure.RedFlags in declare {
+  ty = Conv.TyName "coq.redflag";
+  doc = "Flags for lazy, cbv, ... reductions";
+  pp = (fun fmt (x : red_kind) -> Format.fprintf fmt "TODO");
+  constructors = [
+    K ("coq.redflags.beta", "",N,
+      B fBETA,
+      M (fun ~ok ~ko x -> if x = fBETA then ok else ko ()));
+    K ("coq.redflags.delta", "",N,
+      B fDELTA,
+      M (fun ~ok ~ko x -> if x = fDELTA then ok else ko ()));
+    K ("coq.redflags.match", "",N,
+      B fMATCH,
+      M (fun ~ok ~ko x -> if x = fMATCH then ok else ko ()));
+    K ("coq.redflags.fix", "",N,
+      B fFIX,
+      M (fun ~ok ~ko x -> if x = fFIX then ok else ko ()));
+    K ("coq.redflags.cofix", "",N,
+      B fCOFIX,
+      M (fun ~ok ~ko x -> if x = fCOFIX then ok else ko ()));
+    K ("coq.redflags.zeta", "",N,
+      B fZETA,
+      M (fun ~ok ~ko x -> if x = fZETA then ok else ko ()));
+    K("coq.redflags.const","",A(constant,N),
+      B (function Constant x -> fCONST x | Variable x -> fVAR x),
+      M (fun ~ok ~ko x -> nYI "readback for coq.redflags.const"));
+  ]
+} |> CConv.(!<)
+
 let attribute a = let open API.AlgebraicData in declare {
   ty = Conv.TyName "attribute";
   doc = "Generic attribute";
@@ -3076,35 +3105,71 @@ Supported attributes:
           state, ?: None +? None +! B.mkERROR error, [])),
   DocAbove);
 
+  LPDoc "-- Coq's reduction flags    ------------------------------------";
+
+  MLData reduction_kind;
+  MLData reduction_flags;
+
+  MLCode(Pred("coq.redflags.add",
+    In(reduction_flags,"Flags",
+    In(B.list reduction_kind,"Options",
+    Out(reduction_flags,"NewFlags",
+    Easy "Updates reduction Flags by adding Options"))),
+    (fun f l _ ~depth ->
+       let open CClosure in
+       let f = List.fold_left RedFlags.red_add f l in
+       !: f)),
+  DocAbove);
+
+  MLCode(Pred("coq.redflags.sub",
+    In(reduction_flags,"Flags",
+    In(B.list reduction_kind,"Options",
+    Out(reduction_flags,"NewFlags",
+    Easy "Updates reduction Flags by removing Options"))),
+    (fun f l _ ~depth ->
+       let open CClosure in
+       let f = List.fold_left RedFlags.red_sub f l in
+       !: f)),
+  DocAbove);
+
   LPDoc "-- Coq's reduction machines ------------------------------------";
 
-  MLCode(Pred("coq.reduction.lazy.whd_all",
+  MLCode(Pred("coq.reduction.lazy.whd",
     CIn(term,"T",
     COut(term,"Tred",
-    Read(proof_context, "Puts T in weak head normal form"))),
+    Read(proof_context, {|Puts T in weak head normal form.
+Supported attributes:
+- @redflags! (default coq.redflags.all)|}))),
     (fun t _ ~depth proof_context constraints state ->
        let sigma = get_sigma state in
-       let t = EConstr.of_constr @@ Reduction.whd_all proof_context.env (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) in
+       let flags = Option.default CClosure.all proof_context.options.redflags in
+       let t = Reductionops.clos_whd_flags flags proof_context.env sigma t in
        !: t)),
   DocAbove);
 
   MLCode(Pred("coq.reduction.lazy.norm",
     CIn(term,"T",
     COut(term,"Tred",
-    Read(proof_context, "Puts T in normal form"))),
+    Read(proof_context, {|Puts T in normal form.
+Supported attributes:
+- @redflags! (default coq.redflags.all)|}))),
     (fun t _ ~depth proof_context constraints state ->
        let sigma = get_sigma state in
-       let t = Reductionops.nf_all proof_context.env sigma t in
+       let flags = Option.default CClosure.all proof_context.options.redflags in
+       let t = Reductionops.clos_norm_flags flags proof_context.env sigma t in
        !: t)),
   DocAbove);
 
   MLCode(Pred("coq.reduction.cbv.norm",
     CIn(term,"T",
     COut(term,"Tred",
-    Read(proof_context, "Puts T in weak head normal form"))),
+    Read(proof_context, {|Puts T in weak head normal form.
+Supported attributes:
+- @redflags! (default coq.redflags.all)|}))),
     (fun t _ ~depth proof_context constraints state ->
        let sigma = get_sigma state in
-       let t = Tacred.compute proof_context.env sigma t in
+       let flags = Option.default CClosure.all proof_context.options.redflags in
+       let t = Tacred.cbv_norm_flags flags proof_context.env sigma t in
        !: t)),
   DocAbove);
 
@@ -3161,6 +3226,12 @@ coq.reduction.vm.whd_all T TY R :-
   coq.reduction.vm.norm T TY R.
 |};
 
+  LPCode {|
+pred coq.reduction.lazy.whd_all i:term, o:term.
+coq.reduction.lazy.whd_all X Y :-
+  @redflags! coq.redflags.all => coq.reduction.lazy.whd X Y.
+|};
+
   LPDoc "-- Coq's conversion strategy tweaks --------------------------";
 
   MLData conversion_strategy;