Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg

5 files changed, 113 insertions, 72 deletions

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