diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 8 | ||||
| -rw-r--r-- | interp/constrextern.ml | 8 | ||||
| -rw-r--r-- | interp/constrintern.ml | 63 | ||||
| -rw-r--r-- | interp/constrintern.mli | 28 |
4 files changed, 52 insertions, 55 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8b78a91b5b..7cc8de85d2 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -188,7 +188,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) = Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = - List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && + List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = @@ -260,7 +260,6 @@ let local_binders_loc bll = match bll with (* Legacy functions *) let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y let is_constructor id = try Globnames.isConstructRef @@ -292,8 +291,7 @@ let ids_of_pattern = let ids_of_pattern_list = List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) + (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty let ids_of_cases_indtype p = @@ -571,7 +569,7 @@ let expand_binders ?loc mkC bl c = let c = CAst.make ?loc @@ CCases (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) + [(Loc.tag ?loc:loc1 ([[p]], c))]) in (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bc8debd02d..1330b3741e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -852,7 +852,7 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) eqns in + let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> @@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes vars l in (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pl,c)) = - Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], - extern inctx scopes vars c) +and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + Loc.tag ?loc (pll,extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 977146b2fe..61b33aa415 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -958,8 +958,11 @@ let rec has_duplicate = function | [] -> None | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l +let loc_of_multiple_pattern pl = + Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl)) + let loc_of_lhs lhs = - Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs)) + Loc.merge_opt (loc_of_multiple_pattern (List.hd lhs)) (loc_of_multiple_pattern (List.last lhs)) let check_linearity lhs ids = match has_duplicate ids with @@ -1873,8 +1876,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_local_binder_aux intern ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) - and intern_multiple_pattern env n (loc,pl) = + and intern_multiple_pattern env n pl = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in + let loc = loc_of_multiple_pattern pl in check_number_of_pattern loc n pl; product_of_cases_patterns empty_alias idsl_pll @@ -2094,39 +2098,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 (EConstr.of_constr 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 +2182,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 +2201,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) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 46f96d20b4..632b423b05 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -112,28 +112,28 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.co (** Accepting unresolved evars *) -val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.constr +val interp_constr_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr -val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> EConstr.constr +val interp_casted_constr_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr -val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.types +val interp_type_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_constr_evars_impls : env -> evar_map ref -> +val interp_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - EConstr.constr * Impargs.manual_implicits + evar_map * (EConstr.constr * Impargs.manual_implicits) -val interp_casted_constr_evars_impls : env -> evar_map ref -> +val interp_casted_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> EConstr.types -> - EConstr.constr * Impargs.manual_implicits + evar_map * (EConstr.constr * Impargs.manual_implicits) -val interp_type_evars_impls : env -> evar_map ref -> +val interp_type_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - EConstr.types * Impargs.manual_implicits + evar_map * (EConstr.types * Impargs.manual_implicits) (** Interprets constr patterns *) @@ -158,8 +158,8 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder_expr list -> - internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits) + env -> evar_map -> local_binder_expr list -> + evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) |