From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- checker/univ.ml | 87 ++++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 58 insertions(+), 29 deletions(-) (limited to 'checker/univ.ml') diff --git a/checker/univ.ml b/checker/univ.ml index 3bcb3bc9..648e4781 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -244,7 +244,8 @@ module Level = struct let set = make Set let prop = make Prop - + let var i = make (Var i) + let is_small x = match data x with | Level _ -> false @@ -281,8 +282,8 @@ module Level = struct end (** Level sets and maps *) -module LSet = Set.Make (Level) -module LMap = Map.Make (Level) +module LMap = HMap.Make (Level) +module LSet = LMap.Set type 'a universe_map = 'a LMap.t @@ -559,20 +560,26 @@ let repr g u = in repr_rec u -(* [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 +let get_set_arc g = repr g Level.set +exception AlreadyDeclared + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g in + raise AlreadyDeclared + with Not_found -> + let v = terminal vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -739,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 @@ -749,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 @@ -900,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 @@ -916,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 @@ -928,8 +935,8 @@ let enforce_univ_leq u v g = (* enforce_univ_lt u v will force u g | FastLE -> fst (setlt g arcu arcv) @@ -941,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. *) @@ -970,7 +980,7 @@ module Constraint = Set.Make(UConstraintOrd) let empty_constraint = Constraint.empty let merge_constraints c g = Constraint.fold enforce_constraint c g - + type constraints = Constraint.t (** A value with universe constraints. *) @@ -1146,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 @@ -1158,6 +1168,8 @@ struct type t = LSet.t constrained 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 @@ -1207,6 +1219,9 @@ let subst_instance_constraints s csts = (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) csts Constraint.empty +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + (** Substitute instance inst for ctx in csts *) let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) @@ -1238,6 +1253,20 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) substs nosubst +let merge_context strict ctx g = + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and + constraints due to includes *) + (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + g (UContext.instance ctx) + in merge_constraints (UContext.constraints ctx) g + +let merge_context_set strict ctx g = + let g = LSet.fold + (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) + (ContextSet.levels ctx) g + in merge_constraints (ContextSet.constraints ctx) g + (** Pretty-printing *) let pr_arc = function -- cgit v1.2.3