diff options
-rw-r--r-- | checker/mod_checking.ml | 20 | ||||
-rw-r--r-- | checker/reduction.ml | 2 | ||||
-rw-r--r-- | checker/univ.ml | 42 | ||||
-rw-r--r-- | checker/univ.mli | 5 |
4 files changed, 34 insertions, 35 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 78fff1bbe..3ea5ed0d3 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -18,19 +18,27 @@ 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 u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in - mkArity (ctxt,Prop Null), - Univ.enforce_leq u u' Univ.empty_constraint - | _ -> ar, Univ.empty_constraint + let ul = Univ.Level.make empty_dirpath 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 ppnl (str " checking cst: " ++ prcon kn); pp_flush (); - let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in + let env' = + if cb.const_polymorphic then + let inst = Univ.make_abstract_instance cb.const_universes in + let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in + push_context ~strict:false ctx env + else push_context ~strict:true cb.const_universes env + in let envty, ty = match cb.const_type with RegularArity ty -> let ty', cu = refresh_arity ty in - let envty = add_constraints cu env' in + let envty = push_context_set cu env' in let _ = infer_type envty ty' in envty, ty | TemplateArity(ctxt,par) -> let _ = check_ctxt env' ctxt in diff --git a/checker/reduction.ml b/checker/reduction.ml index 8ddeea2a2..384d883ea 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -175,7 +175,7 @@ let sort_cmp env univ pb s0 s1 = then begin if !Flags.debug then begin let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds + Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() ++ Univ.pr_universes univ)) end; diff --git a/checker/univ.ml b/checker/univ.ml index 50c0367bb..648e47817 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -562,20 +562,6 @@ let repr g u = let get_set_arc g = repr g Level.set -(* [safe_repr] also search for the canonical representative, but - if the graph doesn't contain the searched universe, we add it. *) - -let safe_repr g u = - let rec safe_repr_rec u = - match UMap.find u g with - | Equiv v -> safe_repr_rec v - | Canonical arc -> arc - in - try g, safe_repr_rec u - with Not_found -> - let can = terminal u in - enter_arc can g, can - exception AlreadyDeclared let add_universe vlev strict g = @@ -760,8 +746,8 @@ let is_lt g arcu arcv = (** First, checks on universe levels *) let check_equal g u v = - let g, arcu = safe_repr g u in - let _, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in arcu == arcv let check_eq_level g u v = u == v || check_equal g u v @@ -770,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ let check_smaller g strict u v = - let g, arcu = safe_repr g u in - let g, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if strict then is_lt g arcu arcv else @@ -921,8 +907,8 @@ let error_inconsistency o u v = (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> error_inconsistency Eq v u @@ -937,8 +923,8 @@ let enforce_univ_eq u v g = (* enforce_univ_leq : Level.t -> Level.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) let enforce_univ_leq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if is_leq g arcu arcv then g else match fast_compare g arcv arcu with @@ -949,8 +935,8 @@ let enforce_univ_leq u v g = (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) let enforce_univ_lt u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in match fast_compare g arcu arcv with | FastLT -> g | FastLE -> fst (setlt g arcu arcv) @@ -962,7 +948,10 @@ let enforce_univ_lt u v g = | FastLE | FastLT -> error_inconsistency Lt u v (* Prop = Set is forbidden here. *) -let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty +let initial_universes = + let g = enter_arc (terminal Level.set) UMap.empty in + let g = enter_arc (terminal Level.prop) g in + enforce_univ_lt Level.prop Level.set g (* Constraints and sets of constraints. *) @@ -1167,7 +1156,7 @@ struct (** Universe contexts (variables as a list) *) let empty = (Instance.empty, Constraint.empty) - + let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst end @@ -1180,6 +1169,7 @@ struct let empty = LSet.empty, Constraint.empty let constraints (_, cst) = cst let levels (ctx, _) = ctx + let make ctx cst = (ctx, cst) end type universe_context_set = ContextSet.t diff --git a/checker/univ.mli b/checker/univ.mli index 459adfcd6..02c1bbdb9 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -131,7 +131,7 @@ val check_constraints : constraints -> universes -> bool (** Polymorphic maps from universe levels to 'a *) module LMap : Map.S with type key = universe_level - +module LSet : CSig.SetS with type elt = universe_level type 'a universe_map = 'a LMap.t (** {6 Substitution} *) @@ -184,7 +184,7 @@ sig type t val empty : t - + val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints @@ -193,6 +193,7 @@ end module ContextSet : sig type t + val make : LSet.t -> constraints -> t val empty : t val constraints : t -> constraints end |