From d74f1da437c214cc0c960e87e8bbf04dd214128e Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 10 Oct 2011 22:00:04 +0000 Subject: Passed conv_algo to evar_define and move call to solve_refl to evar_define so that it can recursively deal with evar/evar problems. Also, check_evar_instance now called after each instantiation. Also did a bit of file reformatting. The commit apparently induces a loss of some 0,4% on the compilation of the standard library. Maybe, introducing a heuristic to decide when to call check_evar_instance (which I guess is responsible for the overhead) might be a good thing to look at? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarutil.ml | 128 +++++++++++++++++++++++-------------------------- pretyping/evarutil.mli | 23 ++++----- pretyping/evd.ml | 6 +-- 3 files changed, 74 insertions(+), 83 deletions(-) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ab14495f6..b9f09509c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -347,7 +347,7 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty = evdref := evd'; ev -(* This assumes an evar with identity instance and generalizes it over only +(* This assumes an evar with identity instance and generalizes it over only the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = let evi = Evd.find sigma ev in @@ -379,15 +379,15 @@ let check_restricted_occur evd refine env filter constr = let rec aux k c = let c = whd_evar evd c in match kind_of_term c with - | Var id -> - let idx = list_try_find_i (fun i (id', _, _) -> if id' = id then i else raise (Failure "")) 0 env in + | Var id -> + let idx = list_try_find_i (fun i (id', _, _) -> if id' = id then i else raise (Failure "")) 0 env in if not filter.(idx) then if refine then - (filter.(idx) <- true; c) + (filter.(idx) <- true; c) else raise IllTypedFilter else c | _ -> map_constr_with_binders succ aux k c - in + in let res = aux 0 constr in Array.to_list filter, res @@ -466,24 +466,24 @@ let extend_evar env evdref k (evk1,args1) ty = let subfilter env ccl filter newfilter args = let vars = collect_vars ccl in let (filter, _, _, newargs) = - List.fold_left2 + List.fold_left2 (fun (filter, newl, args, newargs) oldf (n, _, _) -> if oldf then let a, oldargs = match args with hd :: tl -> hd, tl | _ -> assert false in - if Idset.mem n vars then + if Idset.mem n vars then (oldf :: filter, List.tl newl, oldargs, a :: newargs) else if List.hd newl then (true :: filter, List.tl newl, oldargs, a :: newargs) else (false :: filter, List.tl newl, oldargs, newargs) else (oldf :: filter, newl, args, newargs)) ([], newfilter, args, []) filter env in List.rev filter, List.rev newargs - + let restrict_upon_filter ?(refine=false) evd evi evk p args = let filter = evar_filter evi in let newfilter = List.map p args in let env = evar_unfiltered_env evi in let ccl = nf_evar evd evi.evar_concl in - let newfilter, newargs = + let newfilter, newargs = subfilter (named_context env) ccl filter newfilter args in if newfilter <> filter then @@ -753,7 +753,7 @@ let rec do_projection_effects define_fun env ty evd = function let subst = make_pure_subst evi argsv in let ty' = replace_vars subst evi.evar_concl in let ty' = whd_evar evd ty' in - if isEvar ty' then define_fun env (destEvar ty') ty evd else evd + if isEvar ty' then define_fun env evd (destEvar ty') ty else evd else evd @@ -940,7 +940,7 @@ let are_canonical_instances args1 args2 env = exception CannotProject of projectibility_status list -let is_variable_subst args = +let is_variable_subst args = array_for_all (fun c -> isRel c || isVar c) args let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,args2 as ev2) = @@ -951,7 +951,7 @@ let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,args2 as ev2) = let sign = evar_filtered_context (Evd.find evd evk2) in let subst = List.map (fun (id,_,_) -> mkVar id) sign in Evd.define evk2 (mkEvar(evk1,Array.of_list subst)) evd - else + else (* Only try pruning on variable substitutions, postpone otherwise. *) if is_variable_subst args1 && is_variable_subst args2 then let proj1 = array_map_to_list (invert_arg aliases 0 evd evk2 subst) args1 in @@ -977,6 +977,22 @@ let solve_evar_evar f env evd ev1 ev2 = let pb = (Reduction.CONV,env,mkEvar(ev1),mkEvar (ev2)) in add_conv_pb pb evd +type conv_fun = + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool + +let check_evar_instance evd evk1 body conv_algo = + let evi = Evd.find evd evk1 in + let evenv = evar_unfiltered_env evi in + (* FIXME: The body might be ill-typed when this is called from w_merge *) + let ty = + try Retyping.get_type_of evenv evd body + with _ -> error "Ill-typed evar instance" + in + let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in + if b then evd else + user_err_loc (fst (evar_source evk1 evd),"", + str "Unable to find a well-typed instantiation") + (* 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 @@ -1024,7 +1040,7 @@ exception NotInvertibleUsingOurAlgorithm of constr exception NotEnoughInformationToProgress exception OccurCheckIn of evar_map * constr -let rec invert_definition choose env evd (evk,argsv as ev) rhs = +let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = let aliases = make_alias_map env in let evdref = ref evd in let progress = ref false in @@ -1044,7 +1060,7 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = else raise (NotUniqueInType(find_solution_type (evar_env evi) sols)) in let ty = lazy (Retyping.get_type_of env !evdref t) in - let evd = do_projection_effects evar_define env ty !evdref p in + let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in evdref := evd; c with @@ -1079,7 +1095,7 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = (* Try to project (a restriction of) the right evar *) let eprojs' = effective_projections projs' in let evd,args' = - list_fold_map (instance_of_projection evar_define env' t) + list_fold_map (instance_of_projection (evar_define conv_algo) env' t) !evdref eprojs' in let evd,evk' = do_restrict_hyps evd evk' projs' in evdref := evd; @@ -1092,10 +1108,10 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = (try let evd = (* Try to project (a restriction of) the left evar ... *) - try solve_evar_evar_l2r evar_define env' !evdref ev'' ev' + try solve_evar_evar_l2r (evar_define conv_algo) env' !evdref ev'' ev' with CannotProject projs'' -> (* ... or postpone the problem *) - postpone_evar_evar env' !evdref projs'' ev'' projs' ev' + postpone_evar_evar env' evd projs'' ev'' projs' ev' in evdref := evd; evar'' @@ -1132,15 +1148,14 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = * context "hyps" and not referring to itself. *) -and occur_existential evm c = - let rec occrec c = match kind_of_term c with - | Evar (e, _) -> if not (is_defined evm e) then raise Occur - | _ -> iter_constr occrec c - in try occrec c; false with Occur -> true - -and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = +and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = + match kind_of_term rhs with + | Evar (evk2,argsv2 as ev2) -> + if evk = evk2 then solve_refl conv_algo env evd evk argsv argsv2 + else solve_evar_evar (evar_define conv_algo) env evd ev ev2 + | _ -> try - let (evd',body) = invert_definition choose env evd ev rhs in + let (evd',body) = invert_definition conv_algo choose env evd ev rhs in if occur_meta body then error "Meta cannot occur in evar body."; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) @@ -1163,7 +1178,8 @@ and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) - Evd.define evk body evd' + let evd' = Evd.define evk body evd' in + check_evar_instance evd' evk body conv_algo with | NotEnoughInformationToProgress -> postpone_evar_term env evd ev rhs @@ -1357,57 +1373,31 @@ let status_changed lev (pbty,_,t1,t2) = (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false) +let reconsider_conv_pbs conv_algo evd = + let (evd,pbs) = extract_changed_conv_pbs evd status_changed in + List.fold_left + (fun (evd,b as p) (pbty,env,t1,t2) -> + if b then conv_algo env evd pbty t1 t2 else p) (evd,true) + pbs + (* 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. *) -let check_evar_instance evd evk1 conv_algo = - let evi = Evd.find evd evk1 in - let evenv = evar_unfiltered_env evi in - let evc = nf_evar evd evi.evar_concl in - match evi.evar_body with - | Evar_defined body -> - (* FIXME: The body might be ill-typed when this is called from w_merge *) - let ty = - try Retyping.get_type_of evenv evd body - with _ -> error "Ill-typed evar instance" - in - let ty = nf_evar evd ty in - let evd,b = conv_algo evenv evd Reduction.CUMUL ty evc in - if b then evd else - user_err_loc (fst (evar_source evk1 evd),"", - str "Unable to find a well-typed instantiation") - | Evar_empty -> evd (* Resulted in a constraint *) - (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) - let evd = match kind_of_term t2 with - | Evar (evk2,args2 as ev2) -> - if evk1 = evk2 then - solve_refl conv_algo env evd evk1 args1 args2 - else - if pbty = None - then - solve_evar_evar - (fun env ex c evm -> - check_evar_instance (evar_define env ex c evm) (fst ex) conv_algo) - env evd ev1 ev2 - else if pbty = Some true then - add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd - else - add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd + let evd = + match pbty with + | Some true when isEvar t2 -> + add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd + | Some false when isEvar t2 -> + add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd | _ -> - let evd = evar_define ~choose env ev1 t2 evd in - check_evar_instance evd evk1 conv_algo - in - let (evd,pbs) = extract_changed_conv_pbs evd status_changed in - List.fold_left - (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then conv_algo env evd pbty t1 t2 else p) (evd,true) - pbs + evar_define conv_algo ~choose env evd ev1 t2 in + reconsider_conv_pbs conv_algo evd with e when precatchable_exception e -> (evd,false) @@ -1479,7 +1469,7 @@ let check_evars env initial_sigma sigma c = | Evar (evk,_ as ev) -> (match existential_opt_value sigma ev with | Some c -> proc_rec c - | None -> + | None -> if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk sigma in match k with @@ -1609,7 +1599,7 @@ let define_evar_as_sort evd (ev,args) = (* 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 evd = +let judge_of_new_Type evd = let evd', s = new_univ_variable evd in evd', Typeops.judge_of_type s diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index acf92915e..7c06d41c9 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -52,11 +52,15 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list (** {6 Instantiate evars} *) +type conv_fun = + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool + (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map +val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> + existential -> constr -> evar_map (** {6 Evars/Metas switching...} *) @@ -78,14 +82,11 @@ val whd_head_evar : evar_map -> constr -> constr val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool -val solve_refl : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) - -> env -> evar_map -> existential_key -> constr array -> constr array -> - evar_map -val solve_simple_eqn : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) - -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> - evar_map * bool +val solve_refl : conv_fun -> env -> evar_map -> + existential_key -> constr array -> constr array -> evar_map +val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> + bool option * existential * constr -> evar_map * bool +val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) @@ -202,6 +203,6 @@ val push_rel_context_to_named_context : Environ.env -> types -> val generalize_evar_over_rels : evar_map -> existential -> types * constr list -val check_evar_instance : evar_map -> existential_key -> - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) -> evar_map +val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> + evar_map diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 817ee9703..ac604466d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -825,9 +825,9 @@ let pr_evar_map_t depth sigma = in evs ++ svs ++ cs let print_env_short env = - let pr_body = function None -> mt () | Some b -> str " := " ++ print_constr b in - let pr_named_decl (n, b, _) = pr_id n ++ pr_body b in - let pr_rel_decl (n, b, _) = pr_name n ++ pr_body b in + let pr_body n = function None -> pr_name n | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in + let pr_named_decl (n, b, _) = pr_body (Name n) b in + let pr_rel_decl (n, b, _) = pr_body n b in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ prlist_with_sep pr_spc pr_named_decl nc ++ str "]" ++ spc () ++ -- cgit v1.2.3