From af354d63a814b0855eefda81852029d72b3544db Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 29 May 2006 19:59:11 +0000 Subject: The "clean integration of subtac" patch. Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cases.ml | 7 ++++--- pretyping/coercion.ml | 8 ++++++++ pretyping/coercion.mli | 8 +++++++- pretyping/detyping.ml | 2 +- pretyping/pretyping.ml | 51 +++++++++++++++++--------------------------------- pretyping/rawterm.ml | 6 +++++- pretyping/rawterm.mli | 6 +++++- 7 files changed, 47 insertions(+), 41 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7a77d6eabb..b3cff232b9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1482,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x = in decomp_block [] pred (tomatchl,arsign) -let prepare_predicate_from_tycon loc dep env isevars tomatchs c = +let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> let indf' = lift_inductive_family n indf in @@ -1594,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function (match tycon with | Some (None, t) -> let names,pred = - prepare_predicate_from_tycon loc false env isevars tomatchs t + prepare_predicate_from_tycon loc false env isevars tomatchs sign t in Some (build_initial_predicate false names pred) | _ -> None) @@ -1607,7 +1607,8 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in let _ = option_map (fun tycon -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon) + isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val + (lift_tycon_type (List.length arsign) tycon)) tycon in let predccl = (j_nf_isevar !isevars predcclj).uj_val in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 1b128e43a7..8a55a46d2e 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -35,6 +35,12 @@ module type S = sig type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + + (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type its base type (the notion depends on the coercion system) *) + val inh_coerce_to_base : loc -> + env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and @@ -143,6 +149,8 @@ module Default = struct | _ -> inh_tosort_force loc env isevars j + let inh_coerce_to_base loc env isevars j = (isevars, j) + let inh_coerce_to_fail env isevars c1 v t = let v', t' = try diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 667f207307..5476a4820c 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -33,13 +33,19 @@ module type S = sig type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + + (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type its base type (the notion depends on the coercion system) *) + val inh_coerce_to_base : loc -> + env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [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 - + (* [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; it fails if no coercion exists *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ec6edcbdfd..1fcc6d8b7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -374,7 +374,7 @@ let rec detype isgoal avoid env t = RVar (dl, id)) | Sort s -> RSort (dl,detype_sort s) | Cast (c1,k,c2) -> - RCast(dl,detype isgoal avoid env c1, k, + RCast(dl,detype isgoal avoid env c1, CastConv k, detype isgoal avoid env c2) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d1d30980b8..be24d22b59 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -363,17 +363,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon | RApp (loc,f,args) -> - let length = List.length args in - let ftycon = - match tycon with - None -> None - | Some (None, ty) -> mk_abstr_tycon length ty - | Some (Some (init, cur), ty) -> - Some (Some (length + init, length + cur), ty) - in let fj = pretype empty_tycon env isevars lvar f in let floc = loc_of_rawconstr f in - let rec apply_rec env n resj tycon = function + let rec apply_rec env n resj = function | [] -> resj | c::rest -> let argloc = loc_of_rawconstr c in @@ -384,33 +376,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct let hj = pretype (mk_tycon c1) env isevars lvar c in let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in let typ' = nf_isevar !isevars typ in - let tycon = - option_map - (fun (abs, ty) -> - match abs with - None -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' - (abs, ty); - (abs, ty) - | Some (init, cur) -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' - (abs, ty); - (Some (init, pred cur), ty)) - tycon - in apply_rec env (n+1) { uj_val = nf_isevar !isevars value; - uj_type = nf_isevar !isevars typ' } - (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest - + uj_type = typ' } + rest | _ -> let hj = pretype empty_tycon env isevars lvar c in error_cant_apply_not_functional_loc (join_loc floc argloc) env (evars_of !isevars) resj [hj] in - let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in - let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in + let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in let resj = match kind_of_term resj.uj_val with | App (f,args) when isInd f -> @@ -590,12 +566,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct tycon env (* loc *) (po,tml,eqns) | RCast(loc,c,k,t) -> - let tj = pretype_type empty_valcon env isevars lvar t in - let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in - (* User Casts are for helping pretyping, experimentally not to be kept*) - (* ... except for Correctness *) - let v = mkCast (cj.uj_val, k, tj.utj_val) in - let cj = { uj_val = v; uj_type = tj.utj_val } in + let cj = + match k with + CastCoerce -> + let cj = pretype empty_tycon env isevars lvar c in + evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj + | CastConv k -> + let tj = pretype_type empty_valcon env isevars lvar t in + let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in + (* User Casts are for helping pretyping, experimentally not to be kept*) + (* ... except for Correctness *) + let v = mkCast (cj.uj_val, k, tj.utj_val) in + { uj_val = v; uj_type = tj.utj_val } + in inh_conv_coerce_to_tycon loc env isevars cj tycon | RDynamic (loc,d) -> diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index d536adcb0e..480ee13b2b 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -47,6 +47,10 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings +type cast_type = + | CastConv of cast_kind + | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) + type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -64,7 +68,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * cast_kind * rawconstr + | RCast of loc * rawconstr * cast_type * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index d85ca0158a..d64ba03a79 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -44,6 +44,10 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings +type cast_type = + | CastConv of cast_kind + | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) + type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -61,7 +65,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * cast_kind * rawconstr + | RCast of loc * rawconstr * cast_type * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr -- cgit v1.2.3