From dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 1 Dec 1999 08:03:06 +0000 Subject: - Typing -> Safe_typing - proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/environ.ml | 5 +- kernel/environ.mli | 1 + kernel/evd.ml | 2 +- kernel/indtypes.ml | 2 +- kernel/reduction.ml | 6 +- kernel/safe_typing.ml | 416 +++++++++++++++++++++++++++++++++++++++++++++++++ kernel/safe_typing.mli | 78 ++++++++++ kernel/sign.ml | 6 +- kernel/sign.mli | 44 +++--- kernel/typeops.ml | 6 +- kernel/typing.ml | 415 ------------------------------------------------ kernel/typing.mli | 77 --------- 12 files changed, 531 insertions(+), 527 deletions(-) create mode 100644 kernel/safe_typing.ml create mode 100644 kernel/safe_typing.mli delete mode 100644 kernel/typing.ml delete mode 100644 kernel/typing.mli (limited to 'kernel') diff --git a/kernel/environ.ml b/kernel/environ.ml index ccf3e1e20c..bed45797d8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,6 +43,7 @@ let empty_env = { let universes env = env.env_universes let context env = env.env_context +let var_context env = let (ENVIRON(g,_)) = env.env_context in g (* Construction functions. *) @@ -50,8 +51,8 @@ let push_var idvar env = { env with env_context = add_glob idvar env.env_context } let change_hyps f env = - let ctx = env.env_context in - { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) } + let (ENVIRON(g,r)) = env.env_context in + { env with env_context = ENVIRON (f g, r) } let push_rel idrel env = { env with env_context = add_rel idrel env.env_context } diff --git a/kernel/environ.mli b/kernel/environ.mli index d3fd22c01e..9f1c228a00 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -22,6 +22,7 @@ val empty_env : unsafe_env val universes : unsafe_env -> universes val context : unsafe_env -> context +val var_context : unsafe_env -> var_context val push_var : identifier * typed_type -> unsafe_env -> unsafe_env val change_hyps : diff --git a/kernel/evd.ml b/kernel/evd.ml index dd387ddfb4..4599fbdc43 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -65,7 +65,7 @@ let is_defined sigma ev = let info = map sigma ev in not (info.evar_body = Evar_empty) -let evar_hyps ev = get_globals (context ev.evar_env) +let evar_hyps ev = var_context ev.evar_env let id_of_existential ev = id_of_string ("?" ^ string_of_int ev) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 96fe8d5846..00e8a442bb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -244,7 +244,7 @@ let cci_inductive env env_ar kind nparams finite inds cst = let packets = Array.of_list (list_map_i one_packet 1 inds) in { mind_kind = kind; mind_ntypes = ntypes; - mind_hyps = get_globals (context env); + mind_hyps = var_context env; mind_packets = packets; mind_constraints = cst; mind_singl = None; diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4bc551c6aa..2ce121ed12 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables * Similarly we have is_fmachine1_metas and is_resolve1_metas *) -let rec whd_ise1_metas env sigma = function +let rec whd_ise1_metas sigma = function | (DOPN(Evar n,_) as k) -> if Evd.in_dom sigma n then if Evd.is_defined sigma n then - whd_ise1_metas env sigma (existential_value sigma k) + whd_ise1_metas sigma (existential_value sigma k) else let m = DOP0(Meta (new_meta())) in DOP2(Cast,m,existential_type sigma k) else k - | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c + | DOP2(Cast,c,_) -> whd_ise1_metas sigma c | c -> c diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml new file mode 100644 index 0000000000..e523be5108 --- /dev/null +++ b/kernel/safe_typing.ml @@ -0,0 +1,416 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Univ +open Generic +open Term +open Reduction +open Sign +open Constant +open Inductive +open Environ +open Type_errors +open Typeops +open Indtypes + +type judgment = unsafe_judgment + +let j_val j = j.uj_val +let j_type j = j.uj_type +let j_kind j = j.uj_kind + +let vect_lift = Array.mapi lift +let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) + +(*s The machine flags. + [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$) + like [Acc_rec.fw]. + [nocheck] indicates if we can skip some verifications to accelerate + the type inference. *) + +type 'a mach_flags = { + fix : bool; + nocheck : bool } + +(* The typing machine without information. *) + +let rec execute mf env cstr = + let cst0 = Constraint.empty in + match kind_of_term cstr with + | IsMeta _ -> + anomaly "the kernel does not understand metas" + | IsEvar _ -> + anomaly "the kernel does not understand existential variables" + + | IsRel n -> + (relative env n, cst0) + + | IsVar id -> + (make_judge cstr (snd (lookup_var id env)), cst0) + + | IsAbst _ -> + if evaluable_abst env cstr then + execute mf env (abst_value env cstr) + else + error "Cannot typecheck an unevaluable abstraction" + + | IsConst _ -> + (make_judge cstr (type_of_constant env Evd.empty cstr), cst0) + + | IsMutInd _ -> + (make_judge cstr (type_of_inductive env Evd.empty cstr), cst0) + + | IsMutConstruct _ -> + let (typ,kind) = destCast (type_of_constructor env Evd.empty cstr) in + ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0) + + | IsMutCase (_,p,c,lf) -> + let (cj,cst1) = execute mf env c in + let (pj,cst2) = execute mf env p in + let (lfj,cst3) = execute_array mf env lf in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (type_of_case env Evd.empty pj cj lfj, cst) + + | IsFix (vn,i,lar,lfi,vdef) -> + if (not mf.fix) && array_exists (fun n -> n < 0) vn then + error "General Fixpoints not allowed"; + let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in + let fix = mkFix vn i larv lfi vdefv in + check_fix env Evd.empty fix; + (make_judge fix larv.(i), cst) + + | IsCoFix (i,lar,lfi,vdef) -> + let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in + let cofix = mkCoFix i larv lfi vdefv in + check_cofix env Evd.empty cofix; + (make_judge cofix larv.(i), cst) + + | IsSort (Prop c) -> + (make_judge_of_prop_contents c, cst0) + + | IsSort (Type u) -> + make_judge_of_type u + + | IsAppL (f,args) -> + let (j,cst1) = execute mf env f in + let (jl,cst2) = execute_list mf env args in + let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck jl j in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (j, cst) + + | IsLambda (name,c1,c2) -> + let (j,cst1) = execute mf env c1 in + let var = assumption_of_judgment env Evd.empty j in + let env1 = push_rel (name,var) env in + let (j',cst2) = execute mf env1 c2 in + let (j,cst3) = abs_rel env1 Evd.empty name var j' in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (j, cst) + + | IsProd (name,c1,c2) -> + let (j,cst1) = execute mf env c1 in + let var = assumption_of_judgment env Evd.empty j in + let env1 = push_rel (name,var) env in + let (j',cst2) = execute mf env1 c2 in + let (j,cst3) = gen_rel env1 Evd.empty name var j' in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (j, cst) + + | IsCast (c,t) -> + let (cj,cst1) = execute mf env c in + let (tj,cst2) = execute mf env t in + let cst = Constraint.union cst1 cst2 in + (cast_rel env Evd.empty cj tj, cst) + + | _ -> error_cant_execute CCI env cstr + +and execute_fix mf env lar lfi vdef = + let (larj,cst1) = execute_array mf env lar in + let lara = Array.map (assumption_of_judgment env Evd.empty) larj in + let nlara = + List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in + let env1 = + List.fold_left (fun env nvar -> push_rel nvar env) env nlara in + let (vdefj,cst2) = execute_array mf env1 vdef in + let vdefv = Array.map j_val_only vdefj in + let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (lara,vdefv,cst) + +and execute_array mf env v = + let (jl,u1) = execute_list mf env (Array.to_list v) in + (Array.of_list jl, u1) + +and execute_list mf env = function + | [] -> + ([], Constraint.empty) + | c::r -> + let (j,cst1) = execute mf env c in + let (jr,cst2) = execute_list mf env r in + (j::jr, Constraint.union cst1 cst2) + + +(* The typed type of a judgment. *) + +let execute_type mf env constr = + let (j,_) = execute mf env constr in + assumption_of_judgment env Evd.empty j + + +(* Exported machines. First safe machines, with no general fixpoint + allowed (the flag [fix] is not set) and all verifications done (the + flag [nocheck] is not set). *) + +let safe_machine env constr = + let mf = { fix = false; nocheck = false } in + execute mf env constr + +let safe_machine_type env constr = + let mf = { fix = false; nocheck = false } in + execute_type mf env constr + +(* Machines with general fixpoint. *) + +let fix_machine env constr = + let mf = { fix = true; nocheck = false } in + execute mf env constr + +let fix_machine_type env constr = + let mf = { fix = true; nocheck = false } in + execute_type mf env constr + +(* Fast machines without any verification. *) + +let unsafe_machine env constr = + let mf = { fix = true; nocheck = true } in + execute mf env constr + +let unsafe_machine_type env constr = + let mf = { fix = true; nocheck = true } in + execute_type mf env constr + + +(* ``Type of'' machines. *) + +let type_of env c = + let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type + +let type_of_type env c = + let tt = safe_machine_type env c in DOP0 (Sort tt.typ) + +let unsafe_type_of env c = + let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type + +let unsafe_type_of_type env c = + let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ) + +(* Typing of several terms. *) + +let safe_machine_l env cl = + let type_one (cst,l) c = + let (j,cst') = safe_machine env c in + (Constraint.union cst cst', j::l) + in + List.fold_left type_one (Constraint.empty,[]) cl + +let safe_machine_v env cv = + let type_one (cst,l) c = + let (j,cst') = safe_machine env c in + (Constraint.union cst cst', j::l) + in + let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in + (cst', Array.of_list l) + + +(*s Safe environments. *) + +type environment = unsafe_env + +let empty_environment = empty_env + +let universes = universes +let context = context +let var_context = var_context + +let lookup_var = lookup_var +let lookup_rel = lookup_rel +let lookup_constant = lookup_constant +let lookup_mind = lookup_mind +let lookup_mind_specif = lookup_mind_specif + +(* Insertion of variables (named and de Bruijn'ed). They are now typed before + being added to the environment. *) + +let push_rel_or_var push (id,c) env = + let (j,cst) = safe_machine env c in + let env' = add_constraints cst env in + let var = assumption_of_judgment env' Evd.empty j in + push (id,var) env' + +let push_var nvar env = push_rel_or_var push_var nvar env + +let push_rel nrel env = push_rel_or_var push_rel nrel env + +let push_vars vars env = + List.fold_left (fun env nvar -> push_var nvar env) env vars + +let push_rels vars env = + List.fold_left (fun env nvar -> push_rel nvar env) env vars + +(* Insertion of constants and parameters in environment. *) + +let add_constant sp ce env = + let (jb,cst) = safe_machine env ce.const_entry_body in + let env' = add_constraints cst env in + let (env'',ty,cst') = + match ce.const_entry_type with + | None -> + env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty + | Some ty -> + let (jt,cst') = safe_machine env ty in + let env'' = add_constraints cst' env' in + try + let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in + let env'' = add_constraints cst'' env'' in + (env'', assumption_of_judgment env'' Evd.empty jt, + Constraint.union cst' cst'') + with NotConvertible -> + error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val + in + let cb = { + const_kind = kind_of_path sp; + const_body = Some ce.const_entry_body; + const_type = ty; + const_hyps = var_context env; + const_constraints = Constraint.union cst cst'; + const_opaque = false } + in + add_constant sp cb env'' + +let add_parameter sp t env = + let (jt,cst) = safe_machine env t in + let env' = add_constraints cst env in + let cb = { + const_kind = kind_of_path sp; + const_body = None; + const_type = assumption_of_judgment env' Evd.empty jt; + const_hyps = var_context env; + const_constraints = cst; + const_opaque = false } + in + Environ.add_constant sp cb env' + +(* Insertion of inductive types. *) + +(* [for_all_prods p env c] checks a boolean condition [p] on all types + appearing in products in front of [c]. The boolean condition [p] is a + function taking a value of type [typed_type] as argument. *) + +let rec for_all_prods p env c = + match whd_betadeltaiota env Evd.empty c with + | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) -> + (p (make_typed t s)) && + (let ty = { body = t; typ = s } in + let env' = Environ.push_rel (name,ty) env in + for_all_prods p env' c) + | DOP2(Prod, b, DLAM(name,c)) -> + let (jb,cst) = unsafe_machine env b in + let var = assumption_of_judgment env Evd.empty jb in + (p var) && + (let env' = Environ.push_rel (name,var) (add_constraints cst env) in + for_all_prods p env' c) + | _ -> true + +let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c + +let enforce_type_constructor env univ j cst = + match whd_betadeltaiota env Evd.empty j.uj_type with + | DOP0 (Sort (Type uc)) -> + Constraint.add (univ,Geq,uc) cst + | _ -> error "Type of Constructor not well-formed" + +let type_one_constructor env_ar nparams ar c = + let (params,dc) = decompose_prod_n nparams c in + let env_par = push_rels params env_ar in + let (jc,cst) = safe_machine env_par dc in + let cst' = match sort_of_arity env_ar ar with + | Type u -> enforce_type_constructor env_par u jc cst + | Prop _ -> cst + in + let (j,cst'') = safe_machine env_ar c in + let issmall = is_small_type env_par c in + ((issmall,j), Constraint.union cst' cst'') + +let logic_constr env c = + for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c + +let logic_arity env c = + for_all_prods + (fun t -> + (not (is_info_type env Evd.empty t)) or (is_small_type env t.body)) + env c + +let is_unit env_par nparams ar spec = + match decomp_all_DLAMV_name spec with + | (_,[|c|]) -> + (let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) && + (let (_,c') = decompose_prod_n nparams c in logic_constr env_par c') + | _ -> false + +let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) = + let (lna,vc) = decomp_all_DLAMV_name spec in + let ((issmall,jlc),cst') = + List.fold_right + (fun c ((small,jl),cst) -> + let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in + ((small && sm,jc::jl), Constraint.union cst cst')) + (Array.to_list vc) + ((true,[]),Constraint.empty) + in + let castlc = List.map cast_of_judgment jlc in + let spec' = put_DLAMSV lna (Array.of_list castlc) in + let isunit = is_unit env_par nparams ar spec in + let (_,tyar) = lookup_rel (ninds+1-i) env_ar in + ((id,tyar,cnames,issmall,isunit,spec'), cst') + +let add_mind sp mie env = + mind_check_names mie; + mind_check_arities env mie; + let params = mind_extract_and_check_params mie in + let nparams = mie.mind_entry_nparams in + mind_check_lc params mie; + let ninds = List.length mie.mind_entry_inds in + let types_sign = + List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds + in + let env_arities = push_rels types_sign env in + let env_params = push_rels params env_arities in + let _,inds,cst = + List.fold_left + (fun (i,inds,cst) ind -> + let (ind',cst') = + type_one_inductive i env_arities env_params nparams ninds ind + in + (succ i,ind'::inds, Constraint.union cst cst')) + (1,[],Constraint.empty) + mie.mind_entry_inds + in + let kind = kind_of_path sp in + let mib = + cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst + in + add_mind sp mib (add_constraints cst env) + +let add_constraints = add_constraints + +let export = export +let import = import + +let unsafe_env_of_env e = e + +(*s Machines with information. *) + +type information = Logic | Inf of unsafe_judgment diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli new file mode 100644 index 0000000000..392040814f --- /dev/null +++ b/kernel/safe_typing.mli @@ -0,0 +1,78 @@ + +(* $Id$ *) + +(*i*) +open Pp +open Names +open Term +open Univ +open Sign +open Constant +open Inductive +open Environ +open Typeops +(*i*) + +(*s Safe environments. Since we are now able to type terms, we can define an + abstract type of safe environments, where objects are typed before being + added. Internally, the datatype is still [unsafe_env]. We re-export the + functions of [Environ] for the new type [environment]. *) + +type environment + +val empty_environment : environment + +val universes : environment -> universes +val context : environment -> context +val var_context : environment -> var_context + +val push_var : identifier * constr -> environment -> environment +val push_rel : name * constr -> environment -> environment +val add_constant : + section_path -> constant_entry -> environment -> environment +val add_parameter : + section_path -> constr -> environment -> environment +val add_mind : + section_path -> mutual_inductive_entry -> environment -> environment +val add_constraints : constraints -> environment -> environment + +val lookup_var : identifier -> environment -> name * typed_type +val lookup_rel : int -> environment -> name * typed_type +val lookup_constant : section_path -> environment -> constant_body +val lookup_mind : section_path -> environment -> mutual_inductive_body +val lookup_mind_specif : constr -> environment -> mind_specif + +val export : environment -> string -> compiled_env +val import : compiled_env -> environment -> environment + +val unsafe_env_of_env : environment -> unsafe_env + +(*s Typing without information. *) + +type judgment + +val j_val : judgment -> constr +val j_type : judgment -> constr +val j_kind : judgment -> constr + +val safe_machine : environment -> constr -> judgment * constraints +val safe_machine_type : environment -> constr -> typed_type + +val fix_machine : environment -> constr -> judgment * constraints +val fix_machine_type : environment -> constr -> typed_type + +val unsafe_machine : environment -> constr -> judgment * constraints +val unsafe_machine_type : environment -> constr -> typed_type + +val type_of : environment -> constr -> constr + +val type_of_type : environment -> constr -> constr + +val unsafe_type_of : environment -> constr -> constr + + +(*s Typing with information (extraction). *) + +type information = Logic | Inf of judgment + + diff --git a/kernel/sign.ml b/kernel/sign.ml index 5d7d5309b0..0b34c7edf3 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -10,7 +10,7 @@ open Term type 'a signature = identifier list * 'a list type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature let gLOB hyps = ENVIRON (hyps,[]) @@ -233,7 +233,7 @@ let lookup_id id env = | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y) -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature diff --git a/kernel/sign.mli b/kernel/sign.mli index 2a0a567dec..e2ef7d4a1e 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term (*s Signatures with named and de Bruijn variables. *) type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature - -val gLOB : 'b signature -> ('b,'a) env - -val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env -val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env -val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b) -val lookup_rel : int -> ('b,'a) env -> (name * 'a) -val mem_glob : identifier -> ('b,'a) env -> bool - -val get_globals : ('b,'a) env -> 'b signature -val get_rels : ('b,'a) env -> 'a db_signature -val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c -val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c -val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env -val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env -val isnull_rel_env : ('a,'b) env -> bool -val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env -val ids_of_env : ('a, 'b) env -> identifier list +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature + +val gLOB : 'b signature -> ('b,'a) sign + +val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign +val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign +val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b) +val lookup_rel : int -> ('b,'a) sign -> (name * 'a) +val mem_glob : identifier -> ('b,'a) sign -> bool + +val get_globals : ('b,'a) sign -> 'b signature +val get_rels : ('b,'a) sign -> 'a db_signature +val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c +val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c +val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign +val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign +val isnull_rel_env : ('a,'b) sign -> bool +val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign +val ids_of_env : ('a, 'b) sign -> identifier list type ('b,'a) search_result = | GLOBNAME of identifier * 'b | RELNAME of int * 'a -val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result +val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature val unitize_env : 'a assumptions -> unit assumptions diff --git a/kernel/typeops.ml b/kernel/typeops.ml index d224b0209e..0d2d5cba50 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -75,14 +75,14 @@ let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) = current context of [env]. *) let construct_reference id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if hyps_inclusion env sigma hyps hyps' then Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) else error_reference_variables CCI env id let check_hyps id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if not (hyps_inclusion env sigma hyps hyps') then error_reference_variables CCI env id @@ -178,7 +178,7 @@ let type_inst_construct env sigma i mind = let type_of_existential env sigma c = let (ev,args) = destEvar c in let evi = Evd.map sigma ev in - let hyps = get_globals (context evi.Evd.evar_env) in + let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in check_hyps id env sigma hyps; instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) diff --git a/kernel/typing.ml b/kernel/typing.ml deleted file mode 100644 index db3d00302e..0000000000 --- a/kernel/typing.ml +++ /dev/null @@ -1,415 +0,0 @@ - -(* $Id$ *) - -open Pp -open Util -open Names -open Univ -open Generic -open Term -open Reduction -open Sign -open Constant -open Inductive -open Environ -open Type_errors -open Typeops -open Indtypes - -type judgment = unsafe_judgment - -let j_val j = j.uj_val -let j_type j = j.uj_type -let j_kind j = j.uj_kind - -let vect_lift = Array.mapi lift -let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) - -(*s The machine flags. - [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$) - like [Acc_rec.fw]. - [nocheck] indicates if we can skip some verifications to accelerate - the type inference. *) - -type 'a mach_flags = { - fix : bool; - nocheck : bool } - -(* The typing machine without information. *) - -let rec execute mf env cstr = - let cst0 = Constraint.empty in - match kind_of_term cstr with - | IsMeta _ -> - anomaly "the kernel does not understand metas" - | IsEvar _ -> - anomaly "the kernel does not understand existential variables" - - | IsRel n -> - (relative env n, cst0) - - | IsVar id -> - (make_judge cstr (snd (lookup_var id env)), cst0) - - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - - | IsConst _ -> - (make_judge cstr (type_of_constant env Evd.empty cstr), cst0) - - | IsMutInd _ -> - (make_judge cstr (type_of_inductive env Evd.empty cstr), cst0) - - | IsMutConstruct _ -> - let (typ,kind) = destCast (type_of_constructor env Evd.empty cstr) in - ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0) - - | IsMutCase (_,p,c,lf) -> - let (cj,cst1) = execute mf env c in - let (pj,cst2) = execute mf env p in - let (lfj,cst3) = execute_array mf env lf in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (type_of_case env Evd.empty pj cj lfj, cst) - - | IsFix (vn,i,lar,lfi,vdef) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in - let fix = mkFix vn i larv lfi vdefv in - check_fix env Evd.empty fix; - (make_judge fix larv.(i), cst) - - | IsCoFix (i,lar,lfi,vdef) -> - let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in - let cofix = mkCoFix i larv lfi vdefv in - check_cofix env Evd.empty cofix; - (make_judge cofix larv.(i), cst) - - | IsSort (Prop c) -> - (make_judge_of_prop_contents c, cst0) - - | IsSort (Type u) -> - make_judge_of_type u - - | IsAppL (f,args) -> - let (j,cst1) = execute mf env f in - let (jl,cst2) = execute_list mf env args in - let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck jl j in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) - - | IsLambda (name,c1,c2) -> - let (j,cst1) = execute mf env c1 in - let var = assumption_of_judgment env Evd.empty j in - let env1 = push_rel (name,var) env in - let (j',cst2) = execute mf env1 c2 in - let (j,cst3) = abs_rel env1 Evd.empty name var j' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) - - | IsProd (name,c1,c2) -> - let (j,cst1) = execute mf env c1 in - let var = assumption_of_judgment env Evd.empty j in - let env1 = push_rel (name,var) env in - let (j',cst2) = execute mf env1 c2 in - let (j,cst3) = gen_rel env1 Evd.empty name var j' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) - - | IsCast (c,t) -> - let (cj,cst1) = execute mf env c in - let (tj,cst2) = execute mf env t in - let cst = Constraint.union cst1 cst2 in - (cast_rel env Evd.empty cj tj, cst) - - | _ -> error_cant_execute CCI env cstr - -and execute_fix mf env lar lfi vdef = - let (larj,cst1) = execute_array mf env lar in - let lara = Array.map (assumption_of_judgment env Evd.empty) larj in - let nlara = - List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in - let env1 = - List.fold_left (fun env nvar -> push_rel nvar env) env nlara in - let (vdefj,cst2) = execute_array mf env1 vdef in - let vdefv = Array.map j_val_only vdefj in - let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (lara,vdefv,cst) - -and execute_array mf env v = - let (jl,u1) = execute_list mf env (Array.to_list v) in - (Array.of_list jl, u1) - -and execute_list mf env = function - | [] -> - ([], Constraint.empty) - | c::r -> - let (j,cst1) = execute mf env c in - let (jr,cst2) = execute_list mf env r in - (j::jr, Constraint.union cst1 cst2) - - -(* The typed type of a judgment. *) - -let execute_type mf env constr = - let (j,_) = execute mf env constr in - assumption_of_judgment env Evd.empty j - - -(* Exported machines. First safe machines, with no general fixpoint - allowed (the flag [fix] is not set) and all verifications done (the - flag [nocheck] is not set). *) - -let safe_machine env constr = - let mf = { fix = false; nocheck = false } in - execute mf env constr - -let safe_machine_type env constr = - let mf = { fix = false; nocheck = false } in - execute_type mf env constr - -(* Machines with general fixpoint. *) - -let fix_machine env constr = - let mf = { fix = true; nocheck = false } in - execute mf env constr - -let fix_machine_type env constr = - let mf = { fix = true; nocheck = false } in - execute_type mf env constr - -(* Fast machines without any verification. *) - -let unsafe_machine env constr = - let mf = { fix = true; nocheck = true } in - execute mf env constr - -let unsafe_machine_type env constr = - let mf = { fix = true; nocheck = true } in - execute_type mf env constr - - -(* ``Type of'' machines. *) - -let type_of env c = - let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type - -let type_of_type env c = - let tt = safe_machine_type env c in DOP0 (Sort tt.typ) - -let unsafe_type_of env c = - let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type - -let unsafe_type_of_type env c = - let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ) - -(* Typing of several terms. *) - -let safe_machine_l env cl = - let type_one (cst,l) c = - let (j,cst') = safe_machine env c in - (Constraint.union cst cst', j::l) - in - List.fold_left type_one (Constraint.empty,[]) cl - -let safe_machine_v env cv = - let type_one (cst,l) c = - let (j,cst') = safe_machine env c in - (Constraint.union cst cst', j::l) - in - let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in - (cst', Array.of_list l) - - -(*s Safe environments. *) - -type environment = unsafe_env - -let empty_environment = empty_env - -let universes = universes -let context = context - -let lookup_var = lookup_var -let lookup_rel = lookup_rel -let lookup_constant = lookup_constant -let lookup_mind = lookup_mind -let lookup_mind_specif = lookup_mind_specif - -(* Insertion of variables (named and de Bruijn'ed). They are now typed before - being added to the environment. *) - -let push_rel_or_var push (id,c) env = - let (j,cst) = safe_machine env c in - let env' = add_constraints cst env in - let var = assumption_of_judgment env' Evd.empty j in - push (id,var) env' - -let push_var nvar env = push_rel_or_var push_var nvar env - -let push_rel nrel env = push_rel_or_var push_rel nrel env - -let push_vars vars env = - List.fold_left (fun env nvar -> push_var nvar env) env vars - -let push_rels vars env = - List.fold_left (fun env nvar -> push_rel nvar env) env vars - -(* Insertion of constants and parameters in environment. *) - -let add_constant sp ce env = - let (jb,cst) = safe_machine env ce.const_entry_body in - let env' = add_constraints cst env in - let (env'',ty,cst') = - match ce.const_entry_type with - | None -> - env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty - | Some ty -> - let (jt,cst') = safe_machine env ty in - let env'' = add_constraints cst' env' in - try - let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in - let env'' = add_constraints cst'' env'' in - (env'', assumption_of_judgment env'' Evd.empty jt, - Constraint.union cst' cst'') - with NotConvertible -> - error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val - in - let cb = { - const_kind = kind_of_path sp; - const_body = Some ce.const_entry_body; - const_type = ty; - const_hyps = get_globals (context env); - const_constraints = Constraint.union cst cst'; - const_opaque = false } - in - add_constant sp cb env'' - -let add_parameter sp t env = - let (jt,cst) = safe_machine env t in - let env' = add_constraints cst env in - let cb = { - const_kind = kind_of_path sp; - const_body = None; - const_type = assumption_of_judgment env' Evd.empty jt; - const_hyps = get_globals (context env); - const_constraints = cst; - const_opaque = false } - in - Environ.add_constant sp cb env' - -(* Insertion of inductive types. *) - -(* [for_all_prods p env c] checks a boolean condition [p] on all types - appearing in products in front of [c]. The boolean condition [p] is a - function taking a value of type [typed_type] as argument. *) - -let rec for_all_prods p env c = - match whd_betadeltaiota env Evd.empty c with - | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) -> - (p (make_typed t s)) && - (let ty = { body = t; typ = s } in - let env' = Environ.push_rel (name,ty) env in - for_all_prods p env' c) - | DOP2(Prod, b, DLAM(name,c)) -> - let (jb,cst) = unsafe_machine env b in - let var = assumption_of_judgment env Evd.empty jb in - (p var) && - (let env' = Environ.push_rel (name,var) (add_constraints cst env) in - for_all_prods p env' c) - | _ -> true - -let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c - -let enforce_type_constructor env univ j cst = - match whd_betadeltaiota env Evd.empty j.uj_type with - | DOP0 (Sort (Type uc)) -> - Constraint.add (univ,Geq,uc) cst - | _ -> error "Type of Constructor not well-formed" - -let type_one_constructor env_ar nparams ar c = - let (params,dc) = decompose_prod_n nparams c in - let env_par = push_rels params env_ar in - let (jc,cst) = safe_machine env_par dc in - let cst' = match sort_of_arity env_ar ar with - | Type u -> enforce_type_constructor env_par u jc cst - | Prop _ -> cst - in - let (j,cst'') = safe_machine env_ar c in - let issmall = is_small_type env_par c in - ((issmall,j), Constraint.union cst' cst'') - -let logic_constr env c = - for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c - -let logic_arity env c = - for_all_prods - (fun t -> - (not (is_info_type env Evd.empty t)) or (is_small_type env t.body)) - env c - -let is_unit env_par nparams ar spec = - match decomp_all_DLAMV_name spec with - | (_,[|c|]) -> - (let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) && - (let (_,c') = decompose_prod_n nparams c in logic_constr env_par c') - | _ -> false - -let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) = - let (lna,vc) = decomp_all_DLAMV_name spec in - let ((issmall,jlc),cst') = - List.fold_right - (fun c ((small,jl),cst) -> - let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in - ((small && sm,jc::jl), Constraint.union cst cst')) - (Array.to_list vc) - ((true,[]),Constraint.empty) - in - let castlc = List.map cast_of_judgment jlc in - let spec' = put_DLAMSV lna (Array.of_list castlc) in - let isunit = is_unit env_par nparams ar spec in - let (_,tyar) = lookup_rel (ninds+1-i) env_ar in - ((id,tyar,cnames,issmall,isunit,spec'), cst') - -let add_mind sp mie env = - mind_check_names mie; - mind_check_arities env mie; - let params = mind_extract_and_check_params mie in - let nparams = mie.mind_entry_nparams in - mind_check_lc params mie; - let ninds = List.length mie.mind_entry_inds in - let types_sign = - List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds - in - let env_arities = push_rels types_sign env in - let env_params = push_rels params env_arities in - let _,inds,cst = - List.fold_left - (fun (i,inds,cst) ind -> - let (ind',cst') = - type_one_inductive i env_arities env_params nparams ninds ind - in - (succ i,ind'::inds, Constraint.union cst cst')) - (1,[],Constraint.empty) - mie.mind_entry_inds - in - let kind = kind_of_path sp in - let mib = - cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst - in - add_mind sp mib (add_constraints cst env) - -let add_constraints = add_constraints - -let export = export -let import = import - -let unsafe_env_of_env e = e - -(*s Machines with information. *) - -type information = Logic | Inf of unsafe_judgment diff --git a/kernel/typing.mli b/kernel/typing.mli deleted file mode 100644 index 10530d123b..0000000000 --- a/kernel/typing.mli +++ /dev/null @@ -1,77 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Pp -open Names -open Term -open Univ -open Sign -open Constant -open Inductive -open Environ -open Typeops -(*i*) - -(*s Safe environments. Since we are now able to type terms, we can define an - abstract type of safe environments, where objects are typed before being - added. Internally, the datatype is still [unsafe_env]. We re-export the - functions of [Environ] for the new type [environment]. *) - -type environment - -val empty_environment : environment - -val universes : environment -> universes -val context : environment -> context - -val push_var : identifier * constr -> environment -> environment -val push_rel : name * constr -> environment -> environment -val add_constant : - section_path -> constant_entry -> environment -> environment -val add_parameter : - section_path -> constr -> environment -> environment -val add_mind : - section_path -> mutual_inductive_entry -> environment -> environment -val add_constraints : constraints -> environment -> environment - -val lookup_var : identifier -> environment -> name * typed_type -val lookup_rel : int -> environment -> name * typed_type -val lookup_constant : section_path -> environment -> constant_body -val lookup_mind : section_path -> environment -> mutual_inductive_body -val lookup_mind_specif : constr -> environment -> mind_specif - -val export : environment -> string -> compiled_env -val import : compiled_env -> environment -> environment - -val unsafe_env_of_env : environment -> unsafe_env - -(*s Typing without information. *) - -type judgment - -val j_val : judgment -> constr -val j_type : judgment -> constr -val j_kind : judgment -> constr - -val safe_machine : environment -> constr -> judgment * constraints -val safe_machine_type : environment -> constr -> typed_type - -val fix_machine : environment -> constr -> judgment * constraints -val fix_machine_type : environment -> constr -> typed_type - -val unsafe_machine : environment -> constr -> judgment * constraints -val unsafe_machine_type : environment -> constr -> typed_type - -val type_of : environment -> constr -> constr - -val type_of_type : environment -> constr -> constr - -val unsafe_type_of : environment -> constr -> constr - - -(*s Typing with information (extraction). *) - -type information = Logic | Inf of judgment - - -- cgit v1.2.3