wip

abstract univ instances (TODO: keep relations between univs and instances)

Author: gares

builtin-doc/coq-builtin.elpi

@@ -789,6 +789,7 @@ external pred coq.env.current-section-path o:list string.
 % - @using! (default: section variables actually used)
 % - @univpoly! (default unset)
 % - @udecl! (default unset)
+% - @udecl-cumul! (default unset)
 % - @dropunivs! (default: false, drops all universe constraints from the
 % store after the definition)
 % 

src/rocq_elpi_HOAS.mli

@@ -246,6 +246,8 @@ val universe_level_variable : Univ.Level.t Conversion.t
 val univ : Univ.Universe.t Conversion.t
 val isuniv : RawOpaqueData.t -> bool
 val univout : RawOpaqueData.t -> Univ.Universe.t
+val isuinstance : RawOpaqueData.t -> bool
+val uinstanceout : RawOpaqueData.t -> UVars.Instance.t
 
 val is_sort : depth:int -> term -> bool
 val is_prod : depth:int -> term -> (term * term) option (* ty, bo @ depth+1 *)

src/rocq_elpi_builtins.ml

@@ -539,53 +539,62 @@ let err_if_contains_alg_univ ~depth t =
     match Univ.Universe.level u with
     | None -> true
     | Some l -> is_global_level env l in
-  let rec aux ~depth acc t =
+  let rec aux ~depth (acc,acci) t =
     match E.look ~depth t with
+    | E.CData c when isuinstance c -> (acc,acci+1)
     | E.CData c when isuniv c ->
         let u = univout c in
-        if is_global u then acc
+        if is_global u then acc, acci
         else
           begin match Univ.Universe.level u with
           | None ->
             err Pp.(strbrk "The hypothetical clause contains terms of type univ which are not global, you should abstract them out or replace them by global ones: " ++
               Univ.Universe.pr UnivNames.pr_level_with_global_universes u)
-          | _ -> Univ.Universe.Set.add u acc
+          | _ -> Univ.Universe.Set.add u acc, acci
           end
-    | x -> Rocq_elpi_utils.fold_elpi_term aux acc ~depth x
+    | x -> Rocq_elpi_utils.fold_elpi_term aux (acc,acci) ~depth x
   in
-  let univs = aux ~depth Univ.Universe.Set.empty t in
+  let univs = aux ~depth (Univ.Universe.Set.empty,0) t in
   univs
 
 let preprocess_clause ~depth clause =
-  let levels_to_abstract = err_if_contains_alg_univ ~depth clause in
+  let levels_to_abstract, instances_to_abstract = err_if_contains_alg_univ ~depth clause in
   let levels_to_abstract_no = Univ.Universe.Set.cardinal levels_to_abstract in
-  let rec subst ~depth m t =
+  let rec subst ~depth m mi t =
     match E.look ~depth t with
     | E.CData c when isuniv c ->
         begin try E.mkBound (Univ.Universe.Map.find (univout c) m)
         with Not_found -> t end
+    | E.CData c when isuinstance c ->
+        decr mi; E.mkBound !mi
     | E.App(c,x,xs) ->
-        E.mkApp c (subst ~depth m x) (List.map (subst ~depth m) xs)
+        E.mkApp c (subst ~depth m mi x) (List.map (subst ~depth m mi) xs)
     | E.Cons(x,xs) ->
-        E.mkCons (subst ~depth m x) (subst ~depth m xs)
+        E.mkCons (subst ~depth m mi x) (subst ~depth m mi xs)
     | E.Lam x ->
-        E.mkLam (subst ~depth:(depth+1) m x)
+        E.mkLam (subst ~depth:(depth+1) m mi x)
     | E.Builtin(c,xs) ->
-        E.mkBuiltin c (List.map (subst ~depth m) xs)
+        E.mkBuiltin c (List.map (subst ~depth m mi) xs)
     | E.UnifVar _ -> CErrors.user_err Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify them out using 'pi'.")
     | E.Const _ | E.Nil | E.CData _ -> t
     in
   let clause = 
-    let rec bind d map = function
+    let rec bind d (map : int Univ.Universe.Map.t) (mapi : int ref) = function
      | [] ->
-         subst ~depth:d map
-           (API.Utils.move ~from:depth ~to_:(depth + levels_to_abstract_no) clause)
+         subst ~depth:d map mapi
+           (API.Utils.move ~from:depth ~to_:(depth + levels_to_abstract_no + !mapi) clause)
      | l :: ls ->
        E.mkApp E.Constants.pic (E.mkLam (*   pi x\  *)
-           (bind (d+1) (Univ.Universe.Map.add l d map) ls)) []
+           (bind (d+1) (Univ.Universe.Map.add l d map) mapi ls)) []
+     and bindi d (map : int Univ.Universe.Map.t) (mapi : int ref) ua n =
+      if n = 0 then
+         bind d map mapi ua
+      else
+        E.mkApp E.Constants.pic (E.mkLam (*   pi x\  *)
+            (bindi (d+1) map mapi ua (n-1))) []
      in
-       bind depth Univ.Universe.Map.empty
-         (Univ.Universe.Set.elements levels_to_abstract)
+       bindi depth Univ.Universe.Map.empty (ref (depth+instances_to_abstract))
+         (Univ.Universe.Set.elements levels_to_abstract) instances_to_abstract
   in
   let vars = collect_term_variables ~depth clause in
   vars, clause
@@ -2165,7 +2174,7 @@ Supported attributes:
     | B.Given body ->
        let sigma = get_sigma state in
        if not (is_ground sigma body) then
-         err Pp.(str"coq.env.add-const: the body must be ground. Did you forge to call coq.typecheck-indt-decl?");
+         err Pp.(str"coq.env.add-const: the body must be ground. Did you forge to call coq.typecheck?");
        let opaque = opaque = B.Given true in
        let types =
          match types, opaque with
@@ -2177,7 +2186,7 @@ Supported attributes:
             | e when CErrors.is_anomaly e -> err Pp.(str"coq.env.add-const: illtyped opaque") end
          | B.Given ty, _ ->
             if not (is_ground sigma ty) then
-              err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck-indt-decl?");
+              err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck?");
              Some ty in
        let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
        let kind = Decls.(IsDefinition Definition) in
@@ -2200,7 +2209,12 @@ Supported attributes:
        let used = Univ.Level.Set.union used (universes_of_udecl state udecl) in
        let sigma = restricted_sigma_of used state in
 
-       let gr, uctx = declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma in
+       let gr, uctx =
+         try declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma
+       with Loop_checking.Undeclared l as e ->
+          Printf.eprintf "Loop_checking.Undeclared %s\n%!" (Univ.Level.to_string l);
+          raise e
+        in
        let () =
         let lid = CAst.make ~loc:(to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state) (Id.of_string id) in
         match scope with

tests/test_HOAS.v

@@ -66,21 +66,31 @@ Elpi Query lp:{{
   coq.env.end-section
 }}.
 
-Elpi Db univs.db lp:{{ pred u o:univ. }}.
+Polymorphic Definition ut@{u} : Type@{u} := Type.
+
+Elpi Db univs.db lp:{{
+   pred u o:univ.
+   pred ut o:term, o:univ.
+  }}.
 Elpi Command test_u.
 Elpi Accumulate Db univs.db.
 Elpi Query lp:{{
   coq.univ.new U,
-  coq.elpi.accumulate current "univs.db" (clause _ _ (u U))
+  coq.elpi.accumulate current "univs.db" (clause _ _ (u U)),
+  coq.univ.variable U L,
+  coq.univ-instance I [L],
+  coq.elpi.accumulate current "univs.db" (clause _ _ (ut (pglobal {{:gref ut}} I) U))
 }}.
 
 Universe foo.
-
+Universe foo1.
+Elpi Print test_u "elpi.tests/test_u".
 Elpi Query lp:{{
   {{ Type@{foo} }} = sort (typ U),
-  coq.elpi.accumulate current "univs.db" (clause _ _ (u U))
+  u U, ut {{ ut@{foo} }} U
 }}.
 
+stop
 
 Axiom B : bool -> Type.
 Axiom N : nat -> Type.