diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 6 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 23 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 35 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 32 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 28 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 78 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.mli | 4 |
9 files changed, 131 insertions, 83 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5ec44a68d8..1cae8d16de 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -264,7 +264,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 - | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) + (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 + + | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index cad5551c15..5a296de84b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -331,7 +331,7 @@ let extract_nondep_branches test c b l = match r,l with | r, [] -> r | GLambda (_,_,_,_,t), false::l -> strip l t - | GLetIn (_,_,_,t), true::l -> strip l t + | GLetIn (_,_,_,_,t), true::l -> strip l t (* FIXME: do we need adjustment? *) | _,_ -> assert false in if test c l then Some (strip l b) else None @@ -341,7 +341,7 @@ let it_destRLambda_or_LetIn_names l c = match c, l with | _, [] -> (List.rev nal,c) | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c - | GLetIn (_,na,_,c), true::l -> aux l (na::nal) c + | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c | _, false::l -> (* eta-expansion *) @@ -690,9 +690,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let c = if s != InProp then c else - GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in - GLetIn (dl, na', c, r) + let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in + GLetIn (dl, na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in @@ -764,9 +763,9 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | GProd (loc,id,k,t,c) -> let id = convert_name cl id in GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c) - | GLetIn (loc,id,b,e) -> + | GLetIn (loc,id,b,t,e) -> let id = convert_name cl id in - GLetIn(loc,id,detype_closed_glob cl b, detype_closed_glob cl e) + GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e) | GLetTuple (loc,ids,(n,r),b,e) -> let ids = List.map (convert_name cl) ids in let n = convert_name cl n in @@ -825,10 +824,12 @@ let rec subst_glob_constr subst raw = if r1' == r1 && r2' == r2 then raw else GProd (loc,n,bk,r1',r2') - | GLetIn (loc,n,r1,r2) -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in - if r1' == r1 && r2' == r2 then raw else - GLetIn (loc,n,r1',r2') + | GLetIn (loc,n,r1,t,r2) -> + let r1' = subst_glob_constr subst r1 in + let t' = Option.smartmap (subst_glob_constr subst) t in + let r2' = subst_glob_constr subst r2 in + if r1' == r1 && t == t' && r2' == r2 then raw else + GLetIn (loc,n,r1',t',r2') | GCases (loc,sty,rtno,rl,branches) -> let rtno' = Option.smartmap (subst_glob_constr subst) rtno diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a2ffe12e93..d18b437a33 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -500,8 +500,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) - ++ fnl ()) in + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -1129,6 +1128,10 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in + let () = if !debug_unification then + let open Pp in + Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 + ++ cut () ++ print_constr t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty @@ -1193,20 +1196,22 @@ let check_problems_are_solved env evd = | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () +exception MaxUndefined of (Evar.t * evar_info * constr list) + let max_undefined_with_candidates evd = - (* If evar were ordered with highest index first, fold_undefined - would be going decreasingly and we could use fold_undefined to - find the undefined evar of maximum index (alternatively, - max_bindings from ocaml 3.12 could be used); instead we traverse - the whole map *) - let l = Evd.fold_undefined - (fun evk ev_info evars -> - match ev_info.evar_candidates with - | None -> evars - | Some l -> (evk,ev_info,l)::evars) evd [] in - match l with - | [] -> None - | a::l -> Some (List.last (a::l)) + let fold evk evi () = match evi.evar_candidates with + | None -> () + | Some l -> raise (MaxUndefined (evk, evi, l)) + in + (** [fold_right] traverses the undefined map in decreasing order of indices. + The evar with candidates of maximum index is thus the first evar with + candidates found by a [fold_right] traversal. This has a significant impact on + performance. *) + try + let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in + None + with MaxUndefined ans -> + Some ans let rec solve_unconstrained_evars_with_candidates ts evd = (* max_undefined is supposed to return the most recent, hence diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818f4..ebbfa195f0 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -77,8 +77,8 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with | GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) -> Name.equal na1 na2 && binding_kind_eq bk1 bk2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 +| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) -> + Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 | GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) -> case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && List.equal tomatch_tuple_eq tp1 tp2 && @@ -152,10 +152,11 @@ let map_glob_constr_left_to_right f = function let comp1 = f ty in let comp2 = f c in GProd (loc,na,bk,comp1,comp2) - | GLetIn (loc,na,b,c) -> + | GLetIn (loc,na,b,t,c) -> let comp1 = f b in + let compt = Option.map f t in let comp2 = f c in - GLetIn (loc,na,comp1,comp2) + GLetIn (loc,na,comp1,compt,comp2) | GCases (loc,sty,rtntypopt,tml,pl) -> let comp1 = Option.map f rtntypopt in let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in @@ -189,8 +190,10 @@ let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt let fold_glob_constr f acc = function | GVar _ -> acc | GApp (_,c,args) -> List.fold_left f (f acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> + | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) -> f (f acc b) c + | GLetIn (_,_,b,t,c) -> + f (Option.fold_left f (f acc b) t) c | GCases (_,_,rtntypopt,tml,pl) -> let fold_pattern acc (_,idl,p,c) = f acc c in List.fold_left fold_pattern @@ -225,8 +228,8 @@ let occur_glob_constr id = (occur ty) || (not (same_id na id) && (occur c)) | GProd (loc,na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,c) -> - (occur b) || (not (same_id na id) && (occur c)) + | GLetIn (loc,na,b,t,c) -> + (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) | GCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) || (List.exists (fun (tm,_) -> occur tm) tml) @@ -270,10 +273,15 @@ let free_glob_vars = let rec vars bounded vs = function | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bounded vs b in + let vs'' = Option.fold_left (vars bounded) vs' ty in + let bounded' = add_name_to_ids bounded na in + vars bounded' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bounded vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in @@ -346,7 +354,7 @@ let add_and_check_ident id set = let bound_glob_vars = let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c -> + | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> let bound = name_fold add_and_check_ident na bound in fold_glob_constr vars bound c | GCases (loc,sty,rtntypopt,tml,pl) -> @@ -460,7 +468,7 @@ let loc_of_glob_constr = function | GApp (loc,_,_) -> loc | GLambda (loc,_,_,_,_) -> loc | GProd (loc,_,_,_,_) -> loc - | GLetIn (loc,_,_,_) -> loc + | GLetIn (loc,_,_,_,_) -> loc | GCases (loc,_,_,_,_) -> loc | GLetTuple (loc,_,_,_,_) -> loc | GIf (loc,_,_,_,_) -> loc @@ -512,9 +520,9 @@ let rec rename_glob_vars l = function | GLambda (loc,na,bk,t,c) -> let na',l' = update_subst na l in GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLetIn (loc,na,b,c) -> + | GLetIn (loc,na,b,t,c) -> let na',l' = update_subst na l in - GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c) (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) | GCases (loc,ci,po,tomatchl,cls) -> let test_pred_pat (na,ino) = diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9dcb5d2a57..79765a4938 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -44,8 +44,9 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PProd (v1, t1, b1), PProd (v2, t2, b2) -> Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 -| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> - Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 +| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> + Name.equal v1 v2 && constr_pattern_eq b1 b2 && + Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2 | PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> @@ -85,7 +86,8 @@ let rec occur_meta_pattern = function | PProj (_,arg) -> occur_meta_pattern arg | PLambda (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) | PProd (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) - | PLetIn (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) + | PLetIn (na,b,t,c) -> + Option.fold_left (fun b t -> b || occur_meta_pattern t) (occur_meta_pattern b) t || (occur_meta_pattern c) | PIf (c,c1,c2) -> (occur_meta_pattern c) || (occur_meta_pattern c1) || (occur_meta_pattern c2) @@ -101,7 +103,7 @@ exception BoundPattern;; let rec head_pattern_bound t = match t with | PProd (_,_,b) -> head_pattern_bound b - | PLetIn (_,_,b) -> head_pattern_bound b + | PLetIn (_,_,_,b) -> head_pattern_bound b | PApp (c,args) -> head_pattern_bound c | PIf (c,_,_) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c @@ -132,7 +134,7 @@ let pattern_of_constr env sigma t = | Sort (Prop Pos) -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c - | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, + | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) @@ -189,7 +191,7 @@ let map_pattern_with_binders g f l = function | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl) | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b) | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b) - | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b) + | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b) | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) @@ -274,11 +276,12 @@ let rec subst_pattern subst pat = let c2' = subst_pattern subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') - | PLetIn (name,c1,c2) -> + | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in + let t' = Option.smartmap (subst_pattern subst) t in let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLetIn (name,c1',c2') + if c1' == c1 && t' == t && c2' == c2 then pat else + PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> @@ -343,9 +346,10 @@ let rec pat_of_raw metas vars = function name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GLetIn (_,na,c1,c2) -> + | GLetIn (_,na,c1,t,c2) -> name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, + Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) | GSort (_,s) -> PSort s @@ -404,7 +408,9 @@ let rec pat_of_raw metas vars = function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | PatVar(_,na) -> na + | PatVar(_,na) -> + name_iter (fun n -> metas := n::!metas) na; + na | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f92110ea56..27144b279f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -257,16 +257,36 @@ type inference_flags = { [sigma'] into those already in [sigma] or deriving from an evar in [sigma] by restriction, and the evars properly created in [sigma'] *) +type frozen = +| FrozenId of evar_info Evar.Map.t + (** No pending evars. We do not put a set here not to reallocate like crazy, + but the actual data of the map is not used, only keys matter. All + functions operating on this type must have the same behaviour on + [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *) +| FrozenProgress of (Evar.Set.t * Evar.Set.t) Lazy.t + (** Proper partition of the evar map as described above. *) + let frozen_and_pending_holes (sigma, sigma') = - let add_derivative_of evk evi acc = - match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in - let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in - let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in - let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in - (frozen,pending) + let undefined0 = Evd.undefined_map sigma in + (** Fast path when the undefined evars where not modified *) + if undefined0 == Evd.undefined_map sigma' then + FrozenId undefined0 + else + let data = lazy begin + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + (frozen, pending) + end in + FrozenProgress data let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen evk = Evar.Set.mem evk frozen in + let filter_frozen = match frozen with + | FrozenId map -> fun evk -> Evar.Map.mem evk map + | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen + in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) @@ -276,7 +296,9 @@ let apply_typeclasses env evdref frozen fail_evar = evdref := Typeclasses.resolve_typeclasses ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref -let apply_inference_hook hook evdref pending = +let apply_inference_hook hook evdref frozen = match frozen with +| FrozenId _ -> () +| FrozenProgress (lazy (_, pending)) -> evdref := Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then @@ -299,7 +321,9 @@ let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) apply_typeclasses env (ref current_sigma) frozen true -let check_extra_evars_are_solved env current_sigma pending = +let check_extra_evars_are_solved env current_sigma frozen = match frozen with +| FrozenId _ -> () +| FrozenProgress (lazy (_, pending)) -> Evar.Set.iter (fun evk -> if not (Evd.is_defined current_sigma evk) then @@ -326,29 +350,29 @@ let check_evars env initial_sigma sigma c = | _ -> Constr.iter proc_rec c in proc_rec c -let check_evars_are_solved env current_sigma frozen pending = +let check_evars_are_solved env current_sigma frozen = check_typeclasses_instances_are_solved env current_sigma frozen; check_problems_are_solved env current_sigma; - check_extra_evars_are_solved env current_sigma pending + check_extra_evars_are_solved env current_sigma frozen (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let solve_remaining_evars flags env current_sigma init_sigma = + let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then - apply_inference_hook (Option.get flags.use_hook env) evdref pending; + apply_inference_hook (Option.get flags.use_hook env) evdref frozen; if flags.solve_unification_constraints then apply_heuristics env evdref false; - if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; + if flags.fail_evar then check_evars_are_solved env !evdref frozen; !evdref -let check_evars_are_solved env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in - check_evars_are_solved env current_sigma frozen pending +let check_evars_are_solved env current_sigma init_sigma = + let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in + check_evars_are_solved env current_sigma frozen let process_inference_flags flags env initial_sigma (sigma,c) = - let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in + let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c @@ -810,14 +834,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon - | GLetIn(loc,name,c1,c2) -> - let j = - match c1 with - | GCast (loc, c, CastConv t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon tj.utj_val) env evdref lvar c - | _ -> pretype empty_tycon env evdref lvar c1 - in + | GLetIn(loc,name,c1,t,c2) -> + let tycon1 = + match t with + | Some t -> + mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val + | None -> + empty_tycon in + let j = pretype tycon1 env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2c6aa7a21b..23957d5575 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -129,13 +129,13 @@ val type_uconstr : [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : inference_flags -> - env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map + env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, reporting an appropriate error message *) val check_evars_are_solved : - env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit + env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a91c30df6f..11771f7bac 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1520,7 +1520,7 @@ let default_matching_merge_flags sigma = use_pattern_unification = true; } -let default_matching_flags (sigma,_) = +let default_matching_flags sigma = let flags = default_matching_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = default_matching_merge_flags sigma; @@ -1658,7 +1658,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * (evar_map * constr) * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool type 'r abstraction_result = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ad882a9ff..c63502eae1 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -71,11 +71,11 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma + env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma type 'r abstraction_result = Names.Id.t * named_context_val * |