diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index ee4306b7d..586ad716d 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -24,13 +24,13 @@ open Termops module type S = sig (*s Coercions. *) - + (* [inh_app_fun env evd j] coerces [j] to a function; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a product; it returns [j] if no coercion is applicable *) val inh_app_fun : env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment - + (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a sort; it fails if no coercion is applicable *) @@ -42,24 +42,24 @@ module type S = sig 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_coerce_to_prod env evars t] coerces [t] to a product type *) val inh_coerce_to_prod : loc -> env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type - (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type + (* [inh_conv_coerce_to loc env evd 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 -> + 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 -> + 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; it fails if no coercion exists *) - val inh_conv_coerces_to : loc -> + val inh_conv_coerces_to : loc -> env -> evar_defs -> types -> type_constraint_type -> evar_defs (* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases @@ -81,11 +81,11 @@ module Default = struct | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *) match kind_of_term (whd_betadeltaiota env Evd.empty typ) with - | Prod (_,c1,c2) -> + | Prod (_,c1,c2) -> (* Typage garanti par l'appel à app_coercion*) apply_rec (h::acc) (subst1 h c2) restl | _ -> anomaly "apply_coercion_args" - in + in apply_rec [] funj.uj_type argl (* appliquer le chemin de coercions de patterns p *) @@ -107,21 +107,21 @@ module Default = struct (* appliquer le chemin de coercions p à hj *) let apply_coercion env sigma p hj typ_cl = - try + try fst (List.fold_left - (fun (ja,typ_cl) i -> + (fun (ja,typ_cl) i -> let fv,isid = coercion_value i in let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let jres = apply_coercion_args env argl fv in - (if isid then + (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } - else + else jres), jres.uj_type) (hj,typ_cl) p) with _ -> anomaly "apply_coercion" - let inh_app_fun env evd j = + let inh_app_fun env evd j = let t = whd_betadeltaiota env evd j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) @@ -132,7 +132,7 @@ module Default = struct let t,p = lookup_path_to_fun_from env ( evd) j.uj_type in (evd,apply_coercion env ( evd) p j t) - + let inh_app_fun env evd j = try inh_app_fun env evd j with Not_found -> @@ -142,7 +142,7 @@ module Default = struct let inh_tosort_force loc env evd j = try let t,p = lookup_path_to_sort_from env ( evd) j.uj_type in - let j1 = apply_coercion env ( evd) p j t in + let j1 = apply_coercion env ( evd) p j t in let j2 = on_judgment_type (whd_evar ( evd)) j1 in (evd,type_judgment env j2) with Not_found -> @@ -167,16 +167,16 @@ module Default = struct raise NoCoercion else let v', t' = - try + try let t2,t1,p = lookup_path_between env evd (t,c1) in match v with - Some v -> + Some v -> let j = apply_coercion env evd p {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t - with Not_found -> raise NoCoercion + with Not_found -> raise NoCoercion in try (the_conv_x_leq env t' c1 evd, v') with Reduction.NotConvertible -> raise NoCoercion @@ -190,12 +190,12 @@ module Default = struct kind_of_term (whd_betadeltaiota env evd t), kind_of_term (whd_betadeltaiota env evd c1) with - | Prod (name,t1,t2), Prod (_,u1,u2) -> + | 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 + let name = match name with | Anonymous -> Name (id_of_string "x") | _ -> name in let env1 = push_rel (name,None,u1) env in @@ -213,8 +213,8 @@ module Default = struct let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = match n with None -> - let (evd', val') = - try + let (evd', val') = + try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> let evd = saturate_evd env evd in @@ -230,19 +230,19 @@ module Default = struct 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 - let nabsinit, nabs = + (* Still problematic, as it changes unification + let nabsinit, nabs = match abs with None -> 0, 0 | Some (init, cur) -> init, cur in - try - let (rels, rng) = - (* a little more effort to get products is needed *) + try + let (rels, rng) = + (* a little more effort to get products is needed *) try decompose_prod_n nabs t - with _ -> + with _ -> if !Flags.debug then msg_warning (str "decompose_prod_n failed"); raise (Invalid_argument "Coercion.inh_conv_coerces_to") @@ -250,11 +250,11 @@ module Default = struct (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) if noccur_with_meta 0 (succ nabsinit) rng then ( - let env', t, t' = + let env', t, t' = let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in env', rng, lift nabs t' in - try + try pi1 (inh_conv_coerce_to_fail loc env' evd None t t') with NoCoercion -> evd) (* Maybe not enough information to unify *) |