Abstraction de constr

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

9 files changed, 68 insertions, 85 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 257cba2b14..803d197f18 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -9,7 +9,6 @@ open Univ
 (* open Generic *)
 open Term
 open Declarations
-open Abstraction
 
 (* The type of environments. *)
 
@@ -17,12 +16,11 @@ type checksum = int
 
 type import = string * checksum
 
-type global = Constant | Inductive | Abstraction
+type global = Constant | Inductive
 
 type globals = {
   env_constants : constant_body Spmap.t;
   env_inductives : mutual_inductive_body Spmap.t;
-  env_abstractions : abstraction_body Spmap.t;
   env_locals : (global * section_path) list;
   env_imports : import list }
 
@@ -44,7 +42,6 @@ let empty_env = {
   env_globals = {
     env_constants = Spmap.empty;
     env_inductives = Spmap.empty;
-    env_abstractions = Spmap.empty;
     env_locals = [];
     env_imports = [] };
   env_universes = initial_universes }
@@ -110,7 +107,7 @@ let push_rels_to_vars env =
     (fun (na,c,t) (subst,avoid,sign) ->
        let na = if na = Anonymous then Name(id_of_string"_") else na in
        let id = next_name_away na avoid in
-       ((VAR id)::subst,id::avoid,
+       ((mkVar id)::subst,id::avoid,
 	add_var (id,option_app (substl subst) c,typed_app (substl subst) t)
 	  sign))
     env.env_context.env_rel_context ([],ids_of_var_context sign0,sign0)
@@ -166,15 +163,6 @@ let add_mind sp mib env =
 	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
-let add_abstraction sp ab env =
-  let new_abs = Spmap.add sp ab env.env_globals.env_abstractions in
-  let new_locals = (Abstraction,sp)::env.env_globals.env_locals in
-  let new_globals = 
-    { env.env_globals with 
-	env_abstractions = new_abs;
-	env_locals = new_locals } in
-  { env with env_globals = new_globals }
-
 let meta_ctr=ref 0;;
 
 let new_meta ()=incr meta_ctr;!meta_ctr;;
@@ -201,9 +189,6 @@ let lookup_constant sp env =
 let lookup_mind sp env =
   Spmap.find sp env.env_globals.env_inductives
 
-let lookup_abst sp env =
-  Spmap.find sp env.env_globals.env_abstractions
-
 (* First character of a constr *)
 
 let lowercase_first_char id = String.lowercase (first_char id)
@@ -311,12 +296,12 @@ let make_all_name_different env =
     env
 
 (* Constants *)
-let defined_constant env = function
-  | DOPN (Const sp, _) -> is_defined (lookup_constant sp env)
+let defined_constant env c = match kind_of_term c with
+  | IsConst (sp, _) -> is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
 
-let opaque_constant env = function
-  | DOPN (Const sp, _) -> is_opaque (lookup_constant sp env)
+let opaque_constant env c = match kind_of_term c with
+  | IsConst (sp, _) -> is_opaque (lookup_constant sp env)
   | _ -> invalid_arg "opaque_constant"
 
 (* A const is evaluable if it is defined and not opaque *)
@@ -333,15 +318,13 @@ type compiled_env = {
   cenv_stamp : checksum;
   cenv_needed : import list;
   cenv_constants : (section_path * constant_body) list;
-  cenv_inductives : (section_path * mutual_inductive_body) list;
-  cenv_abstractions : (section_path * abstraction_body) list }
+  cenv_inductives : (section_path * mutual_inductive_body) list }
 
 let exported_objects env =
   let gl = env.env_globals in
   let separate (cst,ind,abs) = function
     | (Constant,sp) -> (sp,Spmap.find sp gl.env_constants)::cst,ind,abs
     | (Inductive,sp) -> cst,(sp,Spmap.find sp gl.env_inductives)::ind,abs
-    | (Abstraction,sp) -> cst,ind,(sp,Spmap.find sp gl.env_abstractions)::abs
   in
   List.fold_left separate ([],[],[]) gl.env_locals
 
@@ -351,8 +334,7 @@ let export env id =
     cenv_stamp = 0;
     cenv_needed = env.env_globals.env_imports;
     cenv_constants = cst;
-    cenv_inductives = ind;
-    cenv_abstractions = abs }
+    cenv_inductives = ind }
 
 let check_imports env needed =
   let imports = env.env_globals.env_imports in
@@ -380,7 +362,6 @@ let import cenv env =
   let new_globals = 
     { env_constants = add_list gl.env_constants cenv.cenv_constants;
       env_inductives = add_list gl.env_inductives cenv.cenv_inductives;
-      env_abstractions = add_list gl.env_abstractions cenv.cenv_abstractions;
       env_locals = gl.env_locals;
       env_imports = (cenv.cenv_id,cenv.cenv_stamp) :: gl.env_imports }
   in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 840d10ab76..e9270c5583 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -5,7 +5,6 @@
 open Names
 open Term
 open Declarations
-open Abstraction
 open Univ
 open Sign
 (*i*)
@@ -74,9 +73,6 @@ val add_constant :
   section_path -> constant_body -> env -> env
 val add_mind : 
   section_path -> mutual_inductive_body -> env -> env
-val add_abstraction : 
-  section_path -> abstraction_body -> env -> env
-
 val new_meta : unit -> int
 
 (*s Looks up in environment *)
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 6853fc9c46..b482f94538 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -66,6 +66,7 @@ let is_defined sigma ev =
   not (info.evar_body = Evar_empty)
 
 let evar_hyps ev = var_context ev.evar_env
+let evar_body ev = ev.evar_body
 
 let id_of_existential ev =
   id_of_string ("?" ^ string_of_int ev)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 3ae00f6519..4315994964 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -49,5 +49,6 @@ val is_evar : 'a evar_map -> evar -> bool
 val is_defined : 'a evar_map -> evar -> bool
 
 val evar_hyps : 'a evar_info -> var_context
+val evar_body : 'a evar_info -> evar_body
 
 val id_of_existential : evar -> identifier
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b8649ffb2e..ee58603117 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -128,16 +128,16 @@ let explain_ind_err ntyp env0 nbpar c err =
   let env = push_rels lpar env0 in
   match err with
     | LocalNonPos kt -> 
-	raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
+	raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
     | LocalNotEnoughArgs kt -> 
 	raise (InductiveError 
-		 (NotEnoughArgs (env,c',Rel (kt+nbpar))))
+		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
     | LocalNotConstructor ->
 	raise (InductiveError 
-		 (NotConstructor (env,c',Rel (ntyp+nbpar))))
+		 (NotConstructor (env,c',mkRel (ntyp+nbpar))))
     | LocalNonPar (n,l) ->
 	raise (InductiveError 
-		 (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
+		 (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
 
 let failwith_non_pos_vect n ntypes v =
   for i = 0 to Array.length v - 1 do
@@ -153,8 +153,9 @@ let check_correct_par env nparams ntypes n l largs =
     raise (IllFormedInd (LocalNotEnoughArgs l));
   let (lpar,largs') = array_chop nparams largs in
   for k = 0 to nparams - 1 do
-    if not ((Rel (n-k-1))= whd_betadeltaiotaeta env Evd.empty lpar.(k)) then
-      raise (IllFormedInd (LocalNonPar (k+1,l)))
+    match kind_of_term (whd_betadeltaiotaeta env Evd.empty lpar.(k)) with
+      | IsRel w when (n-k-1 = w) -> ()
+      | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
   done;
   if not (array_for_all (noccur_between n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
@@ -166,7 +167,7 @@ let abstract_mind_lc env ntyps npars lc =
   else 
     let make_abs = 
       list_tabulate
-	(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps 
+	(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps 
     in 
     Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2f5e02ad43..33d15798a4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -67,7 +67,7 @@ let mis_type_nf_mconstruct i mispec =
   let specif = mis_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
@@ -75,7 +75,7 @@ let mis_type_mconstruct i mispec =
   let specif = mis_typed_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index ed625a22f0..7888afd390 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -12,8 +12,8 @@ open Declarations
 open Environ
 
 let is_id_inst inst =
-  let is_id = function
-    | id, VAR id' -> id = id'
+  let is_id (id,c) = match kind_of_term c with
+    | IsVar id' -> id = id'
     | _ -> false
   in
   List.for_all is_id inst
@@ -36,15 +36,14 @@ let constant_type env sigma (sp,args) =
   (* TODO: check args *)
   instantiate_type cb.const_hyps cb.const_type (Array.to_list args)
 
-type const_evaluation_error = NotDefinedConst | OpaqueConst
+type const_evaluation_result = NoBody | Opaque
 
-exception NotEvaluableConst of const_evaluation_error
+exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env cst =
-  let (sp,args) = destConst cst in
+let constant_value env (sp,args) =
   let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst OpaqueConst) else
-  if not (is_defined cb) then raise (NotEvaluableConst NotDefinedConst) else
+  if cb.const_opaque then raise (NotEvaluableConst Opaque) else
+  if not (is_defined cb) then raise (NotEvaluableConst NoBody) else
   match cb.const_body with
     | Some v -> 
 	let body = cook_constant v in
@@ -53,6 +52,10 @@ let constant_value env cst =
 	anomalylabstrm "termenv__constant_value"
 	  [< 'sTR "a defined constant with no body." >]
 
+let constant_opt_value env cst =
+  try Some (constant_value env cst)
+  with NotEvaluableConst _ -> None
+
 (* Existentials. *)
 
 let name_of_existential n = id_of_string ("?" ^ string_of_int n)
@@ -63,23 +66,17 @@ let existential_type sigma (n,args) =
   (* TODO: check args [this comment was in Typeops] *)
   instantiate_constr hyps info.evar_concl (Array.to_list args)
 
+exception NotInstantiatedEvar
+
 let existential_value sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
-  match info.evar_body with
+  match evar_body info with
     | Evar_defined c ->
 	instantiate_constr hyps c (Array.to_list args)
     | Evar_empty ->
-	anomaly "a defined existential with no body"
-
-let const_evar_opt_value env sigma c =
-  match c with
-    | DOPN(Const sp,_) ->
-	if evaluable_constant env c then Some (constant_value env c) else None
-    | DOPN(Evar ev,args) ->
-	if Evd.is_defined sigma ev then 
-	  Some (existential_value sigma (ev,args)) 
-	else 
-	  None
-    | _ -> invalid_arg "const_abst_opt_value"
+	raise NotInstantiatedEvar
 
+let existential_opt_value sigma ev =
+  try Some (existential_value sigma ev)
+  with NotInstantiatedEvar -> None
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 0d8c2a3039..f0719d2f1e 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -16,15 +16,21 @@ val instantiate_constr :
 val instantiate_type : 
   var_context -> typed_type -> constr list -> typed_type
 
-type const_evaluation_error = NotDefinedConst | OpaqueConst
-exception NotEvaluableConst of const_evaluation_error
+(*s [constant_value env c] raises [NotEvaluableConst Opaque] if
+   [c] is opaque and [NotEvaluableConst NoBody] if it has no
+   body and [Not_found] if it does not exist in [env] *)
 
-(* [constant_value env c] raises [NotEvaluableConst OpaqueConst] if
-   [c] is opaque and [NotEvaluableConst NotDefinedConst] if undefined *)
-val constant_value : env -> constr -> constr
+type const_evaluation_result = NoBody | Opaque
+exception NotEvaluableConst of const_evaluation_result
+
+val constant_value : env -> constant -> constr
 val constant_type : env -> 'a evar_map -> constant -> typed_type
+val constant_opt_value : env -> constant -> constr option
+
+(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+no body and [Not_found] if it does not exist in [sigma] *)
 
+exception NotInstantiatedEvar
 val existential_value : 'a evar_map -> existential -> constr
 val existential_type : 'a evar_map -> existential -> constr
-
-val const_evar_opt_value : env -> 'a evar_map -> constr -> constr option
+val existential_opt_value : 'a evar_map -> existential -> constr option
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 58295ee35e..d3b8383262 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -25,14 +25,14 @@ let typed_type_of_judgment env sigma j = j.uj_type
 
 (* This should be a type intended to be assumed *)
 let assumption_of_judgment env sigma j =
-  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) -> make_typed j.uj_val s
+  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    | IsSort s -> make_typed j.uj_val s
     | _ -> error_assumption CCI env j.uj_val
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env sigma j =
-  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) -> {utj_val = j.uj_val; utj_type = s }
+  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    | IsSort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type CCI env j
 
 let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
@@ -42,7 +42,7 @@ let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
 let relative env sigma n = 
   try
     let (_,typ) = lookup_rel_type n env in
-    { uj_val  = Rel n;
+    { uj_val  = mkRel n;
       uj_type = typed_app (lift n) typ }
   with Not_found -> 
     error_unbound_rel CCI env sigma n
@@ -141,7 +141,7 @@ let is_correct_arity env sigma kelim (c,p) indf (pt,t) =
 	    raise (Arity None)
       | IsProd (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env sigma a2 in 
-          let ksort = (match k with DOP0(Sort s) -> s 
+          let ksort = (match kind_of_term k with IsSort s -> s 
 			 | _ -> raise (Arity None)) in
 	  let ind = build_dependent_inductive indf in
           if is_conv env sigma a1 ind then
@@ -219,12 +219,12 @@ let type_of_case env sigma ci pj cj lfj =
 (* Prop and Set *)
 
 let judge_of_prop =
-  { uj_val = DOP0(Sort prop);
-    uj_type = make_typed (DOP0(Sort type_0)) type_1 }
+  { uj_val = mkSort prop;
+    uj_type = make_typed (mkSort type_0) type_1 }
 
 let judge_of_set =
-  { uj_val = DOP0(Sort spec);
-    uj_type = make_typed (DOP0(Sort type_0)) type_1 }
+  { uj_val = mkSort spec;
+    uj_type = make_typed (mkSort type_0) type_1 }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
@@ -234,14 +234,14 @@ let judge_of_prop_contents = function
 
 let judge_of_type u =
   let (uu,uuu,c) = super_super u in
-  { uj_val = DOP0 (Sort (Type u));
-    uj_type = make_typed (DOP0(Sort (Type uu))) (Type uuu) },
+  { uj_val = mkSort (Type u);
+    uj_type = make_typed (mkSort (Type uu)) (Type uuu) },
   c
 
 let type_of_sort c =
-  match c with
-    | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in Type uu, cst
-    | DOP0 (Sort (Prop _)) -> Type prop_univ, Constraint.empty
+  match kind_of_term c with
+    | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst
+    | IsSort (Prop _) -> Type prop_univ, Constraint.empty
     | _ -> invalid_arg "type_of_sort"
 
 (* Type of a lambda-abstraction. *)
@@ -290,8 +290,8 @@ let abs_rel env sigma name var j =
 
 let gen_rel env sigma name varj j =
   let var = assumption_of_type_judgment varj in
-  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) ->
+  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    | IsSort s ->
 	let (s',g) = sort_of_product varj.utj_type s (universes env) in
 	let res_type = mkSort s' in
 	let (res_kind,g') = type_of_sort res_type in