[HOAS] deal with illformed grefs (fix #189)

Changelog.md

@@ -1,8 +1,13 @@
 # Changelog
 
-## [1.8.1] - 10-12-2020
+## [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
 

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 = {
@@ -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 {
@@ -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 =
@@ -1097,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, []

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

@@ -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
@@ -2024,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 ->

tests/test_API.v

@@ -140,6 +140,26 @@ Elpi Query lp:{{
 
 }}.
 
+Elpi Tactic test.
+Elpi Accumulate lp:{{
+solve _ _ _ :-
+  coq.term->string X S,
+  X = global (indc Y),
+  coq.say S.
+}}.
+Goal True.
+Fail elpi test.
+Abort.
+
+Elpi Tactic test2.
+Elpi Accumulate lp:{{
+solve _ _ _ :-
+  coq.term->string (global (indc Y)) S,
+  coq.say S.
+}}.
+Goal True.
+elpi test2.
+Abort.
 
 End elab.
 (****** say *************************************)

theories/elpi.v

@@ -19,6 +19,14 @@ Register hole as elpi.hole.
 Inductive unknown_inductive : Prop := unknown_constructor.
 Register unknown_inductive as elpi.unknown_inductive.
 
+(* Special global constant used to signal a datum of type gref which
+   has no corresponding Coq global reference. This typically signals
+   an error: a term like (global (const X)) has no meaning in Coq, X must
+   be an actual name.
+*)
+Inductive unknown_gref : Prop := .
+Register unknown_gref as elpi.unknown_gref.
+
 (* Common constants available inside Coq's syntax {{ ... lib:<name> ... }} *)
 Register Coq.Init.Logic.eq      as elpi.eq.
 Register Coq.Init.Logic.eq_refl as elpi.erefl.