From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/nativenorm.ml | 404 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 404 insertions(+) create mode 100644 pretyping/nativenorm.ml (limited to 'pretyping/nativenorm.ml') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml new file mode 100644 index 00000000..bd427ecd --- /dev/null +++ b/pretyping/nativenorm.ml @@ -0,0 +1,404 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (j+1) + +let decompose_prod env t = + let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + match name with + | Anonymous -> (Name (id_of_string "x"),dom,codom) + | _ -> res + +let app_type env c = + let t = whd_betadeltaiota env c in + try destApp t with DestKO -> (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 Univ.Instance.empty (* FIXME *)in + let ctyp = substl s typ in + let nparams = Array.length params in + if Int.equal 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) u allargs = + let mib,mip = lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let params = Array.sub allargs 0 nparams in + try + if const then + let ctyp = type_constructor mind mib (mip.mind_nf_lc.(0)) params in + retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp + else + raise Not_found + with Not_found -> + let i = invert_tag const tag mip.mind_reloc_tbl in + let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in + (mkApp(mkConstructU((ind,i),u), 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,u) -> + construct_of_constr_notnative const env tag ind u 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 = Reductionops.splay_prod env Evd.empty typi in + let decl_with_letin,_ = decompose_prod_assum 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 ndecl = List.length decl in + let papp = mkApp(lift ndecl p,crealargs) in + if dep then + let cstr = ith_constructor_of_inductive (fst ind) (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let params = Array.map (lift ndecl) params in + let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in + mkApp(papp,[|dep_cstr|]) + else papp + in + decl, decl_with_letin, 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 ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " 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) -> + begin match engagement env with + | Some ImpredicativeSet -> + (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) + rangsort + | _ -> + (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) + Type (sup u1 type0_univ) + end + (* 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 Int.equal 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 DestKO -> + Errors.anomaly + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") + 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 DestKO -> assert false in + t, s + | _ -> assert false + +and nf_accu env accu = + let atom = atom_of_accu accu in + if Int.equal (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 Int.equal (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 + DestKO -> + Errors.anomaly + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") + 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 + DestKO -> + Errors.anomaly + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") + 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 -> mkConstU cst + | Aind ind -> mkIndU 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) + | Ameta (mv,_) -> mkMeta mv + | Aevar (ev,_) -> mkEvar ev + | Aproj(p,c) -> + let c = nf_accu env c in + mkProj(Projection.make p false,c) + | _ -> 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 -> + mkConstU cst, Typeops.type_of_constant_in env cst + | Aind ind -> + mkIndU 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,_),u as ind),allargs = find_rectype_a env ta in + let (mib,mip) = Inductive.lookup_mind_specif env (fst 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 (fst 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,decl_with_letin,codom = btypes.(i) in + let b = nf_val (Termops.push_rels_assum decl env) v codom in + Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin + 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 (fun t -> nf_type env t) tt in + let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in + let lvl = nb_rel env in + let nbfix = Array.length ft in + let fargs = mk_rels_accu lvl (Array.length ft) in + (* Third argument of the tuple is ignored by push_rec_types *) + let env = push_rec_types (name,tt,[||]) env in + (* We lift here because the types of arguments (in tt) will be evaluated + in an environment where the fixpoints have been pushed *) + let norm_body i v = nf_val env (napply v fargs) (lift nbfix tt.(i)) in + let ft = Array.mapi norm_body 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) + | Aevar(ev,ty) -> + let ty = nf_type env ty in + mkEvar ev, ty + | Ameta(mv,ty) -> + let ty = nf_type env ty in + mkMeta mv, ty + | Aproj(p,c) -> + let c,tc = nf_accu_type env c in + let cj = make_judge c tc in + let uj = Typeops.judge_of_projection env (Projection.make p true) cj in + uj.uj_val, uj.uj_type + + +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 + DestKO -> + Errors.anomaly + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") + 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 Int.equal n 0 then params else Array.map (lift n) params in + let dom = mkApp(mkIndU 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 sigma 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 sigma prefix c in + match Nativelib.compile ml_filename code with + | true, 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); + let res = nf_val env !Nativelib.rt1 ty in + let t2 = Sys.time () in + let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in + if !Flags.debug then Pp.msg_debug (Pp.str time_info); + res + | _ -> anomaly (Pp.str "Compilation failure") -- cgit v1.2.3