Skip to content
Browse files

- Fix generalize tactic

- add ppuniverse_subst
- Start fixing normalize_universe_context w.r.t. normalize_univ_variables.
  • Loading branch information...
1 parent c1f69eb commit 61af86cfa0d0b36706b2c9bc1bae5c0d14ec9331 @mattam82 mattam82 committed
View
1 dev/include
@@ -39,6 +39,7 @@
#install_printer (* univ context set *) ppuniverse_context_set;;
#install_printer (* univ set *) ppuniverse_set;;
#install_printer (* univ list *) ppuniverse_list;;
+#install_printer (* univ subst *) ppuniverse_subst;;
#install_printer (* univ full subst *) ppuniverse_full_subst;;
#install_printer (* univ opt subst *) ppuniverse_opt_subst;;
#install_printer (* evar univ ctx *) ppevar_universe_context;;
View
1 dev/top_printers.ml
@@ -145,6 +145,7 @@ let ppuniverse_set l = pp (LSet.pr l)
let ppuniverse_list l = pp (pr_universe_list l)
let ppuniverse_context l = pp (pr_universe_context l)
let ppuniverse_context_set l = pp (pr_universe_context_set l)
+let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
let ppuniverse_full_subst l = pp (Univ.pr_universe_full_subst l)
let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l)
View
3 kernel/univ.ml
@@ -747,6 +747,9 @@ let pr_universe_context_set (ctx, cst) =
let pr_universe_full_subst =
LMap.pr (fun u -> str" := " ++ Universe.pr u ++ spc ())
+let pr_universe_subst =
+ LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ())
+
(** Constraints *)
let empty_constraint = Constraint.empty
let is_empty_constraint = Constraint.is_empty
View
1 kernel/univ.mli
@@ -291,6 +291,7 @@ val pr_constraints : constraints -> Pp.std_ppcmds
val pr_universe_list : universe_list -> Pp.std_ppcmds
val pr_universe_context : universe_context -> Pp.std_ppcmds
val pr_universe_context_set : universe_context_set -> Pp.std_ppcmds
+val pr_universe_subst : universe_subst -> Pp.std_ppcmds
val pr_universe_full_subst : universe_full_subst -> Pp.std_ppcmds
(** {6 Dumping to a file } *)
View
3 library/universes.ml
@@ -284,7 +284,7 @@ let simplify_max_expressions csts subst =
let subst_univs_subst u l s =
LMap.add u l s
-let normalize_context_set (ctx, csts) us algs =
+let normalize_context_set (ctx, csts) substdef us algs =
let uf = UF.create () in
let noneqs =
Constraint.fold (fun (l,d,r as cstr) noneqs ->
@@ -382,6 +382,7 @@ let normalize_context_set (ctx, csts) us algs =
let usalg, usnonalg =
List.partition (fun (u, _) -> LSet.mem u algs) ussubst
in
+ let subst = LMap.union substdef subst in
let subst =
LMap.union (Univ.LMap.of_list usalg)
(LMap.fold (fun u v acc ->
View
1 library/universes.mli
@@ -78,6 +78,7 @@ val choose_canonical : universe_set -> universe_set -> universe_set ->
val normalize_context_set : universe_context_set ->
+ universe_subst (* Substitution for the defined variables *) ->
universe_set (* univ variables *) ->
universe_set (* univ variables that can be substituted by algebraics *) ->
universe_full_subst in_universe_context_set
View
9 pretyping/evd.ml
@@ -844,11 +844,11 @@ let normalize_evar_universe_context_variables uctx =
let ctx_local = subst_univs_context_with_def def subst uctx.uctx_local in
subst, { uctx with uctx_local = ctx_local; uctx_univ_variables = normalized_variables }
-let normalize_evar_universe_context uctx =
+let normalize_evar_universe_context uctx subst =
let undef, _ = Univ.LMap.partition (fun i b -> b = None) uctx.uctx_univ_variables in
let undef = Univ.LMap.universes undef in
let (subst', us') =
- Universes.normalize_context_set uctx.uctx_local undef
+ Universes.normalize_context_set uctx.uctx_local subst undef
uctx.uctx_univ_algebraic
in
let uctx' = { uctx with uctx_local = us'; uctx_univ_variables = Univ.LMap.empty } in
@@ -865,10 +865,9 @@ let normalize_univ_level fullsubst u =
let nf_constraints ({evars = (sigma, uctx)} as d) =
let subst, uctx' = normalize_evar_universe_context_variables uctx in
- let subst', uctx' = normalize_evar_universe_context uctx' in
+ let subst', uctx' = normalize_evar_universe_context uctx' subst in
let evd' = {d with evars = (sigma, uctx')} in
- let subst'' = Univ.LMap.map (normalize_univ_level subst') subst in
- evd', Univ.LMap.union subst' subst''
+ evd', subst'
(* Conversion w.r.t. an evar map and its local universes. *)
View
2 pretyping/evd.mli
@@ -270,7 +270,7 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context
val add_constraints_context : evar_universe_context ->
Univ.constraints -> evar_universe_context
-val normalize_evar_universe_context : evar_universe_context ->
+val normalize_evar_universe_context : evar_universe_context -> Univ.universe_subst ->
Univ.universe_full_subst in_evar_universe_context
val new_univ_variable : rigid -> evar_map -> evar_map * Univ.universe
View
2 pretyping/termops.ml
@@ -550,7 +550,7 @@ let collect_vars c =
[m] is appropriately lifted through abstractions of [t] *)
let dependent_main noevar univs m t =
- let eqc x y = if univs then fst (eq_constr_univs x y) else eq_constr x y in
+ let eqc x y = if univs then fst (eq_constr_univs x y) else eq_constr_nounivs x y in
let rec deprec m t =
if eqc m t then
raise Occur
View
3 proofs/refiner.ml
@@ -391,6 +391,9 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
let tclPUSHCONTEXT rigid ctx tac gl =
tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl
+let tclPUSHCONSTRAINTS cst gl =
+ tclEVARS (Evd.add_constraints (project gl) cst) gl
+
(* Pretty-printers. *)
let pp_info = ref (fun _ _ _ -> assert false)
View
2 proofs/refiner.mli
@@ -42,6 +42,8 @@ val tclEVARS : evar_map -> tactic
val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
+val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
+
(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
val tclTHEN : tactic -> tactic -> tactic
View
26 tactics/tactics.ml
@@ -1530,14 +1530,14 @@ let generalized_name c t ids cl = function
constante dont on aurait pu prendre directement le nom *)
named_hd (Global.env()) t Anonymous
-let generalize_goal gl i ((occs,c,b),na) cl =
+let generalize_goal gl i ((occs,c,b),na) (cl,cst) =
let t = pf_type_of gl c in
let decls,cl = decompose_prod_n_assum i cl in
let dummy_prod = it_mkProd_or_LetIn mkProp decls in
- let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in
- let cl' = subst_closed_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in
+ let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in
+ let cl',cst' = subst_closed_term_univs_occ occs c (it_mkProd_or_LetIn cl newdecls) in
let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
- mkProd_or_LetIn (na,b,t) cl'
+ mkProd_or_LetIn (na,b,t) cl', Univ.Constraint.union cst cst'
let generalize_dep ?(with_let=false) c gl =
let env = pf_env gl in
@@ -1567,18 +1567,20 @@ let generalize_dep ?(with_let=false) c gl =
| _ -> None
else None
in
- let cl'' = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) cl' in
+ let cl'',cst = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',Univ.empty_constraint) in
let args = Array.to_list (instance_from_named_context to_quantify_rev) in
- tclTHEN
- (apply_type cl'' (if Option.is_empty body then c::args else args))
- (thin (List.rev tothin'))
+ tclTHENLIST
+ [tclPUSHCONSTRAINTS cst;
+ apply_type cl'' (if Option.is_empty body then c::args else args);
+ thin (List.rev tothin')]
gl
let generalize_gen_let lconstr gl =
- let newcl =
- List.fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
- apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
- if Option.is_empty b then Some c else None) lconstr) gl
+ let newcl,cst =
+ List.fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl,Univ.empty_constraint) in
+ tclTHEN (tclPUSHCONSTRAINTS cst)
+ (apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
+ if Option.is_empty b then Some c else None) lconstr)) gl
let generalize_gen lconstr =
generalize_gen_let (List.map (fun ((occs,c),na) ->
View
2 toplevel/ind_tables.ml
@@ -125,7 +125,7 @@ let compute_name internal id =
let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
- let subst, ctx = Evd.normalize_evar_universe_context univs in
+ let subst, ctx = Evd.normalize_evar_universe_context univs Univ.LMap.empty in
let c = Universes.subst_univs_full_constr subst c in
let kn = fd id
(DefinitionEntry

0 comments on commit 61af86c

Please sign in to comment.
Something went wrong with that request. Please try again.