Universes clause check

.gitignore

@@ -351,3 +351,7 @@ erasure/src/eEnvMap.ml
 erasure/src/eEnvMap.mli
 erasure/src/eGlobalEnv.mli
 erasure/src/eGlobalEnv.ml
+template-coq/extraction_clauses/clauses.ml
+template-coq/extraction_clauses/clauses.mli
+template-coq/extraction_clauses/loop_checking.mli
+template-coq/extraction_clauses/loop_checking.ml

pcuic/theories/Conversion/PCUICUnivSubstitutionConv.v

@@ -579,7 +579,7 @@ Proof.
     split; apply LS.union_spec; right; apply H.
 Qed.
 
-Definition is_monomorphic_cstr (c : UnivConstraint.t)
+Definition is_monomorphic_cstr (c : LevelConstraint.t)
   := negb (Level.is_var c.1.1) && negb (Level.is_var c.2).
 
 Lemma monomorphic_global_constraint {cf : checker_flags} Σ (hΣ : wf Σ) c :

template-coq/_CoqProject

@@ -5,6 +5,10 @@
 theories/utils/canonicaltries/String2pos.v
 theories/utils/canonicaltries/CanonicalTries.v
 
+# Generic loop checking algorithm
+theories/LoopChecking.v
+theories/TemplateLoopChecking.v
+
 # utils
 theories/utils/ByteCompare.v
 theories/utils/ByteCompareSpec.v

template-coq/_PluginProject

@@ -130,8 +130,8 @@ gen-src/mSetFacts.ml
 gen-src/mSetFacts.mli
 gen-src/mSetInterface.ml
 gen-src/mSetInterface.mli
-gen-src/mSetList.ml
-gen-src/mSetList.mli
+# gen-src/mSetList.ml
+# gen-src/mSetList.mli
 gen-src/mSetAVL.ml
 gen-src/mSetAVL.mli
 gen-src/mSetProperties.ml

template-coq/src/ast_denoter.ml

@@ -26,7 +26,7 @@ struct
 
   type quoted_sort_family = Universes0.allowed_eliminations
   type quoted_constraint_type = Universes0.ConstraintType.t
-  type quoted_univ_constraint = Universes0.UnivConstraint.t
+  type quoted_univ_constraint = Universes0.LevelConstraint.t
   type quoted_univ_constraints = Universes0.ConstraintSet.t
   type quoted_univ_instance = Universes0.Instance.t
   type quoted_univ_context = Universes0.UContext.t
@@ -214,7 +214,7 @@ struct
     | Universes0.Universe.Coq_lSProp -> evd, Univ.Universe.sprop
     | Universes0.Universe.Coq_lProp -> evd, Univ.Universe.type0m
     | Universes0.Universe.Coq_lType u ->
-       let u = Universes0.t_set u in
+       let u = Universes0.LevelExprSet.t_set u in
        let ux_list = Universes0.LevelExprSet.elements u in
        let l = List.map unquote_level_expr ux_list in
        evd, List.fold_left Univ.Universe.sup (List.hd l) (List.tl l)

template-coq/src/ast_quoter.ml

@@ -27,7 +27,7 @@ struct
 
   type quoted_sort_family = Universes0.allowed_eliminations
   type quoted_constraint_type = Universes0.ConstraintType.t
-  type quoted_univ_constraint = Universes0.UnivConstraint.t
+  type quoted_univ_constraint = Universes0.LevelConstraint.t
   type quoted_univ_constraints = Universes0.ConstraintSet.t
   type quoted_univ_instance = Universes0.Instance.t
   type quoted_univ_context = Universes0.UContext.t

template-coq/src/plugin_core.ml

@@ -161,9 +161,11 @@ let tmQuoteInductive (kn : kername) : (Names.MutInd.t * mutual_inductive_body) o
     with
       Not_found -> success ~st env evm None
 
-let tmQuoteUniverses : UGraph.t tm =
+let tmQuoteUniverses : Univ.ContextSet.t tm =
   fun ~st env evm success _fail ->
-    success ~st env evm (Environ.universes env)
+    let graph = Environ.universes env in
+    let uctx = Tm_util.ugraph_contextset graph in
+    success ~st env evm uctx
 
 (*let universes_entry_of_decl ?withctx d =
   let open Declarations in

template-coq/src/plugin_core.mli

@@ -58,7 +58,7 @@ val tmLocateString : string -> global_reference list tm
 val tmCurrentModPath : Names.ModPath.t tm
 
 val tmQuoteInductive : kername -> (Names.MutInd.t * mutual_inductive_body) option tm
-val tmQuoteUniverses : UGraph.t tm
+val tmQuoteUniverses : Univ.ContextSet.t tm
 val tmQuoteConstant : kername -> bool -> constant_body tm
 
 val tmInductive : bool -> mutual_inductive_entry -> unit tm

template-coq/src/quoter.ml

@@ -181,38 +181,9 @@ struct
     | Polymorphic ctx -> Q.mkPolymorphic_ctx (Q.quote_abstract_univ_context ctx)
 
   let quote_ugraph ?kept (g : UGraph.t) =
-    debug Pp.(fun () -> str"Quoting ugraph");
-    let levels, cstrs, eqs = 
-      match kept with
-      | None ->
-        let cstrs, eqs = UGraph.constraints_of_universes g in
-        UGraph.domain g, cstrs, eqs
-      | Some l -> 
-        debug Pp.(fun () -> str"Quoting graph restricted to: " ++ Univ.LSet.pr Univ.Level.pr l);
-        (* Feedback.msg_debug Pp.(str"Graph is: "  ++ UGraph.pr_universes Univ.Level.pr (UGraph.repr g)); *)
-        let dom = UGraph.domain g in
-        let kept = Univ.LSet.inter dom l in
-        let kept = Univ.LSet.remove Univ.Level.set kept in
-        let cstrs = time Pp.(str"Computing graph restriction") (UGraph.constraints_for ~kept) g in
-        l, cstrs, []
-    in
-    let levels, cstrs = 
-      List.fold_right (fun eqs acc ->
-        match Univ.LSet.elements eqs with
-        | [] -> acc
-        | x :: [] -> acc
-        | x :: rest ->
-          List.fold_right (fun p (levels, cstrs) ->
-            (Univ.LSet.add p levels, Univ.Constraint.add (x, Univ.Eq, p) cstrs)) rest acc)
-        eqs (levels, cstrs)
-    in
-    let levels = Univ.LSet.add Univ.Level.set levels in
-    let levels = Univ.LSet.remove Univ.Level.prop levels in
-    let levels = Univ.LSet.remove Univ.Level.sprop levels in
-    let cstrs = Univ.Constraint.remove (Univ.Level.prop, Univ.Lt, Univ.Level.set) cstrs in
-    debug Pp.(fun () -> str"Universe context: " ++ Univ.pr_universe_context_set Univ.Level.pr (levels, cstrs));
+    let uctx = ugraph_contextset ?kept g in
     time (Pp.str"Quoting universe context") 
-      (fun uctx -> Q.quote_univ_contextset uctx) (levels, cstrs)
+    (fun uctx -> Q.quote_univ_contextset uctx) uctx
 
   let quote_inductive' (ind, i) : Q.quoted_inductive =
     Q.quote_inductive (Q.quote_kn (Names.MutInd.canonical ind), Q.quote_int i)

template-coq/src/run_extractable.ml

@@ -226,7 +226,7 @@ let rec interp_tm (t : 'a coq_TM) : 'a tm =
              None -> Obj.magic (tmFail Pp.(str "inductive does not exist"))
            | Some (mi, mib) -> Obj.magic (tmOfMib mi mib))
   | Coq_tmQuoteUniverses ->
-    tmMap (fun x -> failwith "tmQuoteUniverses") tmQuoteUniverses
+    tmMap (fun x -> Obj.magic (quote_univ_contextset x)) tmQuoteUniverses
   | Coq_tmQuoteConstant (kn, b) ->
     tmBind (tmQuoteConstant (unquote_kn kn) b)
            (fun x -> Obj.magic (tmOfConstantBody x))

template-coq/src/tm_util.ml

@@ -10,8 +10,8 @@ let gen_constant_in_modules s =
   (* lazy (Universes.constr_of_global (Coqlib.gen_reference_in_modules locstr dirs s)) *)
 
 (* This allows to load template_plugin and the extractable plugin at the same time 
-  while have option settings apply to both *)
-  let timing_opt =
+while have option settings apply to both *)
+let timing_opt =
   let open Goptions in
   let key = ["MetaCoq"; "Timing"] in
   let tables = get_tables () in
@@ -261,6 +261,39 @@ module RetypeMindEntry =
     in ctx, mind
 end 
 
+let ugraph_contextset ?kept (g : UGraph.t) =
+  debug Pp.(fun () -> str"Turning universe graph into universe context set");
+  let levels, cstrs, eqs = 
+    match kept with
+    | None ->
+      let cstrs, eqs = UGraph.constraints_of_universes g in
+      UGraph.domain g, cstrs, eqs
+    | Some l -> 
+      debug Pp.(fun () -> str"Graph restricted to: " ++ Univ.LSet.pr Univ.Level.pr l);
+      (* Feedback.msg_debug Pp.(str"Graph is: "  ++ UGraph.pr_universes Univ.Level.pr (UGraph.repr g)); *)
+      let dom = UGraph.domain g in
+      let kept = Univ.LSet.inter dom l in
+      let kept = Univ.LSet.remove Univ.Level.set kept in
+      let cstrs = time Pp.(str"Computing graph restriction") (UGraph.constraints_for ~kept) g in
+      l, cstrs, []
+  in
+  let levels, cstrs = 
+    List.fold_right (fun eqs acc ->
+      match Univ.LSet.elements eqs with
+      | [] -> acc
+      | x :: [] -> acc
+      | x :: rest ->
+        List.fold_right (fun p (levels, cstrs) ->
+          (Univ.LSet.add p levels, Univ.Constraint.add (x, Univ.Eq, p) cstrs)) rest acc)
+      eqs (levels, cstrs)
+  in
+  let levels = Univ.LSet.add Univ.Level.set levels in
+  let levels = Univ.LSet.remove Univ.Level.prop levels in
+  let levels = Univ.LSet.remove Univ.Level.sprop levels in
+  let cstrs = Univ.Constraint.remove (Univ.Level.prop, Univ.Lt, Univ.Level.set) cstrs in
+  debug Pp.(fun () -> str"Universe context: " ++ Univ.pr_universe_context_set Univ.Level.pr (levels, cstrs));
+  (levels, cstrs)
+
 type ('term, 'name, 'nat) adef = { adname : 'name; adtype : 'term; adbody : 'term; rarg : 'nat }
 
 type ('term, 'name, 'nat) amfixpoint = ('term, 'name, 'nat) adef list

template-coq/theories/Constants.v

@@ -120,7 +120,7 @@ Register MetaCoq.Template.Universes.Level.Var as metacoq.ast.level.Var.
 Register MetaCoq.Template.Universes.Universe.lType as metacoq.ast.levelexpr.npe.
 
 Register MetaCoq.Template.Universes.LevelExprSet.Mkt as metacoq.ast.levelexprset.mkt.
-Register MetaCoq.Template.Universes.Build_nonEmptyLevelExprSet as metacoq.ast.universe.build0.
+Register MetaCoq.Template.Universes.LevelExprSet.Build_nonEmptyLevelExprSet as metacoq.ast.universe.build0.
 Register MetaCoq.Template.Universes.Universe.lSProp as metacoq.ast.universe.lsprop.
 Register MetaCoq.Template.Universes.Universe.lProp as metacoq.ast.universe.lprop.
 Register MetaCoq.Template.Universes.Universe.lType as metacoq.ast.universe.lnpe.
@@ -147,7 +147,7 @@ Register MetaCoq.Template.Universes.AUContext.make as metacoq.ast.AUContext.make
 
 Register MetaCoq.Template.Universes.LevelSet.t_ as metacoq.ast.LevelSet.t.
 Register MetaCoq.Template.Universes.LevelSet.elements as metacoq.ast.LevelSet.elements.
-Register MetaCoq.Template.Universes.UnivConstraint.make as metacoq.ast.make_univ_constraint.
+Register MetaCoq.Template.Universes.LevelConstraint.make as metacoq.ast.make_univ_constraint.
 
 Register MetaCoq.Template.common.uGraph.init_graph as metacoq.ast.graph.init.
 (* FIXME wrong! *)