Permalink
Browse files

Add a set of undefined universe variables to unification.

Universe variables can now be declared rigid or flexible (unifiable).
Flexible variables are resolved at the end of typechecking by instantiating
them to their glb, adding upper bound constraints associated to them.
Also:
- Add polymorphic flag for inductives.
- Fix cooking partially
- Fix kernel/univ.ml to do normalization of universe expressions at
the end of substitution.
  • Loading branch information...
1 parent 16a84d7 commit 96829d042dbb5a7c2f936f0f7ce6bf757b1f43b8 @mattam82 mattam82 committed Oct 28, 2012
@@ -1687,7 +1687,7 @@ let interp_open_constr_patvar sigma env c =
| GPatVar (loc,(_,id)) ->
( try Gmap.find id !evars
with Not_found ->
- let ev,_ = Evarutil.e_new_type_evar sigma env in
+ let ev,_ = Evarutil.e_new_type_evar sigma false env in
let ev = Evarutil.e_new_evar sigma env ev in
let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
evars := Gmap.add id rev !evars;
@@ -1824,5 +1824,5 @@ let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_
let j = understand_judgment_tcc evdref env gc in
j, Evd.universe_context_set !evdref) ~global_level ~impl_env !evdref env params
in
- let _ = evdref := Evd.merge_context_set !evdref ctx in
+ let _ = evdref := Evd.merge_context_set true !evdref ctx in
int_env, ((env, par), impls)
View
@@ -240,7 +240,7 @@ type vernac_expr =
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
| VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
- | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of polymorphic * inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list
| VernacScheme of (lident option * scheme) list
View
@@ -42,7 +42,14 @@ type my_global_reference =
| IndRef of inductive
| ConstructRef of constructor
-let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)
+let instantiate_my_gr gr u =
+ match gr with
+ | ConstRef c -> mkConstU (c, u)
+ | IndRef i -> mkIndU (i, u)
+ | ConstructRef c -> mkConstructU (c, u)
+
+let cache = (Hashtbl.create 13 :
+ (my_global_reference, my_global_reference * constr array) Hashtbl.t)
let clear_cooking_sharing () = Hashtbl.clear cache
@@ -52,24 +59,27 @@ let share r (cstl,knl) =
let f,l =
match r with
| IndRef (kn,i) ->
- mkInd (pop_mind kn,i), Mindmap.find kn knl
+ IndRef (pop_mind kn,i), Mindmap.find kn knl
| ConstructRef ((kn,i),j) ->
- mkConstruct ((pop_mind kn,i),j), Mindmap.find kn knl
+ ConstructRef ((pop_mind kn,i),j), Mindmap.find kn knl
| ConstRef cst ->
- mkConst (pop_con cst), Cmap.find cst cstl in
- let c = mkApp (f, Array.map mkVar l) in
+ ConstRef (pop_con cst), Cmap.find cst cstl in
+ let c = (f, Array.map mkVar l) in
Hashtbl.add cache r c;
(* has raised Not_found if not in work_list *)
c
+let share_univs r u cache =
+ let r', args = share r cache in
+ mkApp (instantiate_my_gr r' u, args)
+
let update_case_info ci modlist =
try
let ind, n =
- match kind_of_term (share (IndRef ci.ci_ind) modlist) with
- | App (f,l) -> (destInd f, Array.length l)
- | Ind ind -> ind, 0
+ match share (IndRef ci.ci_ind) modlist with
+ | (IndRef f,l) -> (f, Array.length l)
| _ -> assert false in
- { ci with ci_ind = fst ind; ci_npar = ci.ci_npar + n }
+ { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
with Not_found ->
ci
@@ -86,19 +96,19 @@ let expmod_constr modlist c =
| Ind (ind,u) ->
(try
- share (IndRef ind) modlist
+ share_univs (IndRef ind) u modlist
with
| Not_found -> map_constr substrec c)
| Construct (cstr,u) ->
(try
- share (ConstructRef cstr) modlist
+ share_univs (ConstructRef cstr) u modlist
with
| Not_found -> map_constr substrec c)
| Const (cst,u) ->
(try
- share (ConstRef cst) modlist
+ share_univs (ConstRef cst) u modlist
with
| Not_found -> map_constr substrec c)
View
@@ -251,8 +251,8 @@ let typecheck_inductive env ctx mie =
(* conclusions of the parameters *)
(* We enforce [u >= lev] in case [lev] has a strict upper *)
(* constraints over [u] *)
- (* let arity = mkArity (sign, Type lev) in *)
- (info,full_arity,s), enforce_leq lev u cst
+ let arity = mkArity (sign, Type lev) in
+ (info,arity,Type lev), enforce_leq lev u cst
| Type u (* Not an explicit occurrence of Type *) ->
(info,full_arity,s), enforce_leq lev u cst
| Prop Pos when not (is_impredicative_set env) ->
View
@@ -459,11 +459,12 @@ let check_eq g u v =
let check_leq g u v =
match u,v with
- | Atom ul, Atom vl -> check_smaller g false ul vl
- | Max(le,lt), Atom vl ->
- List.for_all (fun ul -> check_smaller g false ul vl) le &&
- List.for_all (fun ul -> check_smaller g true ul vl) lt
- | _ -> anomaly "check_leq"
+ | Atom UniverseLevel.Prop, v -> true
+ | Atom ul, Atom vl -> check_smaller g false ul vl
+ | Max(le,lt), Atom vl ->
+ List.for_all (fun ul -> check_smaller g false ul vl) le &&
+ List.for_all (fun ul -> check_smaller g true ul vl) lt
+ | _ -> anomaly "check_leq"
(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
@@ -677,7 +678,10 @@ let constraints_depend cstr us =
let remove_dangling_constraints dangling cst =
Constraint.fold (fun (l,d,r as cstr) cst' ->
if List.mem l dangling || List.mem r dangling then cst'
- else Constraint.add cstr cst') cst Constraint.empty
+ else
+ (** Unnecessary constraints Prop <= u *)
+ if l = UniverseLevel.Prop && d = Le then cst'
+ else Constraint.add cstr cst') cst Constraint.empty
let check_context_subset (univs, cst) (univs', cst') =
let newunivs, dangling = List.partition (fun u -> UniverseLSet.mem u univs) univs' in
@@ -713,6 +717,17 @@ let subst_univs_level subst l =
try List.assoc l subst
with Not_found -> l
+let rec normalize_univ x =
+ match x with
+ | Atom _ -> x
+ | Max ([],[]) -> Atom UniverseLevel.Prop
+ | Max ([u],[]) -> Atom u
+ | Max (gel, gtl) ->
+ let gel' = CList.uniquize gel in
+ let gtl' = CList.uniquize gtl in
+ if gel' == gel && gtl' == gtl then x
+ else normalize_univ (Max (gel', gtl'))
+
let subst_univs_universe subst u =
match u with
| Atom a ->
@@ -722,7 +737,7 @@ let subst_univs_universe subst u =
let gel' = CList.smartmap (subst_univs_level subst) gel in
let gtl' = CList.smartmap (subst_univs_level subst) gtl in
if gel == gel' && gtl == gtl' then u
- else Max (gel', gtl')
+ else normalize_univ (Max (gel', gtl'))
let subst_univs_constraint subst (u,d,v) =
(subst_univs_level subst u, d, subst_univs_level subst v)
@@ -747,7 +762,7 @@ type constraint_function =
let constraint_add_leq v u c =
(* We just discard trivial constraints like Set<=u or u<=u *)
- if UniverseLevel.equal v UniverseLevel.Set || UniverseLevel.equal v u then c
+ if UniverseLevel.equal v UniverseLevel.Prop || UniverseLevel.equal v u then c
else Constraint.add (v,Le,u) c
let enforce_leq u v c =
View
@@ -564,14 +564,14 @@ let rec find_map f = function
let uniquize l =
let visited = Hashtbl.create 23 in
- let rec aux acc = function
- | h::t -> if Hashtbl.mem visited h then aux acc t else
+ let rec aux acc changed = function
+ | h::t -> if Hashtbl.mem visited h then aux acc true t else
begin
Hashtbl.add visited h h;
- aux (h::acc) t
+ aux (h::acc) changed t
end
- | [] -> List.rev acc
- in aux [] l
+ | [] -> if changed then List.rev acc else l
+ in aux [] false l
let distinct l =
let visited = Hashtbl.create 23 in
View
@@ -165,7 +165,8 @@ sig
there is none. *)
val uniquize : 'a list -> 'a list
- (** Return the list of elements without duplicates. *)
+ (** Return the list of elements without duplicates.
+ This is the list unchanged if there was none. *)
val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
(** Merge two sorted lists and preserves the uniqueness property. *)
View
@@ -138,34 +138,128 @@ let new_global_univ () =
module LevelUnionFind = Unionfind.Make (Univ.UniverseLSet) (Univ.UniverseLMap)
let remove_trivial_constraints cst =
- Univ.Constraint.fold (fun (l,d,r as cstr) nontriv ->
- if d <> Univ.Lt && Univ.eq_levels l r then nontriv
- else Univ.Constraint.add cstr nontriv)
- cst Univ.empty_constraint
+ Constraint.fold (fun (l,d,r as cstr) nontriv ->
+ if d <> Lt && eq_levels l r then nontriv
+ else Constraint.add cstr nontriv)
+ cst empty_constraint
-let normalize_context_set (ctx, csts) =
- let module UF = LevelUnionFind in
+let add_list_map u t map =
+ let l, d, r = UniverseLMap.split u map in
+ let d' = match d with None -> [t] | Some l -> t :: l in
+ let lr =
+ UniverseLMap.merge (fun k lm rm ->
+ if d = None && eq_levels k u then Some d'
+ else
+ match lm with Some t -> lm | None ->
+ match rm with Some t -> rm | None -> None) l r
+ in
+ if d = None then UniverseLMap.add u d' lr
+ else lr
+
+let find_list_map u map =
+ try UniverseLMap.find u map with Not_found -> []
+
+module UF = LevelUnionFind
+
+let instantiate_univ_variables uf ucstrsl ucstrsr u (subst, cstrs) =
+ try
+ (** The universe variable is already at a fixed level.
+ Simply produce the instantiated constraints. *)
+ let canon = UF.find u uf in
+ let cstrs =
+ let l = find_list_map u ucstrsl in
+ List.fold_left (fun cstrs (d, r) -> Constraint.add (canon, d, r) cstrs)
+ cstrs l
+ in
+ let cstrs =
+ let l = find_list_map u ucstrsr in
+ List.fold_left (fun cstrs (d, l) -> Constraint.add (l, d, canon) cstrs)
+ cstrs l
+ in (subst, cstrs)
+ with Not_found ->
+ (** The universe variable was not fixed yet.
+ Compute its level using its lower bound and generate
+ the upper bound constraints *)
+ let lbound =
+ try
+ let r = UniverseLMap.find u ucstrsr in
+ let lbound = List.fold_left (fun lbound (d, l) ->
+ if d = Le (* l <= ?u *) then (sup (Universe.make l) lbound)
+ else (* l < ?u *) (assert (d = Lt); (sup (super (Universe.make l)) lbound)))
+ type0m_univ r
+ in Some lbound
+ with Not_found ->
+ (** No lower bound, choose the minimal level according to the
+ upper bounds (greatest lower bound), if any.
+ *)
+ None
+ in
+ let uinst, cstrs =
+ try
+ let l = UniverseLMap.find u ucstrsl in
+ let lbound =
+ match lbound with
+ | None -> Universe.make u (** No lower bounds but some upper bounds, u has to stay *)
+ | Some lbound -> lbound
+ in
+ let cstrs =
+ List.fold_left (fun cstr (d,r) ->
+ if d = Le (* ?u <= r *) then enforce_leq lbound (Universe.make r) cstr
+ else (* ?u < r *) enforce_leq (super lbound) (Universe.make r) cstr)
+ cstrs l
+ in Some lbound, cstrs
+ with Not_found -> lbound, cstrs
+ in
+ let subst' =
+ match uinst with
+ | None -> subst
+ | Some uinst -> ((u, uinst) :: subst)
+ in (subst', cstrs)
+
+let normalize_context_set (ctx, csts) us =
let uf = UF.create () in
- let noneqs =
- Univ.Constraint.fold (fun (l,d,r as cstr) noneq ->
- if d = Univ.Eq then (UF.union l r uf; noneq) else
- (Univ.Constraint.add cstr noneq)) csts Univ.empty_constraint
+ let noneqs, ucstrsl, ucstrsr =
+ Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
+ if d = Eq then (UF.union l r uf; (noneq, ucstrsl, ucstrsr)) else
+ let lus = UniverseLSet.mem l us
+ and rus = UniverseLSet.mem r us
+ in
+ let ucstrsl' =
+ if lus then add_list_map l (d, r) ucstrsl
+ else ucstrsl
+ and ucstrsr' =
+ if rus then add_list_map r (d, l) ucstrsr
+ else ucstrsr
+ in
+ let noneqs =
+ if lus || rus then noneq
+ else Constraint.add cstr noneq
+ in (noneqs, ucstrsl', ucstrsr'))
+ csts (empty_constraint, UniverseLMap.empty, UniverseLMap.empty)
in
let partition = UF.partition uf in
let ctx', pcanons = List.fold_left (fun (ctx, canons) s ->
- let canon = Univ.UniverseLSet.max_elt s in
- let rest = Univ.UniverseLSet.remove canon s in
- let ctx' = Univ.UniverseLSet.diff ctx rest in
- let canons' = (canon, Univ.UniverseLSet.elements rest) :: canons in
+ let canon = UniverseLSet.max_elt s in
+ let rest = UniverseLSet.remove canon s in
+ let ctx' = UniverseLSet.diff ctx rest in
+ let canons' = (canon, UniverseLSet.elements rest) :: canons in
(ctx', canons'))
(ctx, []) partition
in
let subst = List.concat (List.rev_map (fun (c, rs) ->
List.rev_map (fun r -> (r, c)) rs) pcanons) in
+ let ussubst, noneqs =
+ UniverseLSet.fold (instantiate_univ_variables uf ucstrsl ucstrsr)
+ us ([], noneqs)
+ in
+ let ctx', subst =
+ List.fold_left (fun (ctx', subst') (u, us) ->
+ match universe_level us with
+ | Some u' -> (UniverseLSet.remove u ctx', (u, u') :: subst')
+ | None -> (** Couldn't find a level, keep the universe *)
+ (ctx', subst'))
+ (ctx, subst) ussubst
+ in
let constraints = remove_trivial_constraints
- (Univ.subst_univs_constraints subst noneqs)
+ (subst_univs_constraints subst noneqs)
in (subst, (ctx', constraints))
-
-(* let normalize_constraints ({evars = (sigma, (us, sm))} as d) = *)
-(* let (ctx', us') = normalize_context_set us in *)
-(* {d with evars = (sigma, (us', sm))} *)
View
@@ -51,12 +51,30 @@ val extend_context : 'a in_universe_context_set -> universe_context_set ->
'a in_universe_context_set
(** Simplification and pruning of constraints:
-
- Normalizes the context w.r.t. equality constraints,
- choosing a canonical universe in each equivalence class and
- transitively saturating the constraints w.r.t to it. *)
+ [normalize_context_set ctx us]
-val normalize_context_set : universe_context_set -> universe_subst in_universe_context_set
+ - Instantiate the variables in [us] with their most precise
+ universe levels respecting the constraints.
+
+ - Normalizes the context [ctx] w.r.t. equality constraints,
+ choosing a canonical universe in each equivalence class
+ (a global one if there is one) and transitively saturate
+ the constraints w.r.t to the equalities. *)
+
+module UF : Unionfind.PartitionSig
+
+val instantiate_univ_variables :
+ UF.t ->
+ (Univ.constraint_type * Univ.universe_level) list
+ Univ.UniverseLMap.t ->
+ (Univ.constraint_type * Univ.universe_level) list
+ Univ.UniverseLMap.t ->
+ UF.elt ->
+ (UF.elt * Univ.universe) list * Univ.constraints ->
+ (UF.elt * Univ.universe) list * Univ.constraints
+
+
+val normalize_context_set : universe_context_set -> universe_set -> universe_subst in_universe_context_set
(** Create a fresh global in the global environment, shouldn't be done while
Oops, something went wrong.

0 comments on commit 96829d0

Please sign in to comment.