Merge pull request #201 from LPCIC/switch-to-813

Switch master to 8.13

.github/workflows/main.yml

@@ -16,7 +16,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.12'
+          - '8.13'
         ocaml_version:
           - 'minimal'
     steps:
@@ -26,26 +26,9 @@ jobs:
         opam_file: './coq-elpi.opam'
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
-        custom_script: |
-          startGroup Print opam config
-            opam config list; opam repo list; opam list
-          endGroup
-          startGroup Build dependencies
-            opam pin add -n -y -k path $PACKAGE $WORKDIR
-            opam update -y
-            opam install -y -j 4 $PACKAGE --deps-only
-          endGroup
-          startGroup List installed packages
+        after_script: |
+          startGroup "Test HB"
+            opam pin add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git --ignore-constraints-on=coq-elpi -y -j 4
             opam list
-          endGroup
-          startGroup Build
-            opam install -y -v -j 4 $PACKAGE
-            opam list
-          endGroup
-          startGroup Test Hierarchy Builder
-            opam pin add coq-hierarchy-builder 'https://github.com/math-comp/hierarchy-builder.git' --ignore-constraints-on=coq-elpi -y -j 4
             opam remove coq-hierarchy-builder -y
-          endGroup
-          startGroup Uninstallation test
-            opam remove $PACKAGE -y
-          endGroup
+          endGroup

Changelog.md

@@ -1,5 +1,14 @@
 # Changelog
 
+## [1.8.1] - 11-12-2020
+
+Requires Elpi 1.12 and Coq 8.13.
+### HOAS
+- Illformed terms like `global (const X)` (which have no
+  representation in Coq) are now reported with a proper error message.
+  Whe passed to `coq.term->string`, instead of a fatal error, we pick for
+  the illformed sub term the `unknown_gref` special constant.
+
 ## [1.8.0] - 29-11-2020
 
 Requires Elpi 1.12 and Coq 8.12.

coq-elpi.opam

@@ -12,7 +12,7 @@ build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "elpi" {>= "1.12.0" & < "1.13.0~"}
-  "coq" {>= "8.12" & < "8.13~" }
+  "coq" {>= "8.13" & < "8.14~" }
   ]
 tags: [ "logpath:elpi" ]
 synopsis: "Elpi extension language for Coq"

src/coq_elpi_HOAS.ml

@@ -78,13 +78,15 @@ type options = {
   local : bool option;
   deprecation : Deprecation.t option;
   primitive : bool option;
+  failsafe : bool; (* don't fail, e.g. we are trying to print a term *)
 }
 
 let default_options = {
   hoas_holes = Some Verbatim;
   local = None;
   deprecation = None;
   primitive = None;
+  failsafe = false;
 }
 
 type 'a coq_context = {
@@ -268,7 +270,7 @@ let abbreviation =
   }
 
 module GROrd = struct
-  include Names.GlobRef.Ordered
+  include Names.GlobRef.CanOrd
   let show x = Pp.string_of_ppcmds (Printer.pr_global x)
   let pp fmt x = Format.fprintf fmt "%s" (show x)
 end
@@ -282,10 +284,17 @@ let in_elpi_gr ~depth s r =
   assert (gl = []);
   E.mkApp globalc t []
 
-let in_coq_gref ~depth s t =
-  let s, t, gls = gref.API.Conversion.readback ~depth s t in
-  assert(gls = []);
-  s, t
+let in_coq_gref ~depth ~origin ~failsafe s t =
+  try
+    let s, t, gls = gref.API.Conversion.readback ~depth s t in
+    assert(gls = []);
+    s, t
+  with API.Conversion.TypeErr _ ->
+    if failsafe then
+      s, Coqlib.lib_ref "elpi.unknown_gref"
+    else
+      err Pp.(str "The term " ++ str(pp2string (P.term depth) origin) ++
+        str " cannot be represented in Coq since its gref part is illformed")
 
 let mpin, ismp, mpout, modpath =
   let { CD.cin; isc; cout }, x = CD.declare {
@@ -429,8 +438,8 @@ let show_coq_engine = Format.asprintf "%a" pp_coq_engine
  let from_env env = from_env_sigma env (Evd.from_env env)
 
  let from_env_keep_univ_of_sigma env sigma0 =
-   let sigma = Evd.update_sigma_env sigma0 env in
-   let sigma = Evd.from_ctx (UState.demote_global_univs env (Evd.evar_universe_context sigma)) in
+   let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
+   let sigma = Evd.from_ctx (UState.demote_global_univs env uctx) in
    from_env_sigma env sigma
  let init () = from_env (Global.env ())
 
@@ -617,6 +626,7 @@ let get_options ~depth hyps state =
     local = locality @@ get_string_option "coq:locality";
     deprecation = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecation";
     primitive = get_bool_option "coq:primitive";
+    failsafe = false;
   }
 
 let mk_coq_context ~options state =
@@ -792,7 +802,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
          check_univ_inst (EC.EInstance.kind sigma i);
          state, in_elpi_gr ~depth state (G.ConstructRef construct)
     | C.Case((*{ C.ci_ind; C.ci_npar; C.ci_cstr_ndecls; C.ci_cstr_nargs }*)_,
-             rt,t,bs) ->
+             rt,_,t,bs) ->
          let state, t = aux ~depth env state t in
          let state, rt = aux ~depth env state rt in
          let state, bs = CArray.fold_left_map (aux ~depth env) state bs in
@@ -811,6 +821,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
     | C.CoFix _ -> nYI "HOAS for cofix"
     | C.Int i -> in_elpi_uint63 ~depth state i
     | C.Float f -> in_elpi_float64 ~depth state f
+    | C.Array _ -> nYI "HOAS for persistent arrays"
   in
   if debug () then
     Feedback.msg_debug Pp.(str"term2lp: depth=" ++ int depth ++
@@ -1096,7 +1107,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
       state, EC.mkSort u, gsl
  (* constants *)
   | E.App(c,d,[]) when globalc == c ->
-     let state, gr = in_coq_gref ~depth state d in
+     let state, gr = in_coq_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d in
      begin match gr with
      | G.VarRef x -> state, EC.mkVar x, []
      | G.ConstRef x -> state, EC.mkConst x, []
@@ -1183,7 +1194,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
         match ind with
         | Some ind -> Inductiveops.make_case_info (get_global_env state) ind Sorts.Relevant C.RegularStyle
         | None -> default_case_info () in
-      state, EC.mkCase (ci,rt,t,Array.of_list bt), gl1 @ gl2 @ gl3
+      state, EC.mkCase (ci,rt,C.NoInvert,t,Array.of_list bt), gl1 @ gl2 @ gl3
 
  (* fix *)
   | E.App(c,name,[rno;ty;bo]) when fixc == c ->
@@ -2062,7 +2073,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
       mind_entry_inds = [oe];
       mind_entry_universes =
         Monomorphic_entry (Evd.universe_context_set sigma);
-      mind_entry_cumulative = false;
+      mind_entry_variance = None;
       mind_entry_private = None; }, i_impls, kimpls, List.(concat (rev gls_rev))
   in
 

src/coq_elpi_HOAS.mli

@@ -20,6 +20,7 @@ type options = {
   local : bool option;
   deprecation : Deprecation.t option;
   primitive : bool option;
+  failsafe : bool; (* readback is resilient to illformed terms *)
 }
 
 type 'a coq_context = {

src/coq_elpi_builtins.ml

@@ -85,7 +85,7 @@ let add_universe_constraint state c =
   | Univ.UniverseInconsistency p ->
       Feedback.msg_debug
         (Univ.explain_universe_inconsistency
-           UnivNames.pr_with_global_universes p);
+           UnivNames.(pr_with_global_universes empty_binders) p);
       raise Pred.No_clause
   | Evd.UniversesDiffer | UState.UniversesDiffer ->
       Feedback.msg_debug Pp.(str"UniversesDiffer");
@@ -176,6 +176,14 @@ let term = {
   readback = lp2constr;
   embed = constr2lp;
 }
+let failsafe_term = {
+  CConv.ty = Conv.TyName "term";
+  pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing evars");
+  pp = (fun fmt t -> Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_econstr_env (Global.env()) Evd.empty t)));
+  readback = (fun ~depth coq_ctx csts s t -> lp2constr ~depth { coq_ctx with options = { coq_ctx.options with failsafe = true }} csts s t);
+  embed = constr2lp;
+}
+
 let proof_context : (full coq_context, API.Data.constraints) CConv.ctx_readback =
   fun ~depth hyps constraints state ->
     let state, proof_context, _, gls = get_current_env_sigma ~depth hyps constraints state in
@@ -204,7 +212,10 @@ let closed_ground_term = {
 let term_skeleton =  {
   CConv.ty = Conv.TyName "term";
   pp_doc = (fun fmt () -> Format.fprintf fmt "A Coq term containing holes");
-  pp = (fun fmt t -> Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_glob_constr_env (Global.env()) t)));
+  pp = (fun fmt t ->
+      let env = Global.env() in
+      let sigma = Evd.from_env env in
+      Format.fprintf fmt "%s" (Pp.string_of_ppcmds (Printer.pr_glob_constr_env env sigma t)));
   readback = lp2skeleton;
   embed = (fun ~depth _ _ _ _ -> assert false);
 }
@@ -310,13 +321,19 @@ let cs_pattern =
   doc = "Pattern for canonical values";
   pp = (fun fmt -> function
     | Const_cs x -> Format.fprintf fmt "Const_cs %s" "<todo>"
+    | Proj_cs x -> Format.fprintf fmt "Proj_cs %s" "<todo>"
     | Prod_cs -> Format.fprintf fmt "Prod_cs"
     | Sort_cs _ ->  Format.fprintf fmt "Sort_cs"
     | Default_cs -> Format.fprintf fmt "Default_cs");
   constructors = [
     K("cs-gref","",A(gref,N),
-      B (fun x -> Const_cs x),
-      M (fun ~ok ~ko -> function Const_cs x -> ok x | _ -> ko ()));
+      B (function
+          | GlobRef.ConstructRef _ | GlobRef.IndRef _ | GlobRef.VarRef _ as x -> Const_cs x
+          | GlobRef.ConstRef cst as x ->
+          match Recordops.find_primitive_projection cst with
+          | None -> Const_cs x
+          | Some p -> Proj_cs p),
+      M (fun ~ok ~ko -> function Const_cs x -> ok x | Proj_cs p -> ok (GlobRef.ConstRef (Projection.Repr.constant p)) | _ -> ko ()));
     K("cs-prod","",N,
       B Prod_cs,
       M (fun ~ok ~ko -> function Prod_cs -> ok | _ -> ko ()));
@@ -518,8 +535,8 @@ let attribute_value = let open API.AlgebraicData in let open Attributes in let o
   pp = (fun fmt a -> Format.fprintf fmt "TODO");
   constructors = [
     K("leaf","",A(B.string,N),
-      B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf s),
-      M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf x -> ok x | _ -> ko ()));
+      B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf (FlagString s)),
+      M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf (FlagString x | FlagIdent x) -> ok x | _ -> ko ()));
     K("node","",C((fun self -> !> (B.list (attribute (!< self)))),N),
       B (fun l -> VernacFlagList l),
       M (fun ~ok ~ko -> function VernacFlagList l -> ok l | _ -> ko ())
@@ -592,11 +609,6 @@ let gr2path state gr =
     | Names.GlobRef.IndRef _  | Names.GlobRef.ConstructRef _ ->
           nYI "mutual inductive (make-derived...)"
 
-(* See https://github.com/coq/coq/pull/12759 , the system asserts no evars
-   and the allow_evars flag is gone! *)
-let hack_prune_all_evars sigma =
-  Evd.from_ctx (Evd.evar_universe_context sigma)
-
 let coq_builtins =
   let open API.BuiltIn in
   let open Pred in
@@ -993,7 +1005,7 @@ Supported attributes:
            ComAssumption.declare_variable false ~kind (EConstr.to_constr sigma ty) impargs Glob_term.Explicit variable;
            GlobRef.VarRef(Id.of_string id), Univ.Instance.empty
          end else
-           ComAssumption.declare_axiom false ~local:Declare.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty)
+           ComAssumption.declare_axiom false ~local:Locality.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty)
              (uentry, ubinders) impargs Declaremods.NoInline
              variable
        in
@@ -1012,13 +1024,11 @@ Supported attributes:
        let udecl = UState.default_univ_decl in
        let kind = Decls.(IsDefinition Definition) in
        let scope = if local
-         then Declare.Discharge
-         else Declare.Global Declare.ImportDefaultBehavior in
-       let gr = DeclareDef.declare_definition
-           ~name:(Id.of_string id) ~scope ~kind ~impargs:[]
-           ~poly:false ~udecl ~opaque:(opaque = Given true) ~types ~body
-           (hack_prune_all_evars sigma)
-       in
+         then Locality.Discharge
+         else Locality.(Global ImportDefaultBehavior) in
+       let cinfo = Declare.CInfo.make ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
+       let info = Declare.Info.make ~scope ~kind ~poly:false ~udecl () in
+       let gr = Declare.declare_definition ~cinfo ~info ~opaque:(opaque = Given true) ~body sigma in
        state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
@@ -1041,15 +1051,15 @@ Supported attributes:
      | Some (primitive,field_specs) -> (* record: projection... *)
          let names, flags =
            List.(split (map (fun { name; is_coercion; is_canonical } -> name,
-               { Record.pf_subclass = is_coercion ; pf_canonical = is_canonical })
+               { Record.Internal.pf_subclass = is_coercion ; pf_canonical = is_canonical })
              field_specs)) in
          let is_implicit = List.map (fun _ -> []) names in
          let cstr = (ind,1) in
          let open Entries in
          let k_ty = List.(hd (hd me.mind_entry_inds).mind_entry_lc) in
          let fields_as_relctx = Term.prod_assum k_ty in
          let kinds, sp_projs =
-           Record.declare_projections ind ~kind:Decls.Definition
+           Record.Internal.declare_projections ind ~kind:Decls.Definition
              (Evd.univ_entry ~poly:false sigma)
              (Names.Id.of_string "record")
              flags is_implicit fields_as_relctx
@@ -1062,7 +1072,7 @@ Supported attributes:
            s_EXPECTEDPARAM = npars;
          }
          in
-         Record.declare_structure_entry struc;
+         Record.Internal.declare_structure_entry struc;
      end;
      state, !: ind, []))),
   DocAbove);
@@ -1426,8 +1436,8 @@ Supported attributes:
   (fun gref imps ~depth {options} _ -> on_global_state "coq.arguments.set-implicit" (fun state ->
      let local = options.local <> Some false in
      let imps = imps |> List.(map (map (function
-       | Unspec -> Glob_term.Explicit
-       | Given x -> x))) in
+       | Unspec -> Anonymous, Glob_term.Explicit
+       | Given x -> Anonymous, x))) in
      Impargs.set_implicits local gref imps;
      state, (), []))),
   DocAbove);
@@ -2022,7 +2032,7 @@ coq.id->name S N :- coq.string->name S N.
   DocAbove);
 
   MLCode(Pred("coq.term->string",
-    CIn(term,"T",
+    CIn(failsafe_term,"T",
     Out(B.string, "S",
     Full(proof_context, "prints a term T to a string S using Coq's pretty printer"))),
   (fun t _ ~depth proof_context constraints state ->

src/coq_elpi_glob_quotation.ml

@@ -90,7 +90,7 @@ let type_gen = ref 0
 let rec gterm2lp ~depth state x =
   if debug () then
     Feedback.msg_debug Pp.(str"gterm2lp: depth=" ++ int depth ++
-      str " term=" ++Printer.pr_glob_constr_env (get_global_env state) x);
+      str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x);
   match (DAst.get x) (*.CAst.v*) with
   | GRef(GlobRef.ConstRef p,_ul) when Recordops.is_primitive_projection p ->
       let p = Option.get @@ Recordops.find_primitive_projection p in
@@ -109,8 +109,8 @@ let rec gterm2lp ~depth state x =
       let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in
       state, in_elpi_flex_sort s
   | GSort(UNamed [name,0]) ->
-      let env = get_global_env state in
-      state, in_elpi_sort (Sorts.sort_of_univ @@ Univ.Universe.make @@ Pretyping.interp_known_glob_level (Evd.from_env env) name)
+    let env = get_global_env state in
+      state, in_elpi_sort (Sorts.sort_of_univ @@ Univ.Universe.make @@ Pretyping.known_glob_level (Evd.from_env env) name)
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
   | GProd(name,_,s,t) ->
@@ -302,6 +302,7 @@ let rec gterm2lp ~depth state x =
   | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix"
   | GInt i -> in_elpi_uint63 ~depth state i
   | GFloat f -> in_elpi_float64 ~depth state f
+  | GArray _ -> nYI "(glob)HOAS persistent arrays"
 ;;
 
 let coq_quotation ~depth state _loc src =

src/coq_elpi_goal_HOAS.ml

@@ -68,7 +68,7 @@ let rec list_map_acc f acc = function
       let acc, xs = list_map_acc f acc xs in
       acc, x :: xs
 
-let contract_params env name params t =
+let contract_params env sigma name params t =
   let open Glob_term in
   let loc = Option.map Coq_elpi_utils.of_coq_loc t.CAst.loc in
   let rec contract params args =
@@ -85,7 +85,7 @@ let contract_params env name params t =
        | GHole _ -> contract ps rest
        | _ -> Coq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++
                 str" is not applied to parameter " ++ Names.Id.print pname ++
-                str" but rather " ++ Printer.pr_glob_constr_env env arg)
+                str" but rather " ++ Printer.pr_glob_constr_env env sigma arg)
        end
     in
   let rec aux x =
@@ -102,7 +102,7 @@ let contract_params env name params t =
 let ginductive2lp ~depth state { finiteness; name; arity; params; nuparams; constructors } =
   let open Coq_elpi_glob_quotation in
   let space, indt_name = name in
-  let contract state x = contract_params (get_global_env state) indt_name params x in
+  let contract state x = contract_params (get_global_env state) (get_sigma state) indt_name params x in
   let do_constructor ~depth state (name, ty) =
     let state, ty = do_params nuparams (do_arity (contract state ty)) ~depth state in
     state, in_elpi_indtdecl_constructor (Name.Name name) ty