aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml7
-rw-r--r--pretyping/glob_ops.ml11
-rw-r--r--pretyping/miscops.ml2
-rw-r--r--pretyping/nativenorm.ml347
-rw-r--r--pretyping/nativenorm.mli15
-rw-r--r--pretyping/pretyping.ml17
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/reductionops.ml4
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:11:07 +0000