From 0f12f2334e6c921a13e2e2186c44b7fb017714c1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 21 Jun 2018 16:30:23 +0200
Subject: Remove enforce_leq from checker

---
 checker/mod_checking.ml | 27 +++++----------------------
 checker/univ.ml         | 42 ------------------------------------------
 checker/univ.mli        |  2 --
 3 files changed, 5 insertions(+), 66 deletions(-)

(limited to 'checker')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ca9581167..6b2af71f3 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -2,7 +2,6 @@ open Pp
 open Util
 open Names
 open Cic
-open Term
 open Reduction
 open Typeops
 open Indtypes
@@ -13,17 +12,6 @@ open Environ
 
 (** {6 Checking constants } *)
 
-let refresh_arity ar =
-  let ctxt, hd = decompose_prod_assum ar in
-  match hd with
-      Sort (Type u) when not (Univ.is_univ_variable u) ->
-      let ul = Univ.Level.make DirPath.empty 1 in
-      let u' = Univ.Universe.make ul in
-      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
-      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
-        mkArity (ctxt,Prop Null), ctx
-    | _ -> ar, Univ.ContextSet.empty
-
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
   (** Locally set the oracle for further typechecking *)
@@ -37,18 +25,13 @@ let check_constant_declaration env kn cb =
       let ctx = Univ.AUContext.repr auctx in
       push_context ~strict:false ctx env
   in
-  let envty, ty = 
-    let ty = cb.const_type in
-    let ty', cu = refresh_arity ty in
-    let envty = push_context_set cu env' in
-    let _ = infer_type envty ty' in
-    envty, ty
-  in
-  let () = 
+  let ty = cb.const_type in
+  let _ = infer_type env' ty in
+  let () =
     match body_of_constant cb with
     | Some bd ->
-      let j = infer envty bd in
-      conv_leq envty j ty
+      let j = infer env' bd in
+      conv_leq env' j ty
     | None -> ()
   in
   let env =
diff --git a/checker/univ.ml b/checker/univ.ml
index 15673736f..e50e883ad 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -190,13 +190,6 @@ struct
       (let (u,n) = x and (v,n') = y in
 	 Int.equal n n' && Level.equal u v)
 
-    let leq (u,n) (v,n') =
-      let cmp = Level.compare u v in
-	if Int.equal cmp 0 then n <= n'
-	else if n <= n' then 
-	  (Level.is_prop u && Level.is_small v)
-	else false
-
     let successor (u,n) =
       if Level.is_prop u then type1
       else (u, n + 1)
@@ -833,41 +826,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-let constraint_add_leq v u c =
-  (* We just discard trivial constraints like u<=u *)
-  if Expr.equal v u then c
-  else 
-    match v, u with
-    | (x,n), (y,m) -> 
-    let j = m - n in
-      if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
-	Constraint.add (x,Lt,y) c
-      else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
-	if Level.equal x y then (* u+(k+1) <= u *)
-	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
-      else if j = 0 then
-	Constraint.add (x,Le,y) c
-      else (* j >= 1 *) (* m = n + k, u <= v+k *)
-	if Level.equal x y then c (* u <= u+k, trivial *)
-	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
-	  
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
-
-let check_univ_leq u v = 
-  Universe.for_all (fun u -> check_univ_leq_one u v) u
-
-let enforce_leq u v c =
-  match v with
-  | [v] ->
-    List.fold_right (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
-
-let enforce_leq u v c =
-  if check_univ_leq u v then c
-  else enforce_leq u v c
-
 let check_constraint g (l,d,r) =
   match d with
   | Eq -> check_equal g l r
diff --git a/checker/univ.mli b/checker/univ.mli
index 6cd3b3638..3b29b158f 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-val enforce_leq : universe constraint_function
-
 (** {6 ... } *)
 (** Merge of constraints in a universes graph.
   The function [merge_constraints] merges a set of constraints in a given
-- 
cgit v1.2.3