Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 124 insertions, 100 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 38d1c70b..fc5e32cf 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1,12 +1,19 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reduction.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* Created under Benjamin Werner account by Bruno Barras to implement
+   a call-by-value conversion algorithm and a lazy reduction machine
+   with sharing, Nov 1996 *)
+(* Addition of zeta-reduction (let-in contraction) by Hugo Herbelin, Oct 2000 *)
+(* Irreversibility of opacity by Bruno Barras *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+(* Equal inductive types by Jacek Chrzaszcz as part of the module
+   system, Aug 2002 *)
 
 open Util
 open Names
@@ -190,9 +197,9 @@ let sort_cmp pb s0 s1 cuniv =
     | (_, _) -> raise NotConvertible
 
 
-let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty
+let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint
 
-let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty
+let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint
 
 let rec no_arg_available = function
   | [] -> true
@@ -232,14 +239,14 @@ let in_whnf (t,stk) =
     | FLOCKED -> assert false
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
-  eqappr cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+  eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Util.check_for_interrupt ();
   (* First head reduce both terms *)
-  let rec  whd_both (t1,stk1) (t2,stk2) =
+  let rec whd_both (t1,stk1) (t2,stk2) =
     let st1' = whd_stack (snd infos) t1 stk1 in
     let st2' = whd_stack (snd infos) t2 stk2 in
     (* Now, whd_stack on term2 might have modified st1 (due to sharing),
@@ -260,13 +267,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
 	       sort_cmp cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if n=m
-	       then convert_stacks infos lft1 lft2 v1 v2 cuniv
+	       then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if ev1=ev2 then
-          let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
-          convert_vect infos el1 el2
+          let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
+          convert_vect l2r infos el1 el2
             (Array.map (mk_clos env1) args1)
             (Array.map (mk_clos env2) args2) u1
         else raise NotConvertible
@@ -274,19 +281,19 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 index known to be bound to no constant *)
     | (FRel n, FRel m) ->
         if reloc_rel n el1 = reloc_rel m el2
-        then convert_stacks infos lft1 lft2 v1 v2 cuniv
+        then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
 	(try (* try first intensional equality *)
 	  if eq_table_key fl1 fl2
-          then convert_stacks infos lft1 lft2 v1 v2 cuniv
+          then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
           else raise NotConvertible
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
-            if Conv_oracle.oracle_order fl1 fl2 then
+            if Conv_oracle.oracle_order l2r fl1 fl2 then
               match unfold_reference infos fl1 with
                 | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
                 | None ->
@@ -300,79 +307,95 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
                     (match unfold_reference infos fl1 with
                     | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
 		    | None -> raise NotConvertible) in
-          eqappr cv_pb infos app1 app2 cuniv)
-
-    (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, _)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
-           | None -> raise NotConvertible)
-    | (_, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
-           | None -> raise NotConvertible)
+          eqappr cv_pb l2r infos app1 app2 cuniv)
 
     (* other constructors *)
     | (FLambda _, FLambda _) ->
+        (* Inconsistency: we tolerate that v1, v2 contain shift and update but
+           we throw them away *)
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly "conversion was given ill-typed terms (FLambda)";
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
-        let u1 = ccnv CONV infos el1 el2 ty1 ty2 cuniv in
-        ccnv CONV infos (el_lift el1) (el_lift el2) bd1 bd2 u1
+        let u1 = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+        ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 u1
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly "conversion was given ill-typed terms (FProd)";
 	(* Luo's system *)
-        let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
-        ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
+        let u1 = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
+        ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 u1
+
+    (* Eta-expansion on the fly *)
+    | (FLambda _, _) ->
+        if v1 <> [] then
+	  anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+	eqappr CONV l2r infos
+	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
+    | (_, FLambda _) ->
+        if v2 <> [] then
+	  anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+	eqappr CONV l2r infos
+	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
+
+    (* only one constant, defined var or defined rel *)
+    | (FFlex fl1, _)      ->
+        (match unfold_reference infos fl1 with
+           | Some def1 ->
+	       eqappr cv_pb l2r infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
+           | None -> raise NotConvertible)
+    | (_, FFlex fl2)      ->
+        (match unfold_reference infos fl2 with
+           | Some def2 ->
+	       eqappr cv_pb l2r infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
+           | None -> raise NotConvertible)
 
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
-     | (FInd ind1, FInd ind2) ->
-         if eq_ind ind1 ind2
-	 then
-           convert_stacks infos lft1 lft2 v1 v2 cuniv
-         else raise NotConvertible
-
-     | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
-	 if j1 = j2 && eq_ind ind1 ind2
-	 then
-           convert_stacks infos lft1 lft2 v1 v2 cuniv
-         else raise NotConvertible
-
-     | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
-	 if op1 = op2
-	 then
-	   let n = Array.length cl1 in
-           let fty1 = Array.map (mk_clos e1) tys1 in
-           let fty2 = Array.map (mk_clos e2) tys2 in
-           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
-           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-	   let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
-           let u2 =
-             convert_vect infos
-		 (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
-           convert_stacks infos lft1 lft2 v1 v2 u2
-         else raise NotConvertible
-
-     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
-         if op1 = op2
-         then
-	   let n = Array.length cl1 in
-           let fty1 = Array.map (mk_clos e1) tys1 in
-           let fty2 = Array.map (mk_clos e2) tys2 in
-           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
-           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-           let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
-           let u2 =
-	     convert_vect infos
-		 (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
-           convert_stacks infos lft1 lft2 v1 v2 u2
-         else raise NotConvertible
+    | (FInd ind1, FInd ind2) ->
+        if eq_ind ind1 ind2
+	then
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+        else raise NotConvertible
+
+    | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+	if j1 = j2 && eq_ind ind1 ind2
+	then
+          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+        else raise NotConvertible
+
+    | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
+	if op1 = op2
+	then
+	  let n = Array.length cl1 in
+          let fty1 = Array.map (mk_clos e1) tys1 in
+          let fty2 = Array.map (mk_clos e2) tys2 in
+          let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
+          let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
+	  let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+          let u2 =
+            convert_vect l2r infos
+	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
+          convert_stacks l2r infos lft1 lft2 v1 v2 u2
+        else raise NotConvertible
+
+    | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
+        if op1 = op2
+        then
+	  let n = Array.length cl1 in
+          let fty1 = Array.map (mk_clos e1) tys1 in
+          let fty2 = Array.map (mk_clos e2) tys2 in
+          let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
+          let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
+          let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+          let u2 =
+	    convert_vect l2r infos
+	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
+          convert_stacks l2r infos lft1 lft2 v1 v2 u2
+        else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
@@ -382,13 +405,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
      (* In all other cases, terms are not convertible *)
      | _ -> raise NotConvertible
 
-and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
-    (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
+    (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 c)
     (eq_ind)
     lft1 stk1 lft2 stk2 cuniv
 
-and convert_vect infos lft1 lft2 v1 v2 cuniv =
+and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
   let lv2 = Array.length v2 in
   if lv1 = lv2
@@ -396,62 +419,62 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
     let rec fold n univ =
       if n >= lv1 then univ
       else
-        let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in
+        let u1 = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) univ in
         fold (n+1) u1 in
     fold 0 cuniv
   else raise NotConvertible
 
-let clos_fconv trans cv_pb evars env t1 t2 =
+let clos_fconv trans cv_pb l2r evars env t1 t2 =
   let infos = trans, create_clos_infos ~evars betaiotazeta env in
-  ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
+  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) empty_constraint
 
-let trans_fconv reds cv_pb evars env t1 t2 =
-  if eq_constr t1 t2 then Constraint.empty
-  else clos_fconv reds cv_pb evars env t1 t2
+let trans_fconv reds cv_pb l2r evars env t1 t2 =
+  if eq_constr t1 t2 then empty_constraint
+  else clos_fconv reds cv_pb l2r evars env t1 t2
 
-let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
-let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars
-let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars
+let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None)
+let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars
+let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars
 
 let fconv = trans_fconv (Idpred.full, Cpred.full)
 
-let conv_cmp cv_pb = fconv cv_pb (fun _->None)
-let conv ?(evars=fun _->None) = fconv CONV evars
-let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
+let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
+let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
+let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars
 
-let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
+let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
   array_fold_left2_i
     (fun i c t1 t2 ->
       let c' =
-        try conv_leq ~evars env t1 t2
+        try conv_leq ~l2r ~evars env t1 t2
         with NotConvertible -> raise (NotConvertibleVect i) in
-      Constraint.union c c')
-    Constraint.empty
+      union_constraints c c')
+    empty_constraint
     v1
     v2
 
 (* option for conversion *)
 
-let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
+let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb (fun _->None) env t1 t2
+      fconv cv_pb false (fun _->None) env t1 t2
 
 
-let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
+let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
 
 let set_default_conv f = default_conv := f
 
-let default_conv cv_pb env t1 t2 =
+let default_conv cv_pb ?(l2r=false) env t1 t2 =
   try
-    !default_conv cv_pb env t1 t2
+    !default_conv ~l2r cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb (fun _->None) env t1 t2
+      fconv cv_pb false (fun _->None) env t1 t2
 
 let default_conv_leq = default_conv CUMUL
 (*
@@ -511,15 +534,16 @@ let dest_prod_assum env =
   in
   prodec_rec env empty_rel_context
 
+exception NotArity
+
 let dest_arity env c =
   let l, c = dest_prod_assum env c in
   match kind_of_term c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> raise NotArity
 
 let is_arity env c =
   try
     let _ = dest_arity env c in
     true
-  with UserError _ -> false
-
+  with NotArity -> false