diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/evarconv.ml | 14 | ||||
-rw-r--r-- | pretyping/evarsolve.ml | 107 | ||||
-rw-r--r-- | pretyping/evarsolve.mli | 2 | ||||
-rw-r--r-- | pretyping/evd.ml | 41 | ||||
-rw-r--r-- | pretyping/evd.mli | 1 |
5 files changed, 101 insertions, 64 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 44138a8ee..f756b3a4f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -651,8 +651,11 @@ let apply_on_subterm evdref f c t = let filter_possible_projections c ty ctxt args = let fv1 = free_rels c in let fv2 = collect_vars c in + let len = Array.length args in let tyvars = collect_vars ty in - List.map2 (fun (id,b,_) a -> + List.map_i (fun i (id,b,_) -> + let () = assert (i < len) in + let a = Array.unsafe_get args i in not (Option.is_empty b) || a == c || (* Here we make an approximation, for instance, we could also be *) @@ -661,7 +664,7 @@ let filter_possible_projections c ty ctxt args = isRel a && Int.Set.mem (destRel a) fv1 || isVar a && Id.Set.mem (destVar a) fv2 || Id.Set.mem id tyvars) - ctxt args + 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") let set_solve_evars f = solve_evars := f @@ -687,7 +690,6 @@ exception TypingFailed of evar_map let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = try - let args = Array.to_list args in let evi = Evd.find_undefined evd evk in let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in @@ -728,7 +730,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = set_holes evdref (apply_on_subterm evdref set_var c rhs) subst | [] -> rhs in - let subst = make_subst (ctxt,args,argoccs) in + let subst = make_subst (ctxt,Array.to_list args,argoccs) in let evdref = ref evd in let rhs = set_holes evdref rhs subst in @@ -791,7 +793,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty && List.for_all (fun a -> eq_constr a term2 || isEvar a) - (remove_instance_local_defs evd evk1 (Array.to_list args1)) -> + (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with @@ -799,7 +801,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> eq_constr a term1 || isEvar a) - (remove_instance_local_defs evd evk2 (Array.to_list args2)) -> + (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 7ae44faf8..a4fc330c6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -48,9 +48,15 @@ let extract_subfilter initial_filter refined_filter = List.filter_with initial_filter refined_filter let apply_subfilter filter subfilter = - fst (List.fold_right (fun oldb (l,filter) -> - if oldb then List.hd filter::l,List.tl filter else (false::l,filter)) - filter ([], List.rev subfilter)) + let len = Array.length subfilter in + let fold b (i, ans) = + if b then + let () = assert (0 <= i) in + (pred i, Array.unsafe_get subfilter i :: ans) + else + (i, false :: ans) + in + snd (List.fold_right fold filter (pred len, [])) (*------------------------------------* * Restricting existing evars * @@ -62,6 +68,8 @@ let rec eq_filter l1 l2 = match l1, l2 with (if h1 then h2 else not h2) && eq_filter l1 l2 | _ -> false +let inst_of_vars sign = Array.map_of_list (fun (id,_,_) -> mkVar id) sign + let restrict_evar_key evd evk filter candidates = match filter, candidates with | None, None -> evd, evk @@ -83,7 +91,7 @@ let restrict_evar_key evd evk filter candidates = let src = evi.evar_source in let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in let ctxt = List.filter_with filter (evar_context evi) in - let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in + let id_inst = inst_of_vars ctxt in Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk end @@ -317,12 +325,17 @@ let get_actual_deps aliases l t = let remove_instance_local_defs evd evk args = let evi = Evd.find evd evk in - let rec aux = function - | (_,Some _,_)::sign, a::args -> aux (sign,args) - | (_,None,_)::sign, a::args -> a::aux (sign,args) - | [], [] -> [] - | _ -> assert false in - aux (evar_filtered_context evi, args) + let len = Array.length args in + let rec aux sign i = match sign with + | [] -> + let () = assert (i = len) in [] + | (_, None _, _) :: sign -> + let () = assert (i < len) in + (Array.unsafe_get args i) :: aux sign (succ i) + | (_, Some _, _) :: sign -> + aux sign (succ i) + in + aux (evar_filtered_context evi) 0 (* Check if an applied evar "?X[args] l" is a Miller's pattern *) @@ -348,7 +361,7 @@ let is_unification_pattern_meta env nb m l t = let is_unification_pattern_evar env evd (evk,args) l t = if List.for_all (fun x -> isRel x || isVar x) l && noccur_evar env evd evk t then - let args = remove_instance_local_defs evd evk (Array.to_list args) in + let args = remove_instance_local_defs evd evk args in let n = List.length args in match find_unification_pattern_args env (args @ l) t with | Some l -> Some (List.skipn n l) @@ -455,9 +468,9 @@ let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter in let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in let t_in_env = whd_evar evd t_in_env in let evd = define_fun env evd (destEvar evar_in_env) t_in_env in - let ids = List.map pi1 (named_context_of_val sign) in - let inst_in_sign = List.map mkVar (List.filter_with filter ids) in - let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in + let ctxt = named_context_of_val sign in + let inst_in_sign = inst_of_vars (List.filter_with filter ctxt) in + let evar_in_sign = mkEvar (fst (destEvar evar_in_env), inst_in_sign) in (evd,whd_evar evd evar_in_sign) (* We have x1..xq |- ?e1 : τ and had to solve something like @@ -512,8 +525,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (evd, ev2_in_sign, ev2_in_env) let restrict_upon_filter evd evk p args = - let newfilter = List.map p args in - if List.for_all (fun id -> id) newfilter then + let newfilter = Array.map p args in + if Array.for_all (fun id -> id) newfilter then None else let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in @@ -728,17 +741,16 @@ let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_ exception NotEnoughInformationToInvert -let extract_unique_projections projs = - List.map (function - | Invertible (UniqueProjection (c,_)) -> c - | _ -> - (* For instance, there are evars with non-invertible arguments and *) - (* we cannot arbitrarily restrict these evars before knowing if there *) - (* will really be used; it can also be due to some argument *) - (* (typically a rel) that is not inversible and that cannot be *) - (* inverted either because it is needed for typing the conclusion *) - (* of the evar to project *) - raise NotEnoughInformationToInvert) projs +let extract_unique_projection = function +| Invertible (UniqueProjection (c,_)) -> c +| _ -> + (* For instance, there are evars with non-invertible arguments and *) + (* we cannot arbitrarily restrict these evars before knowing if there *) + (* will really be used; it can also be due to some argument *) + (* (typically a rel) that is not inversible and that cannot be *) + (* inverted either because it is needed for typing the conclusion *) + (* of the evar to project *) + raise NotEnoughInformationToInvert let extract_candidates sols = try @@ -750,9 +762,11 @@ let extract_candidates sols = let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = let evi = Evd.find_undefined evd evk in let subst,_ = make_projectable_subst aliases evd evi argsv in - let projs = - Array.map_to_list (invert_arg fullenv evd aliases k evk subst) args' in - Array.of_list (extract_unique_projections projs) + let invert arg = + let p = invert_arg fullenv evd aliases k evk subst arg in + extract_unique_projection p + in + Array.map invert args' (* Redefines an evar with a smaller context (i.e. it may depend on less * variables) such that c becomes closed. @@ -837,7 +851,7 @@ let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs = (* arbitrary complex term *) (fun a -> not (isRel a || isVar a) || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols) - (Array.to_list argsv) in + argsv in let filter = closure_of_filter evd evk filter in let candidates = extract_candidates sols in match candidates with @@ -899,7 +913,7 @@ let are_canonical_instances args1 args2 env = 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 (evar_filtered_context evi) c args in + let c' = instantiate_evar_array (evar_filtered_context evi) c args in match conv_algo env evd Reduction.CONV rhs c' with | Success evd -> Some (c,evd) | UnifFailure _ -> None @@ -915,12 +929,10 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = | _, None -> cand1 | None, Some _ -> raise DoesNotPreserveCandidateRestriction | Some l1, Some l2 -> - let args1 = Array.to_list argsv1 in - let args2 = Array.to_list argsv2 in let l1' = List.filter (fun c1 -> - let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in + let c1' = instantiate_evar_array (evar_filtered_context evi1) c1 argsv1 in let filter c2 = - let compatibility = filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2 in + let compatibility = filter_compatible_candidates conv_algo env evd evi2 argsv2 c1' c2 in match compatibility with | None -> false | Some _ -> true @@ -971,14 +983,12 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= let filter1 = - restrict_upon_filter evd evk1 (noccur_evar env evd evk2) - (Array.to_list argsv1) + restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1 in let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in let filter2 = - restrict_upon_filter evd evk2 (noccur_evar env evd evk1) - (Array.to_list argsv2) + restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2 in let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in @@ -991,7 +1001,7 @@ let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 (has_constrainable_free_vars evd aliases k2 evk2 fvs2) - (Array.to_list argsv1) in + argsv1 in (* Only try pruning on variable substitutions, postpone otherwise. *) (* Rules out non-linear instances. *) if is_unification_pattern_pure_evar env evd ev2 (mkEvar ev1) then @@ -1018,7 +1028,7 @@ let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 a if are_canonical_instances args1 args2 env then (* If instances are canonical, we solve the problem in linear time *) let sign = evar_filtered_context (Evd.find evd evk2) in - let id_inst = Array.map (fun (id,_,_) -> mkVar id) (Array.of_list sign) in + let id_inst = inst_of_vars sign in Evd.define evk2 (mkEvar(evk1,id_inst)) evd else let evd,ev1,ev2 = @@ -1061,10 +1071,10 @@ let check_evar_instance evd evk1 body conv_algo = let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 = if Array.equal eq_constr argsv1 argsv2 then evd else (* Filter and restrict if needed *) + let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk - (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2) - (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in + (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2) args in let candidates = filter_candidates evd evk untypedfilter None in let filter = closure_of_filter evd evk untypedfilter in let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in @@ -1086,13 +1096,12 @@ exception IncompatibleCandidates let solve_candidates conv_algo env evd (evk,argsv) rhs = let evi = Evd.find evd evk in - let args = Array.to_list argsv in match evi.evar_candidates with | None -> raise NoCandidates | Some l -> let l' = List.map_filter - (filter_compatible_candidates conv_algo env evd evi args rhs) l in + (filter_compatible_candidates conv_algo env evd evi argsv rhs) l in match l' with | [] -> raise IncompatibleCandidates | [c,evd] -> @@ -1163,13 +1172,13 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = (* materializing is necessary, but is restricting useful? *) let ty = find_solution_type (evar_filtered_env evi) sols in let sign = evar_filtered_context evi in - let ty' = instantiate_evar sign ty (Array.to_list argsv) in + let ty' = instantiate_evar_array sign ty argsv in let (evd,evar,(evk',argsv' as ev')) = materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in let ts = expansions_of_var aliases t in + (** FIXME : [List.mem] on constr ???*) let test c = isEvar c || List.mem c ts in - let filter = - restrict_upon_filter evd evk test (Array.to_list argsv') in + let filter = restrict_upon_filter evd evk test argsv' in let filter = closure_of_filter evd evk' filter in let candidates = extract_candidates sols in let evd = match candidates with diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index e81fe83d2..28f2fb479 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -61,4 +61,4 @@ val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> evar_map val remove_instance_local_defs : - evar_map -> existential_key -> constr list -> constr list + evar_map -> existential_key -> constr array -> constr list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 751809bc5..d242dbc34 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -89,15 +89,34 @@ let eq_evar_info ei1 ei2 = (* This exception is raised by *.existential_value *) exception NotInstantiatedEvar +let instance_mismatch () = + anomaly (Pp.str "Signature and its instance do not match") + (* Note: let-in contributes to the instance *) let make_evar_instance sign args = - let rec instrec = function - | (id,_,_) :: sign, c::args when isVarId id c -> instrec (sign,args) - | (id,_,_) :: sign, c::args -> (id,c) :: instrec (sign,args) - | [],[] -> [] - | [],_ | _,[] -> anomaly (Pp.str "Signature and its instance do not match") + let rec instrec sign args = match sign, args with + | [], [] -> [] + | (id,_,_) :: sign, c :: args -> + if isVarId id c then instrec sign args + else (id, c) :: instrec sign args + | [], _ | _, [] -> instance_mismatch () + in + instrec sign args + +let make_evar_instance_array sign args = + let len = Array.length args in + let rec instrec sign i = match sign with + | [] -> + if Int.equal i len then [] + else instance_mismatch () + | (id, _, _) :: sign -> + if i < len then + let c = Array.unsafe_get args i in + if isVarId id c then instrec sign (succ i) + else (id, c) :: instrec sign (succ i) + else instance_mismatch () in - instrec (sign,args) + instrec sign 0 let instantiate_evar sign c args = let inst = make_evar_instance sign args in @@ -105,6 +124,12 @@ let instantiate_evar sign c args = | [] -> c | _ -> replace_vars inst c +let instantiate_evar_array sign c args = + let inst = make_evar_instance_array sign args in + match inst with + | [] -> c + | _ -> replace_vars inst c + (*******************************************************************) (* Metamaps *) @@ -291,7 +316,7 @@ let existential_value d (n, args) = let hyps = evar_filtered_context info in match evar_body info with | Evar_defined c -> - instantiate_evar hyps c (Array.to_list args) + instantiate_evar_array hyps c args | Evar_empty -> raise NotInstantiatedEvar @@ -305,7 +330,7 @@ let existential_type d (n, args) = with Not_found -> anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in let hyps = evar_filtered_context info in - instantiate_evar hyps info.evar_concl (Array.to_list args) + instantiate_evar_array hyps info.evar_concl args let add_constraints d cstrs = { d with univ_cstrs = Univ.merge_constraints cstrs d.univ_cstrs } diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 12699309b..20fbba63d 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -167,6 +167,7 @@ val existential_opt_value : evar_map -> existential -> constr option exception. *) val instantiate_evar : named_context -> constr -> constr list -> constr +val instantiate_evar_array : named_context -> constr -> constr array -> constr val subst_evar_defs_light : substitution -> evar_map -> evar_map (** Assume empty universe constraints in [evar_map] and [conv_pbs] *) |