From 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 8 Sep 2008 00:15:04 +0200 Subject: Imported Upstream version 8.2~beta4.svn20080907+dfsg --- pretyping/classops.ml | 103 ++++++++++++++++++++++++++++++--------------- pretyping/classops.mli | 25 ++++++----- pretyping/coercion.ml | 33 ++++++--------- pretyping/reductionops.ml | 9 +++- pretyping/reductionops.mli | 15 ++++--- 5 files changed, 113 insertions(+), 72 deletions(-) (limited to 'pretyping') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b5a5709e..398da529 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: classops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Pp @@ -128,6 +128,10 @@ let class_exists cl = Bijint.mem cl !class_tab let class_info_from_index i = Bijint.map i !class_tab +let cl_fun_index = fst(class_info CL_FUN) + +let cl_sort_index = fst(class_info CL_SORT) + (* coercion_info : coe_typ -> coe_info_typ *) let coercion_info coe = Gmap.find coe !coercion_tab @@ -136,32 +140,10 @@ let coercion_exists coe = Gmap.mem coe !coercion_tab let coercion_params coe_info = coe_info.coe_param -let lookup_path_between (s,t) = - Gmap.find (s,t) !inheritance_graph - -let lookup_path_to_fun_from s = - lookup_path_between (s,fst(class_info CL_FUN)) +(* find_class_type : env -> evar_map -> constr -> cl_typ * int *) -let lookup_path_to_sort_from s = - lookup_path_between (s,fst(class_info CL_SORT)) - -let lookup_pattern_path_between (s,t) = - let l = Gmap.find (s,t) !inheritance_graph in - List.map - (fun coe -> - let c, _ = - Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty - coe.coe_value - in - match kind_of_term c with - | Construct cstr -> - (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) - | _ -> raise Not_found) l - -(* find_class_type : constr -> cl_typ * int *) - -let find_class_type t = - let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in +let find_class_type env sigma t = + let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in match kind_of_term t' with | Var id -> CL_SECVAR id, args | Const sp -> CL_CONST sp, args @@ -178,7 +160,7 @@ let subst_cl_typ subst ct = match ct with | CL_CONST kn -> let kn',t = subst_con subst kn in if kn' == kn then ct else - fst (find_class_type t) + fst (find_class_type (Global.env()) Evd.empty t) | CL_IND (kn,i) -> let kn' = subst_kn subst kn in if kn' == kn then ct else @@ -188,19 +170,17 @@ let subst_cl_typ subst ct = match ct with to declare any term as a coercion *) let subst_coe_typ subst t = fst (subst_global subst t) -(* classe d'un terme *) - (* class_of : Term.constr -> int *) let class_of env sigma t = let (t, n1, i, args) = try - let (cl,args) = find_class_type t in + let (cl,args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let (cl, args) = find_class_type t in + let (cl, args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, args) in @@ -208,7 +188,7 @@ let class_of env sigma t = let inductive_class_of ind = fst (class_info (CL_IND ind)) -let class_args_of c = snd (find_class_type c) +let class_args_of env sigma c = snd (find_class_type env sigma c) let string_of_class = function | CL_FUN -> "Funclass" @@ -222,6 +202,61 @@ let string_of_class = function let pr_class x = str (string_of_class x) +(* lookup paths *) + +let lookup_path_between_class (s,t) = + Gmap.find (s,t) !inheritance_graph + +let lookup_path_to_fun_from_class s = + lookup_path_between_class (s,cl_fun_index) + +let lookup_path_to_sort_from_class s = + lookup_path_between_class (s,cl_sort_index) + +(* advanced path lookup *) + +let apply_on_class_of env sigma t cont = + try + let (cl,args) = find_class_type env sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + if List.length args <> n1 then raise Not_found; + t, cont i + with Not_found -> + (* Is it worth to be more incremental on the delta steps? *) + let t = Tacred.hnf_constr env sigma t in + let (cl, args) = find_class_type env sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + if List.length args <> n1 then raise Not_found; + t, cont i + +let lookup_path_between env sigma (s,t) = + let (s,(t,p)) = + apply_on_class_of env sigma s (fun i -> + apply_on_class_of env sigma t (fun j -> + lookup_path_between_class (i,j))) in + (s,t,p) + +let lookup_path_to_fun_from env sigma s = + apply_on_class_of env sigma s lookup_path_to_fun_from_class + +let lookup_path_to_sort_from env sigma s = + apply_on_class_of env sigma s lookup_path_to_sort_from_class + +let get_coercion_constructor coe = + let c, _ = + Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value + in + match kind_of_term c with + | Construct cstr -> + (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) + | _ -> + raise Not_found + +let lookup_pattern_path_between (s,t) = + let i = inductive_class_of s in + let j = inductive_class_of t in + List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph) + (* coercion_value : coe_index -> unsafe_judgment * bool *) let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } = @@ -255,11 +290,11 @@ let add_coercion_in_graph (ic,source,target) = try if i=j then begin if different_class_params i j then begin - let _ = lookup_path_between ij in + let _ = lookup_path_between_class ij in ambig_paths := (ij,p)::!ambig_paths end end else begin - let _ = lookup_path_between (i,j) in + let _ = lookup_path_between_class (i,j) in ambig_paths := (ij,p)::!ambig_paths end; false diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 1436a11b..a76fe75c 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classops.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id: classops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*) (*i*) open Names @@ -52,17 +52,17 @@ val class_info : cl_typ -> (cl_index * cl_info_typ) val class_exists : cl_typ -> bool val class_info_from_index : cl_index -> cl_typ * cl_info_typ -(* [find_class_type c] returns the head reference of c and its +(* [find_class_type env sigma c] returns the head reference of [c] and its arguments *) -val find_class_type : constr -> cl_typ * constr list +val find_class_type : env -> evar_map -> types -> cl_typ * constr list (* raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> constr -> constr * cl_index +val class_of : env -> evar_map -> types -> types * cl_index (* raises [Not_found] if not mapped to a class *) val inductive_class_of : inductive -> cl_index -val class_args_of : constr -> constr list +val class_args_of : env -> evar_map -> types -> constr list (*s [declare_coercion] adds a coercion in the graph of coercion paths *) val declare_coercion : @@ -75,11 +75,16 @@ val coercion_exists : coe_typ -> bool val coercion_value : coe_index -> (unsafe_judgment * bool) (*s Lookup functions for coercion paths *) -val lookup_path_between : cl_index * cl_index -> inheritance_path -val lookup_path_to_fun_from : cl_index -> inheritance_path -val lookup_path_to_sort_from : cl_index -> inheritance_path -val lookup_pattern_path_between : - cl_index * cl_index -> (constructor * int) list +val lookup_path_between_class : cl_index * cl_index -> inheritance_path + +val lookup_path_between : env -> evar_map -> types * types -> + types * types * inheritance_path +val lookup_path_to_fun_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_path_to_sort_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_pattern_path_between : + inductive * inductive -> (constructor * int) list (*i Crade *) open Pp diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3074c4c4..73fcd0ea 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Names @@ -78,10 +78,6 @@ module Default = struct | App (f,l) -> mkApp (whd_evar sigma f,l) | _ -> whd_evar sigma t - let class_of1 env evd t = - let sigma = evars_of evd in - class_of env sigma (whd_app_evar sigma t) - (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function @@ -107,18 +103,16 @@ module Default = struct (* raise Not_found if no coercion found *) let inh_pattern_coerce_to loc pat ind1 ind2 = - let i1 = inductive_class_of ind1 in - let i2 = inductive_class_of ind2 in - let p = lookup_pattern_path_between (i1,i2) in + let p = lookup_pattern_path_between (ind1,ind2) in apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = + let apply_coercion env sigma p hj typ_cl = try fst (List.fold_left (fun (ja,typ_cl) i -> let fv,isid = coercion_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] 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 { uj_val = ja.uj_val; uj_type = jres.uj_type } @@ -137,16 +131,15 @@ module Default = struct (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env evd j.uj_type in - let p = lookup_path_to_fun_from i1 in - (evd,apply_coercion env p j t) + let t,p = + lookup_path_to_fun_from env (evars_of evd) j.uj_type in + (evd,apply_coercion env (evars_of evd) p j t) with Not_found -> (evd,j)) let inh_tosort_force loc env evd j = try - let t,i1 = class_of1 env evd j.uj_type in - let p = lookup_path_to_sort_from i1 in - let j1 = apply_coercion env p j t in + let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in + let j1 = apply_coercion env (evars_of evd) p j t in let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in (evd,type_judgment env j2) with Not_found -> @@ -173,12 +166,12 @@ module Default = struct else let v', t' = try - let t1,i1 = class_of1 env evd c1 in - let t2,i2 = class_of1 env evd t in - let p = lookup_path_between (i2,i1) in + let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in match v with Some v -> - let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in + let j = + apply_coercion env (evars_of 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 diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2f507318..21e881b9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: reductionops.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Pp open Util @@ -233,6 +233,7 @@ let evar = mkflags [fevar] let betaevar = mkflags [fevar; fbeta] let betaiota = mkflags [fiota; fbeta] let betaiotazeta = mkflags [fiota; fbeta;fzeta] +let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar] (* Contextual *) let delta = mkflags [fdelta;fevar] @@ -483,6 +484,12 @@ let whd_betaiotazeta_stack x = let whd_betaiotazeta x = app_stack (whd_betaiotazeta_state (x, empty_stack)) +let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar +let whd_betaiotazetaevar_stack env sigma x = + appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) +let whd_betaiotazetaevar env sigma x = + app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) + let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e let whd_betaiotaevar_stack env sigma x = appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack)) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1ac36b2a..c026d9fe 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: reductionops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*) (*i*) open Names @@ -98,6 +98,7 @@ val whd_evar : evar_map -> constr -> constr val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function +val whd_betaiotazetaevar : contextual_reduction_function val whd_betadeltaiota : contextual_reduction_function val whd_betadeltaiota_nolet : contextual_reduction_function val whd_betaetalet : local_reduction_function @@ -105,17 +106,17 @@ val whd_betalet : local_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function -val whd_betaiotazeta_stack : local_stack_reduction_function -val whd_betadeltaiota_stack : contextual_stack_reduction_function -val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function +val whd_betaiotazetaevar_stack : contextual_stack_reduction_function +val whd_betadeltaiota_stack : contextual_stack_reduction_function +val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function val whd_betaetalet_stack : local_stack_reduction_function val whd_betalet_stack : local_stack_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function -val whd_betaiotazeta_state : local_state_reduction_function -val whd_betadeltaiota_state : contextual_state_reduction_function -val whd_betadeltaiota_nolet_state : contextual_state_reduction_function +val whd_betaiotazetaevar_state : contextual_state_reduction_function +val whd_betadeltaiota_state : contextual_state_reduction_function +val whd_betadeltaiota_nolet_state : contextual_state_reduction_function val whd_betaetalet_state : local_state_reduction_function val whd_betalet_state : local_state_reduction_function -- cgit v1.2.3