diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 26 | ||||
| -rw-r--r-- | vernac/declareUniv.ml | 60 | ||||
| -rw-r--r-- | vernac/declareUniv.mli | 9 |
3 files changed, 76 insertions, 19 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 848cd501c6..792f07bb89 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -165,6 +165,28 @@ let label_of = let open GlobRef in function | ConstructRef ((kn,_),_) -> MutInd.label kn | VarRef id -> Label.of_id id +let fold_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_,c) -> f n acc c + | Evar (_,l) -> List.fold_left (f n) acc l + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty + let rec traverse current ctx accu t = let open GlobRef in match Constr.kind t with @@ -189,10 +211,10 @@ let rec traverse current ctx accu t = traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> - Constr.fold_with_full_binders + fold_with_full_binders Context.Rel.add (traverse current) ctx accu t end -| _ -> Constr.fold_with_full_binders +| _ -> fold_with_full_binders Context.Rel.add (traverse current) ctx accu t and traverse_object ?inhabits (curr, data, ax2ty) body obj = diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 1987d48e0f..834ef0d29a 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -9,6 +9,8 @@ (************************************************************************) open Names +open Declarations +open Univ (* object_kind , id *) exception AlreadyDeclared of (string option * Id.t) @@ -72,23 +74,51 @@ let input_univ_names : universe_name_decl -> Libobject.obj = subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } +let invent_name (named,cnt) u = + let rec aux i = + let na = Id.of_string ("u"^(string_of_int i)) in + if Id.Map.mem na named then aux (i+1) + else na, (Id.Map.add na u named, i+1) + in + aux cnt + +let label_and_univs_of = let open GlobRef in function + | ConstRef c -> + let l = Label.to_id @@ Constant.label c in + let univs = (Global.lookup_constant c).const_universes in + l, univs + | IndRef (c,_) -> + let l = Label.to_id @@ MutInd.label c in + let univs = (Global.lookup_mind c).mind_universes in + l, univs + | VarRef id -> + CErrors.anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | ConstructRef _ -> + CErrors.anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on a constructor reference") + let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = let open GlobRef in match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> - CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on a constructor reference") + let l, univs = label_and_univs_of gr in + match univs with + | Polymorphic _ -> () + | Monomorphic (levels,_) -> + (* First the explicitly named universes *) + let named, univs = Id.Map.fold (fun id univ (named,univs) -> + let univs = match Univ.Level.name univ with + | None -> assert false (* having Prop/Set/Var as binders is nonsense *) + | Some univ -> (id,univ)::univs + in + let named = LSet.add univ named in + named, univs) + pl (LSet.empty,[]) in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] + (* then invent names for the rest *) + let _, univs = LSet.fold (fun univ (aux,univs) -> + let id, aux = invent_name aux univ in + let univ = Option.get (Level.name univ) in + aux, (id,univ) :: univs) + (LSet.diff levels named) ((pl,0),univs) in Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index ca990a58eb..a7e942be5a 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -10,11 +10,16 @@ open Names -(* object_kind , id *) +(** Also used by [Declare] for constants, [DeclareInd] for inductives, etc. + Containts [object_kind , id]. *) exception AlreadyDeclared of (string option * Id.t) -(** Global universe contexts, names and constraints *) +(** Internally used to declare names of universes from monomorphic + constants/inductives. Noop on polymorphic references. *) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit +(** Command [Universes]. *) val do_universe : poly:bool -> lident list -> unit + +(** Command [Constraint]. *) val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit |