Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 106 insertions, 71 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 97cd4c00d7..61051c001d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -21,6 +21,7 @@ open CErrors
 open Util
 open Names
 open Constr
+open Declarations
 open Vars
 open Environ
 open CClosure
@@ -59,16 +60,23 @@ let compare_stack_shape stk1 stk2 =
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
+    | Zprimitive(op1,_,rargs1, _kargs1)::s1, Zprimitive(op2,_,rargs2, _kargs2)::s2 ->
+        bal=0 && op1=op2 && List.length rargs1=List.length rargs2 &&
+        compare_rec 0 s1 s2
     | [], _ :: _
-    | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false
+    | (Zproj _ | ZcaseT _ | Zfix _ | Zprimitive _) :: _, _ -> false
   in
   compare_rec 0 stk1 stk2
 
+type lft_fconstr = lift * fconstr
+
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
   | Zlproj of Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * constr * constr array * fconstr subs
+  | Zlprimitive of
+     CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args
 and lft_constr_stack = lft_constr_stack_elt list
 
 let rec zlapp v = function
@@ -102,7 +110,10 @@ let pure_stack lfts stk =
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
             | (ZcaseT(ci,p,br,e),(l,pstk)) ->
-                (l,Zlcase(ci,l,p,br,e)::pstk))
+                (l,Zlcase(ci,l,p,br,e)::pstk)
+            | (Zprimitive(op,c,rargs,kargs),(l,pstk)) ->
+                (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs,
+                            List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk))
   in
   snd (pure_rec lfts stk)
 
@@ -127,10 +138,10 @@ let nf_betaiota env t =
 let whd_betaiotazeta env x =
   match kind x with
   | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _) -> x
+       Prod _|Lambda _|Fix _|CoFix _|Int _) -> x
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
+      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ -> x
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
@@ -141,10 +152,10 @@ let whd_betaiotazeta env x =
 let whd_all env t =
   match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _) -> t
+       Prod _|Lambda _|Fix _|CoFix _|Int _) -> t
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ -> t
+      | Ind _ | Construct _ | Evar _ | Meta _ | Int _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos all env) (create_tab ()) (inject t)
@@ -155,10 +166,10 @@ let whd_all env t =
 let whd_allnolet env t =
   match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
+       Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _) -> t
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
+      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
         | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
@@ -296,6 +307,15 @@ let rec skip_pattern n c =
   | Lambda (_, _, c) -> skip_pattern (pred n) c
   | _ -> raise IrregularPatternShape
 
+let unfold_ref_with_args infos tab fl v =
+  match unfold_reference infos tab fl with
+  | Def def -> Some (def, v)
+  | Primitive op when check_native_args op v ->
+    let c = match fl with ConstKey c -> c | _ -> assert false in
+    let rargs, a, nargs, v = get_native_args1 op c v in
+    Some (whd_stack infos tab a (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v)))
+  | Undef _ | OpaqueDef _ | Primitive _ -> None
+
 type conv_tab = {
   cnv_inf : clos_infos;
   lft_tab : clos_tab;
@@ -355,28 +375,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
       (try
-          let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
-           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+         let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
+         convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible | Univ.UniverseInconsistency _ ->
-           (* else the oracle tells which constant is to be expanded *)
+         (* else the oracle tells which constant is to be expanded *)
          let oracle = CClosure.oracle_of_infos infos.cnv_inf in
          let (app1,app2) =
+           let aux appr1 lft1 fl1 tab1 v1 appr2 lft2 fl2 tab2 v2 =
+             match unfold_ref_with_args infos.cnv_inf tab1 fl1 v1 with
+             | Some t1 -> ((lft1, t1), appr2)
+             | None -> match unfold_ref_with_args infos.cnv_inf tab2 fl2 v2 with
+               | Some t2 -> (appr1, (lft2, t2))
+               | None -> raise NotConvertible
+           in
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
-             match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
-             | Some def1 -> ((lft1, (def1, v1)), appr2)
-             | None ->
-               (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
-               | Some def2 -> (appr1, (lft2, (def2, v2)))
-	       | None -> raise NotConvertible)
+             aux appr1 lft1 fl1 infos.lft_tab v1 appr2 lft2 fl2 infos.rgt_tab v2
            else
-             match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
-             | Some def2 -> (appr1, (lft2, (def2, v2)))
-             | None ->
-               (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
-               | Some def1 -> ((lft1, (def1, v1)), appr2)
-	       | None -> raise NotConvertible) 
-	 in
-           eqappr cv_pb l2r infos app1 app2 cuniv)
+             let (app2,app1) = aux appr2 lft2 fl2 infos.rgt_tab v2 appr1 lft1 fl1 infos.lft_tab v1 in
+             (app1,app2)
+         in
+         eqappr cv_pb l2r infos app1 app2 cuniv)
 
     | (FProj (p1,c1), FProj (p2, c2)) ->
       (* Projections: prefer unfolding to first-order unification,
@@ -400,31 +418,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
-      (match unfold_projection infos.cnv_inf p1 with
-      | Some s1 ->
+      begin match unfold_projection infos.cnv_inf p1 with
+       | Some s1 ->
          eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
-      | None -> 
-	 (match t2 with 
-	  | FFlex fl2 ->
-            (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
-              | Some def2 ->
-                 eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
-              | None -> raise NotConvertible)
-	  | _ -> raise NotConvertible))
-      
+       | None ->
+         begin match t2 with
+          | FFlex fl2 ->
+            begin match unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 with
+             | Some t2 ->
+               eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv
+             | None -> raise NotConvertible
+            end
+          | _ -> raise NotConvertible
+         end
+      end
+
     | (t1, FProj (p2,c2)) ->
-      (match unfold_projection infos.cnv_inf p2 with
-      | Some s2 ->
+      begin match unfold_projection infos.cnv_inf p2 with
+       | Some s2 ->
          eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
-      | None -> 
-	 (match t1 with 
-	  | FFlex fl1 ->
-            (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
-              | Some def1 ->
-                 eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
-              | None -> raise NotConvertible)
-	  | _ -> raise NotConvertible))
-      
+       | None ->
+         begin match t1 with
+          | FFlex fl1 ->
+            begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with
+             | Some t1 ->
+               eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv
+             | None -> raise NotConvertible
+            end
+          | _ -> raise NotConvertible
+         end
+      end
+
     (* other constructors *)
     | (FLambda _, FLambda _) ->
         (* Inconsistency: we tolerate that v1, v2 contain shift and update but
@@ -469,8 +493,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
-       (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
-	| Some def1 ->
+      begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with
+        | Some (def1,v1) ->
           (** By virtue of the previous case analyses, we know [c2] is rigid.
               Conversion check to rigid terms eventually implies full weak-head
               reduction, so instead of repeatedly performing small-step
@@ -478,32 +502,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
             let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
             let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in
             eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
-	| None -> 
-	   match c2 with
+        | None ->
+          (match c2 with
            | FConstruct ((ind2,_j2),_u2) ->
-	      (try
-	      let v2, v1 =
-                eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
-              in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-	      with Not_found -> raise NotConvertible)
-	   | _ -> raise NotConvertible)
-       
+             (try
+                let v2, v1 =
+                  eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
+                in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+              with Not_found -> raise NotConvertible)
+           | _ -> raise NotConvertible)
+      end
+
     | (c1, FFlex fl2)      ->
-       (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
-        | Some def2 ->
+       begin match unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 with
+        | Some (def2, v2) ->
           (** Symmetrical case of above. *)
           let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
           let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in
           eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
-        | None -> 
-	   match c1 with
-           | FConstruct ((ind1,_j1),_u1) ->
- 	      (try let v1, v2 =
-                    eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
-                   in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-	       with Not_found -> raise NotConvertible)
-	   | _ -> raise NotConvertible)
-       
+        | None ->
+          match c1 with
+          | FConstruct ((ind1,_j1),_u1) ->
+            (try let v1, v2 =
+                   eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
+               in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+             with Not_found -> raise NotConvertible)
+          | _ -> raise NotConvertible
+       end
+
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
       if eq_ind ind1 ind2 then
@@ -584,13 +610,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
+    | FInt i1, FInt i2 ->
+       if Uint63.equal i1 i2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+       else raise NotConvertible
+
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
-        | FProd _ | FEvar _), _ -> raise NotConvertible
+        | FProd _ | FEvar _ | FInt _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
@@ -613,7 +643,12 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
                   raise NotConvertible;
                 let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
                 convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
-            | _ -> assert false)
+            | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) ->
+              if not (CPrimitives.equal op1 op2) then raise NotConvertible else
+                let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in
+                let fk (_,a1) (_,a2) cu = f a1 a2 cu in
+                List.fold_right2 fk kargs1 kargs2 cu2
+            | ((Zlapp _ | Zlproj _ | Zlfix _| Zlcase _| Zlprimitive _), _) -> assert false)
       | _ -> cuniv in
   if compare_stack_shape stk1 stk2 then
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv