diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 49 |
1 files changed, 23 insertions, 26 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6c27d59375..648f960354 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Pre_env open Environ open Evd open Termops @@ -86,7 +85,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=nf_evar sigma v;utj_type=t} let nf_evars_universes evm = - Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) + UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm) (Evd.universe_subst evm) let nf_evars_and_universes evm = @@ -214,7 +213,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta()) let non_instantiated sigma = let listev = Evd.undefined_map sigma in - Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev + Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev (************************) (* Manipulating filters *) @@ -436,7 +435,7 @@ let new_pure_evar_full evd evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -463,14 +462,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca in (evd, newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = +let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with @@ -480,7 +479,7 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = +let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -490,7 +489,7 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnami | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = +let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) @@ -613,10 +612,11 @@ let rec check_and_clear_in_constr env evdref err ids global c = | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c -let clear_hyps_in_evi_main env evdref hyps terms ids = +let clear_hyps_in_evi_main env sigma hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let evdref = ref sigma in let terms = List.map EConstr.Unsafe.to_constr terms in let global = Id.Set.exists is_section_variable ids in let terms = @@ -639,16 +639,16 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = in remove_hyps ids check_context check_value hyps in - (nhyps,List.map EConstr.of_constr terms) + (!evdref, nhyps,List.map EConstr.of_constr terms) -let clear_hyps_in_evi env evdref hyps concl ids = - match clear_hyps_in_evi_main env evdref hyps [concl] ids with - | (nhyps,[nconcl]) -> (nhyps,nconcl) +let clear_hyps_in_evi env sigma hyps concl ids = + match clear_hyps_in_evi_main env sigma hyps [concl] ids with + | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl) | _ -> assert false -let clear_hyps2_in_evi env evdref hyps t concl ids = - match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with - | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) +let clear_hyps2_in_evi env sigma hyps t concl ids = + match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with + | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl) | _ -> assert false (* spiwack: a few functions to gather evars on which goals depend. *) @@ -829,13 +829,13 @@ let subterm_source evk ?where (loc,k) = (* Add equality constraints for covariant/invariant positions. For irrelevant positions, unify universes when flexible. *) let compare_cumulative_instances cv_pb variances u u' sigma = - let open Universes in + let open UnivProblem in let cstrs = Univ.Constraint.empty in - let soft = Constraints.empty in + let soft = Set.empty in let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> let open Univ.Variance in match v with - | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft + | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft | Covariant when cv_pb == Reduction.CUMUL -> Univ.Constraint.add (u,Univ.Le,u') cstrs, soft | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) @@ -847,10 +847,10 @@ let compare_cumulative_instances cv_pb variances u u' sigma = | exception Univ.UniverseInconsistency p -> Inr p let compare_constructor_instances evd u u' = - let open Universes in + let open UnivProblem in let soft = - Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs) - Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') + Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs) + Set.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') in Evd.add_universe_constraints evd soft @@ -869,12 +869,9 @@ let eq_constr_univs_test sigma1 sigma2 t u = with Univ.UniverseInconsistency _ | UniversesDiffer -> None in let ans = - Universes.eq_constr_univs_infer_with + UnivProblem.eq_constr_univs_infer_with (fun t -> kind_of_term_upto sigma1 t) (fun u -> kind_of_term_upto sigma2 u) (universes sigma2) fold t u sigma2 in match ans with None -> false | Some _ -> true - -type type_constraint = EConstr.types option -type val_constraint = EConstr.constr option |