From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 31 Mar 2018 17:43:18 +0200 Subject: Evar maps contain econstrs. We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. --- pretyping/unification.ml | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ca03b96ab..d98ce9aba 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -84,7 +84,7 @@ let occur_meta_or_undefined_evar evd c = | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with | Evar_defined c -> - occrec c; Array.iter occrec args + occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args | Evar_empty -> raise Occur) | _ -> Constr.iter occrec c in try occrec c; false with Occur | Not_found -> true @@ -189,10 +189,9 @@ let pose_all_metas_as_evars env evd t = let rec aux t = match EConstr.kind !evdref t with | Meta mv -> (match Evd.meta_opt_fvalue !evdref mv with - | Some ({rebus=c},_) -> EConstr.of_constr c + | Some ({rebus=c},_) -> c | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in - let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let ty = if Flags.version_strictly_greater Flags.V8_6 @@ -200,7 +199,7 @@ let pose_all_metas_as_evars env evd t = else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar env evdref ~src ty in - evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref; + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) | _ -> EConstr.map !evdref aux t in @@ -1060,7 +1059,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (evd,t2::ks, m-1) else let mv = new_meta () in - let evd' = meta_declare mv (EConstr.Unsafe.to_constr (substl ks b)) evd in + let evd' = meta_declare mv (substl ks b) evd in (evd', mkMeta mv :: ks, m - 1)) (sigma,[],List.length bs) bs in @@ -1247,7 +1246,7 @@ let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in - let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in + let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in (evd',j'.uj_val) let w_coerce_to_type env evd c cty mvty = @@ -1359,11 +1358,11 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = if meta_defined evd mv then let {rebus=c'},(status',_) = meta_fvalue evd mv in let (take_left,st,(evd,metas',evars')) = - merge_instances env evd flags status' status (EConstr.of_constr c') c + merge_instances env evd flags status' status c' c in let evd' = if take_left then evd - else meta_reassign mv (EConstr.Unsafe.to_constr c,(st,TypeProcessed)) evd + else meta_reassign mv (c,(st,TypeProcessed)) evd in w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns else @@ -1372,7 +1371,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = if isMetaOf evd mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else - meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in + meta_assign mv (c,(status,TypeProcessed)) evd in w_merge_rec evd' (metas''@metas) evars'' eqns | [] -> (* Process type eqns *) @@ -1396,17 +1395,17 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags - (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in + (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' - then Evd.define sp (EConstr.Unsafe.to_constr c) evd''' - else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in + then Evd.define sp c evd''' + else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in let check_types evd = let metas = Evd.meta_list evd in let eqns = List.fold_left (fun acc (mv, b) -> match b with - | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, EConstr.of_constr t.rebus) :: acc + | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc | _ -> acc) [] metas in w_merge_rec evd [] [] eqns in @@ -1417,11 +1416,6 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = in if with_types then check_types res else res -let retract_coercible_metas evd = - let (metas, evd) = retract_coercible_metas evd in - let map (mv, c, st) = (mv, EConstr.of_constr c, st) in - (List.map map metas, evd) - let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in w_merge env true flags.merge_unify_flags (evd,metas,[]) -- cgit v1.2.3