From 53f5cc210da4debd5264d6d8651a76281b0b4256 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 13 Dec 2017 01:38:39 +0100 Subject: [econstr] Switch constrintern API to non-imperative style. We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there. --- interp/constrintern.ml | 55 +++++++++++++++++++++++--------------------------- 1 file changed, 25 insertions(+), 30 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c2157bb2e..909eab27e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2094,39 +2094,36 @@ let interp_open_constr env sigma c = (* Not all evars expected to be resolved and computation of implicit args *) -let interp_constr_evars_gen_impls env evdref +let interp_constr_evars_gen_impls env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - let evd, c = understand_tcc env !evdref ~expected_type c in - evdref := evd; - c, imps + let sigma, c = understand_tcc env sigma ~expected_type c in + sigma, (c, imps) -let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c +let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c -let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env evdref ~impls IsType c +let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env sigma ~impls IsType c (* Not all evars expected to be resolved, with side-effect on evars *) -let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c = +let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in - let evd, c = understand_tcc env !evdref ~expected_type c in - evdref := evd; - c + understand_tcc env sigma ~expected_type c let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c -let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType typ) c +let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen env sigma ~impls (OfType typ) c -let interp_type_evars env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen env evdref IsType ~impls c +let interp_type_evars env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen env sigma IsType ~impls c (* Miscellaneous *) @@ -2181,17 +2178,16 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_glob_context_evars env evdref k bl = +let interp_glob_context_evars env sigma k bl = let open EConstr in - let (env, par, _, impls) = + let env, sigma, par, _, impls = List.fold_left - (fun (env,params,n,impls) (na, k, b, t) -> + (fun (env,sigma,params,n,impls) (na, k, b, t) -> let t' = if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t else t in - let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in - evdref := evd; + let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in match b with None -> let d = LocalAssum (na,t) in @@ -2201,16 +2197,15 @@ let interp_glob_context_evars env evdref k bl = (ExplByPos (n, na), (true, true, true)) :: impls else impls in - (push_rel d env, d::params, succ n, impls) + (push_rel d env, sigma, d::params, succ n, impls) | Some b -> - let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in - evdref := evd; + let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in let d = LocalDef (na, c, t) in - (push_rel d env, d::params, n, impls)) - (env,[],k+1,[]) (List.rev bl) - in (env, par), impls + (push_rel d env, sigma, d::params, n, impls)) + (env,sigma,[],k+1,[]) (List.rev bl) + in sigma, ((env, par), impls) -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_glob_context_evars env evdref shift bl in - int_env, x + let sigma, x = interp_glob_context_evars env sigma shift bl in + sigma, (int_env, x) -- cgit v1.2.3