diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 2 | ||||
-rw-r--r-- | pretyping/detyping.ml | 2 | ||||
-rw-r--r-- | pretyping/detyping.mli | 4 | ||||
-rw-r--r-- | pretyping/glob_ops.ml | 2 | ||||
-rw-r--r-- | pretyping/glob_term.ml | 4 | ||||
-rw-r--r-- | pretyping/indrec.ml | 8 | ||||
-rw-r--r-- | pretyping/indrec.mli | 3 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 20 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 59 |
9 files changed, 53 insertions, 51 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0dd3c5944..93ca9dc5e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1425,7 +1425,7 @@ and match_current pb (initial,tomatch) = let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = - make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals + make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5a54c6f05..fe49d64c7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : reference -> inductive + val encode : qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 5310455fe..8695d52b1 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -87,7 +87,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -95,7 +95,7 @@ module PrintingInductiveMake : sig type t = Names.inductive val compare : t -> t -> int - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t val key : Goptions.option_name diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 11cfd2040..ba193da60 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2 | _ -> false let binding_kind_eq bk1 bk2 = match bk1, bk2 with diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 54fa5328f..86245d479 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -33,11 +33,11 @@ type 'a universe_kind = | UUnknown | UNamed of 'a -type level_info = Libnames.reference universe_kind +type level_info = Libnames.qualid universe_kind type glob_level = level_info glob_sort_gen type glob_constraint = glob_level * Univ.constraint_type * glob_level -type sort_info = (Libnames.reference * int) option list +type sort_info = (Libnames.qualid * int) option list type glob_sort = sort_info glob_sort_gen (** Casts *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 27b029aad..4ab932723 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr env 0 f (List.rev cstr.cs_args, recargs) (* Main function *) -let mis_make_indrec env sigma listdepkind mib u = +let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in @@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u = (* Body on make_one_rec *) let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in - if (mis_is_recursive_subset + if force_mutual || (mis_is_recursive_subset (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) then @@ -558,7 +558,7 @@ let check_arities env listdepkind = [] listdepkind in true -let build_mutual_induction_scheme env sigma = function +let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in if dep && not (Inductiveops.has_dependent_elim mib) then @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function lrecspec) in let _ = check_arities env listdepkind in - mis_make_indrec env sigma listdepkind mib u + mis_make_indrec env sigma ~force_mutual listdepkind mib u | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index d87a19d28..de9d3a0ab 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive -> (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list + env -> evar_map -> ?force_mutual:bool -> + (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1a790be64..1003f86c5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -356,8 +356,8 @@ let make_case_or_project env sigma indf ci pred c branches = | None -> (mkCase (ci, pred, c, branches)) | Some ps -> assert(Array.length branches == 1); + let na, ty, t = destLambda sigma pred in let () = - let _, _, t = destLambda sigma pred in let (ind, _), _ = dest_ind_family indf in let mib, _ = Inductive.lookup_mind_specif env ind in if (* dependent *) not (Vars.noccurn sigma 1 t) && @@ -368,16 +368,18 @@ let make_case_or_project env sigma indf ci pred c branches = in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in - let n, subst = + let n, len, ctx = List.fold_right - (fun decl (i, subst) -> + (fun decl (i, j, ctx) -> match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) - in Vars.substl subst br + | LocalAssum (na, ty) -> + let t = mkProj (Projection.make ps.(i) true, mkRel j) in + (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx) + | LocalDef (na, b, ty) -> + (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx)) + ctx (0, 1, []) + in + mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx) (* substitution in a signature *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9e024b1c2..57c4d363b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -171,38 +171,37 @@ let _ = (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd r = - let qid = Libnames.qualid_of_reference r in +let interp_known_universe_level evd qid = try - match r.CAst.v with - | Libnames.Ident id -> Evd.universe_of_name evd id - | Libnames.Qualid _ -> raise Not_found + let open Libnames in + if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid + else raise Not_found with Not_found -> - let univ, k = Nametab.locate_universe qid.CAst.v in + let univ, k = Nametab.locate_universe qid in Univ.Level.make univ k -let interp_universe_level_name ~anon_rigidity evd r = - try evd, interp_known_universe_level evd r +let interp_universe_level_name ~anon_rigidity evd qid = + try evd, interp_known_universe_level evd qid with Not_found -> - match r with (* Qualified generated name *) - | {CAst.loc; v=Libnames.Qualid qid} -> - let dp, i = Libnames.repr_qualid qid in - let num = - try int_of_string (Id.to_string i) - with Failure _ -> - user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) - in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *) - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:id univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ Id.print id)) + if Libnames.qualid_is_ident qid then (* Undeclared *) + let id = Libnames.qualid_basename qid in + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd + else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) + else + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in @@ -232,10 +231,10 @@ let interp_known_level_info ?loc evd = function | UUnknown | UAnonymous -> user_err ?loc ~hdr:"interp_known_level_info" (str "Anonymous universes not allowed here.") - | UNamed ref -> - try interp_known_universe_level evd ref + | UNamed qid -> + try interp_known_universe_level evd qid with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd |