Define a new type instance_flag instead of using [unit option]

dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh

@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then
+
+    elpi_CI_REF=noinstance
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi

vernac/g_vernac.mlg

@@ -436,12 +436,12 @@ GRAMMAR EXTEND Gram
       | l = binders; ":="; b = lconstr -> { fun id ->
          match b.CAst.v with
          | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
-             (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
+             (NoInstance,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
          | _ ->
-             (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
+             (NoInstance,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
   ;
   record_binder:
-    [ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
+    [ [ id = name -> { (NoInstance,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
       | id = name; f = record_binder_body -> { f id } ] ]
   ;
   assum_list:
@@ -452,13 +452,13 @@ GRAMMAR EXTEND Gram
   ;
   simple_assum_coe:
     [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
-        { (not (Option.is_empty oc),(idl,c)) } ] ]
+        { (oc <> NoInstance,(idl,c)) } ] ]
   ;
 
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-                    { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) }
+                    { fun l id -> (coe <> NoInstance,(id,mkProdCN ~loc l c)) }
             |  ->
                  { fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
          -> { t l }
@@ -469,9 +469,9 @@ GRAMMAR EXTEND Gram
     [ [ id = identref; c=constructor_type -> { c id } ] ]
   ;
   of_type_with_opt_coercion:
-    [ [   ":>" -> { Some () }
-        | ":"; ">" -> { Some () }
-        | ":" -> { None } ] ]
+    [ [   ":>" -> { BackInstance }
+        | ":"; ">" -> { BackInstance }
+        | ":" -> { NoInstance } ] ]
   ;
 END
 

vernac/ppvernac.ml

@@ -503,8 +503,8 @@ let pr_lconstrarg c =
 let pr_intarg n = spc () ++ int n
 
 let pr_oc = function
-  | None -> str" :"
-  | Some () -> str" :>"
+  | NoInstance -> str" :"
+  | BackInstance -> str" :>"
 
 let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
   let prx = match x with

vernac/record.ml

@@ -518,7 +518,7 @@ let implicits_of_context ctx =
     (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
 let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
-    template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities =
+    template fieldimpls fields ?(kind=Decls.StructureComponent) coers =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
     let impls = implicits_of_context params in
@@ -556,10 +556,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       Impargs.declare_manual_implicits false cref paramimpls;
       Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
-      let sub = match List.hd coers with
-        | Some () -> Some (List.hd priorities)
-        | None -> None
-      in
+      let sub = List.hd coers in
       let m = {
         meth_name = Name proj_name;
         meth_info = sub;
@@ -572,10 +569,6 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Decls.Method ~name:[|binder_name|] record_data
       in
-       let coers = List.map2 (fun coe pri ->
-                              Option.map (fun () -> pri) coe)
-          coers priorities
-       in
       let map ind =
         let map decl b y = {
           meth_name = RelDecl.get_name decl;
@@ -739,16 +732,21 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
-    let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
-    let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
+    let coers = List.map (fun (_, { rf_subclass=coe; rf_priority=pri }) ->
+        match coe with
+        | Vernacexpr.BackInstance -> Some {hint_priority = pri ; hint_pattern = None}
+        | Vernacexpr.NoInstance -> None)
+        cfs
+    in
     declare_class def cumulative ubinders univs id.CAst.v idbuild
-      implpars params univ arity template implfs fields coers priorities
+      implpars params univ arity template implfs fields coers
   | _ ->
     let map impls = implpars @ [CAst.make None] @ impls in
     let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
     let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
       let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
-          { pf_subclass = not (Option.is_empty rf_subclass);
+          { pf_subclass =
+              (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
             pf_canonical = rf_canonical })
           cfs
       in

vernac/vernacentries.ml

@@ -776,7 +776,7 @@ let vernac_inductive ~atts kind indl =
       | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.")
     in
     let (coe, (lid, ce)) = l in
-    let coe' = if coe then Some () else None in
+    let coe' = if coe then BackInstance else NoInstance in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
             { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]

vernac/vernacexpr.ml

@@ -106,8 +106,7 @@ type search_restriction =
 
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
-type instance_flag  = unit option
-  (* Some () = Backward instance, None = NoInstance *)
+type instance_flag  = BackInstance | NoInstance
 
 type export_flag    = bool (* true = Export;        false = Import         *)