diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 182 |
1 files changed, 102 insertions, 80 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6f594186..4665486f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -84,7 +84,7 @@ let occur_meta_or_undefined_evar evd c = | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with | Evar_defined c -> - occrec c; Array.iter occrec args + occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args | Evar_empty -> raise Occur) | _ -> Constr.iter occrec c in try occrec c; false with Occur | Not_found -> true @@ -189,18 +189,14 @@ let pose_all_metas_as_evars env evd t = let rec aux t = match EConstr.kind !evdref t with | Meta mv -> (match Evd.meta_opt_fvalue !evdref mv with - | Some ({rebus=c},_) -> EConstr.of_constr c + | Some ({rebus=c},_) -> c | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in - let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in - let ty = - if Flags.version_strictly_greater Flags.V8_6 - then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) - else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in + let ty = nf_betaiota env evd ty in let src = Evd.evar_source_of_meta mv !evdref in - let ev = Evarutil.e_new_evar env evdref ~src ty in - evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref; + let evd, ev = Evarutil.new_evar env !evdref ~src ty in + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd; ev) | _ -> EConstr.map !evdref aux t in @@ -399,8 +395,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with modulo_betaiota = false; } -let default_no_delta_unify_flags () = - let flags = default_no_delta_core_unify_flags () in { +let default_no_delta_unify_flags ts = + let flags = default_no_delta_core_unify_flags () in + let flags = { flags with + modulo_conv_on_closed_terms = Some ts; + modulo_delta_types = ts + } in + { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = flags; @@ -474,12 +475,8 @@ let expand_table_key env = function | RelKey _ -> None let unfold_projection env p stk = - (match try Some (lookup_projection p env) with Not_found -> None with - | Some pb -> - let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - p, Cst_stack.empty) in - s :: stk - | None -> assert false) + let s = Stack.Proj (p, Cst_stack.empty) in + s :: stk let expand_key ts env sigma = function | Some (IsKey k) -> Option.map EConstr.of_constr (expand_table_key env k) @@ -508,7 +505,7 @@ let key_of env sigma b flags f = match EConstr.kind sigma f with | Const (cst, u) when is_transparent env (ConstKey cst) && (Cpred.mem cst (snd flags.modulo_delta) - || Environ.is_projection cst env) -> + || Recordops.is_primitive_projection cst) -> let u = EInstance.kind sigma u in Some (IsKey (ConstKey (cst, u))) | Var id when is_transparent env (VarKey id) && @@ -562,16 +559,16 @@ let is_rigid_head sigma flags t = | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = - let open Universes in - Constraints.fold + let open UnivProblem in + Set.fold (fun c acc -> let c' = match c with (* Should we be forcing weak constraints? *) | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) | ULe _ | UEq _ -> c in - Constraints.add c' acc) - c Constraints.empty + Set.add c' acc) + c Set.empty let constr_cmp pb env sigma flags t u = let cstrs = @@ -580,16 +577,16 @@ let constr_cmp pb env sigma flags t u = in match cstrs with | Some cstrs -> - begin try Evd.add_universe_constraints sigma cstrs, true - with Univ.UniverseInconsistency _ -> sigma, false + begin try Some (Evd.add_universe_constraints sigma cstrs) + with Univ.UniverseInconsistency _ -> None | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true - with Univ.UniverseInconsistency _ -> sigma, false - else sigma, false + try Some (Evd.add_universe_constraints sigma (force_eqs cstrs)) + with Univ.UniverseInconsistency _ -> None + else None end | None -> - sigma, false + None let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state @@ -624,9 +621,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in - if b then sigma - else error_cannot_unify env sigma (m,n) + match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with + | Some sigma -> sigma + | None -> error_cannot_unify env sigma (m,n) else sigma @@ -652,10 +649,12 @@ let rec is_neutral env sigma ts t = let is_eta_constructor_app env sigma ts f l1 term = match EConstr.kind sigma f with - | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> + | Construct (((_, i as ind), j), u) when j == 1 -> + let open Declarations in let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && + let (_, projs, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term @@ -666,12 +665,12 @@ let eta_constructor_app env sigma f l1 term = match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) -> let mib = lookup_mind (fst ind) env in - (match mib.Declarations.mind_record with - | Some (Some (_, projs, _)) -> + (match get_projections env ind with + | Some projs -> let npars = mib.Declarations.mind_nparams in let pars, l1' = Array.chop npars l1 in let arg = Array.append pars [|term|] in - let l2 = Array.map (fun p -> mkApp (mkConstU (p,u), arg)) projs in + let l2 = Array.map (fun p -> mkApp (mkConstU (Projection.Repr.constant p,u), arg)) projs in l1', l2 | _ -> assert false) | _ -> assert false @@ -682,8 +681,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and cN = Evarutil.whd_head_evar sigma curn in let () = if !debug_unification then - Feedback.msg_debug (print_constr_env curenv sigma cM ++ str" ~= " ++ print_constr_env curenv sigma cN) - in + Feedback.msg_debug ( + Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++ + Termops.Internal.print_constr_env curenv sigma cN) + in match (EConstr.kind sigma cM, EConstr.kind sigma cN) with | Meta k1, Meta k2 -> if Int.equal k1 k2 then substn else @@ -699,7 +700,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ - when not (dependent sigma cM cN) (* helps early trying alternatives *) -> + when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -719,7 +720,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k - when not (dependent sigma cN cM) (* helps early trying alternatives *) -> + when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -741,11 +742,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb env sigma flags cM cN in - if b then - sigma',metasubst,evarsubst - else + begin match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> + sigma, metasubst, evarsubst + | None -> sigma,metasubst,((curenv,ev,cN)::evarsubst) + end | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar sigma evk cN) -> @@ -838,6 +840,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e with ex when precatchable_exception ex -> reduce curenvnb pb opt substn cM cN) + | Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + + | CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when + Int.equal i1 i2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + | App (f1,l1), _ when (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1 || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) -> @@ -923,9 +945,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb env sigma flags cM cN in - if b then (sigma', metas, evars) - else + match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> (sigma, metas, evars) + | None -> try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = @@ -982,12 +1004,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in - let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in - if b then Some (sigma, metasubst, evarsubst) - else - if is_ground_term sigma m1 && is_ground_term sigma n1 then - error_cannot_unify curenv sigma (cM,cN) - else None + match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with + | Some sigma -> + Some (sigma, metasubst, evarsubst) + | None -> + if is_ground_term sigma m1 && is_ground_term sigma n1 then + error_cannot_unify curenv sigma (cM,cN) + else None in match res with | Some substn -> substn @@ -1060,7 +1083,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (evd,t2::ks, m-1) else let mv = new_meta () in - let evd' = meta_declare mv (EConstr.Unsafe.to_constr (substl ks b)) evd in + let evd' = meta_declare mv (substl ks b) evd in (evd', mkMeta mv :: ks, m - 1)) (sigma,[],List.length bs) bs in @@ -1090,11 +1113,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e then None else - let sigma, b = match flags.modulo_conv_on_closed_terms with + let ans = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in - if b then Some sigma - else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with + match ans with + | Some sigma -> ans + | None -> + if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k | None,(dl_id, dl_k) -> @@ -1247,7 +1272,7 @@ let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in - let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in + let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in (evd',j'.uj_val) let w_coerce_to_type env evd c cty mvty = @@ -1359,11 +1384,11 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = if meta_defined evd mv then let {rebus=c'},(status',_) = meta_fvalue evd mv in let (take_left,st,(evd,metas',evars')) = - merge_instances env evd flags status' status (EConstr.of_constr c') c + merge_instances env evd flags status' status c' c in let evd' = if take_left then evd - else meta_reassign mv (EConstr.Unsafe.to_constr c,(st,TypeProcessed)) evd + else meta_reassign mv (c,(st,TypeProcessed)) evd in w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns else @@ -1372,7 +1397,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = if isMetaOf evd mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else - meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in + meta_assign mv (c,(status,TypeProcessed)) evd in w_merge_rec evd' (metas''@metas) evars'' eqns | [] -> (* Process type eqns *) @@ -1396,17 +1421,17 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags - (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in + (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' - then Evd.define sp (EConstr.Unsafe.to_constr c) evd''' - else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in + then Evd.define sp c evd''' + else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in let check_types evd = let metas = Evd.meta_list evd in let eqns = List.fold_left (fun acc (mv, b) -> match b with - | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, EConstr.of_constr t.rebus) :: acc + | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc | _ -> acc) [] metas in w_merge_rec evd [] [] eqns in @@ -1417,11 +1442,6 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = in if with_types then check_types res else res -let retract_coercible_metas evd = - let (metas, evd) = retract_coercible_metas evd in - let map (mv, c, st) = (mv, EConstr.of_constr c, st) in - (List.map map metas, evd) - let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in w_merge env true flags.merge_unify_flags (evd,metas,[]) @@ -1506,12 +1526,12 @@ let indirectly_dependent sigma c d decls = it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls + let open Context.Named.Declaration in + List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in - let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, nf_evar sigma c) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1589,8 +1609,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> - let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in - if b then Some (evd, c1, x) else raise (NotUnifiable None) + begin match infer_conv ~pb:CONV env evd c1 c2 with + | Some evd -> Some (evd, c1, x) + | None -> raise (NotUnifiable None) + end | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in @@ -1599,9 +1621,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in - let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + let c = applist (local_strong whd_meta sigma c, l) in + Some (sigma, c)) let make_eq_test env evd c = let out cstr = @@ -1908,10 +1929,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in - if not b then + match infer_conv ~pb:CUMUL env evd' predtyp typp with + | None -> error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; + | Some evd' -> w_merge env false flags.merge_unify_flags (evd',[p,pred,(Conv,TypeProcessed)],[]) |