diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 8 | ||||
| -rw-r--r-- | pretyping/classops.mli | 3 | ||||
| -rw-r--r-- | pretyping/clenv.ml | 44 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 95 | ||||
| -rw-r--r-- | pretyping/coercion.mli | 3 | ||||
| -rw-r--r-- | pretyping/evd.ml | 24 | ||||
| -rw-r--r-- | pretyping/evd.mli | 18 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
| -rw-r--r-- | pretyping/unification.ml | 52 | ||||
| -rw-r--r-- | pretyping/unification.mli | 5 |
10 files changed, 139 insertions, 119 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5b0c2eb367..0d7e3d611c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -44,7 +44,7 @@ type coe_typ = global_reference type coe_info_typ = { coe_value : constr; coe_type : types; - coe_strength : strength; + coe_strength : locality; coe_is_identity : bool; coe_param : int } @@ -290,7 +290,7 @@ let add_coercion_in_graph (ic,source,target) = if (!ambig_paths <> []) && is_verbose () then ppnl (message_ambig !ambig_paths) -type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int +type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int (* Calcul de l'arit้ d'une classe *) @@ -304,7 +304,7 @@ let class_params = function | CL_SECVAR sp -> reference_arity_length (VarRef sp) | CL_IND sp -> reference_arity_length (IndRef sp) -(* add_class : cl_typ -> strength option -> bool -> unit *) +(* add_class : cl_typ -> locality_flag option -> bool -> unit *) let add_class cl = add_new_class cl { cl_param = class_params cl } @@ -366,6 +366,8 @@ let coercion_identity v = v.coe_is_identity (* For printing purpose *) let get_coercion_value v = v.coe_value +let pr_cl_index n = int n + let classes () = Bijint.dom !class_tab let coercions () = Gmap.rng !coercion_tab let inheritance_graph () = Gmap.to_list !inheritance_graph diff --git a/pretyping/classops.mli b/pretyping/classops.mli index dd51ee970a..c1a62b34fd 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -66,7 +66,7 @@ val class_args_of : constr -> constr list (*s [declare_coercion] adds a coercion in the graph of coercion paths *) val declare_coercion : - coe_typ -> strength -> isid:bool -> + coe_typ -> locality -> isid:bool -> src:cl_typ -> target:cl_typ -> params:int -> unit (*s Access to coercions infos *) @@ -90,6 +90,7 @@ val install_path_printer : (*s This is for printing purpose *) val string_of_class : cl_typ -> string val pr_class : cl_typ -> std_ppcmds +val pr_cl_index : cl_index -> std_ppcmds val get_coercion_value : coe_index -> constr val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list val classes : unit -> cl_typ list diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index ed9d779ad7..e7423c748b 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -28,15 +28,7 @@ open Unification open Mod_subst open Coercion.Default -(* *) -let w_coerce env c ctyp target evd = - try - let j = make_judge c ctyp in - let tycon = mk_tycon_type target in - let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in - (evd',j'.uj_val) - with e when precatchable_exception e -> - evd,c +(* Abbreviations *) let pf_env gls = Global.env_of_context gls.it.evar_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c @@ -398,36 +390,24 @@ let error_already_defined b = anomalylabstrm "" (str "Position " ++ int n ++ str" already defined") -let rec similar_type_shapes t u = - let t,_ = decompose_app t and u,_ = decompose_app u in - match kind_of_term t, kind_of_term u with - | Prod (_,t1,t2), Prod (_,u1,u2) -> similar_type_shapes t2 u2 - | Const cst, Const cst' -> cst = cst' - | Var id, Var id' -> id = id' - | Ind ind, Ind ind' -> ind = ind' - | Rel n, Rel n' -> n = n' - | Sort s, Sort s' -> family_of_sort s = family_of_sort s' - | Case (_,_,c,_), Case (_,_,c',_) -> similar_type_shapes c c' - | _ -> false - -let clenv_unify_similar_types clenv c t u = - if occur_meta u then - if similar_type_shapes t u then - try TypeProcessed, clenv_unify true CUMUL t u clenv, c - with e when precatchable_exception e -> TypeNotProcessed, clenv, c - else - CoerceToType, clenv, c +let clenv_unify_binding_type clenv c t u = + if isMeta (fst (whd_stack u)) then + (* Not enough information to know if some subtyping is needed *) + CoerceToType, clenv, c else - let evd,c = w_coerce (cl_env clenv) c t u clenv.evd in - TypeProcessed, { clenv with evd = evd }, c + (* Enough information so as to try a coercion now *) + try + let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in + TypeProcessed, { clenv with evd = evd }, c + with e when precatchable_exception e -> + TypeNotProcessed, clenv, c let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in let c_typ = clenv_hnf_constr clenv' c_typ in - let status,clenv'',c = clenv_unify_similar_types clenv' c c_typ k_typ in -(* let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*) + let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } let clenv_match_args bl clenv = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 729bd84f1f..bd023721ae 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -48,7 +48,9 @@ module type S = sig [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment - + + val inh_conv_coerce_rigid_to : loc -> + env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; @@ -158,7 +160,11 @@ module Default = struct let inh_coerce_to_base loc env evd j = (evd, j) - let inh_coerce_to_fail env evd c1 v t = + let inh_coerce_to_fail env evd rigidonly v c1 t = + if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) + then + raise NoCoercion + else let v', t' = try let t1,i1 = class_of1 env evd c1 in @@ -171,77 +177,44 @@ module Default = struct | None -> None, t with Not_found -> raise NoCoercion in - try (the_conv_x_leq env t' c1 evd, v', t') + try (the_conv_x_leq env t' c1 evd, v') with Reduction.NotConvertible -> raise NoCoercion - let rec inh_conv_coerce_to_fail loc env evd v t c1 = - try (the_conv_x_leq env t c1 evd, v, t) + let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = + try (the_conv_x_leq env t c1 evd, v) with Reduction.NotConvertible -> - try inh_coerce_to_fail env evd c1 v t + try inh_coerce_to_fail env evd rigidonly v c1 t with NoCoercion -> match kind_of_term (whd_betadeltaiota env (evars_of evd) t), kind_of_term (whd_betadeltaiota env (evars_of evd) c1) with - | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in - let (evd',b) = - match v' with - | Some v' -> - (match kind_of_term v' with - | Lambda (x,v1,v2) -> - (* sous-typage non contravariant: pas de "leq v1 u1" *) - (try the_conv_x env v1 u1 evd, Some (x, v1, v2) - with Reduction.NotConvertible -> (evd, None)) - | _ -> (evd, None)) - | None -> (evd, None) - in - (match b with - | Some (x, v1, v2) -> - let env1 = push_rel (x,None,v1) env in - let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' - (Some v2) t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', - mkProd (x, v1, t2')) - | None -> - (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) - (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) - (* has type (name:u1)u2 (with v' recursively obtained) *) - let name = match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name - in - let env1 = push_rel (name,None,u1) env in - let (evd', v1', t1') = - inh_conv_coerce_to_fail loc env1 evd - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) - in - let (evd'', v2', t2') = - let v2 = - match v with - | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1' - | None -> None - and evd', t2 = - match v1' with - | Some v1' -> evd', subst_term v1' t2 - | None -> - let evd', ev = - new_evar evd' env ~src:(loc, InternalHole) t1' in - evd', subst_term ev t2 - in - inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 - in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2', - mkProd (name, u1, t2'))) + | Prod (name,t1,t2), Prod (_,u1,u2) -> + (* Conversion did not work, we may succeed with a coercion. *) + (* We eta-expand (hence possibly modifying the original term!) *) + (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) + (* has type forall (x:u1), u2 (with v' recursively obtained) *) + let name = match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name in + let env1 = push_rel (name,None,u1) env in + let (evd', v1) = + inh_conv_coerce_to_fail loc env1 evd rigidonly + (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in + let v1 = Option.get v1 in + let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in + let t2 = subst_term v1 t2 in + let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to loc env evd cj (n, t) = + let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = match n with None -> - let (evd', val', type') = + let (evd', val') = try - inh_conv_coerce_to_fail loc env evd (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> let sigma = evars_of evd in error_actual_type_loc loc env sigma cj t @@ -249,6 +222,10 @@ module Default = struct let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (evd, cj) + + let inh_conv_coerce_to = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerces_to loc env (evd : evar_defs) t (abs, t') = evd (* Still problematic, as it changes unification diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 5476a4820c..00735d8746 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -45,6 +45,9 @@ module type S = sig [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment + + val inh_conv_coerce_rigid_to : loc -> + env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 3adf749f07..ddc3654dc7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -341,7 +341,7 @@ let mk_freelisted c = let map_fl f cfl = { cfl with rebus=f cfl.rebus } -(* Status of an instance wrt to the meta it solves: +(* Status of an instance found by unification wrt to the meta it solves: - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) - a term that can be eta-expanded n times while still being a solution @@ -351,9 +351,24 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus } type instance_constraint = IsSuperType | IsSubType | ConvUpToEta of int | UserGiven +(* Status of the unification of the type of an instance against the type of + the meta it instantiates: + - CoerceToType means that the unification of types has not been done + and that a coercion can still be inserted: the meta should not be + substituted freely (this happens for instance given via the + "with" binding clause). + - TypeProcessed means that the information obtainable from the + unification of types has been extracted. + - TypeNotProcessed means that the unification of types has not been + done but it is known that no coercion may be inserted: the meta + can be substituted freely. +*) + type instance_typing_status = CoerceToType | TypeNotProcessed | TypeProcessed +(* Status of an instance together with the status of its type unification *) + type instance_status = instance_constraint * instance_typing_status (* Clausal environments *) @@ -519,6 +534,13 @@ let metas_of evd = | (n,Cltyp (_,typ)) -> (n,typ.rebus)) (meta_list evd) +let map_metas_fvalue f evd = + { evd with metas = + Metamap.map + (function + | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ) + | x -> x) evd.metas } + let meta_opt_fvalue evd mv = match Metamap.find mv evd.metas with | Clval(_,b,_) -> Some b diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 352d3021d9..71c6bb0dc3 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -122,11 +122,28 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted type instance_constraint = IsSuperType | IsSubType | ConvUpToEta of int | UserGiven +(* Status of the unification of the type of an instance against the type of + the meta it instantiates: + - CoerceToType means that the unification of types has not been done + and that a coercion can still be inserted: the meta should not be + substituted freely (this happens for instance given via the + "with" binding clause). + - TypeProcessed means that the information obtainable from the + unification of types has been extracted. + - TypeNotProcessed means that the unification of types has not been + done but it is known that no coercion may be inserted: the meta + can be substituted freely. +*) + type instance_typing_status = CoerceToType | TypeNotProcessed | TypeProcessed +(* Status of an instance together with the status of its type unification *) + type instance_status = instance_constraint * instance_typing_status +(* Clausal environments *) + type clbinding = | Cltyp of name * constr freelisted | Clval of name * (constr freelisted * instance_status) * constr freelisted @@ -198,6 +215,7 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs val undefined_metas : evar_defs -> metavariable list val metas_of : evar_defs -> metamap +val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs type metabinding = metavariable * constr * instance_status diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e118a659e9..e825b3f488 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -946,7 +946,7 @@ let meta_reducible_instance evd b = (match try let g,s = List.assoc m metas in - if isConstruct g or s = TypeProcessed then Some g else None + if isConstruct g or s <> CoerceToType then Some g else None with Not_found -> None with | Some g -> irec (mkCase (ci,p,g,bl)) @@ -956,13 +956,13 @@ let meta_reducible_instance evd b = (match try let g,s = List.assoc m metas in - if isLambda g or s = TypeProcessed then Some g else None + if isLambda g or s <> CoerceToType then Some g else None with Not_found -> None with | Some g -> irec (mkApp (g,l)) | None -> mkApp (f,Array.map irec l)) | Meta m -> - (try let g,s = List.assoc m metas in if s=TypeProcessed then irec g else u + (try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u with Not_found -> u) | _ -> map_constr irec u in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c5e9dff8b4..b140ad51aa 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -24,6 +24,7 @@ open Pattern open Evarutil open Pretype_errors open Retyping +open Coercion.Default (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) @@ -380,14 +381,39 @@ let is_mimick_head f = (Const _|Var _|Rel _|Construct _|Ind _) -> true | _ -> false -let w_coerce env c ctyp target evd = +let pose_all_metas_as_evars env evd t = + let evdref = ref evd in + let rec aux t = match kind_of_term t with + | Meta mv -> + (match Evd.meta_opt_fvalue !evdref mv with + | Some ({rebus=c},_) -> c + | None -> + let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in + let ty = if mvs = Evd.Metaset.empty then ty else aux ty in + let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in + evdref := meta_assign mv (ev,(ConvUpToEta 0,TypeNotProcessed)) !evdref; + ev) + | _ -> + map_constr aux t in + let c = aux t in + (* side-effect *) + (!evdref, c) + +let w_coerce_to_type env evd c cty mvty = try - let j = make_judge c ctyp in - let tycon = mk_tycon_type target in - let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j tycon in + let j = make_judge c cty in + let evd,mvty = pose_all_metas_as_evars env evd mvty in + let tycon = mk_tycon_type mvty in + let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in + let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in (evd',j'.uj_val) with e when precatchable_exception e -> - evd,c + (evd,c) + +let w_coerce env evd mv c = + let cty = get_type_of env (evars_of evd) c in + let mvty = Typing.meta_type evd mv in + w_coerce_to_type env evd c cty mvty let unify_to_type env evd flags c u = let sigma = evars_of evd in @@ -398,20 +424,6 @@ let unify_to_type env evd flags c u = try unify_0 env sigma Cumul flags t u with e when precatchable_exception e -> ([],[]) -let coerce_to_type env evd c u = - let c = refresh_universes c in - let t = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in - w_coerce env c t u evd - -let unify_or_coerce_type env evd flags mv c = - let mvty = Typing.meta_type evd mv in - (* nf_betaiota was before in type_of - useful to reduce - types like (x:A)([x]P u) *) - if occur_meta mvty then - (evd,c),unify_to_type env evd flags c mvty - else - coerce_to_type env evd c mvty,([],[]) - let unify_type env evd flags mv c = let mvty = Typing.meta_type evd mv in if occur_meta mvty then @@ -471,7 +483,7 @@ let w_merge env with_types flags metas evars evd = if with_types & to_type <> TypeProcessed then if to_type = CoerceToType then (* Some coercion may have to be inserted *) - (unify_or_coerce_type env evd flags mv c,[]) + (w_coerce env evd mv c,([],[])),[] else (* No coercion needed: delay the unification of types *) ((evd,c),([],[])),(mv,c)::eqns diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 9156623f50..1b8f9ccd8b 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -35,6 +35,11 @@ val w_unify_to_subterm : val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs +(* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type + [ctyp] so that its gets type [typ]; [typ] may contain metavariables *) +val w_coerce_to_type : env -> evar_defs -> constr -> types -> types -> + evar_defs * constr + (*i This should be in another module i*) (* [abstract_list_all env evd t c l] *) |