New implementation of the conversion test, using normalization by evaluation to

native OCaml code.

Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.



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

8 files changed, 398 insertions, 6 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d9d82faa2b..545366a70f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -401,7 +401,12 @@ let rec detype (isgoal:bool) avoid env t =
     | Cast (c1,k,c2) ->
         let d1 = detype isgoal avoid env c1 in
 	let d2 = detype isgoal avoid env c2 in
-	GCast(dl,d1,if k == VMcast then CastVM d2 else CastConv d2)
+    let cast = match k with
+    | VMcast -> CastVM d2
+    | NATIVEcast -> CastNative d2
+    | _ -> CastConv d2
+    in
+	GCast(dl,d1,cast)
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 65c21f1be2..e219bbeb15 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -104,7 +104,11 @@ let fold_glob_constr f acc =
 	  (List.fold_left (fun acc (na,k,bbd,bty) ->
 	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
 	Array.fold_left fold (Array.fold_left fold acc tyl) bv
-    | GCast (_,c,k) -> fold (match k with CastConv t | CastVM t -> fold acc t | CastCoerce -> acc) c
+    | GCast (_,c,k) ->
+        let r = match k with
+        | CastConv t | CastVM t | CastNative t -> fold acc t | CastCoerce -> acc
+        in
+        fold r c
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
   and fold_pattern acc (_,idl,p,c) = fold acc c
@@ -150,7 +154,8 @@ let occur_glob_constr id =
                 (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false)
+    | GCast (loc,c,k) -> (occur c) or (match k with CastConv t
+      | CastVM t | CastNative t -> occur t | CastCoerce -> false)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
@@ -208,7 +213,7 @@ let free_glob_vars  =
 	in
 	Array.fold_left_i vars_fix vs idl
     | GCast (loc,c,k) -> let v = vars bounded vs c in
-	(match k with CastConv t | CastVM t -> vars bounded v t | _ -> v)
+	(match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) =
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 1050123e18..264deeb051 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -16,12 +16,14 @@ let map_cast_type f = function
   | CastConv a -> CastConv (f a)
   | CastVM a -> CastVM (f a)
   | CastCoerce -> CastCoerce
+  | CastNative a -> CastNative (f a)
 
 let smartmap_cast_type f c =
   match c with
     | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
     | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
     | CastCoerce -> CastCoerce
+    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
 
 (** Printing of [intro_pattern] *)
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
new file mode 100644
index 0000000000..84ad8e3dd8
--- /dev/null
+++ b/pretyping/nativenorm.ml
@@ -0,0 +1,347 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+open Errors
+open Term
+open Environ
+open Reduction
+open Univ
+open Declarations
+open Names
+open Inductive
+open Util
+open Unix
+open Nativecode
+open Inductiveops
+open Closure
+open Nativevalues
+
+(** This module implements normalization by evaluation to OCaml code *)
+
+exception Find_at of int
+
+let invert_tag cst tag reloc_tbl =
+  try
+    for j = 0 to Array.length reloc_tbl - 1 do
+      let tagj,arity = reloc_tbl.(j) in
+      if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
+	raise (Find_at j)
+      else ()
+    done;raise Not_found
+  with Find_at j -> (j+1)
+
+let decompose_prod env t =
+  let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+  if name = Anonymous then (Name (id_of_string "x"),dom,codom)
+  else res
+
+let app_type env c =
+  let t = whd_betadeltaiota env c in
+  try destApp t with _ -> (t,[||])
+
+ 
+let find_rectype_a env c =
+  let (t, l) = app_type env c in
+  match kind_of_term t with
+  | Ind ind -> (ind, l)
+  | _ -> raise Not_found
+
+(* Instantiate inductives and parameters in constructor type *)
+
+let type_constructor mind mib typ params = 
+  let s = ind_subst mind mib in
+  let ctyp = substl s typ in
+  let nparams = Array.length params in
+  if nparams = 0 then ctyp
+  else
+    let _,ctyp = decompose_prod_n nparams ctyp in   
+    substl (List.rev (Array.to_list params)) ctyp
+
+let construct_of_constr_notnative const env tag (mind, _ as ind) allargs =
+  let mib,mip = lookup_mind_specif env ind in
+  let nparams = mib.mind_nparams in
+  let i = invert_tag const tag mip.mind_reloc_tbl in
+  let params = Array.sub allargs 0 nparams in
+  let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in
+  (mkApp(mkConstruct(ind,i), params), ctyp)
+ 
+
+let construct_of_constr const env tag typ =
+  let t, l = app_type env typ in
+  match kind_of_term t with
+  | Ind ind -> 
+      construct_of_constr_notnative const env tag ind l
+  | _ -> assert false
+
+let construct_of_constr_const env tag typ = 
+  fst (construct_of_constr true env tag typ)
+
+let construct_of_constr_block = construct_of_constr false
+
+let build_branches_type env (mind,_ as _ind) mib mip params dep p =
+  let rtbl = mip.mind_reloc_tbl in
+  (* [build_one_branch i cty] construit le type de la ieme branche (commence
+     a 0) et les lambda correspondant aux realargs *)
+  let build_one_branch i cty =
+    let typi = type_constructor mind mib cty params in
+    let decl,indapp = Term.decompose_prod typi in
+    let ind,cargs = find_rectype_a env indapp in
+    let nparams = Array.length params in
+    let carity = snd (rtbl.(i)) in
+    let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
+    let codom = 
+      let papp = mkApp(lift (List.length decl) p,crealargs) in
+      if dep then
+	let cstr = ith_constructor_of_inductive ind (i+1) in
+        let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
+	let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in
+	mkApp(papp,[|dep_cstr|])
+      else papp
+    in 
+    decl, codom
+  in Array.mapi build_one_branch mip.mind_nf_lc
+
+let build_case_type dep p realargs c = 
+  if dep then mkApp(mkApp(p, realargs), [|c|])
+  else mkApp(p, realargs)
+
+(* TODO move this function *)
+let type_of_rel env n = 
+  let (_,_,ty) = lookup_rel n env in
+  lift n ty
+
+let type_of_prop = mkSort type1_sort
+
+let type_of_sort s = 
+  match s with
+  | Prop _ -> type_of_prop
+  | Type u -> mkType (Univ.super u)
+
+let type_of_var env id = 
+  try let (_,_,ty) = lookup_named id env in ty
+  with Not_found ->
+    anomaly ("type_of_var: variable "^(string_of_id id)^" unbound")
+
+let sort_of_product env domsort rangsort =
+  match (domsort, rangsort) with
+    (* Product rule (s,Prop,Prop) *)
+    | (_,       Prop Null)  -> rangsort
+    (* Product rule (Prop/Set,Set,Set) *)
+    | (Prop _,  Prop Pos) -> rangsort
+    (* Product rule (Type,Set,?) *)
+    | (Type u1, Prop Pos) ->
+        if engagement env = Some ImpredicativeSet then
+          (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
+          rangsort
+        else
+          (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
+          Type (sup u1 type0_univ)
+    (* Product rule (Prop,Type_i,Type_i) *)
+    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
+    (* Product rule (Prop,Type_i,Type_i) *)
+    | (Prop Null, Type _)  -> rangsort
+    (* Product rule (Type_i,Type_i,Type_i) *)
+    | (Type u1, Type u2) -> Type (sup u1 u2)
+
+(* normalisation of values *)
+
+let branch_of_switch lvl ans bs = 
+  let tbl = ans.asw_reloc in
+  let branch i = 
+    let tag,arity = tbl.(i) in
+    let ci = 
+      if arity = 0 then mk_const tag
+      else mk_block tag (mk_rels_accu lvl arity) in
+    bs ci in
+  Array.init (Array.length tbl) branch
+
+let rec nf_val env v typ =
+  match kind_of_value v with
+  | Vaccu accu -> nf_accu env accu
+  | Vfun f -> 
+      let lvl = nb_rel env in
+      let name,dom,codom = 
+	try decompose_prod env typ
+	with _ -> (* TODO: is this the right exception to raise? *)
+	  raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
+      in
+      let env = push_rel (name,None,dom) env in
+      let body = nf_val env (f (mk_rel_accu lvl)) codom in
+      mkLambda(name,dom,body)
+  | Vconst n -> construct_of_constr_const env n typ
+  | Vblock b ->
+      let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+      let args = nf_bargs env b ctyp in
+      mkApp(capp,args)
+
+and nf_type env v =
+  match kind_of_value v with
+  | Vaccu accu -> nf_accu env accu
+  | _ -> assert false
+
+and nf_type_sort env v =
+  match kind_of_value v with
+  | Vaccu accu -> 
+      let t,s = nf_accu_type env accu in
+      let s = try destSort s with _ -> assert false in
+      t, s
+  | _ -> assert false
+
+and nf_accu env accu =
+  let atom = atom_of_accu accu in
+  if accu_nargs accu = 0 then nf_atom env atom
+  else
+    let a,typ = nf_atom_type env atom in
+    let _, args = nf_args env accu typ in
+    mkApp(a,Array.of_list args)
+
+and nf_accu_type env accu =
+  let atom = atom_of_accu accu in
+  if accu_nargs accu = 0 then nf_atom_type env atom
+  else
+    let a,typ = nf_atom_type env atom in
+    let t, args = nf_args env accu typ in
+    mkApp(a,Array.of_list args), t
+
+and nf_args env accu t =
+  let aux arg (t,l) = 
+	let _,dom,codom = try decompose_prod env t with _ -> exit 123 in
+	let c = nf_val env arg dom in
+	(subst1 c codom, c::l)
+  in
+  let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in
+  t, List.rev l
+
+and nf_bargs env b t =
+  let t = ref t in
+  let len = block_size b in
+  Array.init len
+    (fun i ->
+      let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
+      let c = nf_val env (block_field b i) dom in
+      t := subst1 c codom; c)
+
+and nf_atom env atom =
+  match atom with
+  | Arel i -> mkRel (nb_rel env - i)
+  | Aconstant cst -> mkConst cst
+  | Aind ind -> mkInd ind
+  | Asort s -> mkSort s
+  | Avar id -> mkVar id
+  | Aprod(n,dom,codom) ->
+      let dom = nf_type env dom in
+      let vn = mk_rel_accu (nb_rel env) in
+      let env = push_rel (n,None,dom) env in
+      let codom = nf_type env (codom vn) in
+      mkProd(n,dom,codom)
+  | _ -> fst (nf_atom_type env atom)
+
+and nf_atom_type env atom = 
+  match atom with
+  | Arel i ->
+      let n = (nb_rel env - i) in
+      mkRel n, type_of_rel env n
+  | Aconstant cst ->
+      mkConst cst, Typeops.type_of_constant env cst
+  | Aind ind ->
+      mkInd ind, Inductiveops.type_of_inductive env ind 
+  | Asort s ->
+      mkSort s, type_of_sort s
+  | Avar id ->
+      mkVar id, type_of_var env id
+  | Acase(ans,accu,p,bs) ->
+      let a,ta = nf_accu_type env accu in
+      let (mind,_ as ind),allargs = find_rectype_a env ta in
+      let (mib,mip) = Inductive.lookup_mind_specif env ind in
+      let nparams = mib.mind_nparams in
+      let params,realargs = Array.chop nparams allargs in
+      let pT = 
+	hnf_prod_applist env 
+	  (Inductiveops.type_of_inductive env ind) (Array.to_list params) in
+      let pT = whd_betadeltaiota env pT in
+      let dep, p = nf_predicate env ind mip params p pT in
+      (* Calcul du type des branches *)
+      let btypes = build_branches_type env ind mib mip params dep p in
+      (* calcul des branches *)
+      let bsw = branch_of_switch (nb_rel env) ans bs in
+      let mkbranch i v =
+	let decl,codom = btypes.(i) in
+	let env = 
+	  List.fold_right 
+	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
+	let b = nf_val env v codom in
+	compose_lam decl b 
+      in 
+      let branchs = Array.mapi mkbranch bsw in
+      let tcase = build_case_type dep p realargs a in
+      let ci = ans.asw_ci in
+      mkCase(ci, p, a, branchs), tcase 
+  | Afix(tt,ft,rp,s) ->
+      let tt = Array.map (nf_type env) tt in
+      let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in
+      let lvl = nb_rel env in
+      let fargs = mk_rels_accu lvl (Array.length ft) in
+      let env = push_rec_types (name,tt,[||]) env in
+      let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in
+      mkFix((rp,s),(name,tt,ft)), tt.(s)
+  | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) ->
+      let tt = Array.map (nf_type env) tt in
+      let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in
+      let lvl = nb_rel env in
+      let fargs = mk_rels_accu lvl (Array.length ft) in
+      let env = push_rec_types (name,tt,[||]) env in
+      let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in
+      mkCoFix(s,(name,tt,ft)), tt.(s)
+  | Aprod(n,dom,codom) ->
+      let dom,s1 = nf_type_sort env dom in
+      let vn = mk_rel_accu (nb_rel env) in
+      let env = push_rel (n,None,dom) env in
+      let codom,s2 = nf_type_sort env (codom vn) in
+      mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
+
+and  nf_predicate env ind mip params v pT =
+  match kind_of_value v, kind_of_term pT with
+  | Vfun f, Prod _ ->
+      let k = nb_rel env in
+      let vb = f (mk_rel_accu k) in
+      let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
+      let dep,body = 
+	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
+      dep, mkLambda(name,dom,body)
+  | Vfun f, _ -> 
+      let k = nb_rel env in
+      let vb = f (mk_rel_accu k) in
+      let name = Name (id_of_string "c") in
+      let n = mip.mind_nrealargs in
+      let rargs = Array.init n (fun i -> mkRel (n-i)) in
+      let params = if n=0 then params else Array.map (lift n) params in
+      let dom = mkApp(mkInd ind,Array.append params rargs) in
+      let body = nf_type (push_rel (name,None,dom) env) vb in
+      true, mkLambda(name,dom,body)
+  | _, _ -> false, nf_type env v
+
+let native_norm env c ty =  
+  if !Flags.no_native_compiler then
+    error "Native_compute reduction has been disabled"
+  else
+  let penv = Environ.pre_env env in 
+  (*
+  Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
+  Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
+  *)
+  let ml_filename, prefix = Nativelib.get_ml_filename () in
+  let code, upd = mk_norm_code penv prefix c in
+  match Nativelib.compile ml_filename code with
+    | 0,fn ->
+        if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ...");
+        let t0 = Sys.time () in
+        Nativelib.call_linker ~fatal:true prefix fn (Some upd);
+        let t1 = Sys.time () in
+        let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+        if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+        nf_val env !Nativelib.rt1 ty
+    | _ -> anomaly "Compilation failure" 
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
new file mode 100644
index 0000000000..ecc3489bee
--- /dev/null
+++ b/pretyping/nativenorm.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+open Names
+open Term
+open Environ
+open Reduction
+
+(** This module implements normalization by evaluation to OCaml code *)
+
+val native_norm : env -> constr -> types -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 358d53e48f..15395ca7f9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -637,8 +637,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	| CastCoerce ->
 	  let cj = pretype empty_tycon env evdref lvar c in
 	    evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
-	| CastConv t | CastVM t ->
-	  let k = (match k with CastVM _ -> VMcast | _ -> DEFAULTcast) in
+	| CastConv t | CastVM t | CastNative t ->
+	  let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
 	  let tj = pretype_type empty_valcon env evdref lvar t in
 	  let tval = nf_evar !evdref tj.utj_val in
 	  let cj = match k with
@@ -654,6 +654,19 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 		  end
 		else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
 				   str "unresolved arguments remain.")
+	    | NATIVEcast ->
+ 	      let cj = pretype empty_tycon env evdref lvar c in
+	      let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
+		if not (occur_existential cty || occur_existential tval) then
+		  begin 
+		    try 
+		      ignore (Nativeconv.native_conv Reduction.CUMUL env cty tval); cj
+		    with Reduction.NotConvertible -> 
+		    error_actual_type_loc loc env !evdref cj tval 
+		  end
+		else user_err_loc (loc,"",str "Cannot check cast with native compiler: " ++
+				   str "unresolved arguments remain.")
+
 	    | _ -> 
  	      pretype (mk_tycon tval) env evdref lvar c
 	  in
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index ea08e7c5d2..506c59ef39 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -5,6 +5,7 @@ Reductionops
 Vnorm
 Namegen
 Inductiveops
+Nativenorm
 Retyping
 Cbv
 Pretype_errors
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f1f31ec6e3..0fb3a99a47 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -621,6 +621,10 @@ let whd_betaiota_preserving_vm_cast env sigma t =
            let c = zip (whrec (c,empty_stack)) in
            let t = zip (whrec (t,empty_stack)) in
            (mkCast(c,VMcast,t),stack)
+       | Cast (c,NATIVEcast,t) ->
+           let c = zip (whrec (c,empty_stack)) in
+           let t = zip (whrec (t,empty_stack)) in
+           (mkCast(c,NATIVEcast,t),stack)
        | Cast (c,DEFAULTcast,_) ->
            whrec (c, stack)
        | App (f,cl)  -> whrec (f, append_stack_app cl stack)