Add support for syntactic command arguments

Author: Jan-Oliver Kaiser

elpi/coq-arg-HOAS.elpi

@@ -54,6 +54,8 @@ external symbol str      : string -> argument. % Eg. x "y" z.w. or any Coq keywo
 external symbol trm      : term   -> argument. % Eg. (t).
 external symbol open-trm : int -> term -> argument.
 
+external symbol syntax.arg : syntax.argument -> argument.
+
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").
 %

src/rocq_elpi_arg_HOAS.ml

@@ -5,24 +5,47 @@
 open Elpi.API.RawData
 open Rocq_elpi_utils
 
+module API = Elpi.API
+module CD = Elpi.API.RawOpaqueData
+
 type phase = Interp | Synterp | Both
 type proof =
   | Begin of string option (* None = always, Some x only if #[x] present*)
   | End
 
+module GS : sig
+  type 'a t = {
+    gs : Genintern.glob_sign;
+    vl : 'a
+  }
+  val get : 'a t -> 'a
+  val mk : Genintern.glob_sign -> 'a -> 'a t
+end
+
+module IS : sig
+  type 'a t = {
+    is : Geninterp.interp_sign;
+    gs : Genintern.glob_sign;
+    vl : 'a
+  }
+  val get : 'a t -> 'a
+  val mk : Geninterp.interp_sign -> Genintern.glob_sign ->  'a -> 'a t
+  val of_gs : Geninterp.interp_sign -> 'a GS.t -> 'a t
+end
+
 module Cmd : sig
 
 type raw_term = Constrexpr.constr_expr
-type glob_term = Genintern.glob_constr_and_expr
-type top_term = Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr
+type glob_term = raw_term GS.t
+type top_term = raw_term IS.t
 
 type raw_record_decl = Vernacentries.Preprocessed_Mind_decl.record
-type glob_record_decl = Genintern.glob_sign * raw_record_decl
-type top_record_decl = Geninterp.interp_sign * glob_record_decl
+type glob_record_decl = raw_record_decl GS.t
+type top_record_decl = raw_record_decl IS.t
 
 type raw_indt_decl = Vernacentries.Preprocessed_Mind_decl.inductive
-type glob_indt_decl = Genintern.glob_sign * raw_indt_decl
-type top_indt_decl = Geninterp.interp_sign * glob_indt_decl
+type glob_indt_decl = raw_indt_decl GS.t
+type top_indt_decl = raw_indt_decl IS.t
 
 type raw_constant_decl = {
   name : qualified_name;
@@ -33,12 +56,12 @@ type raw_constant_decl = {
   red : Genredexpr.raw_red_expr option;
 }
 val pr_raw_constant_decl : Environ.env -> Evd.evar_map -> raw_constant_decl -> Pp.t
-type glob_constant_decl = Genintern.glob_sign * raw_constant_decl
-type top_constant_decl = Geninterp.interp_sign * glob_constant_decl
+type glob_constant_decl = raw_constant_decl GS.t
+type top_constant_decl = raw_constant_decl IS.t
 
 type raw_context_decl = Constrexpr.local_binder_expr list
-type glob_context_decl = Genintern.glob_sign * raw_context_decl
-type top_context_decl = Geninterp.interp_sign * glob_context_decl
+type glob_context_decl = raw_context_decl GS.t
+type top_context_decl = raw_context_decl IS.t
 
 type ('a,'b,'c,'d,'e) t =
   | Int : int            -> ('a,'b,'c,'d,'e) t
@@ -125,14 +148,56 @@ val in_elpi_tac_econstr :
   Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals
 
 (* for commands *)
+val arg_type : API.Data.term API.Conversion.t
+module Syntactic : sig
+  module Tag :
+    sig
+      type 'a t = {
+        is : Geninterp.interp_sign;
+        gs : Genintern.glob_sign;
+        vl : 'a;
+        tag : int;
+      }
+      val compare_tag : 'a t -> 'b t -> int
+      val counter : int ref
+      val fresh : 'a IS.t -> 'a t
+      val drop_tag : 'a t -> 'a IS.t
+    end
+  type res_term = Cmd.raw_term Tag.t
+  type res_record_decl = Cmd.raw_record_decl Tag.t
+  type res_indt_decl = Cmd.raw_indt_decl Tag.t
+  type res_constant_decl = Cmd.raw_constant_decl Tag.t
+  type res_context_decl = Cmd.raw_context_decl Tag.t
+  type res =
+      (res_term, res_record_decl, res_indt_decl, res_constant_decl,
+       res_context_decl)
+      Cmd.t
+  val pp_res : Environ.env -> Evd.evar_map -> res -> Pp.t
+  val trm : res_term CD.cdata
+  val trm_type : res_term API.Conversion.t
+  val constant_decl : res_constant_decl CD.cdata
+  val constant_decl_type : res_constant_decl API.Conversion.t
+  val indt_decl : res_indt_decl CD.cdata
+  val indt_decl_type : res_indt_decl API.Conversion.t
+  val record_decl : res_record_decl CD.cdata
+  val record_decl_type : res_record_decl API.Conversion.t
+  val context : res_context_decl CD.cdata
+  val context_type : res_context_decl API.Conversion.t
+  val arg_type : res API.Conversion.t
+  val delimiter_depth : Constrexpr.delimiter_depth API.Conversion.t
+  val as_normal_arg : API.RawData.constant
+  val res_of_top : Cmd.top -> res
+  val top_of_res : res -> Cmd.top
+  val ml_data : API.BuiltIn.declaration list
+end
 val in_elpi_cmd :
   loc:Loc.t ->
   depth:int ->
   base:Elpi.API.Compile.program ->
   ?calldepth:int -> 
+  kind:arg_kind ->
   Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.coq_context ->
   Elpi.API.State.t ->
-  raw:bool ->
   Cmd.top ->
   Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals
 val in_elpi_cmd_synterp :

src/rocq_elpi_arg_HOAS.mli

@@ -195,7 +195,21 @@ let skip_and_synterp_attributes = Attributes.Notations.(skip_attribute ++ synter
 let scope_and_skip_and_synterp_attributes = Attributes.Notations.(scope_attribute ++ skip_attribute ++ synterp_attribute)
 
 let raw_args_attributes =
-  Attributes.(qualify_attribute "arguments" (bool_attribute ~name:"raw"))
+  Attributes.qualify_attribute "arguments"
+    (Attributes.attribute_of_list
+      ["elaborated", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Elaborated
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"elaborated\" does not expect a value"));
+       "unelaborated", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Unelaborated
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"unelaborated\" does not expect a value"));
+       "raw", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Unelaborated
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"raw\" does not expect a value"));
+       "syntactic", (fun ?loc old -> function
+        | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Syntactic
+        | _ -> CErrors.user_err ?loc Pp.(str "Argument \"syntactic\" does not expect a value"));
+      ])    
 
 let validate_attributes a flags =
   let extra, raw_args = Attributes.parse_with_extra a flags in

src/rocq_elpi_arg_syntax.mlg

@@ -27,6 +27,7 @@ open Names
 
 open Rocq_elpi_utils
 open Rocq_elpi_HOAS
+open Rocq_elpi_arg_HOAS
 
 let string_of_ppcmds options pp =
   let b = Buffer.create 512 in
@@ -252,6 +253,27 @@ let term_skeleton =  {
   embed = (fun ~depth _ _ _ _ -> assert false);
 }
 
+let type_constraint =
+  API.AlgebraicData.declare {
+    ty = TyName "type-constraint";
+    doc = "The expected type for elaborating syntactic terms";
+    pp = (fun fmt _ -> Format.fprintf fmt "<TODO>");
+    constructors = Pretyping.[
+        K("without-type-constraint", "Pretype without type constraint", N,
+          B (WithoutTypeConstraint),
+          M (fun ~ok ~ko -> function WithoutTypeConstraint -> ok | _ -> ko ())
+         );
+        K("of-type", "Pretype with a specific expected type", CA(term, N),
+          B (fun t -> OfType t),
+          M (fun ~ok ~ko -> function OfType t -> ok t | _ -> ko ())
+         );
+        K("is-type", "Pretype as a type", N,
+          B (IsType),
+          M (fun ~ok ~ko -> function IsType -> ok | _ -> ko ())
+         );
+      ];
+    }
+
 let sealed_goal = {
   Conv.ty = Conv.TyName "sealed-goal";
   pp_doc = (fun fmt () -> ());
@@ -4390,5 +4412,104 @@ Supported attributes:
   DocAbove)
 
   ]
+  @ Syntactic.ml_data @
+  [MLDataC(type_constraint);
+   MLCode(Pred("syntax.default-elab",
+    In(Syntactic.arg_type, "SyntaxArg",
+    Out(Rocq_elpi_arg_HOAS.arg_type, "Arg",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(global, "Elaborates the syntactic argument with the settings of #[arguments(elaborated)]")))),
+    fun sarg _ diag ~depth coq_ctx _csts state ->
+      let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
+      let base = Option.get (State.get base state) in
+      try
+        let state, res, extra_goals =
+          Syntactic.top_of_res sarg |>
+          Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind:Elaborated coq_ctx state
+        in
+        state, (!: res +! B.mkOK), extra_goals
+      with e ->
+        diag_error_lazy diag @@ fun () ->
+        let error =
+          string_of_ppcmds coq_ctx.options @@
+          try CErrors.print_no_report e with | _ -> raise No_clause
+        in
+        state, ?: None +! B.mkERROR error, []
+   ),
+   DocAbove);
+   MLCode(Pred("syntax.default-unelab",
+    In(Syntactic.arg_type, "SyntaxArg",
+    Out(Rocq_elpi_arg_HOAS.arg_type, "Arg",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(global, "Elaborates the syntactic argument with the settings of #[arguments(unelaborated)]")))),
+    fun sarg _ diag ~depth coq_ctx _csts state ->
+      let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
+      let base = Option.get (State.get base state) in
+      try
+        let state, res, extra_goals =
+          Syntactic.top_of_res sarg |>
+          Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind:Unelaborated coq_ctx state
+        in
+        state, (!: res +! B.mkOK), extra_goals
+      with e ->
+        diag_error_lazy diag @@ fun () ->
+        let error =
+          string_of_ppcmds coq_ctx.options @@
+          try CErrors.print_no_report e with | _ -> raise No_clause
+        in
+        state, ?: None +! B.mkERROR error, []
+     ),
+   DocAbove);
+   MLCode(Pred("syntax.push-scope",
+    In(Syntactic.trm_type, "SyntaxTerm",
+    In(Syntactic.delimiter_depth, "DelimiterDepth",
+    In(B.string, "ScopeName",
+    Out(Syntactic.trm_type, "ScopedSyntaxTerm",
+    Full(global, "Pushes the scope ScopeName on top of SyntaxTerm."))))),
+    fun t delim_depth scope _ ~depth coq_context _csts state ->
+      let open Syntactic in
+      let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
+      let Tag.{vl; _} = t in
+      let vl = CAst.make ~loc (Constrexpr.CDelimiters (delim_depth, scope, vl)) in
+      let ot = Tag.{t with vl} in
+      state, (!: ot), []
+    ),
+   DocAbove);
+   MLCode(Pred("syntax.elaborate",
+    In(Syntactic.trm_type, "SyntaxTerm",
+    CIn(type_constraint, "TypeConstraint",
+    COut(term, "Term",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(proof_context, "Elaborates SyntaxTerm using TypeConstraint. Respects @no-tc! and @no-coercion!"))))),
+    fun t expected_type _ diag ~depth coq_ctx csts state ->
+      let open Syntactic in
+      let Tag.{is;gs;vl} = t in
+      let vl = Ltac_plugin.Tacintern.intern_constr gs vl in
+      let sigma = get_sigma state in
+      let flags =
+        let open Pretyping in
+        let flags = all_no_fail_flags in
+        let options = coq_ctx.options in
+        let use_typeclasses = if Option.default false options.no_tc then NoUseTC else UseTC in
+        let use_coercions = not @@ Option.default false options.no_coercion in
+        { flags with use_typeclasses; use_coercions }
+      in
+      try
+        let sigma, vl =
+          Ltac_plugin.Tacinterp.interp_open_constr ~flags ~expected_type is coq_ctx.env sigma vl
+        in
+        let state, extra_goals = set_current_sigma ~depth state sigma in
+        state, (!: vl +! B.mkOK), extra_goals
+      with e ->
+        diag_error_lazy diag @@ fun () ->
+        let error =
+          string_of_ppcmds coq_ctx.options @@
+          try CErrors.print_no_report e with | _ -> raise No_clause
+        in
+        state, ?: None +! B.mkERROR error, []
+    ),
+   DocAbove);
+  ]
+
 
 ;;

src/rocq_elpi_builtins.ml

@@ -19,6 +19,7 @@ open Names
 
 open Rocq_elpi_utils
 open Rocq_elpi_HOAS
+open Rocq_elpi_arg_HOAS
 
 let prop = { B.any with Conv.ty = Conv.TyName "prop" }
 
@@ -1229,7 +1230,7 @@ Supported attributes:
   ] @ SynterpAction.get_parsing_actions_synterp @ [
   MLData attribute_value;
   MLData attribute;
-  ]
+  ] @ Syntactic.ml_data
 
 let synterp_api_doc = ". bla bla"
 

src/rocq_elpi_builtins_synterp.ml

@@ -163,7 +163,7 @@ type db = {
   units : Names.KNset.t;
 }
 
-type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool }
+type nature = Command of { args : arg_kind } | Tactic | Program of { args : arg_kind }
 
 type program = {
   sources_rev : qualified_name Code.t;
@@ -242,7 +242,7 @@ module type Programs = sig
   val db_inspect : qualified_name -> int
 
   val get_and_compile_existing_db : loc:Loc.t -> qualified_name -> EC.program
-  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (EC.program * bool) option
+  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (EC.program * arg_kind) option
 
 end
 
@@ -804,7 +804,7 @@ let compile ~loc src =
   in
     compile_code src
 
-let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option =
+let get_and_compile ~loc ?even_if_empty name : (EC.program * arg_kind) option =
   let t = Unix.gettimeofday () in
   let res = code ?even_if_empty name |> Option.map (fun src ->
     (* Format.eprintf "compile %a = %a" pp_qualified_name name (Code.pp Chunk.pp) src; *)
@@ -815,9 +815,9 @@ let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option =
     let prog = recache_code 0 old_hash new_hash prog src in
     let raw_args =
       match get_nature name with
-      | Command { raw_args } -> raw_args
-      | Program { raw_args } -> raw_args
-      | Tactic -> true in
+      | Command { args } -> args
+      | Program { args } -> args
+      | Tactic -> Elaborated in
       (prog, raw_args)) in
     Rocq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t))));
     res

src/rocq_elpi_programs.ml

@@ -24,7 +24,7 @@ and src_db_header = {
   dast : cunit;
 }
 
-type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool }
+type nature = Command of { args : arg_kind } | Tactic | Program of { args : arg_kind }
 
 
 module Chunk : sig
@@ -120,7 +120,7 @@ module type Programs = sig
   val db_inspect : qualified_name -> int
 
   val get_and_compile_existing_db : loc:Loc.t -> qualified_name -> Compile.program
-  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (Compile.program * bool) option
+  val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (Compile.program * arg_kind) option
 
 
 end

src/rocq_elpi_programs.mli

@@ -90,6 +90,13 @@ val gr2path: Names.GlobRef.t -> string list
 
 val eta_contract : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
 
+(* Command argument specifiers *)
+type arg_kind =
+  | Elaborated
+  | Unelaborated
+  | Syntactic
+val arg_kind_merge : ?loc:Loc.t -> arg_kind option -> arg_kind -> arg_kind
+
 (* Diagnostics *)
 val diag_error_lazy : ?on_ok:(unit -> 'a) -> (* defaults to [raise No_clause] *)
   Elpi.Builtin.diagnostic Elpi.API.BuiltInPredicate.ioarg ->