Merge pull request #570 from LPCIC/fix-tc-options

avoid declaring options twice
LPCIC · Jan 8, 2024 · 75b6197 · 75b6197
2 parents e4960ad + 08a6554
commit 75b6197
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 9 deletions.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
@@ -42,8 +42,10 @@ Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
     all-options Options,
-    std.forall Options (x\ sigma L\ x L, 
-      coq.option.add L (coq.option.bool ff) ff).
+    std.forall Options (x\ sigma L\ x L,
+      if (coq.option.available? L _)
+         true
+         (coq.option.add L (coq.option.bool ff) ff)).
 }}.
 Elpi Typecheck.
 

diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
@@ -960,6 +960,8 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       let open Vernacentries.Preprocessed_Mind_decl in
       let { flags = { template; poly; cumulative; udecl; finite }; primitive_proj; kind; records } = raw_rdecl in
       let template = handle_template_polymorphism template in
+      (* Definitional type classes cannot be interpreted using this function (why?) *)
+      let kind = if kind = Vernacexpr.Class true then Vernacexpr.Class false else kind in
       let e = Record.interp_structure ~template udecl kind ~cumulative ~poly ~primitive_proj finite records in
       record_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
   | IndtDecl (_ist,(glob_sign,raw_indt)) when raw ->

diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
@@ -59,18 +59,22 @@ let is_restricted_name =
   fun s -> Str.(string_match rex (Id.to_string s) 0)
 
 
-let glob_environment : Environ.env S.component =
+let glob_environment : Environ.env option S.component =
   S.declare_component ~name:"coq-elpi:glob-environment" ~descriptor:interp_state
-    ~pp:(fun _ _ -> ()) ~init:(fun () -> Global.env ())
-                        ~start:(fun _ -> Global.env ()) ()
+    ~pp:(fun _ _ -> ()) ~init:(fun () -> None)
+                        ~start:(fun _ -> Some (Global.env ())) ()
+
+(* Since Accumulate runs before the interpreter starts, the state
+   may be empty: ~start not called, ~init called too early *)
+let ensure_some f = function None -> Some (f (Global.env ())) | Some x -> Some (f x)
 
 let push_env state name =
   let open Context.Rel.Declaration in
-  S.update glob_environment state (Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,Constr.mkProp)))
+  S.update glob_environment state (ensure_some (Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,Constr.mkProp))))
 let pop_env state =
-  S.update glob_environment state (Environ.pop_rel_context 1)
+  S.update glob_environment state (ensure_some (Environ.pop_rel_context 1))
 
-let get_glob_env state = S.get glob_environment state
+let get_glob_env state = Option.get @@ ensure_some (fun x -> x) @@ S.get glob_environment state
 
 (* XXX: I don't get why we use a coq_ctx here *)
 let under_ctx name ty bo gterm2lp ~depth state x =
@@ -396,7 +400,7 @@ let coq_quotation ~depth state loc src =
       Constrintern.intern_constr (get_glob_env state) (get_sigma state) ce
     with e ->
       CErrors.user_err
-        Pp.(str(API.Ast.Loc.show loc) ++str":" ++ spc() ++ CErrors.print_no_report e)
+        Pp.(str(API.Ast.Loc.show loc) ++ spc() ++ CErrors.print_no_report e)
   in
   gterm2lp ~depth state glob
 

diff --git a/tests/test_arg_HOAS.v b/tests/test_arg_HOAS.v
@@ -245,6 +245,12 @@ End full_definition.
 
 (*****************************************)
 
+Module classes.
+Elpi declarations Class foo := bar : True.
+End classes.
+
+(*****************************************)
+
 Module copy.
 Import inductive_nup.
 

diff --git a/tests/test_quotation.v b/tests/test_quotation.v
@@ -83,3 +83,14 @@ Fail Elpi Query lp:{{ std.do! [
   std.assert-ok! (coq.typecheck T _) "does not typecheck",
 ]
 }}.
+
+Section A.
+Variable A : Type.
+Check 1.
+Elpi Accumulate lp:{{
+
+pred p i:term.
+p {{ A }}.
+
+}}.
+End A.