Des progres dans l'integration

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@140 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 83 insertions, 77 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 07eb0fdc8..7959b5c7c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,172 +1,178 @@
-open Std;;
+
+(* $Id$ *)
+
+open Util;;
 open Generic;;
 open Names;;
 open Term;;
 open Reduction;;
-open Himsg;;
-open Machops;;
-open Mach;;
+open Environ;;
+open Typeops;;
+open Type_errors;;
 open Classops;;
 open Recordops;;
 open Evarconv;;
 
 (* Typing operations dealing with coercions *)
 
-let class_of1 sigma t = class_of sigma (nf_ise1 sigma t);;
+let class_of1 env sigma t = class_of sigma (nf_ise1 env sigma t);;
 
-let j_nf_ise sigma {_VAL=v;_TYPE=t;_KIND=k} =
-  {_VAL=nf_ise1 sigma v;_TYPE=nf_ise1 sigma t;_KIND=k}
-let jl_nf_ise sigma = List.map (j_nf_ise sigma)
+let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} =
+  {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k}
+let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
 
 (* Here, funj is a coercion therefore already typed in global context *)
-let apply_coercion_args argl funj =
+let apply_coercion_args env argl funj =
   let rec apply_rec acc typ = function
-      [] -> {_VAL=applist(j_val_only funj,argl);
-             _TYPE= typ;
-             _KIND = funj._KIND}
+      [] -> {uj_val=applist(j_val_only funj,argl);
+             uj_type= typ;
+             uj_kind = funj.uj_kind}
     | h::restl ->
  (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
-  match hnf_constr (Evd.mt_evd ()) typ with
+  match whd_betadeltaiota env Evd.empty typ with
      DOP2(Prod,c1,DLAM(_,c2)) -> (* Typage garanti par l'appel a app_coercion*)
        apply_rec (h::acc) (subst1 h c2) restl
     | _ -> anomaly "apply_coercion_args"
-  in apply_rec [] funj._TYPE argl;;
+  in apply_rec [] funj.uj_type argl;;
 
 (* appliquer le chemin de coercions p a` hj *)
 
-let apply_pcoercion p hj typ_cl =
+let apply_pcoercion env p hj typ_cl =
   if !compter then
     (nbpathc := !nbpathc +1; nbcoer := !nbcoer + (List.length p));
   try fst (List.fold_left
              (fun (ja,typ_cl) i -> 
                 let fv,b= coe_value i in
-                let argl = (class_args_of typ_cl)@[ja._VAL] in
-                let jres = apply_coercion_args argl fv in
-                  (if b then {_TYPE=jres._TYPE;_KIND=jres._KIND;_VAL=ja._VAL}
-                   else jres),jres._TYPE)
+                let argl = (class_args_of typ_cl)@[ja.uj_val] in
+                let jres = apply_coercion_args env argl fv in
+                  (if b then {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val}
+                   else jres),jres.uj_type)
              (hj,typ_cl) p)
   with _ -> failwith "apply_pcoercion"
 
-let inh_app_fun isevars env j = 
- match whd_betadeltaiota !isevars j._TYPE with
+let inh_app_fun env isevars j = 
+ match whd_betadeltaiota env !isevars j.uj_type with
     DOP2(Prod,_,DLAM(_,_)) -> j
    | _ ->
        (try
- 	let t,i1 = class_of1 !isevars j._TYPE in
+ 	let t,i1 = class_of1 env !isevars j.uj_type in
       	let p = lookup_path_to_fun_from i1 in
-        apply_pcoercion p j t
+        apply_pcoercion env p j t
       with _ -> j)
 (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *)
 
-let inh_tosort_force isevars env j =
-  let t,i1 = class_of1 !isevars j._TYPE in
+let inh_tosort_force env isevars j =
+  let t,i1 = class_of1 env !isevars j.uj_type in
   let p = lookup_path_to_sort_from i1 in
-  apply_pcoercion p j t 
+  apply_pcoercion env p j t 
 
-let inh_tosort isevars env j = 
-  let typ = whd_betadeltaiota !isevars j._TYPE in
+let inh_tosort env isevars j = 
+  let typ = whd_betadeltaiota env !isevars j.uj_type in
   match typ with
     DOP0(Sort(_)) -> j  (* idem inh_app_fun *)
-  | _ -> (try inh_tosort_force isevars env j with _ -> j)
+  | _ -> (try inh_tosort_force env isevars j with _ -> j)
 
-let inh_ass_of_j isevars env j =
-   let typ = whd_betadeltaiota !isevars j._TYPE in
+let inh_ass_of_j env isevars j =
+   let typ = whd_betadeltaiota env !isevars j.uj_type in
      match typ with
-         DOP0(Sort s) -> {body=j._VAL;typ=s}
+         DOP0(Sort s) -> {body=j.uj_val;typ=s}
        | _ ->
            (try
-             let j1 = inh_tosort_force isevars env j
-             in assumption_of_judgement !isevars env j1 
-           with _ -> error_assumption CCI env (nf_ise1 !isevars j._VAL))
+             let j1 = inh_tosort_force env isevars j
+             in assumption_of_judgment env !isevars j1 
+           with _ -> error_assumption CCI env (nf_ise1 env !isevars j.uj_val))
                    (* try ... with _ -> ... is BAD *)
 
-let inh_coerce_to1 isevars env c1 v t k =
- let t1,i1 = class_of1 !isevars c1 in
- let t2,i2 = class_of1 !isevars t in
+let inh_coerce_to1 env isevars c1 v t k =
+ let t1,i1 = class_of1 env !isevars c1 in
+ let t2,i2 = class_of1 env !isevars t in
  let p = lookup_path_between (i2,i1) in
- let hj = {_VAL=v;_TYPE=t;_KIND=k} in
- let hj' = apply_pcoercion p hj t2 in
- if the_conv_x_leq isevars env hj'._TYPE c1 then hj'
+ let hj = {uj_val=v;uj_type=t;uj_kind=k} in
+ let hj' = apply_pcoercion env p hj t2 in
+ if the_conv_x_leq env isevars hj'.uj_type c1 then hj'
  else failwith "inh_coerce_to"
 
-let inh_coerce_to isevars env c1 hj =
-  inh_coerce_to1 isevars env c1 hj._VAL hj._TYPE hj._KIND
+let inh_coerce_to env isevars c1 hj =
+  inh_coerce_to1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind
 
-let rec inh_conv_coerce1 isevars env c1 v t k =
- if the_conv_x_leq isevars env t c1 
- then {_VAL=v; _TYPE=t; _KIND=k}
- else try inh_coerce_to1 isevars env c1 v t k
+let rec inh_conv_coerce1 env isevars c1 v t k =
+ if the_conv_x_leq env isevars t c1 
+ then {uj_val=v; uj_type=t; uj_kind=k}
+ else try inh_coerce_to1 env isevars c1 v t k
  with _ ->  (* try ... with _ -> ... is BAD *)
 
-   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with
+(*   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
+   (match (whd_betadeltaiota env !isevars t,
+	   whd_betadeltaiota env !isevars c1) with
       | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> 
-          let v' = hnf_constr !isevars v in
+(*          let v' = hnf_constr !isevars v in*)
+          let v' = whd_betadeltaiota env !isevars v in
             if (match v' with
                     DOP2(Lambda,v1,DLAM(_,v2)) ->
-                      the_conv_x isevars env v1 u1 (* leq v1 u1? *)
+                      the_conv_x env isevars v1 u1 (* leq v1 u1? *)
                   |         _                -> false)
             then 
 	      let (x,v1,v2) = destLambda v' in
-(*              let jv1 = exemeta_rec def_vty_con isevars env v1 in 
-	      let assv1 = assumption_of_judgement !isevars env jv1 in
+(*              let jv1 = exemeta_rec def_vty_con env isevars v1 in 
+	      let assv1 = assumption_of_judgement env !isevars jv1 in
  *)
 	      let assv1 = outcast_type v1 in
-              let env1 = add_rel (x,assv1) env in
-              let h2 = inh_conv_coerce1 isevars env1 u2 v2 t2 (mkSort (sort_of !isevars env1 t2)) in
+              let env1 = push_rel (x,assv1) env in
+              let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 (mkSort (sort_of env !isevars1 t2)) in
               abs_rel !isevars x assv1 h2
             else 
 (*
-	      let ju1 = exemeta_rec def_vty_con isevars env u1 in 
-              let assu1 = assumption_of_judgement !isevars env ju1 in
+	      let ju1 = exemeta_rec def_vty_con env isevars u1 in 
+              let assu1 = assumption_of_judgement env !isevars ju1 in
  *)
 	      let assu1 = outcast_type u1 in
               let name = (match name with Anonymous -> Name (id_of_string "x")
                             | _ -> name) in
               let env1 = add_rel (name,assu1) env in
               let h1 = 
-		inh_conv_coerce1 isevars env1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in
-              let h2 = inh_conv_coerce1 isevars env1 u2  
-			 (DOPN(AppL,[|(lift 1 v);h1._VAL|])) 
-                         (subst1 h1._VAL t2) 
-			 (mkSort (sort_of !isevars env1 t2)) in
+		inh_conv_coerce1 env isevars1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in
+              let h2 = inh_conv_coerce1 env isevars1 u2  
+			 (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) 
+                         (subst1 h1.uj_val t2) 
+			 (mkSort (sort_of env !isevars1 t2)) in
 	      abs_rel !isevars name assu1 h2
       | _ -> failwith "inh_coerce_to")
             
-let inh_conv_coerce isevars env c1 hj =
-  inh_conv_coerce1 isevars env c1 hj._VAL hj._TYPE hj._KIND
+let inh_conv_coerce env isevars c1 hj =
+  inh_conv_coerce1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind
 
-let inh_cast_rel isevars env cj tj =
-    let cj' = (try inh_conv_coerce isevars env tj._VAL cj 
+let inh_cast_rel env isevars cj tj =
+    let cj' = (try inh_conv_coerce env isevars tj.uj_val cj 
               with Not_found | Failure _ -> error_actual_type CCI env 
 		  (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)) in
-      { _VAL = mkCast cj'._VAL tj._VAL;
-        _TYPE = tj._VAL;
-        _KIND = whd_betadeltaiota !isevars tj._TYPE}
+      { uj_val = mkCast cj'.uj_val tj.uj_val;
+        uj_type = tj.uj_val;
+        uj_kind = whd_betadeltaiota env !isevars tj.uj_type}
 
-let inh_apply_rel_list nocheck isevars env argjl funj vtcon =
+let inh_apply_rel_list nocheck env isevars argjl funj vtcon =
   let rec apply_rec acc typ = function
     [] -> let resj =
-      {_VAL=applist(j_val_only funj,List.map j_val_only (List.rev acc));
-       _TYPE= typ;
-       _KIND = funj._KIND} in
+      {uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc));
+       uj_type= typ;
+       uj_kind = funj.uj_kind} in
       (match vtcon with 
       | (_,(_,Some typ')) ->
-          (try inh_conv_coerce isevars env typ' resj
+          (try inh_conv_coerce env isevars typ' resj
           with _ -> resj) (* try ... with _ -> ... is BAD *)
       | (_,(_,None)) -> resj)
 
   | hj::restjl ->
-      match whd_betadeltaiota !isevars typ with
+      match whd_betadeltaiota env !isevars typ with
           DOP2(Prod,c1,DLAM(_,c2)) ->
             let hj' =
               if nocheck then hj else 
-	      (try inh_conv_coerce isevars env c1 hj 
+	      (try inh_conv_coerce env isevars c1 hj 
                with (Failure _ | Not_found) ->
                  error_cant_apply "Type Error" CCI env
 		   (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) in
-            apply_rec (hj'::acc) (subst1 hj'._VAL c2) restjl
+            apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl
         | _ ->
             error_cant_apply "Non-functional construction" CCI env
 	      (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)
-  in apply_rec [] funj._TYPE argjl
+  in apply_rec [] funj.uj_type argjl
 ;;