diff options
Diffstat (limited to 'pretyping')
32 files changed, 355 insertions, 279 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fdb19d37..fcbe90b6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind = applist (mkIndU indu,List.rev evarl) let try_find_ind env sigma typ realnames = - let (IndType(_,realargs) as ind) = find_rectype env sigma typ in + let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in let names = match realnames with | Some names -> names - | None -> List.make (List.length realargs) Anonymous in + | None -> + let ind = fst (fst (dest_ind_family indf)) in + List.make (inductive_nrealdecls ind) Anonymous in IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = @@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t) let recover_initial_subpattern_names = List.map2 set_declaration_name -let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) +let recover_and_adjust_alias_names names sign = + let rec aux = function + | [],[] -> + [] + | x::names, (_,None,t)::sign -> + (x,(alias_of_pat x,None,t)) :: aux (names,sign) + | names, (na,(Some _ as c),t)::sign -> + (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign) + | _ -> assert false + in + List.split (aux (names,sign)) let push_rels_eqn sign eqn = {eqn with @@ -1644,7 +1656,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = in aux (0,extenv,subst0) t0 -let build_tycon loc env tycon_env subst tycon extenv evdref t = +let build_tycon loc env tycon_env s subst tycon extenv evdref t = let t,tt = match t with | None -> (* This is the situation we are building a return predicate and @@ -1659,6 +1671,8 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = let evd,tt = Typing.e_type_of extenv !evdref t in evdref := evd; (t,tt) in + let b = e_cumul env evdref tt (mkSort s) (* side effect *) in + if not b then anomaly (Pp.str "Build_tycon: should be a type"); { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1693,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t = let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in let sign = make_arity_signature env true indf' in - let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in - let p = List.length realargs in + let patl = pat :: List.rev patl in + let patl,sign = recover_and_adjust_alias_names patl sign in + let p = List.length patl in let env' = push_rel_context sign env in - let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in - patl@pat::patl',acc_sign,acc + let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in + List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in let d = (alias_of_pat pat,None,typ) in @@ -1780,7 +1795,7 @@ let build_inversion_problem loc env sigma tms t = mat = [eqn1;eqn2]; caseloc = loc; casestyle = RegularStyle; - typing_function = build_tycon loc env pb_env subst} in + typing_function = build_tycon loc env pb_env s subst} in let pred = (compile pb).uj_val in (!evdref,pred) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 559f5fe6..055996de 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 = let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2 - | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2 + | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2 + | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) module ClTyp = struct diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index a6e2bc19..161cffa8 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -351,34 +351,45 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next = else mkresult subst (mk_ctx (mkMeta special_meta)) next with PatternMatchingFailure -> next () +let subargs env v = Array.map_to_list (fun c -> (env, c)) v + (* Tries to match a subterm of [c] with [pat] *) let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let rec aux env c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> - let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in - let next () = try_aux [env] [c1] next_mk_ctx next in + let next_mk_ctx = function + | [c1] -> mk_ctx (mkCast (c1, k, c2)) + | _ -> assert false + in + let next () = try_aux [env, c1] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Lambda (x,c1,c2) -> - let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in + let next_mk_ctx = function + | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) + | _ -> assert false + in let next () = let env' = Environ.push_rel (x,None,c1) env in - try_aux [env;env'] [c1; c2] next_mk_ctx next in + try_aux [(env, c1); (env', c2)] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Prod (x,c1,c2) -> - let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in + let next_mk_ctx = function + | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) + | _ -> assert false + in let next () = let env' = Environ.push_rel (x,None,c1) env in - try_aux [env;env'] [c1;c2] next_mk_ctx next in + try_aux [(env, c1); (env', c2)] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function - | [c1;c2] -> mkLetIn (x,c1,t,c2) + | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in let next () = let env' = Environ.push_rel (x,Some c1,t) env in - try_aux [env;env'] [c1;c2] next_mk_ctx next in + try_aux [(env, c1); (env', c2)] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | App (c1,lc) -> let next () = @@ -390,14 +401,15 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let mk_ctx = function | [app';c] -> mk_ctx (mkApp (app',[|c|])) | _ -> assert false in - try_aux [env] [app;Array.last lc] mk_ctx next + try_aux [(env, app); (env, Array.last lc)] mk_ctx next else let rec aux2 app args next = match args with | [] -> let mk_ctx le = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - try_aux [env] (c1::Array.to_list lc) mk_ctx next + let sub = (env, c1) :: subargs env lc in + try_aux sub mk_ctx next | arg :: args -> let app = mkApp (app,[|arg|]) in let next () = aux2 app args next in @@ -407,7 +419,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = else let mk_ctx le = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - try_aux [env] (c1::Array.to_list lc) mk_ctx next + let sub = (env, c1) :: subargs env lc in + try_aux sub mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Case (ci,hd,c1,lc) -> @@ -415,24 +428,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in + let sub = (env, c1) :: subargs env lc in + let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let next () = - try_aux - [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + let sub = subargs env types @ subargs env bodies in + let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | CoFix (i,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let next () = - try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + let sub = subargs env types @ subargs env bodies in + let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Proj (p,c') -> let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in @@ -441,27 +454,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = try let term = Retyping.expand_projection env sigma p c' [] in aux env term mk_ctx next - with Retyping.RetypeError _ -> raise PatternMatchingFailure + with Retyping.RetypeError _ -> next () else - try_aux [env] [c'] next_mk_ctx next in + try_aux [env, c'] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> authorized_occ env sigma partial_app closed pat c mk_ctx next (* Tries [sub_match] for all terms in the list *) - and try_aux lenv lc mk_ctx next = - let rec try_sub_match_rec lacc lenv lc = - match lenv, lc with - | _, [] -> next () - | env :: tlenv, c::tl -> - let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in - let next () = - let env' = match tlenv with [] -> lenv | _ -> tlenv in - try_sub_match_rec (c::lacc) env' tl - in - aux env c mk_ctx next - | _ -> assert false in - try_sub_match_rec [] lenv lc in + and try_aux lc mk_ctx next = + let rec try_sub_match_rec lacc lc = + match lc with + | [] -> next () + | (env, c) :: tl -> + let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in + let next () = try_sub_match_rec (c :: lacc) tl in + aux env c mk_ctx next + in + try_sub_match_rec [] lc in let lempty () = IStream.Nil in let result () = aux env c (fun x -> x) lempty in IStream.thunk result diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 046ee0da..28fb8cbe 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -498,16 +498,17 @@ let rec detype flags avoid env sigma t = else noparams () | Evar (evk,cl) -> - let bound_to_itself id c = + let bound_to_itself_or_letin (id,b,_) c = + b != None || try let n = List.index Name.equal (Name id) (fst env) in - isRelN n c + isRelN n c with Not_found -> isVarId id c in let id,l = try let id = Evd.evar_ident evk sigma in - let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in - let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in - let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in + let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in + let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in + let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a95af253..f388f900 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( - let evd, b = - try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 - with Univ.UniverseInconsistency _ -> evd, false + let evd, e = + try + let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) + env evd term1 term2 + in + if b then evd, None + else evd, Some (ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e) in - if b then Some (evd, true) - else if is_ground_env evd env then Some (evd, false) - else None) + match e with + | None -> Some (evd, e) + | Some e -> + if is_ground_env evd env then Some (evd, Some e) + else None) else None in match ground_test with - | Some (evd, true) -> Success evd - | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2)) + | Some (evd, None) -> Success evd + | Some (evd, Some e) -> UnifFailure (evd,e) | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) @@ -555,8 +562,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) -> let f1 i = ise_and i - [(fun i -> evar_conv_x ts env i CONV t1 t2); - (fun i -> evar_conv_x ts env i CONV b1 b2); + [(fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 5aa72c90..bfd19c6c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -64,30 +64,33 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = in modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> - mkProd (na,u,refresh dir v) + mkProd (na,u,refresh dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) - and refresh_term_evars onevars t = + and refresh_term_evars onevars top t = match kind_of_term t with | App (f, args) when is_template_polymorphic env f -> let pos = get_polymorphic_positions f in refresh_polymorphic_positions args pos + | App (f, args) when top && isEvar f -> + refresh_term_evars true false f; + Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in let ty' = refresh true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () - | _ -> iter_constr (refresh_term_evars onevars) t + | _ -> iter_constr (refresh_term_evars onevars false) t and refresh_polymorphic_positions args pos = let rec aux i = function | Some l :: ls -> if i < Array.length args then - ignore(refresh_term_evars true args.(i)); + ignore(refresh_term_evars true false args.(i)); aux (succ i) ls | None :: ls -> if i < Array.length args then - ignore(refresh_term_evars false args.(i)); + ignore(refresh_term_evars false false args.(i)); aux (succ i) ls | [] -> () in aux 0 pos @@ -97,7 +100,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = (match pbty with | None -> t | Some dir -> refresh dir t) - else (refresh_term_evars false t; t) + else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t @@ -118,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false let test_success conv_algo env evd c c' rhs = is_success (conv_algo env evd c c' rhs) -let add_conv_oriented_pb (pbty,env,t1,t2) evd = +let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = match pbty with - | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd - | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd - | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd + | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd + | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd + | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd (*------------------------------------* * Restricting existing evars * @@ -175,20 +178,31 @@ let restrict_instance evd evk filter argsv = Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv let noccur_evar env evd evk c = - let rec occur_rec k c = match kind_of_term c with + let cache = ref Int.Set.empty (* cache for let-ins *) in + let rec occur_rec (k, env as acc) c = + match kind_of_term c with | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec k c + | Some c -> occur_rec acc c | None -> if Evar.equal evk evk' then raise Occur - else Array.iter (occur_rec k) args') + else Array.iter (occur_rec acc) args') | Rel i when i > k -> - (match pi2 (Environ.lookup_rel (i-k) env) with + if not (Int.Set.mem (i-k) !cache) then + (match pi2 (Environ.lookup_rel i env) with | None -> () - | Some b -> occur_rec k (lift i b)) - | _ -> iter_constr_with_binders succ occur_rec k c + | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) + | Proj (p,c) -> + let c = + try Retyping.expand_projection env evd p c [] + with Retyping.RetypeError _ -> + (* Can happen when called from w_unify which doesn't assign evars/metas + eagerly enough *) c + in occur_rec acc c + | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) + occur_rec acc c in - try occur_rec 0 c; true with Occur -> false + try occur_rec (0,env) c; true with Occur -> false (***************************************) (* Managing chains of local definitons *) @@ -213,7 +227,7 @@ let compute_var_aliases sign = sign Id.Map.empty let compute_rel_aliases var_aliases rels = - snd (List.fold_right (fun (_,b,t) (n,aliases) -> + snd (List.fold_right (fun (_,b,u) (n,aliases) -> (n-1, match b with | Some t -> @@ -227,7 +241,7 @@ let compute_rel_aliases var_aliases rels = try Int.Map.find (p+n) aliases with Not_found -> [] in Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases | _ -> - Int.Map.add n [lift n t] aliases) + Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases) | None -> aliases)) rels (List.length rels,Int.Map.empty)) @@ -311,6 +325,7 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env) let free_vars_and_rels_up_alias_expansion aliases c = let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in + let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in let is_in_cache depth = function | Rel n -> Int.Set.mem (n-depth) !cache_rel @@ -325,8 +340,13 @@ let free_vars_and_rels_up_alias_expansion aliases c = | Rel _ | Var _ as ck -> if is_in_cache depth ck then () else begin put_in_cache depth ck; - let c = expansion_of_var aliases c in + let c' = expansion_of_var aliases c in + (if c != c' then (* expansion, hence a let-in *) match kind_of_term c with + | Var id -> acc4 := Id.Set.add id !acc4 + | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3 + | _ -> ()); + match kind_of_term c' with | Var id -> acc2 := Id.Set.add id !acc2 | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 | _ -> frec (aliases,depth) c end @@ -338,7 +358,7 @@ let free_vars_and_rels_up_alias_expansion aliases c = frec (aliases,depth) c in frec (aliases,0) c; - (!acc1,!acc2) + (!acc1,!acc2,!acc3,!acc4) (********************************) (* Managing pattern-unification *) @@ -374,7 +394,7 @@ let get_actual_deps aliases l t = l else (* Probably strong restrictions coming from t being evar-closed *) - let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in + let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in List.filter (fun c -> match kind_of_term c with | Var id -> Id.Set.mem id fv_ids @@ -1013,52 +1033,52 @@ exception CannotProject of evar_map * existential of subterms to eventually discard so as to be allowed to keep ti. *) -let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t = - let f,args = decompose_app_vect t in +let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = + let f,args2 = decompose_app_vect t in + let f,args1 = decompose_app_vect (whd_evar evd f) in + let args = Array.append args1 args2 in match kind_of_term f with | Construct ((ind,_),u) -> let n = Inductiveops.inductive_nparams ind in if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false k g) params - | Ind _ -> Array.for_all (is_constrainable_in false k g) args - | Prod (_,t1,t2) -> is_constrainable_in false k g t1 && is_constrainable_in false k g t2 + Array.for_all (is_constrainable_in false evd k g) params + | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args + | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2 | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | Sort _ -> true | _ -> (* We don't try to be more clever *) true -let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = - let t = expansion_of_var aliases t in - match kind_of_term t with - | Var id -> Id.Set.mem id fv_ids - | Rel n -> n <= k || Int.Set.mem n fv_rels - | _ -> is_constrainable_in true k (ev,fvs) t - -let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= - let filter1 = - restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1 - in - let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in - let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in - let filter2 = - restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2 - in - let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in - let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in - evd,ev1,ev2 +let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t = + let t' = expansion_of_var aliases t in + if t' != t then + (* t is a local definition, we keep it only if appears in the list *) + (* of let-in variables effectively occurring on the right-hand side, *) + (* which is the only reason to keep it when inverting arguments *) + match kind_of_term t with + | Var id -> Id.Set.mem id let_ids + | Rel n -> Int.Set.mem n let_rels + | _ -> assert false + else + (* t is an instance for a proper variable; we filter it along *) + (* the free variables allowed to occur *) + match kind_of_term t with + | Var id -> Id.Set.mem id fv_ids + | Rel n -> n <= k || Int.Set.mem n fv_rels + | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t exception EvarSolvedOnTheFly of evar_map * constr (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on the common domain of definition *) -let project_evar_on_evar g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = +let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 - (has_constrainable_free_vars evd aliases k2 evk2 fvs2) + (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2) argsv1 in let candidates1 = try restrict_candidates g env evd filter1 ev1 ev2 @@ -1094,9 +1114,9 @@ let check_evar_instance evd evk1 body conv_algo = | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) -let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) = +let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try - let evd,body = project_evar_on_evar g env evd aliases 0 pbty ev1 ev2 in + let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in let evd' = Evd.define evk2 body evd in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> @@ -1113,27 +1133,23 @@ let preferred_orientation evd evk1 evk2 = | _,Evar_kinds.QuestionMark _ -> false | _ -> true -let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env in if preferred_orientation evd evk1 evk2 then - try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1 + try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> - try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 + try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 + try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> - try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1 + try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd - -let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 = - let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty = - (* If an evar occurs in the instance of the other evar and the - use of an heuristic is forced, we restrict *) - if force then ensure_evar_independent g env evd ev1 ev2, None - else (evd,ev1,ev2),pbty in + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd + +let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = + let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in let evd = try @@ -1162,7 +1178,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 = downcast evk2 t2 (downcast evk1 t1 evd) with Reduction.NotArity -> evd in - solve_evar_evar_aux f g env evd pbty ev1 ev2 + solve_evar_evar_aux force f g env evd pbty ev1 ev2 type conv_fun = env -> evar_map -> conv_pb -> constr -> constr -> unification_result @@ -1321,7 +1337,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let aliases = lift_aliases k aliases in (try let ev = (evk,Array.map (lift k) argsv) in - let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k None ev' ev in + let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in evdref := evd; body with @@ -1338,7 +1354,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let evd = (* Try to project (a restriction of) the left evar ... *) try - let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 None ev'' ev' in + let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in check_evar_instance evd evk' body conv_algo with @@ -1384,19 +1400,6 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - let _fast rhs = - let filter_ctxt = evar_filtered_context evi in - let names = ref Idset.empty in - let rec is_id_subst ctxt s = - match ctxt, s with - | ((id, _, _) :: ctxt'), (c :: s') -> - names := Idset.add id !names; - isVarId id c && is_id_subst ctxt' s' - | [], [] -> true - | _ -> false in - is_id_subst filter_ctxt (Array.to_list argsv) && - closed0 rhs && - Idset.subset (collect_vars rhs) !names in let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d286b98e..201a16eb 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -212,9 +212,11 @@ let whd_head_evar sigma c = (* Creating new metas *) (**********************) +let meta_counter_summary_name = "meta counter" + (* Generator of metavariables *) let new_meta = - let meta_ctr = Summary.ref 0 ~name:"meta counter" in + let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in fun () -> incr meta_ctr; !meta_ctr let mk_new_meta () = mkMeta(new_meta()) @@ -241,9 +243,11 @@ let make_pure_subst evi args = (* Creating new evars *) (**********************) +let evar_counter_summary_name = "evar counter" + (* Generator of existential names *) let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:"evar counter" in + let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr (*------------------------------------* @@ -838,3 +842,8 @@ let subterm_source evk (loc,k) = | Evar_kinds.SubEvar (evk) -> evk | _ -> evk in (loc,Evar_kinds.SubEvar evk) + + +(** Term exploration up to isntantiation. *) +let kind_of_term_upto sigma t = + Constr.kind (Reductionops.whd_evar sigma t) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f89266a6..49036798 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) exception Uninstantiated_evar of existential_key val flush_and_check_evars : evar_map -> constr -> constr +(** {6 Term manipulation up to instantiation} *) + +(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] + as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the + value of [e] in [sigma] is (recursively) used. *) +val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds @@ -236,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> val subterm_source : existential_key -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located + +val meta_counter_summary_name : string +val evar_counter_summary_name : string diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ee72d314..bf519fb7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -230,20 +230,20 @@ let evar_instance_array test_id info args = else instance_mismatch () | false :: filter, _ :: ctxt -> instrec filter ctxt i - | true :: filter, (id, _, _) :: ctxt -> + | true :: filter, (id,_,_ as d) :: ctxt -> if i < len then let c = Array.unsafe_get args i in - if test_id id c then instrec filter ctxt (succ i) + if test_id d c then instrec filter ctxt (succ i) else (id, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in match Filter.repr (evar_filter info) with | None -> - let map i (id, _, _) = + let map i (id,_,_ as d) = if (i < len) then let c = Array.unsafe_get args i in - if test_id id c then None else Some (id,c) + if test_id d c then None else Some (id,c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -251,7 +251,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array isVarId info args + evar_instance_array (fun (id,_,_) -> isVarId id) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -568,14 +568,6 @@ type evar_map = { (*** Lifting primitive from Evar.Map. ***) -(* HH: The progress tactical now uses this function. *) -let progress_evar_map d1 d2 = - let is_new k v = - assert (v.evar_body == Evar_empty); - EvMap.mem k d2.defn_evars - in - not (d1 == d2) && EvMap.exists is_new d1.undf_evars - let add_name_newly_undefined naming evk evi (evtoid,idtoev) = let id = match naming with | Misctypes.IntroAnonymous -> @@ -779,7 +771,9 @@ let merge_universe_context evd uctx' = let set_universe_context evd uctx' = { evd with universes = uctx' } -let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} +let add_conv_pb ?(tail=false) pb d = + if tail then {d with conv_pbs = d.conv_pbs @ [pb]} + else {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (find d evk).evar_source @@ -1195,6 +1189,18 @@ let abstract_undefined_variables uctx = in { uctx with uctx_local = Univ.ContextSet.empty; uctx_univ_algebraic = vars' } +let fix_undefined_variables ({ universes = uctx } as evm) = + let algs', vars' = + Univ.LMap.fold (fun u v (algs, vars as acc) -> + if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) + else acc) + uctx.uctx_univ_variables + (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) + in + {evm with universes = + { uctx with uctx_univ_variables = vars'; + uctx_univ_algebraic = algs' } } + let refresh_undefined_univ_variables uctx = let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in @@ -1301,27 +1307,6 @@ let e_eq_constr_univs evdref t u = let eq_constr_univs_test evd t u = snd (eq_constr_univs evd t u) -let eq_named_context_val d ctx1 ctx2 = - ctx1 == ctx2 || - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 - && (eq_constr_univs_test d) t1 t2 - in List.equal eq_named_declaration c1 c2 - -let eq_evar_body d b1 b2 = match b1, b2 with -| Evar_empty, Evar_empty -> true -| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2 -| _ -> false - -let eq_evar_info d ei1 ei2 = - ei1 == ei2 || - eq_constr_univs_test d ei1.evar_concl ei2.evar_concl && - eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) && - eq_evar_body d ei1.evar_body ei2.evar_body - (** ppedrot: [eq_constr] may be a bit too permissive here *) - - (**********************************************************) (* Accessing metas *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 53f8b0db..fe785a83 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -12,7 +12,6 @@ open Names open Term open Context open Environ -open Mod_subst (** {5 Existential variables and unification states} @@ -127,10 +126,6 @@ type evar_map (** Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction. *) -val progress_evar_map : evar_map -> evar_map -> bool -(** Assuming that the second map extends the first one, this says if - some existing evar has been refined *) - val empty : evar_map (** The empty evar map. *) @@ -205,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map val undefined_map : evar_map -> evar_info Evar.Map.t (** Access the undefined evar mapping directly. *) -val eq_evar_info : evar_map -> evar_info -> evar_info -> bool -(** Compare the evar_info's up to the universe constraints of the evar map. *) - val drop_all_defined : evar_map -> evar_map (** {6 Instantiating partial terms} *) @@ -224,7 +216,7 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> constr -> constr array -> constr @@ -398,7 +390,7 @@ type clbinding = (** Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : evar_constraint -> evar_map -> evar_map +val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> @@ -538,6 +530,8 @@ val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> e val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : evar_universe_context -> evar_universe_context +val fix_undefined_variables : evar_map -> evar_map + val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst val nf_constraints : evar_map -> evar_map diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 7f7f4d76..95a6ba79 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -11,7 +11,6 @@ open Util open Errors open Names open Locus -open Context open Term open Nameops open Termops diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 82330b84..47d9654e 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Locus open Context open Term diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 67f3cb41..e514fd52 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,9 @@ open Glob_term val cases_pattern_eq : cases_pattern -> cases_pattern -> bool +val cast_type_eq : ('a -> 'a -> bool) -> + 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + val glob_constr_eq : glob_constr -> glob_constr -> bool (** Operations on [glob_constr] *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 654f914b..dfdc24d4 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -18,7 +18,6 @@ open Declarations open Declareops open Environ open Reductionops -open Inductive (* The following three functions are similar to the ones defined in Inductive, but they expect an env *) @@ -274,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = - rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in + rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = Array.map2 (fun c n -> let d,_ = decompose_prod_assum c in @@ -366,14 +365,16 @@ let get_arity env ((ind,u),params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in let parsign = (* Dynamically detect if called with an instance of recursively - uniform parameter only or also of non recursively uniform + uniform parameter only or also of recursively non-uniform parameters *) - let parsign = mib.mind_params_ctxt in - let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in - if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then - snd (List.chop nnonrecparams mib.mind_params_ctxt) - else - parsign in + let nparams = List.length params in + if Int.equal nparams mib.mind_nparams then + mib.mind_params_ctxt + else begin + assert (Int.equal nparams mib.mind_nparams_rec); + let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in + snd (List.chop nnonrecparamdecls mib.mind_params_ctxt) + end in let parsign = Vars.subst_instance_context u parsign in let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in @@ -527,7 +528,7 @@ let type_case_branches_with_names env indspec p c = let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in (* Build case type *) - let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in + let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then (set_pattern_names env (fst ind) lbrty, conclty) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index af1783b7..7959759a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array (** Return constructor types in normal form *) val arities_of_constructors : env -> pinductive -> types array -(** An inductive type with its parameters *) +(** An inductive type with its parameters (transparently supports + reasoning either with only recursively uniform parameters or with all + parameters including the recursively non-uniform ones *) type inductive_family val make_ind_family : inductive puniverses * constr list -> inductive_family val dest_ind_family : inductive_family -> inductive puniverses * constr list @@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary val get_constructor : pinductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary -val get_arity : env -> inductive_family -> rel_context * sorts_family val get_constructors : env -> inductive_family -> constructor_summary array val get_projections : env -> inductive_family -> constant array option +(** [get_arity] returns the arity of the inductive family instantiated + with the parameters; if recursively non-uniform parameters are not + part of the inductive family, they appears in the arity *) +val get_arity : env -> inductive_family -> rel_context * sorts_family + val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : env -> bool -> inductive_family -> rel_context diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c49bec9a..705e594a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with let pattern_of_constr env sigma t = let ctx = ref [] in + let keep = ref Evar.Set.empty in + let remove = ref Evar.Set.empty in let rec pattern_of_constr env t = match kind_of_term t with | Rel n -> PRel n @@ -141,28 +143,38 @@ let pattern_of_constr env sigma t = | App (f,a) -> (match match kind_of_term f with - Evar (evk,args as ev) -> - (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - Some id - | _ -> None) - | _ -> None - with - | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) - | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) + | Evar (evk,args as ev) -> + (match snd (Evd.evar_source evk sigma) with + Evar_kinds.MatchingVar (true,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + keep := Evar.Set.union (evars_of_term ty) !keep; + remove := Evar.Set.add evk !remove; + Some id + | _ -> None) + | _ -> None + with + | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) + | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> pattern_of_constr env (Retyping.expand_projection env sigma p c []) | Evar (evk,ctxt as ev) -> - (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) - | _ -> PMeta None) + remove := Evar.Set.add evk !remove; + (match snd (Evd.evar_source evk sigma) with + | Evar_kinds.MatchingVar (b,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + let () = ignore (pattern_of_constr env ty) in + assert (not b); PMeta (Some id) + | Evar_kinds.GoalEvar -> + PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | _ -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + let () = ignore (pattern_of_constr env ty) in + PMeta None) | Case (ci,p,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; @@ -178,9 +190,11 @@ let pattern_of_constr env sigma t = | Fix f -> PFix f | CoFix f -> PCoFix f in let p = pattern_of_constr env t in + let remove = Evar.Set.diff !remove !keep in + let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in (* side-effect *) (* Warning: the order of dependencies in ctx is not ensured *) - (!ctx,p) + (sigma,!ctx,p) (* To process patterns, we need a translation without typing at all. *) @@ -220,7 +234,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - snd (pattern_of_constr env sigma c) + pi3 (pattern_of_constr env sigma c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in @@ -245,7 +259,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - snd (pattern_of_constr (Global.env()) Evd.empty t) + pi3 (pattern_of_constr (Global.env()) Evd.empty t) | PVar _ | PEvar _ | PRel _ -> pat diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index cf02421c..9e72280f 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) -val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern +val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> + Evd.evar_map * named_context * constr_pattern (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 040792ef..0cadffa4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs = iraise (e, info)); indexes else - (* we now search recursively amoungst all combinations *) + (* we now search recursively among all combinations *) (try List.iter (fun l -> @@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) = let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c -(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) +(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false (* Utilisé pour inférer le prédicat des Cases *) @@ -324,12 +324,6 @@ let pretype_id pretype loc env evdref lvar id = (* Check if [id] is a section or goal variable *) try let (_,_,typ) = lookup_named id env in - (* let _ = *) - (* try *) - (* let ctx = Decls.variable_context id in *) - (* evdref := Evd.merge_context_set univ_rigid !evdref ctx; *) - (* with Not_found -> () *) - (* in *) { uj_val = mkVar id; uj_type = typ } with Not_found -> (* [id] not found, standard error message *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7d1e0c9b..142b5451 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags val all_and_fail_flags : inference_flags -(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) +(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) val allow_anonymous_refs : bool ref (** Generic call to the interpreter from glob_constr to open_constr, leaving diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a23963ab..dd671f11 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -60,13 +60,20 @@ module ReductionBehaviour = struct let discharge = function | _,(ReqGlobal (ConstRef c, req), (_, b)) -> - let c' = pop_con c in - let vars, _subst, _ctx = Lib.section_segment_of_constant c in - let extra = List.length vars in - let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in - let recargs' = List.map ((+) extra) b.b_recargs in - let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in - Some (ReqGlobal (ConstRef c', req), (ConstRef c', b')) + let b = + if Lib.is_in_section (ConstRef c) then + let vars, _, _ = Lib.section_segment_of_constant c in + let extra = List.length vars in + let nargs' = + if b.b_nargs = max_int then max_int + else if b.b_nargs < 0 then b.b_nargs + else b.b_nargs + extra in + let recargs' = List.map ((+) extra) b.b_recargs in + { b with b_nargs = nargs'; b_recargs = recargs' } + else b + in + let c = Lib.discharge_con c in + Some (ReqGlobal (ConstRef c, req), (ConstRef c, b)) | _ -> None let rebuild = function @@ -842,7 +849,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let (tm',sk'),cst_l' = whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) in - if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk' + let rec is_case x = match kind_of_term x with + | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x + | App (hd, _) -> is_case hd + | Case _ -> true + | _ -> false in + if equal_stacks (x, app_sk) (tm', sk') + || Stack.will_expose_iota sk' + || is_case tm' then fold () else whrec cst_l' (tm', sk' @ sk) else match recargs with @@ -980,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, ((Stack.Case _ |Stack.Proj _)::s') -> reduce_and_refold_cofix whrec env cst_l cofix stack |_ -> fold () else fold () @@ -1059,7 +1073,7 @@ let local_whd_state_gen flags sigma = | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) |_ -> s else s @@ -1279,7 +1293,8 @@ let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances } -let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = +let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) + env sigma x y = try let b, sigma = let b, cstrs = @@ -1301,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y sigma', true with | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ -> sigma, false + | Univ.UniverseInconsistency _ when catch_incon -> sigma, false | e when is_anomaly e -> error "Conversion test raised an anomaly" (********************************************************************) @@ -1617,3 +1632,16 @@ let head_unfold_under_prod ts env _ c = | Const cst -> beta_applist (unfold cst,l) | _ -> c in aux c + +let betazetaevar_applist sigma n c l = + let rec stacklam n env t stack = + if Int.equal n 0 then applist (substl env t, stack) else + match kind_of_term t, stack with + | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl + | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | Evar ev, _ -> + (match safe_evar_value sigma ev with + | Some body -> stacklam n env body stack + | None -> applist (substl env t, stack)) + | _ -> anomaly (Pp.str "Not enough lambda/let's") in + stacklam n [] c l diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 7c61d4e1..1df2a73b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_fconv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. + @raises UniverseInconsistency iff catch_incon is set to false, + otherwise returns false in that case. *) -val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> - evar_map * bool +val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> + env -> evar_map -> constr -> constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) @@ -278,6 +280,7 @@ val whd_meta : evar_map -> constr -> constr val plain_instance : constr Metamap.t -> constr -> constr val instance : evar_map -> constr Metamap.t -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function +val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index cd52ba44..a56861c6 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma = | Ind ind -> rename_type_of_inductive env ind | Construct cstr -> rename_type_of_constructor env cstr | Case (_,p,c,lf) -> - let Inductiveops.IndType(_,realargs) = + let Inductiveops.IndType(indf,realargs) = let t = type_of env c in try Inductiveops.find_rectype env sigma t with Not_found -> @@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma = Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in - let t = whd_beta sigma (applist (p, realargs)) in + let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in + let t = betazetaevar_applist sigma n p realargs in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b4e0459c..372b26aa 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,7 +23,6 @@ open Reductionops open Cbv open Patternops open Locus -open Pretype_errors (* Errors *) @@ -190,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = if Array.for_all (noccurn k) tys && Array.for_all (noccurn (k+nbfix)) bds + && k <= n then (k, List.nth labs (k-1)) else @@ -597,13 +597,6 @@ let reduce_proj env sigma whfun whfun' c = | _ -> raise Redelimination in redrec c - -let dont_expose_case = function - | EvalVar _ | EvalRel _ | EvalEvar _ -> false - | EvalConst c -> - Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z) - false (ReductionBehaviour.get (ConstRef c)) - let whd_nothing_for_iota env sigma s = let rec whrec (x, stack as s) = match kind_of_term x with @@ -1212,9 +1205,10 @@ let one_step_reduce env sigma c = (ci,p,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (match reduce_fix (whd_construct_stack env) sigma fix stack with + (try match reduce_fix (whd_construct_stack env) sigma fix stack with | Reduced s' -> s' - | NotReducible -> raise NotStepReducible) + | NotReducible -> raise NotStepReducible + with Redelimination -> raise NotStepReducible) | _ when isEvalRef env x -> let ref,u = destEvalRefU x in (try diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5862a852..9f04faa8 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -15,7 +15,6 @@ open Term open Vars open Context open Environ -open Locus (* Sorts and sort family *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9f3efd72..2552c67e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -11,7 +11,6 @@ open Names open Term open Context open Environ -open Locus (** printers *) val print_sort : sorts -> std_ppcmds diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 817d6878..18e83056 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -14,7 +14,6 @@ open Term open Vars open Context open Evd -open Environ open Util open Typeclasses_errors open Libobject @@ -427,7 +426,6 @@ let add_class cl = cl.cl_projs -open Declarations (* * interface functions @@ -485,15 +483,6 @@ let is_instance = function is_class (IndRef ind) | _ -> false -let is_implicit_arg = function -| Evar_kinds.GoalEvar -> false -| _ -> true - (* match k with *) - (* ImplicitArg (ref, (n, id), b) -> true *) - (* | InternalHole -> true *) - (* | _ -> false *) - - (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to goals and do not need to be resolved when we have nested [resolve_all_evars] diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 1a0b6696..b3170b97 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -77,8 +77,6 @@ val instance_priority : instance -> int option val is_class : global_reference -> bool val is_instance : global_reference -> bool -val is_implicit_arg : Evar_kinds.t -> bool - (** Returns the term and type for the given instance of the parameters and fields of the type class. *) diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 4f88dd86..585f066d 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -10,7 +10,6 @@ open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index dd808771..7982fc85 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -10,7 +10,6 @@ open Loc open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames diff --git a/pretyping/typing.mli b/pretyping/typing.mli index c933106d..1f822f1a 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ open Evd diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 203b1ec8..01e1154e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -673,6 +673,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst, evarsubst) else error_cannot_unify_local curenv sigma (m,n,cM) + | Evar (evk,_ as ev), Evar (evk',_) + when not (Evar.Set.mem evk flags.frozen_evars) + && Evar.equal evk evk' -> + sigma,metasubst,((curenv,ev,cN)::evarsubst) | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar evk cN) -> @@ -1673,11 +1677,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = matchrec t with ex when precatchable_exception ex -> matchrec c) + | Lambda (_,t,c) -> (try matchrec t with ex when precatchable_exception ex -> matchrec c) + | _ -> error "Match_subterm")) in try matchrec cl @@ -1774,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = try (* This is up to delta for subterms w/o metas ... *) w_unify_to_subterm env evd ~flags (strip_outer_cast op,t) - with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op) + with PretypeError (env,_,NoOccurrenceFound _) when + allow_K || + (* w_unify_to_subterm does not go through evars, so + the next step, which was already in <= 8.4, is + needed at least for compatibility of rewrite *) + dependent op t -> (evd,op) in if not allow_K && (* ensure we found a different instance *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 19613c4e..8198db1b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -166,8 +166,15 @@ and nf_whd env whd typ = mkApp(cfd,args) | Vconstr_const n -> construct_of_constr_const env n typ | Vconstr_block b -> - let capp,ctyp = construct_of_constr_block env (btag b) typ in - let args = nf_bargs env b ctyp in + let tag = btag b in + let (tag,ofs) = + if tag = Cbytecodes.last_variant_tag then + match whd_val (bfield b 0) with + | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1) + | _ -> assert false + else (tag, 0) in + let capp,ctyp = construct_of_constr_block env tag typ in + let args = nf_bargs env b ofs ctyp in mkApp(capp,args) | Vatom_stk(Aid idkey, stk) -> let c,typ = constr_type_of_idkey env idkey in @@ -242,14 +249,14 @@ and nf_args env vargs t = t := subst1 c codom; c) in !t,args -and nf_bargs env b t = +and nf_bargs env b ofs t = let t = ref t in - let len = bsize b in + let len = bsize b - ofs in let args = Array.init len (fun i -> let _,dom,codom = decompose_prod env !t in - let c = nf_val env (bfield b i) dom in + let c = nf_val env (bfield b (i+ofs)) dom in t := subst1 c codom; c) in args |