(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* [] | x::l -> if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l) else x::filter_unique l (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) exception Uninstantiated_evar of existential_key let rec whd_ise sigma c = match kind_of_term c with | Evar (ev,args) when Evd.mem sigma ev -> if Evd.is_defined sigma ev then whd_ise sigma (existential_value sigma (ev,args)) else raise (Uninstantiated_evar ev) | _ -> c (* Expand evars, possibly in the head of an application *) let whd_castappevar_stack sigma c = let rec whrec (c, l as s) = match kind_of_term c with | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) | Cast (c,_,_) -> whrec (c, l) | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) | _ -> s in whrec (c, []) let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c) let nf_evar = Pretype_errors.nf_evar let j_nf_evar = Pretype_errors.j_nf_evar let jl_nf_evar = Pretype_errors.jl_nf_evar let jv_nf_evar = Pretype_errors.jv_nf_evar let tj_nf_evar = Pretype_errors.tj_nf_evar let nf_evar_info evc info = { evar_concl = Reductionops.nf_evar evc info.evar_concl; evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; evar_body = info.evar_body} let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty let nf_evar_defs isevars = Evd.evars_reset_evd (nf_evars (Evd.evars_of isevars)) isevars let nf_isevar isevars = nf_evar (Evd.evars_of isevars) let j_nf_isevar isevars = j_nf_evar (Evd.evars_of isevars) let jl_nf_isevar isevars = jl_nf_evar (Evd.evars_of isevars) let jv_nf_isevar isevars = jv_nf_evar (Evd.evars_of isevars) let tj_nf_isevar isevars = tj_nf_evar (Evd.evars_of isevars) (**********************) (* Creating new metas *) (**********************) (* Generator of metavariables *) let new_meta = let meta_ctr = ref 0 in fun () -> incr meta_ctr; !meta_ctr let mk_new_meta () = mkMeta(new_meta()) let collect_evars emap c = let rec collrec acc c = match kind_of_term c with | Evar (k,_) -> if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc else (* No recursion on the evar instantiation *) acc | _ -> fold_constr collrec acc c in list_uniquize (collrec [] c) let push_dependent_evars sigma emap = Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') -> List.fold_left (fun (sigma',emap') ev -> (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev)) (sigma',emap') (collect_evars emap' ccl)) emap (sigma,emap) (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in let change_exist evar = let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in let n = new_meta() in mkCast (mkMeta n, DEFAULTcast, ty) in let rec replace c = match kind_of_term c with Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev | _ -> map_constr replace c in (sigma', replace c) (* The list of non-instantiated existential declarations *) let non_instantiated sigma = let listev = to_list sigma in List.fold_left (fun l (ev,evd) -> if evd.evar_body = Evar_empty then ((ev,nf_evar_info sigma evd)::l) else l) [] listev (*************************************) (* Metas *) let meta_value evd mv = let rec valrec mv = try let b = meta_fvalue evd mv in instance (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus with Anomaly _ | Not_found -> mkMeta mv in valrec mv let meta_instance env b = let c_sigma = List.map (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) in instance c_sigma b.rebus let nf_meta env c = meta_instance env (mk_freelisted c) (**********************) (* Creating new evars *) (**********************) (* Generator of existential names *) let new_untyped_evar = let evar_ctr = ref 0 in fun () -> incr evar_ctr; existential_of_int !evar_ctr (*------------------------------------* * functional operations on evar sets * *------------------------------------*) (* All ids of sign must be distincts! *) let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance = let ctxt = named_context_of_val sign in assert (List.length instance = named_context_length ctxt); if not (list_distinct (ids_of_named_context ctxt)) then anomaly "new_evar_instance: two vars have the same name"; let newev = new_untyped_evar() in (evar_declare sign newev typ ~src:src evd, mkEvar (newev,Array.of_list instance)) let make_evar_instance_with_rel env = let n = rel_context_length (rel_context env) in let vars = fold_named_context (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*)) env ~init:[] in snd (fold_rel_context (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*))) env ~init:(n,vars)) let make_subst env args = snd (fold_named_context (fun env (id,b,c) (args,l) -> match b, args with | (* None *) _ , a::rest -> (rest, (id,a)::l) (* | Some _, _ -> g*) | _ -> anomaly "Instance does not match its signature") env ~init:(List.rev args,[])) (* [new_isevar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let push_rel_context_to_named_context env = let (subst,_,env) = Sign.fold_rel_context (fun (na,c,t) (subst,avoid,env) -> let na = if na = Anonymous then Name(id_of_string"_") else na in let id = next_name_away na avoid in ((mkVar id)::subst, id::avoid, push_named (id,option_map (substl subst) c, type_app (substl subst) t) env)) (rel_context env) ~init:([],ids_of_named_context (named_context env),env) in (subst, (named_context_val env)) let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ = let subst,sign = push_rel_context_to_named_context env in let typ' = substl subst typ in let instance = make_evar_instance_with_rel env in new_evar_instance sign evd typ' ~src:src instance (* The same using side-effect *) let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty = let (evd',ev) = new_evar !evd env ~src:src ty in evd := evd'; ev (*------------------------------------* * operations on the evar constraints * *------------------------------------*) (* Pb: defined Rels and Vars should not be considered as a pattern... *) let is_pattern inst = let rec is_hopat l = function [] -> true | t :: tl -> (isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in is_hopat [] (Array.to_list inst) let evar_well_typed_body evd ev evi body = try let env = evar_env evi in let ty = evi.evar_concl in Typing.check env (evars_of evd) body ty; true with e -> pperrnl (str "Ill-typed evar instantiation: " ++ fnl() ++ pr_evar_defs evd ++ fnl() ++ str "----> " ++ int ev ++ str " := " ++ print_constr body); false let strict_inverse = false let inverse_instance env isevars ev evi inst rhs = let subst = make_subst (evar_env evi) (Array.to_list inst) in let subst = List.map (fun (x,y) -> (y,mkVar x)) subst in let evd = ref isevars in let error () = error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in let rec subs rigid k t = match kind_of_term t with | Rel i -> if i<=k then t else (try List.assoc (mkRel (i-k)) subst with Not_found -> if rigid then error() else if strict_inverse then failwith "cannot solve pb yet" else t) | Var id -> (try List.assoc t subst with Not_found -> if rigid then error() else if not strict_inverse && List.exists (fun (id',_,_) -> id=id') (evar_context evi) then failwith "cannot solve pb yet" else t) | Evar (ev,args) -> if Evd.is_defined_evar !evd (ev,args) then subs rigid k (existential_value (evars_of !evd) (ev,args)) else let args' = Array.map (subs false k) args in mkEvar (ev,args') | _ -> map_constr_with_binders succ (subs rigid) k t in let body = subs true 0 (nf_evar (evars_of isevars) rhs) in (!evd,body) let is_defined_equation env evd (ev,inst) rhs = is_pattern inst && not (occur_evar ev rhs) && try let evi = Evd.find (evars_of evd) ev in let (evd',body) = inverse_instance env evd ev evi inst rhs in evar_well_typed_body evd' ev evi body with Failure _ -> false (* Redefines an evar with a smaller context (i.e. it may depend on less * variables) such that c becomes closed. * Example: in [x:?1; y:(list ?2)] x=y /\ x=(nil bool) * ?3 <-- ?1 no pb: env of ?3 is larger than ?1's * ?1 <-- (list ?2) pb: ?2 may depend on x, but not ?1. * What we do is that ?2 is defined by a new evar ?4 whose context will be * a prefix of ?2's env, included in ?1's env. *) let do_restrict_hyps evd ev args = let args = Array.to_list args in let evi = Evd.find (evars_of !evd) ev in let env = evar_env evi in let hyps = evar_context evi in let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in (* No care is taken in case the evar type uses vars filtered out! Is it important ? *) let nc = let env = Sign.fold_named_context push_named sign ~init:(reset_context env) in e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in evd := Evd.evar_define ev nc !evd; let (evn,_) = destEvar nc in mkEvar(evn,Array.of_list ncargs) let need_restriction isevars args = not (array_for_all closed0 args) (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times. *) (* Note: error_not_clean should not be an error: it simply means that the * conversion test that lead to the faulty call to [real_clean] should return * false. The problem is that we won't get the right error message. *) let real_clean env isevars ev evi args rhs = let evd = ref isevars in let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in let rec subs rigid k t = match kind_of_term t with | Rel i -> if i<=k then t else (try List.assoc (mkRel (i-k)) subst with Not_found -> t) | Evar (ev,args) -> if Evd.is_defined_evar !evd (ev,args) then subs rigid k (existential_value (evars_of !evd) (ev,args)) else let args' = Array.map (subs false k) args in if need_restriction !evd args' then do_restrict_hyps evd ev args' else mkEvar (ev,args') | Var id -> (try List.assoc t subst with Not_found -> if not rigid or List.exists (fun (id',_,_) -> id=id') (evar_context evi) then t else error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd)) | _ -> map_constr_with_binders succ (subs rigid) k t in let body = subs true 0 (nf_evar (evars_of isevars) rhs) in if not (closed0 body) then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd); (!evd,body) (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args) * ?sp [ sp.hyps \ args ] unifies to rhs * ?sp must be a closed term, not referring to itself. * Not so trivial because some terms of args may be terms that are not * variables. In this case, the non-var-or-Rels arguments are replaced * by . [clean_rhs] will ignore this part of the subtitution. * This leads to incompleteness (we don't deal with pbs that require * inference of dependent types), but it seems sensible. * * If after cleaning, some free vars still occur, the function [restrict_hyps] * tries to narrow the env of the evars that depend on Rels. * * If after that free Rels still occur it means that the instantiation * cannot be done, as in [x:?1; y:nat; z:(le y y)] x=z * ?1 would be instantiated by (le y y) but y is not in the scope of ?1 *) (* env needed for error messages... *) let evar_define env (ev,argsv) rhs isevars = if occur_evar ev rhs then error_occur_check env (evars_of isevars) ev rhs; let args = Array.to_list argsv in let evi = Evd.find (evars_of isevars) ev in (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev evi worklist rhs in if occur_meta body then error "Meta cannot occur in evar body" else (* needed only if an inferred type *) let body = refresh_universes body in (* Cannot strictly type instantiations since the unification algorithm * does not unifies applications from left to right. * e.g problem f x == g y yields x==y and f==g (in that order) * Another problem is that type variables are evars of type Type let _ = try let env = evar_env evi in let ty = evi.evar_concl in Typing.check env (evars_of isevars') body ty with e -> pperrnl (str "Ill-typed evar instantiation: " ++ fnl() ++ pr_evar_defs isevars' ++ fnl() ++ str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) let isevars'' = Evd.evar_define ev body isevars' in isevars'',[ev] (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars *) let has_undefined_evars isevars t = try let _ = local_strong (whd_ise (evars_of isevars)) t in false with Uninstantiated_evar _ -> true let is_ground_term isevars t = not (has_undefined_evars isevars t) let head_is_evar isevars = let rec hrec k = match kind_of_term k with | Evar n -> not (Evd.is_defined_evar isevars n) | App (f,_) -> hrec f | Cast (c,_,_) -> hrec c | _ -> false in hrec let rec is_eliminator c = match kind_of_term c with | App _ -> true | Case _ -> true | Cast (c,_,_) -> is_eliminator c | _ -> false let head_is_embedded_evar isevars c = (head_is_evar isevars c) & (is_eliminator c) let head_evar = let rec hrec c = match kind_of_term c with | Evar (ev,_) -> ev | Case (_,_,c,_) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c | _ -> failwith "headconstant" in hrec (* This code (i.e. solve_pb, etc.) takes a unification * problem, and tries to solve it. If it solves it, then it removes * all the conversion problems, and re-runs conversion on each one, in * the hopes that the new solution will aid in solving them. * * The kinds of problems it knows how to solve are those in which * the usable arguments of an existential var are all themselves * universal variables. * The solution to this problem is to do renaming for the Var's, * to make them match up with the Var's which are found in the * hyps of the existential, to do a "pop" for each Rel which is * not an argument of the existential, and a subst1 for each which * is, again, with the corresponding variable. This is done by * evar_define * * Thus, we take the arguments of the existential which we are about * to assign, and zip them with the identifiers in the hypotheses. * Then, we process all the Var's in the arguments, and sort the * Rel's into ascending order. Then, we just march up, doing * subst1's and pop's. * * NOTE: We can do this more efficiently for the relative arguments, * by building a long substituend by hand, but this is a pain in the * ass. *) let status_changed lev (pbty,t1,t2) = try List.mem (head_evar t1) lev or List.mem (head_evar t2) lev with Failure _ -> try List.mem (head_evar t2) lev with Failure _ -> false (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint * definitions. We try to unify the xi with the yi pairwise. The pairs * that don't unify are discarded (i.e. ?i is redefined so that it does not * depend on these args). *) let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then (isevars,[]) else let evd = Evd.find (evars_of isevars) ev in let hyps = evar_context evd in let (isevars',_,rsign) = array_fold_left2 (fun (isevars,sgn,rsgn) a1 a2 -> let (isevars',b) = conv_algo env isevars Reduction.CONV a1 a2 in if b then (isevars',List.tl sgn, add_named_decl (List.hd sgn) rsgn) else (isevars,List.tl sgn, rsgn)) (isevars,hyps,[]) argsv1 argsv2 in let nsign = List.rev rsign in let (evd',newev) = let env = Sign.fold_named_context push_named nsign ~init:(reset_context env) in new_evar isevars env ~src:(evar_source ev isevars) evd.evar_concl in let evd'' = Evd.evar_define ev newev evd' in evd'', [ev] (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None * if the problem couldn't be solved. *) (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = try let t2 = nf_evar (evars_of isevars) t2 in let (isevars,lsp) = match kind_of_term t2 with | Evar (n2,args2 as ev2) -> if n1 = n2 then solve_refl conv_algo env isevars n1 args1 args2 else (try evar_define env ev1 t2 isevars with e when precatchable_exception e -> evar_define env ev2 (mkEvar ev1) isevars) (* if Array.length args1 < Array.length args2 then evar_define env ev2 (mkEvar ev1) isevars else evar_define env ev1 t2 isevars*) | _ -> evar_define env ev1 t2 isevars in let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in List.fold_left (fun (isevars,b as p) (pbty,t1,t2) -> if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) pbs with e when precatchable_exception e -> (isevars,false) (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr type type_constraint = type_constraint_type option type val_constraint = constr option (* Old comment... * Basically, we have the following kind of constraints (in increasing * strength order): * (false,(None,None)) -> no constraint at all * (true,(None,None)) -> we must build a judgement which _TYPE is a kind * (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty * (_,(Some v,_)) -> we must build a judgement which _VAL is v * Maybe a concrete datatype would be easier to understand. * We differentiate (true,(None,None)) from (_,(None,Some Type)) * because otherwise Case(s) would be misled, as in * (n:nat) Case n of bool [_]nat end would infer the predicate Type instead * of Set. *) (* The empty type constraint *) let empty_tycon = None let mk_tycon_type c = (None, c) let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second is current abstraction *) (* Builds a type constraint *) let mk_tycon ty = Some (mk_tycon_type ty) let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty) (* Constrains the value of a type *) let empty_valcon = None (* Builds a value constraint *) let mk_valcon c = Some c (* Refining an evar to a product or a sort *) (* Declaring any type to be in the sort Type shouldn't be harmful since cumulativity now includes Prop and Set in Type... It is, but that's not too bad *) let define_evar_as_abstraction abs evd (ev,args) = let evi = Evd.find (evars_of evd) ev in let evenv = evar_env evi in let (evd1,dom) = new_evar evd evenv (new_Type()) in let nvar = next_ident_away (id_of_string "x") (ids_of_named_context (evar_context evi)) in let newenv = push_named (nvar, None, dom) evenv in let (evd2,rng) = new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in let prod = abs (Name nvar, dom, subst_var nvar rng) in let evd3 = Evd.evar_define ev prod evd2 in let evdom = fst (destEvar dom), args in let evrng = fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in (evd3,prod') let define_evar_as_arrow evd (ev,args) = define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args) let define_evar_as_lambda evd (ev,args) = define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args) let define_evar_as_sort isevars (ev,args) = let s = new_Type () in Evd.evar_define ev s isevars, destSort s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type constraint on its domain and codomain. If the input constraint is an evar instantiate it with the product of 2 new evars. *) let split_tycon loc env isevars tycon = let rec real_split c = let sigma = evars_of isevars in let t = whd_betadeltaiota env sigma c in match kind_of_term t with | Prod (na,dom,rng) -> isevars, (na, dom, rng) | Evar ev when not (Evd.is_defined_evar isevars ev) -> let (isevars',prod) = define_evar_as_arrow isevars ev in let (_,dom,rng) = destProd prod in isevars',(Anonymous, dom, rng) | _ -> error_not_product_loc loc env sigma c in match tycon with | None -> isevars,(Anonymous,None,None) | Some (abs, c) -> (match abs with None -> let isevars', (n, dom, rng) = real_split c in isevars', (n, mk_tycon dom, mk_tycon rng) | Some (init, cur) -> if cur = 0 then let isevars', (x, dom, rng) = real_split c in isevars, (Anonymous, Some (Some (init, 0), dom), Some (Some (init, 0), rng)) else isevars, (Anonymous, None, Some (Some (init, pred cur), c))) let valcon_of_tycon x = match x with | Some (None, t) -> Some t | _ -> None let lift_abstr_tycon_type n (abs, t) = match abs with None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction") | Some (init, abs) -> let abs' = abs + n in if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type") else (Some (init, abs'), t) let lift_tycon_type n (abs, t) = (abs, lift n t) let lift_tycon n = option_map (lift_tycon_type n) let pr_tycon_type env (abs, t) = match abs with None -> Termops.print_constr_env env t | Some (init, cur) -> str "Abstract (" ++ int init ++ str "," ++ int cur ++ str ") " ++ Termops.print_constr_env env t let pr_tycon env = function None -> str "None" | Some t -> pr_tycon_type env t