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/typing.ml | 415 -------------------------------------------------------
 1 file changed, 415 deletions(-)
 delete mode 100644 kernel/typing.ml

(limited to 'kernel/typing.ml')

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
-- 
cgit v1.2.3