diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 7 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 8 | ||||
| -rw-r--r-- | pretyping/coercion.mli | 8 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 51 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 6 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 6 |
7 files changed, 47 insertions, 41 deletions
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 |