diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 43 |
1 files changed, 20 insertions, 23 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4eae0cf86c..63cc8c7581 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -217,7 +217,7 @@ type 'a update = | NoUpdate open Context.Named.Declaration -let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign +let inst_of_vars sign = List.map (get_id %> mkVar) sign let restrict_evar_key evd evk filter candidates = match filter, candidates with @@ -247,7 +247,7 @@ let restrict_applied_evar evd (evk,argsv) filter candidates = | Some filter -> let evi = Evd.find evd evk in let subfilter = Filter.compose (evar_filter evi) filter in - Filter.filter_array subfilter argsv in + Filter.filter_list subfilter argsv in evd,(newevk,newargsv) (* Restrict an evar in the current evar_map *) @@ -258,7 +258,7 @@ let restrict_evar evd evk filter candidates = let restrict_instance evd evk filter argsv = match filter with None -> argsv | Some filter -> let evi = Evd.find evd evk in - Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv + Filter.filter_list (Filter.compose (evar_filter evi) filter) argsv open Context.Rel.Declaration let noccur_evar env evd evk c = @@ -269,7 +269,7 @@ let noccur_evar env evd evk c = if Evar.equal evk evk' then raise Occur else (if check_types then occur_rec false acc (existential_type evd ev'); - Array.iter (occur_rec check_types acc) args') + List.iter (occur_rec check_types acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then let decl = Environ.lookup_rel i env in @@ -561,17 +561,13 @@ let get_actual_deps env evd aliases l t = 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 [] - | LocalAssum _ :: sign -> - let () = assert (i < len) in - (Array.unsafe_get args i) :: aux sign (succ i) - | LocalDef _ :: sign -> - aux sign (succ i) + let rec aux sign args = match sign, args with + | [], [] -> [] + | LocalAssum _ :: sign, c :: args -> c :: aux sign args + | LocalDef _ :: sign, _ :: args -> aux sign args + | _ -> assert false in - aux (evar_filtered_context evi) 0 + aux (evar_filtered_context evi) args (* Check if an applied evar "?X[args] l" is a Miller's pattern *) @@ -697,7 +693,7 @@ let make_projectable_subst aliases sigma evi args = let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in (rest,all,cstrs,revmap)) | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0 - sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in + sign (List.rev args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in (full_subst,cstr_subst) (*------------------------------------* @@ -774,7 +770,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (mkRel 1)::(List.map (lift 1) inst_in_sign), push_rel d env,evd,Id.Set.add id.binder_name avoid)) rel_sign - (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) + (sign1,filter1,args1,inst_in_sign,env1,evd,avoid) in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in @@ -784,11 +780,12 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ty_t_in_sign sign2 filter2 inst2_in_env in let (evd, ev2_in_sign) = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in - let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in + let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in (evd, ev2_in_sign, ev2_in_env) let restrict_upon_filter evd evk p args = let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in + let args = Array.of_list args in let len = Array.length args in Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i)) @@ -1043,7 +1040,7 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = let p = invert_arg fullenv evd aliases k evk subst arg in extract_unique_projection p in - Array.map invert args' + List.map invert args' (* Redefines an evar with a smaller context (i.e. it may depend on less * variables) such that c becomes closed. @@ -1399,9 +1396,9 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = try evdref := Evd.add_universe_constraints !evdref cstr; true with UniversesDiffer -> false in - if Array.equal eq_constr argsv1 argsv2 then !evdref else + if List.equal eq_constr argsv1 argsv2 then !evdref else (* Filter and restrict if needed *) - let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in + let args = List.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk (fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in @@ -1461,7 +1458,7 @@ let occur_evar_upto_types sigma n c = | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> if Evar.Set.mem sp !seen then - Array.iter occur_rec args + List.iter occur_rec args else ( seen := Evar.Set.add sp !seen; Option.iter occur_rec (existential_opt_value0 sigma e); @@ -1579,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs (* Evar/Evar problem (but left evar is virtual) *) let aliases = lift_aliases k aliases in (try - let ev = (evk,Array.map (lift k) argsv) in + let ev = (evk,List.map (lift k) argsv) in let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in evdref := evd; body @@ -1657,7 +1654,7 @@ let rec invert_definition unify flags choose imitate_defs | [], [] -> true | _ -> false in - is_id_subst filter_ctxt (Array.to_list argsv) && + is_id_subst filter_ctxt argsv && closed0 evd rhs && Id.Set.subset (collect_vars evd rhs) !names in |