Passage à des contextes de vars et de rels pouvant contenir des déclarations

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

5 files changed, 146 insertions, 59 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 0bce97fe4c..404ecda317 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -38,11 +38,15 @@ let make_strength_2 () =
   make_strength path
 
 
-(* Variables. *)
+(* Section variables. *)
+
+type section_variable_entry =
+  | SectionLocalDef of constr
+  | SectionLocalDecl of constr
 
 type sticky = bool
 
-type variable_declaration = constr * strength * sticky
+type variable_declaration = section_variable_entry * strength * sticky
 
 let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 
@@ -51,8 +55,11 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,(id,(ty,_,_) as vd,imps)) = 
-  Global.push_var (id,ty);
+let cache_variable (sp,((id,(d,_,_) as vd),imps)) =
+  begin match d with (* Fails if not well-typed *)
+    | SectionLocalDecl ty -> Global.push_var_decl (id,ty)
+    | SectionLocalDef c -> Global.push_var_def (id,c)
+  end;
   Nametab.push id sp;
   if imps then declare_var_implicits id;
   vartab := Spmap.add sp vd !vartab
@@ -63,7 +70,7 @@ let open_variable _ = ()
 
 let specification_variable x = x
 
-let (in_variable, out_variable) =
+let (in_variable, _ (* out_variable *) ) =
   let od = {
     cache_function = cache_variable;
     load_function = load_variable;
@@ -197,8 +204,8 @@ let is_variable id =
   
 let out_variable sp = 
   let (id,(_,str,sticky)) = Spmap.find sp !vartab in
-  let (_,ty) = Global.lookup_var id in
-  (id,ty,str,sticky)
+  let (c,ty) = Global.lookup_var id in
+  ((id,c,ty),str,sticky)
 
 let variable_strength id =
   let sp = Nametab.sp_of_id CCI id in 
@@ -229,22 +236,68 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let construct_operator env sp id =
+let global_sp_operator env sp id =
   try
     let cb = Environ.lookup_constant sp env in Const sp, cb.const_hyps
   with Not_found -> 
     let mib = Environ.lookup_mind sp env in
     mind_oper_of_id sp id mib, mib.mind_hyps
 
-let global_operator sp id = construct_operator (Global.env()) sp id
+let global_operator kind id =
+  let sp = Nametab.sp_of_id kind id in
+  global_sp_operator (Global.env()) sp id
 
+(*
 let construct_sp_reference env sp id =
-  let (oper,hyps) = construct_operator env sp id in
+  let (oper,hyps) = global_sp_operator env sp id in
   let hyps' = Global.var_context () in
   if not (hyps_inclusion env Evd.empty hyps hyps') then
     error_reference_variables CCI env id;
   let ids = ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+*)
+
+let occur_decl env (id,c,t) hyps =
+  try
+    let (c',t') = Sign.lookup_id id hyps in
+    let matching_bodies = match c,c' with
+      | None, _ -> true
+      | Some c, None -> false
+      | Some c, Some c' -> is_conv env Evd.empty c c' in
+    let matching_types = 
+      is_conv env Evd.empty (body_of_type t) (body_of_type t') in
+    matching_types & matching_bodies
+  with Not_found -> false
+
+(*
+let rec find_common_hyps_then_abstract c env hyps' = function
+  | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
+      find_common_hyps_then_abstract c (Environ.push_var d env) hyps' hyps
+  | hyps ->
+      Environ.it_mkNamedLambda_or_LetIn c hyps
+
+let find_common_hyps_then_abstract c env hyps' hyps =
+  find_common_hyps_then_abstract c env hyps' (List.rev hyps)
+*)
+
+let find_common_hyps_then_abstract c env hyps' hyps = 
+  snd (fold_var_context_both_sides
+	 (fun
+	    (env,c) (id,_,_ as d) hyps ->
+	      if occur_decl env d hyps' then 
+		(Environ.push_var d env,c)
+	      else
+		(env, Environ.it_mkNamedLambda_or_LetIn c hyps))
+	 hyps
+	 (env,c))
+
+let construct_sp_reference env sp id =
+  let (oper,hyps) = global_sp_operator env sp id in
+  let hyps0 = Global.var_context () in
+  let env0 = Environ.reset_context env in
+  let args = List.map mkVar (ids_of_var_context hyps) in
+  let body = DOPN(oper,Array.of_list args) in
+  find_common_hyps_then_abstract body env0 hyps0 hyps
 
 let construct_reference env kind id =
   try
@@ -271,11 +324,11 @@ let global_reference_imps kind id =
     | VAR id ->
 	c, implicits_of_var id
     | _ -> assert false
-
+(*
 let global env id =
   try let _ = lookup_glob id (Environ.context env) in VAR id
   with Not_found -> global_reference CCI id
-
+*)
 let is_global id =
   try 
     let osp = Nametab.sp_of_id CCI id in
@@ -299,10 +352,20 @@ let path_of_inductive_path (sp,tyi) =
 
 (* Eliminations. *)
 
+let eliminations = [ (prop,"_ind") ; (spec,"_rec") ; (types,"_rect") ]
+
+let elimination_suffix = function
+  | Type _    -> "_rect"
+  | Prop Null -> "_ind"
+  | Prop Pos  -> "_rec"
+
 let declare_eliminations sp i =
   let oper = MutInd (sp,i) in
   let mib = Global.lookup_mind sp in
-  let ids = ids_of_sign mib.mind_hyps in
+  let ids = ids_of_var_context mib.mind_hyps in
+  if not (list_subset ids (ids_of_var_context (Global.var_context ()))) then
+    error ("Declarations of elimination scheme outside the section "^
+    "of the inductive definition is not implemented");
   let ctxt = Array.of_list (List.map (fun id -> VAR id) ids) in
   let mispec = Global.lookup_mind_specif ((sp,i),ctxt) in 
   let mindstr = string_of_id (mis_typename mispec) in
@@ -318,11 +381,15 @@ let declare_eliminations sp i =
   let npars = mis_nparams mispec in
   let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
   let kelim = mis_kelim mispec in
-  if List.mem prop kelim then
-    declare (mindstr^"_ind") (make_elim prop);
-  if List.mem spec kelim then
-    declare (mindstr^"_rec") (make_elim spec);
-  if List.mem types kelim then
-    declare (mindstr^"_rect") (make_elim (Type (Univ.new_univ sp)))
+  List.iter
+    (fun (sort,suff) -> 
+       if List.mem sort kelim then declare (mindstr^suff) (make_elim sort))
+    eliminations
+
+(* Look up function for the default elimination constant *)
+
+let lookup_eliminator env path s =
+  let s = (string_of_id (basename path))^(elimination_suffix s) in
+  construct_reference env (kind_of_path path) (id_of_string s)
 
       
diff --git a/library/declare.mli b/library/declare.mli
index 9bb9c1607c..f078c91661 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -20,9 +20,13 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
+type section_variable_entry =
+  | SectionLocalDef of constr
+  | SectionLocalDecl of constr
+
 type sticky = bool
 
-type variable_declaration = constr * strength * sticky
+type variable_declaration = section_variable_entry * strength * sticky
 val declare_variable : identifier -> variable_declaration -> unit
 
 type constant_declaration = constant_entry * strength
@@ -46,16 +50,15 @@ val constant_strength : section_path -> strength
 val constant_or_parameter_strength : section_path -> strength
 
 val is_variable : identifier -> bool
-val out_variable : 
-  section_path -> identifier * typed_type * strength * sticky
+val out_variable : section_path -> var_declaration * strength * sticky
 val variable_strength : identifier -> strength
 
 
-(*s [global_operator sp id] returns the operator (constant, inductive or
-    construtor) corresponding to [(sp,id)] in global environment, together
+(*s [global_operator k id] returns the operator (constant, inductive or
+    construtor) corresponding to [id] in global environment, together
     with its definition environment. *)
 
-val global_operator : section_path -> identifier -> sorts oper * var_context
+val global_operator : path_kind -> identifier -> sorts oper * var_context
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant, 
@@ -76,3 +79,7 @@ val is_global : identifier -> bool
 
 val path_of_inductive_path : inductive_path -> section_path
 val path_of_constructor_path : constructor_path -> section_path
+
+(* Look up function for the default elimination constant *)
+val elimination_suffix : sorts -> string
+val lookup_eliminator : Environ.env -> section_path -> sorts -> constr
diff --git a/library/global.ml b/library/global.ml
index cf3d88ca93..a37863a78f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -30,8 +30,12 @@ let universes () = universes !global_env
 let context () = context !global_env
 let var_context () = var_context !global_env
 
-let push_var idc = global_env := push_var idc !global_env
-let push_rel nac = global_env := push_rel nac !global_env
+let push_var_def idc = global_env := push_var_def idc !global_env
+let push_var_decl idc = global_env := push_var_decl idc !global_env
+(*
+let push_rel_def nac = global_env := push_rel nac !global_env
+let push_rel_decl nac = global_env := push_rel nac !global_env
+*)
 let add_constant sp ce = global_env := add_constant sp ce !global_env
 let add_parameter sp c = global_env := add_parameter sp c !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
@@ -40,7 +44,9 @@ let add_constraints c = global_env := add_constraints c !global_env
 let pop_vars ids = global_env := pop_vars ids !global_env
 
 let lookup_var id = lookup_var id !global_env
+(*
 let lookup_rel n = lookup_rel n !global_env
+*)
 let lookup_constant sp = lookup_constant sp !global_env
 let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
diff --git a/library/global.mli b/library/global.mli
index 19d5166257..c2e8ac386c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -23,8 +23,13 @@ val universes : unit -> universes
 val context : unit -> context
 val var_context : unit -> var_context
 
-val push_var : identifier * constr -> unit
-val push_rel : name * constr -> unit
+val push_var_decl : identifier * constr -> unit
+val push_var_def : identifier * constr -> unit
+(*
+val push_var : identifier * constr option * constr -> unit
+val push_rel_decl : name * constr -> unit
+val push_rel_def : name * constr -> unit
+*)
 val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
@@ -32,8 +37,8 @@ val add_constraints : constraints -> unit
 
 val pop_vars : identifier list -> unit
 
-val lookup_var : identifier -> name * typed_type
-val lookup_rel : int -> name * typed_type
+val lookup_var : identifier -> constr option * typed_type
+(*val lookup_rel : int -> name * typed_type*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
diff --git a/library/indrec.ml b/library/indrec.ml
index d24ce2aa6a..42d067d492 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -70,7 +70,7 @@ let mis_make_case_com depopt env sigma mispec kind =
   in
   let indf = make_ind_family (mispec,rel_list 0 nparams) in
   let typP = make_arity env' dep indf kind in
-  it_lambda_name env (mkLambda_string "P" typP (add_branch 0)) lnamespar
+  it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP (add_branch 0)) lnamespar
     
 (* check if the type depends recursively on one of the inductive scheme *)
 
@@ -154,32 +154,34 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
     prec 0 
   in
   (* ici, cstrprods est la liste des produits du constructeur instantié *)
-  let rec process_constr i cstrprods f recargs = 
-    match cstrprods with 
-      | (n,t)::cprest -> 
-          let (optionpos,rest) = 
-	    match recargs with 
-	      | [] -> (* Impossible?! *) None,[] 
-              | (Param(i)::rest) -> None,rest 
-              | (Norec::rest) -> None,rest 
-              | (Imbr _::rest) -> None,rest 
-              | (Mrec i::rest) -> fvect.(i),rest 
-	  in 
-          (match optionpos with 
-             | None -> 
-		 lambda_name env
-		   (n,t,process_constr (i+1) cprest 
-		      (applist(whd_beta_stack (lift 1 f) [(Rel 1)])) rest)
-             | Some(_,f_0) -> 
-		 let nF = lift (i+1+decF) f_0 in
-		 let arg = process_pos nF (lift 1 t) in 
-                 lambda_name env
-		   (n,t,process_constr (i+1) cprest 
-		      (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) 
-		      rest))
-      | [] -> f
-  in 
-  process_constr 0 (List.rev cstr.cs_args) f recargs 
+  let rec process_constr i f = function
+    | (n,None,t)::cprest, recarg::rest -> 
+        let optionpos = 
+	  match recarg with 
+            | Param i -> None
+            | Norec   -> None
+            | Imbr _  -> None
+            | Mrec i  -> fvect.(i)
+	in 
+        (match optionpos with 
+           | None -> 
+	       lambda_name env
+		 (n,incast_type t,process_constr (i+1)
+		    (applist(whd_beta_stack (lift 1 f) [(Rel 1)]))
+		    (cprest,rest))
+           | Some(_,f_0) -> 
+	       let nF = lift (i+1+decF) f_0 in
+	       let arg = process_pos nF (lift 1 (body_of_type t)) in 
+               lambda_name env
+		 (n,incast_type t,process_constr (i+1)
+		    (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) 
+		    (cprest,rest)))
+    | (n,Some c,t)::cprest, rest -> failwith "TODO"
+    | [],[] -> f
+    | _,[] | [],_ -> anomaly "process_constr"
+
+  in
+  process_constr 0 f (List.rev cstr.cs_args, recargs)
 
 (* Main function *)
 let mis_make_indrec env sigma listdepkind mispec =
@@ -290,7 +292,7 @@ let mis_make_indrec env sigma listdepkind mispec =
     if mis_is_recursive_subset
       (List.map (fun (mispec,_,_) -> mis_index mispec) listdepkind) mispeci
     then 
-      it_lambda_name env (put_arity 0 listdepkind) lnamespar
+      it_mkLambda_or_LetIn_name env (put_arity 0 listdepkind) lnamespar
     else 
       mis_make_case_com (Some dep) env sigma mispeci kind 
   in