diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 173 |
1 files changed, 92 insertions, 81 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4084ee579..a97e248ae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -7,11 +7,10 @@ (************************************************************************) open Util -open Errors +open CErrors open Names open Term open Vars -open Context open Environ open Termops open Evd @@ -20,6 +19,7 @@ open Retyping open Reductionops open Evarutil open Pretype_errors +open Sigma.Notations let normalize_evar evd ev = match kind_of_term (whd_evar evd (mkEvar ev)) with @@ -85,7 +85,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () - | _ -> iter_constr (refresh_term_evars onevars false) t + | _ -> Constr.iter (refresh_term_evars onevars false) t and refresh_polymorphic_positions args pos = let rec aux i = function | Some l :: ls -> @@ -145,7 +145,7 @@ let recheck_applications conv_algo env evdref t = let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in let rec aux i ty = if i < Array.length argsty then - match kind_of_term (whd_betadeltaiota env !evdref ty) with + match kind_of_term (whd_all env !evdref ty) with | Prod (na, dom, codom) -> (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; @@ -168,7 +168,8 @@ type 'a update = | UpdateWith of 'a | NoUpdate -let inst_of_vars sign = Array.map_of_list (fun (id,_,_) -> mkVar id) sign +open Context.Named.Declaration +let inst_of_vars sign = Array.map_of_list (mkVar % get_id) sign let restrict_evar_key evd evk filter candidates = match filter, candidates with @@ -186,7 +187,9 @@ let restrict_evar_key evd evk filter candidates = let candidates = match candidates with | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in - restrict_evar evd evk filter candidates + let sigma = Sigma.Unsafe.of_evar_map evd in + let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in + (Sigma.to_evar_map sigma, evk) end (* Restrict an applied evar and returns its restriction in the same context *) @@ -211,6 +214,7 @@ let restrict_instance evd evk filter argsv = let evi = Evd.find evd evk in Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv +open Context.Rel.Declaration let noccur_evar env evd evk c = let cache = ref Int.Set.empty (* cache for let-ins *) in let rec occur_rec check_types (k, env as acc) c = @@ -227,10 +231,10 @@ let noccur_evar env evd evk c = if not (Int.Set.mem (i-k) !cache) then let decl = Environ.lookup_rel i env in if check_types then - (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (pi3 decl))); - (match pi2 decl with - | None -> () - | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b)) + (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (get_type decl))); + (match decl with + | LocalAssum _ -> () + | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b)) | Proj (p,c) -> occur_rec true acc c | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) (occur_rec check_types) acc c @@ -246,9 +250,11 @@ let noccur_evar env evd evk c = variable in its family of aliased variables *) let compute_var_aliases sign = - List.fold_right (fun (id,b,c) aliases -> - match b with - | Some t -> + let open Context.Named.Declaration in + List.fold_right (fun decl aliases -> + let id = get_id decl in + match decl with + | LocalDef (_,t,_) -> (match kind_of_term t with | Var id' -> let aliases_of_id = @@ -256,27 +262,30 @@ let compute_var_aliases sign = Id.Map.add id (aliases_of_id@[t]) aliases | _ -> Id.Map.add id [t] aliases) - | None -> aliases) + | LocalAssum _ -> aliases) sign Id.Map.empty let compute_rel_aliases var_aliases rels = - snd (List.fold_right (fun (_,b,u) (n,aliases) -> - (n-1, - match b with - | Some t -> - (match kind_of_term t with - | Var id' -> - let aliases_of_n = - try Id.Map.find id' var_aliases with Not_found -> [] in - Int.Map.add n (aliases_of_n@[t]) aliases - | Rel p -> - let aliases_of_n = - try Int.Map.find (p+n) aliases with Not_found -> [] in - Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases - | _ -> - Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases) - | None -> aliases)) - rels (List.length rels,Int.Map.empty)) + snd (List.fold_right + (fun decl (n,aliases) -> + (n-1, + match decl with + | LocalDef (_,t,u) -> + (match kind_of_term t with + | Var id' -> + let aliases_of_n = + try Id.Map.find id' var_aliases with Not_found -> [] in + Int.Map.add n (aliases_of_n@[t]) aliases + | Rel p -> + let aliases_of_n = + try Int.Map.find (p+n) aliases with Not_found -> [] in + Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases + | _ -> + Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases) + | LocalAssum _ -> aliases) + ) + rels + (List.length rels,Int.Map.empty)) let make_alias_map env = (* We compute the chain of aliases for each var and rel *) @@ -310,13 +319,13 @@ let normalize_alias aliases x = let normalize_alias_var var_aliases id = destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id)) -let extend_alias (_,b,_) (var_aliases,rel_aliases) = +let extend_alias decl (var_aliases,rel_aliases) = let rel_aliases = Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l)) rel_aliases Int.Map.empty in let rel_aliases = - match b with - | Some t -> + match decl with + | LocalDef(_,t,_) -> (match kind_of_term t with | Var id' -> let aliases_of_binder = @@ -328,7 +337,7 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) = Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases | _ -> Int.Map.add 1 [lift 1 t] rel_aliases) - | None -> rel_aliases in + | LocalAssum _ -> rel_aliases in (var_aliases, rel_aliases) let expand_alias_once aliases x = @@ -434,16 +443,17 @@ let get_actual_deps aliases l t = | Rel n -> Int.Set.mem n fv_rels | _ -> assert false) l +open Context.Named.Declaration let remove_instance_local_defs evd evk args = let evi = Evd.find evd evk in let len = Array.length args in let rec aux sign i = match sign with | [] -> let () = assert (i = len) in [] - | (_, None, _) :: sign -> + | LocalAssum _ :: sign -> let () = assert (i < len) in (Array.unsafe_get args i) :: aux sign (succ i) - | (_, Some _, _) :: sign -> + | LocalDef _ :: sign -> aux sign (succ i) in aux (evar_filtered_context evi) 0 @@ -505,7 +515,8 @@ let solve_pattern_eqn env l c = match kind_of_term a with (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> - let d = map_rel_declaration (lift n) (lookup_rel n env) in + let open Context.Rel.Declaration in + let d = map_constr (lift n) (lookup_rel n env) in mkLambda_or_LetIn d c' | Var id -> let d = lookup_named id env in mkNamedLambda_or_LetIn d c' @@ -513,7 +524,7 @@ let solve_pattern_eqn env l c = l c in (* Warning: we may miss some opportunity to eta-reduce more since c' is not in normal form *) - whd_eta c' + shrink_eta c' (*****************************************) (* Refining/solving unification problems *) @@ -534,9 +545,9 @@ let make_projectable_subst aliases sigma evi args = let evar_aliases = compute_var_aliases sign in let (_,full_subst,cstr_subst) = List.fold_right - (fun (id,b,c) (args,all,cstrs) -> - match b,args with - | None, a::rest -> + (fun decl (args,all,cstrs) -> + match decl,args with + | LocalAssum (id,c), a::rest -> let a = whd_evar sigma a in let cstrs = let a',args = decompose_app_vect a in @@ -546,7 +557,7 @@ let make_projectable_subst aliases sigma evi args = Constrmap.add (fst cstr) ((args,id)::l) cstrs | _ -> cstrs in (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs) - | Some c, a::rest -> + | LocalDef (id,c,_), a::rest -> let a = whd_evar sigma a in (match kind_of_term c with | Var id' -> @@ -575,7 +586,9 @@ let make_projectable_subst aliases sigma evi args = *) let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env = - let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in + let evd = Sigma.to_evar_map evd in let t_in_env = whd_evar evd t_in_env in let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in let ctxt = named_context_of_val sign in @@ -606,10 +619,12 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let sign1 = evar_hyps evi1 in let filter1 = evar_filter evi1 in let src = subterm_source evk1 evi1.evar_source in - let ids1 = List.map pi1 (named_context_of_val sign1) in + let ids1 = List.map get_id (named_context_of_val sign1) in let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in + let open Context.Rel.Declaration in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = - List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) -> + List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) -> + let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in let id = next_name_away na avoid in let evd,t_in_sign = let s = Retyping.get_sort_of env evd t_in_env in @@ -617,13 +632,13 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env in - let evd,b_in_sign = match b with - | None -> evd,None - | Some b -> + let evd,b_in_sign = match d with + | LocalAssum _ -> evd,None + | LocalDef (_,b,_) -> let evd,b = define_evar_from_virtual_equation define_fun env evd src b t_in_sign sign filter inst_in_env in evd,Some b in - (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.extend 1 filter, + (push_named_context_val (Context.Named.Declaration.of_tuple (id,b_in_sign,t_in_sign)) sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), push_rel d env,evd,id::avoid)) @@ -636,8 +651,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in - let evd,ev2_in_sign = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (ev2_in_sign, evd, _) = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in + let evd = Sigma.to_evar_map evd in let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in (evd, ev2_in_sign, ev2_in_env) @@ -761,9 +778,10 @@ let project_with_effects aliases sigma effects t subst = effects := p :: !effects; c +open Context.Named.Declaration let rec find_solution_type evarenv = function - | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv) - | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv) + | (id,ProjectVar)::l -> get_type (lookup_named id evarenv) + | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv) | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false @@ -783,7 +801,7 @@ let rec do_projection_effects define_fun env ty evd = function let evd = Evd.define evk (mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in - let ty = whd_betadeltaiota env evd (Lazy.force ty) in + let ty = whd_all env evd (Lazy.force ty) in if not (isSort ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right @@ -897,7 +915,7 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = *) let set_of_evctx l = - List.fold_left (fun s (id,_,_) -> Id.Set.add id s) Id.Set.empty l + List.fold_left (fun s decl -> Id.Set.add (get_id decl) s) Id.Set.empty l let filter_effective_candidates evi filter candidates = match filter with @@ -929,7 +947,13 @@ let closure_of_filter evd evk = function | Some filter -> let evi = Evd.find_undefined evd evk in let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in - let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in + let test b decl = b || Idset.mem (get_id decl) vars || + match decl with + | LocalAssum _ -> + false + | LocalDef (_,c,_) -> + not (isRel c || isVar c) + in let newfilter = Filter.map_along test filter (evar_context evi) in (* Now ensure that restriction is at least what is was originally *) let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in @@ -1011,21 +1035,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let are_canonical_instances args1 args2 env = - let n1 = Array.length args1 in - let n2 = Array.length args2 in - let rec aux n = function - | (id,_,c)::sign - when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) -> - aux (n+1) sign - | [] -> - let rec aux2 n = - Int.equal n n1 || - (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1)) - in aux2 n - | _ -> false in - Int.equal n1 n2 && aux 0 (named_context env) - let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in match conv_algo env evd Reduction.CONV rhs c' with @@ -1300,7 +1309,7 @@ let occur_evar_upto_types sigma n c = seen := Evar.Set.add sp !seen; Option.iter occur_rec (existential_opt_value sigma e); occur_rec (existential_type sigma e)) - | _ -> iter_constr occur_rec c + | _ -> Constr.iter occur_rec c in try occur_rec c; false with Occur -> true @@ -1385,15 +1394,16 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let t = whd_evar !evdref t in match kind_of_term t with | Rel i when i>k -> - (match pi2 (Environ.lookup_rel (i-k) env') with - | None -> project_variable (mkRel (i-k)) - | Some b -> + let open Context.Rel.Declaration in + (match Environ.lookup_rel (i-k) env' with + | LocalAssum _ -> project_variable (mkRel (i-k)) + | LocalDef (_,b,_) -> try project_variable (mkRel (i-k)) with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b)) | Var id -> - (match pi2 (Environ.lookup_named id env') with - | None -> project_variable t - | Some b -> + (match Environ.lookup_named id env' with + | LocalAssum _ -> project_variable t + | LocalDef (_,b,_) -> try project_variable t with NotInvertibleUsingOurAlgorithm _ -> imitate envk b) | LetIn (na,b,u,c) -> @@ -1454,7 +1464,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in t::l - with e when Errors.noncritical e -> l in + with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x | _ -> @@ -1473,7 +1483,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let names = ref Idset.empty in let rec is_id_subst ctxt s = match ctxt, s with - | ((id, _, _) :: ctxt'), (c :: s') -> + | (decl :: ctxt'), (c :: s') -> + let id = get_id decl in names := Idset.add id !names; isVarId id c && is_id_subst ctxt' s' | [], [] -> true @@ -1546,7 +1557,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = raise e | OccurCheckIn (evd,rhs) -> (* last chance: rhs actually reduces to ev *) - let c = whd_betadeltaiota env evd rhs in + let c = whd_all env evd rhs in match kind_of_term c with | Evar (evk',argsv2) when Evar.equal evk evk' -> solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') |