diff options
Diffstat (limited to 'vernac/comInductive.ml')
-rw-r--r-- | vernac/comInductive.ml | 98 |
1 files changed, 82 insertions, 16 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index db2f16525..b93e8d9ac 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -27,9 +27,7 @@ open Impargs open Reductionops open Indtypes open Pretyping -open Evarutil open Indschemes -open Misctypes open Context.Rel.Declaration open Entries @@ -159,7 +157,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) + (EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -178,6 +176,72 @@ let is_flexible_sort evd u = | Some l -> Evd.is_flexible_level evd l | None -> false +(**********************************************************************) +(* Tools for template polymorphic inductive types *) + +(* Miscellaneous functions to remove or test local univ assumed to + occur only in the le constraints *) + +(* + Solve a system of universe constraint of the form + + u_s11, ..., u_s1p1, w1 <= u1 + ... + u_sn1, ..., u_snpn, wn <= un + +where + + - the ui (1 <= i <= n) are universe variables, + - the sjk select subsets of the ui for each equations, + - the wi are arbitrary complex universes that do not mention the ui. +*) + +let is_direct_sort_constraint s v = match s with + | Some u -> Univ.univ_level_mem u v + | None -> false + +let solve_constraints_system levels level_bounds = + let open Univ in + let levels = + Array.mapi (fun i o -> + match o with + | Some u -> + (match Universe.level u with + | Some u -> Some u + | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) + | None -> None) + levels in + let v = Array.copy level_bounds in + let nind = Array.length v in + let clos = Array.map (fun _ -> Int.Set.empty) levels in + (* First compute the transitive closure of the levels dependencies *) + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then + clos.(i) <- Int.Set.add j clos.(i); + done; + done; + let rec closure () = + let continue = ref false in + Array.iteri (fun i deps -> + let deps' = + Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps + in + if Int.Set.equal deps deps' then () + else (clos.(i) <- deps'; continue := true)) + clos; + if !continue then closure () + else () + in + closure (); + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && Int.Set.mem j clos.(i) then + (v.(i) <- Universe.sup v.(i) level_bounds.(j)); + done; + done; + v + let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> @@ -206,8 +270,8 @@ let inductive_levels env evd poly arities inds = in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) - let levels' = Universes.solve_constraints_system (Array.of_list levels) - (Array.of_list cstrs_levels) (Array.of_list min_levels) + let levels' = solve_constraints_system (Array.of_list levels) + (Array.of_list cstrs_levels) in let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> @@ -261,14 +325,14 @@ let check_param = function | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern {CAst.loc} -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in let pl = (List.hd indl).ind_univs in - let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let sigma, decl = interp_univ_decl_opt env0 pl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars env0 sigma paramsl in @@ -302,22 +366,24 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = () in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in + let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in (* Compute renewed arities *) - let sigma, nf = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in - let sigma, nf' = nf_evars_and_universes sigma in - let arities = List.map nf' arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let arities = List.map nf arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let uctx = Evd.check_univ_decl ~poly sigma decl in - List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; - Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params; + List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; + Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps) + List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) @@ -378,7 +444,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl |