export 8.11 attributes for record fields

.gitignore

@@ -14,6 +14,8 @@
 .*.swp
 
 *.vo
+*.vos
+*.vok
 *.d
 *.glob
 .*.aux

coq-HOAS.elpi

@@ -246,7 +246,6 @@ type nabla (term -> goal) -> goal.
 % unspecified means "_" or a variable.
 
 % tt = Yes, ff = No, unspecified = No
-typeabbrev coercion? bool.  macro @coercion! :- tt.
 typeabbrev opaque?   bool.  macro @opaque!   :- tt.
 typeabbrev global?   bool.  macro @global!   :- tt.
 typeabbrev local?    bool.  macro @local!    :- tt.
@@ -260,7 +259,7 @@ type inductive   id -> int -> term -> (term -> list indc-decl) -> indt-decl.
 type coinductive id -> int -> term -> (term -> list indc-decl) -> indt-decl.
 type constructor id -> term -> indc-decl.
 type record      id -> term -> id -> record-decl -> indt-decl.
-type field       coercion? -> id -> term -> (term -> record-decl) -> record-decl.
+type field       field-attributes -> id -> term -> (term -> record-decl) -> record-decl.
 type end-record  record-decl.
 % Eg (remark A is a parameter, y is a non-uniform parameter and t also has
 % an index of type bool):
@@ -293,3 +292,8 @@ kind context-decl type.
 % Eg. (x : T) or (x := B), body is optional, type may be a variable
 type context-item  id -> term -> option term -> (term -> context-decl) -> context-decl.
 type context-end   context-decl.
+
+typeabbrev field-attributes (list field-attribute).
+
+% retrocompatibility macro for Coq v8.10
+macro @coercion! :- [coercion tt].

coq-builtin.elpi

@@ -261,7 +261,6 @@ type nabla (term -> goal) -> goal.
 % unspecified means "_" or a variable.
 
 % tt = Yes, ff = No, unspecified = No
-typeabbrev coercion? bool.  macro @coercion! :- tt.
 typeabbrev opaque?   bool.  macro @opaque!   :- tt.
 typeabbrev global?   bool.  macro @global!   :- tt.
 typeabbrev local?    bool.  macro @local!    :- tt.
@@ -275,7 +274,7 @@ type inductive   id -> int -> term -> (term -> list indc-decl) -> indt-decl.
 type coinductive id -> int -> term -> (term -> list indc-decl) -> indt-decl.
 type constructor id -> term -> indc-decl.
 type record      id -> term -> id -> record-decl -> indt-decl.
-type field       coercion? -> id -> term -> (term -> record-decl) -> record-decl.
+type field       field-attributes -> id -> term -> (term -> record-decl) -> record-decl.
 type end-record  record-decl.
 % Eg (remark A is a parameter, y is a non-uniform parameter and t also has
 % an index of type bool):
@@ -309,6 +308,17 @@ kind context-decl type.
 type context-item  id -> term -> option term -> (term -> context-decl) -> context-decl.
 type context-end   context-decl.
 
+typeabbrev field-attributes (list field-attribute).
+
+% retrocompatibility macro for Coq v8.10
+macro @coercion! :- [coercion tt].
+
+
+% Attributes for a record field. Can be left unspecified, see defaults
+% below.
+kind field-attribute type.
+type coercion bool -> field-attribute. % default false
+type canonical bool -> field-attribute. % default true, if field is named
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

src/coq_elpi_HOAS.ml

@@ -1424,10 +1424,10 @@ let set_current_sigma ~depth state sigma =
 let get_goal_ref ~depth cst s t =
   get_goal_ref ~depth (E.constraints cst) s t
 
-(* {{{ elpi -> Entries.mutual_inductive_entry **************************** *)
+(* elpi -> Entries.mutual_inductive_entry **************************** *)
 
 (* documentation of the Coq API
- 
+
   Coq < Inductive foo (A : Type) (a : A) : A -> Prop := K : foo A a a.
 
   {Entries.mind_entry_record = None; mind_entry_finite = Finite;
@@ -1456,9 +1456,70 @@ let get_goal_ref ~depth cst s t =
         _UNBOUND_REL_4 _UNBOUND_REL_3 _UNBOUND_REL_2]}];
    mind_entry_universes = Entries.Monomorphic_ind_entry ;
    mind_entry_private = None}
-*
 *)
 
+
+type 'a unspec = Given of 'a | Unspec
+let unspec2opt = function Given x -> Some x | Unspec -> None
+let opt2unspec = function Some x -> Given x | None -> Unspec
+
+let unspecC data = let open API.ContextualConversion 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 hyps constraints state -> function
+     | Given x -> data.embed ~depth hyps constraints state x
+     | Unspec -> state, E.mkDiscard, []);
+  readback = (fun ~depth hyps constraints state x ->
+      match E.look ~depth x with
+      | E.UnifVar _ -> state, Unspec, []
+      | t ->
+        let state, x, gls = data.readback ~depth hyps constraints state (E.kool t) in
+        state, Given x, gls)
+}
+let unspec d = API.ContextualConversion.(!<(unspecC (!> d)))
+
+type record_field_att =
+  | Coercion of bool
+  | Canonical of bool
+
+let record_field_att = let open API.Conversion in let open API.AlgebraicData in let open Elpi.Builtin in declare {
+  ty = TyName "field-attribute";
+  doc = "Attributes for a record field. Can be left unspecified, see defaults below.";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("coercion","default false",A(bool,N),
+        B (fun x -> Coercion(x)),
+        M (fun ~ok ~ko -> function Coercion x -> ok (x) | _ -> ko ()));
+    K("canonical","default true, if field is named",A(bool,N),
+        B (fun x -> Canonical(x)),
+        M (fun ~ok ~ko -> function Canonical x -> ok (x) | _ -> ko ()));
+  ]
+} |> API.ContextualConversion.(!<)
+
+let record_field_attributes = unspec (API.BuiltInData.list record_field_att)
+
+let is_coercion_att = function
+  | Unspec -> false
+  | Given l ->
+      let rec aux = function
+      | [] -> false
+      | Coercion x :: _ -> x
+      | _ :: l -> aux l
+      in
+        aux l
+let is_canonical_att = function
+  | Unspec -> true
+  | Given l ->
+      let rec aux = function
+      | [] -> true
+      | Canonical x :: _ -> x
+      | _ :: l -> aux l
+      in
+        aux l
+
 let parameterc = E.Constants.declare_global_symbol "parameter"
 let constructorc = E.Constants.declare_global_symbol "constructor"
 let inductivec = E.Constants.declare_global_symbol "inductive"
@@ -1479,15 +1540,18 @@ let in_elpi_indtdecl_parameter id ty rest =
   E.mkApp parameterc (in_elpi_name id) [ty;E.mkLam rest]
 let in_elpi_indtdecl_record rid arity kid rest =
   E.mkApp recordc (in_elpi_id rid) [arity;in_elpi_id kid;rest]
-let in_elpi_indtdecl_field s coe id ty rest =
-  E.mkApp fieldc (in_elpi_bool s coe) [in_elpi_id id;ty;E.mkLam rest]
 let in_elpi_indtdecl_endrecord () =
   E.mkConst end_recordc
 
-type record_field_spec = { name : string; is_coercion : bool }
+type record_field_spec = { name : Name.t; is_coercion : bool; is_canonical : bool }
+let in_elpi_indtdecl_field ~depth s { name; is_coercion; is_canonical } ty rest =
+  let open API.Conversion in
+  let s, att, gl = record_field_attributes.embed ~depth s (Given [Coercion is_coercion; Canonical is_canonical]) in
+  assert(gl = []);
+  s, E.mkApp fieldc att [in_elpi_id name;ty;E.mkLam rest], gl
 
 let force_name =
-  let n = ref 0 in      
+  let n = ref 0 in
   function
   | Name.Name x -> x
   | _ ->
@@ -1653,22 +1717,21 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
       mind_entry_private = None; }, List.(concat (rev gls_rev))
   in
 
-  let rec aux_fields depth ind fields =
+  let rec aux_fields depth state ind fields =
     match E.look ~depth fields with
-    | E.App(c,coercion,[n; ty; fields]) when c == fieldc ->
-      begin match E.look ~depth n, E.look ~depth fields with
-      | E.CData name, E.Lam fields when CD.is_string name ->
-        (* HACK for tt, we should not use = but rather [unspec bool] that is
-           not in this file ... *)
-        let tt = in_elpi_bool state true in
-        let fs, tf = aux_fields (depth+1) ind fields in
-        let name = CD.to_string name in
-        { name; is_coercion = coercion = tt } :: fs,
+    | E.App(c,atts,[n; ty; fields]) when c == fieldc ->
+      begin match E.look ~depth fields with
+      | E.Lam fields ->
+        let state, fs, tf = aux_fields (depth+1) state ind fields in
+        let name = in_coq_name ~depth n in
+        let state, atts, gls = record_field_attributes.API.Conversion.readback ~depth state atts in
+        assert(gls = []);
+        state, { name; is_coercion = is_coercion_att atts; is_canonical = is_canonical_att atts } :: fs,
           in_elpi_prod (in_coq_name ~depth n) ty tf
       | _ -> err Pp.(str"field/end-record expected: "++
                    str (pp2string P.(term depth) fields))
       end
-    | E.Const c when c == end_recordc -> [], ind
+    | E.Const c when c == end_recordc -> state, [], ind
     | _ ->  err Pp.(str"field/end-record expected: "++ 
                  str (pp2string P.(term depth) fields))
   in
@@ -1724,7 +1787,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         let fields = U.move ~from:depth ~to_:(depth+1) fields in
         (* We simulate the missing binders for the inductive *)
         let ind = E.mkConst depth in
-        let fields_names_coercions, kty = aux_fields (depth+1) ind fields in
+        let state, fields_names_coercions, kty = aux_fields (depth+1) state ind fields in
         let k = [E.mkApp constructorc kn [kty]] in
         let state, idecl, gl2 =
           aux_construtors (push_coq_ctx_local depth e coq_ctx) ~depth:(depth+1) params 0 arity iname Declarations.BiFinite
@@ -1740,7 +1803,6 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
     | E.Lam t -> aux_decl (push_coq_ctx_local depth e coq_ctx) ~depth:(depth+1) params state extra t
     | _ -> err Pp.(str"lambda expected: "  ++
                  str (pp2string P.(term depth) t))
-
   in
     aux_decl coq_ctx ~depth [] state [] t
 

src/coq_elpi_HOAS.mli

@@ -54,7 +54,7 @@ val lp2constr_closed_ground :  depth:int -> State.t ->
 
 val get_global_env_sigma : State.t -> Environ.env * Evd.evar_map
 
-type record_field_spec = { name : string; is_coercion : bool }
+type record_field_spec = { name : Name.t; is_coercion : bool; is_canonical : bool }
 
 val lp2inductive_entry :
   depth:int -> coq_context -> constraints -> State.t -> term ->
@@ -64,13 +64,18 @@ val in_elpi_id : Names.Name.t -> term
 val in_elpi_bool : State.t -> bool -> term
 val in_elpi_indtdecl_parameter : Names.Name.t -> term -> term -> term
 val in_elpi_indtdecl_record : Names.Name.t -> term -> Names.Name.t -> term -> term
-val in_elpi_indtdecl_field : State.t -> bool -> Names.Name.t -> term -> term -> term
 val in_elpi_indtdecl_endrecord : unit -> term
+val in_elpi_indtdecl_field : depth:int -> State.t -> record_field_spec -> term -> term -> State.t * term * Conversion.extra_goals
 
 val get_goal_ref : depth:int -> constraints -> State.t -> term -> Evar.t option
 val embed_goal : depth:int -> State.t -> Evar.t -> State.t * term * Conversion.extra_goals
 
 (* *** Low level API to reuse parts of the embedding *********************** *)
+type 'a unspec = Given of 'a | Unspec
+val unspec : 'a Conversion.t -> 'a unspec Conversion.t
+val unspec2opt : 'a unspec -> 'a option
+val opt2unspec : 'a option -> 'a unspec
+
 val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
 val in_elpi_sort : Sorts.t -> term
 val in_elpi_flex_sort : term -> term
@@ -125,6 +130,11 @@ val modtypath : Names.ModPath.t 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
 
+type record_field_att =
+  | Coercion of bool
+  | Canonical of bool
+val record_field_att : record_field_att Conversion.t
+
 val new_univ : State.t -> State.t * Univ.Universe.t
 val add_constraints : State.t -> UnivProblem.Set.t -> State.t
 val type_of_global : State.t -> Names.GlobRef.t -> State.t * EConstr.types

src/coq_elpi_builtins.ml

@@ -118,28 +118,6 @@ let clauses_for_later =
             Elpi.API.Pp.Ast.program code) l)
 ;;
 
-type 'a unspec = Given of 'a | Unspec
-let unspec2opt = function Given x -> Some x | Unspec -> None
-let opt2unspec = function Some x -> Given x | None -> Unspec
-
-let unspecC data = {
-  CConv.ty = data.CConv.ty;
-  pp_doc = (fun fmt () -> Format.fprintf fmt "Can be left _");
-  pp = (fun fmt -> function
-    | Unspec -> Format.fprintf fmt "Unspec"
-    | Given x -> Format.fprintf fmt "Given %a" data.CConv.pp x);
-  embed = (fun ~depth hyps constraints state -> function
-     | Given x -> data.CConv.embed ~depth hyps constraints state x
-     | Unspec -> state, E.mkDiscard, []);
-  readback = (fun ~depth hyps constraints state x ->
-      match E.look ~depth x with
-      | E.UnifVar _ -> state, Unspec, []
-      | t ->
-        let state, x, gls = data.CConv.readback ~depth hyps constraints state (E.kool t) in
-        state, Given x, gls)
-}
-let unspec d = CConv.(!<(unspecC (!> d)))
-
 let term = {
   CConv.ty = Conv.TyName "term";
   pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing evars");
@@ -551,6 +529,7 @@ let coq_builtins =
 
 |};
   LPCode Coq_elpi_builtins_HOAS.code;
+  MLData Coq_elpi_HOAS.record_field_att;
   LPCode {|
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% builtins %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

src/coq_elpi_builtins_HOAS.ml

@@ -248,7 +248,6 @@ type nabla (term -> goal) -> goal.
 % unspecified means "_" or a variable.
 
 % tt = Yes, ff = No, unspecified = No
-typeabbrev coercion? bool.  macro @coercion! :- tt.
 typeabbrev opaque?   bool.  macro @opaque!   :- tt.
 typeabbrev global?   bool.  macro @global!   :- tt.
 typeabbrev local?    bool.  macro @local!    :- tt.
@@ -262,7 +261,7 @@ type inductive   id -> int -> term -> (term -> list indc-decl) -> indt-decl.
 type coinductive id -> int -> term -> (term -> list indc-decl) -> indt-decl.
 type constructor id -> term -> indc-decl.
 type record      id -> term -> id -> record-decl -> indt-decl.
-type field       coercion? -> id -> term -> (term -> record-decl) -> record-decl.
+type field       field-attributes -> id -> term -> (term -> record-decl) -> record-decl.
 type end-record  record-decl.
 % Eg (remark A is a parameter, y is a non-uniform parameter and t also has
 % an index of type bool):
@@ -295,4 +294,9 @@ kind context-decl type.
 % Eg. (x : T) or (x := B), body is optional, type may be a variable
 type context-item  id -> term -> option term -> (term -> context-decl) -> context-decl.
 type context-end   context-decl.
+
+typeabbrev field-attributes (list field-attribute).
+
+% retrocompatibility macro for Coq v8.10
+macro @coercion! :- [coercion tt].
 |}

src/coq_elpi_goal_HOAS.ml

@@ -12,12 +12,11 @@ open Names
 type parsed_term =
   Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr
 
-type glob_field_attributes = { canonical : bool; coercion : bool; }
 type glob_record_decl = {
   name : string list * Id.t;
   arity : Genintern.glob_constr_and_expr;
   constructor : Names.Id.t option;
-  fields : (Names.Name.t * Genintern.glob_constr_and_expr * glob_field_attributes) list
+  fields : (Genintern.glob_constr_and_expr * record_field_spec) list
 }
 let pr_glob_record_decl _ = Pp.str "TODO: pr_glob_record_decl"
 type parsed_record_decl = Geninterp.interp_sign * glob_record_decl
@@ -67,11 +66,13 @@ let grecord2lp ~depth sigma state ist { name; arity; constructor; fields } =
     | _ -> CErrors.user_err Pp.(str "It does not look like a record declaration")
   and do_fields ~depth state = function
     | [] -> state, in_elpi_indtdecl_endrecord ()
-    | (name,f,{ coercion }) :: fields ->
+    | (f,({ name; is_coercion; is_canonical } as att)) :: fields ->
         let f = glob_of_closure ist (get_global_env state) sigma f in
         let state, f = gterm2lp ~depth state f in
         let state, fields = under_ctx name f None do_fields ~depth state fields in
-        state, in_elpi_indtdecl_field state coercion name f fields
+        let state, field, gls = in_elpi_indtdecl_field ~depth state att f fields in
+        assert(gls = []);
+        state, field
   in
   let arity = glob_of_closure ist (get_global_env state) sigma arity in
   let state, r = do_params ~depth state arity in

src/coq_elpi_goal_HOAS.mli

@@ -7,12 +7,11 @@ open Elpi.API.RawData
 type parsed_term =
   Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr
 
-type glob_field_attributes = { canonical : bool; coercion : bool; }
 type glob_record_decl = {
   name : string list * Names.Id.t;
   arity : Genintern.glob_constr_and_expr;
   constructor : Names.Id.t option;
-  fields : (Names.Name.t * Genintern.glob_constr_and_expr * glob_field_attributes) list
+  fields : (Genintern.glob_constr_and_expr * Coq_elpi_HOAS.record_field_spec) list
 }
 val pr_glob_record_decl : glob_record_decl -> Pp.t
 type parsed_record_decl = Geninterp.interp_sign * glob_record_decl

src/coq_elpi_vernacular.ml

@@ -111,15 +111,15 @@ let intern_record_decl glob_sign { name; arity = (spine,sort); constructor; fiel
         if nots <> [] then Coq_elpi_utils.nYI "notation in record fields";
         if pr <> None then Coq_elpi_utils.nYI "priority in record fields";
         if inst = Some false then Coq_elpi_utils.nYI "instance :>> flag in record fields";
-        let atts = { Coq_elpi_goal_HOAS.canonical = canon; coercion = inst <> None } in
-        push_name gs fn, (name, Ltac_plugin.Tacintern.intern_constr gs x, atts) :: acc
+        let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = inst <> None; name } in
+        push_name gs fn, (Ltac_plugin.Tacintern.intern_constr gs x, atts) :: acc
     | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr")
         (glob_sign_params,[]) fields in
   { Coq_elpi_goal_HOAS.name = (space, Names.Id.of_string name); arity; constructor; fields = List.rev fields }
 
 let subst_record_decl s { Coq_elpi_goal_HOAS.name; arity; constructor; fields } =
   let arity = Ltac_plugin.Tacsubst.subst_glob_constr_and_expr s arity in
-  let fields = List.map (fun (id,t,att) -> id, Ltac_plugin.Tacsubst.subst_glob_constr_and_expr s t,att) fields in
+  let fields = List.map (fun (t,att) -> Ltac_plugin.Tacsubst.subst_glob_constr_and_expr s t,att) fields in
   { Coq_elpi_goal_HOAS.name; arity; constructor; fields }
 
 let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None)