Ajout de constantes locales dans les Records

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

3 files changed, 133 insertions, 121 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 826732c24..45f50d441 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -5,167 +5,166 @@ open Pp
 open Util
 open Names
 open Term
+open Environ
 open Declarations
 open Declare
 open Coqast
-open Ast
 open Astterm
 open Command
 
 (********** definition d'un record (structure) **************)
 
-let make_constructor fields appc =
+let make_constructor idstruc idps fields  =
+  let app_constructor = 
+    Ast.ope("APPLISTEXPL",
+        (Ast.nvar (string_of_id idstruc))::
+        List.map (fun id -> Ast.nvar(string_of_id id)) idps) in
   let rec aux fields =
     match fields with
-      | [] -> appc
-      | (id,ty)::l -> ope("PROD",[ty; slam(Some (string_of_id id), aux l)]) 
+      | [] -> app_constructor
+      | (id,true,ty)::l ->
+	  Ast.ope("PROD",[ty; Ast.slam(Some (string_of_id id), aux l)])
+      | (id,false,c)::l ->
+	  Ast.ope("LETIN",[c; Ast.slam(Some (string_of_id id), aux l)])
   in 
   aux fields
 
-(* free_vars existe de'ja` dans ast.ml *)
-
-let rec drop = function
-  | [] -> []
-  | (None::t) -> drop t
-  | ((Some id)::t) -> id::(drop t)
-
-let fold curriedf l base =
-  List.fold_right (fun a -> fun b -> curriedf(a,b)) l base
-    
-let free_vars t = 
-  let rec aux = function
-    | (Nvar(_,s),accum) -> list_add_set (id_of_string s) accum
-    | (Node(_,_,tl),accum) -> fold aux tl accum
-    | (Slam(_,None,body),accum) -> (aux(body,[]))@accum
-    | (Slam(_,Some id,body),accum) ->
-	(list_subtract (aux(body,[])) [(id_of_string id)])@accum
-    | (_,accum) -> accum
-  in 
-  aux(t,[]) 
-
-let free_in_asts id l = 
-  let rec aux =
-    function 
-      | [] -> true
-      | a::l -> (not (List.mem id (free_vars a))) & (aux l) 
-  in
-  aux l
+let occur_fields id fs =
+  List.exists (fun (_,_,a) -> Ast.occur_var_ast (string_of_id id) a) fs
 
-let all_vars t = 
-  let rec aux = function
-    | (Nvar(_,id),accum) -> list_add_set (id_of_string id) accum
-    | (Node(_,_,tl),accum) -> fold aux tl accum
-    | (Slam(_,None,body),accum) -> aux (body,accum)
-    | (Slam(_,Some id,body),accum) ->
-	aux (body,(list_union accum [(id_of_string id)]))
-    | (_,accum) -> accum
-  in 
-  aux(t,[]) 
-   
-let pr_id_list l = 
-  [< 'sTR "[" ; prlist_with_sep pr_coma pr_id l; 'sTR "]" >]
-
-open Environ
+let interp_decl sigma env (id,assum,t) =
+  if assum then
+    (id,None,interp_type Evd.empty env t)
+  else
+    let j = judgment_of_rawconstr Evd.empty env t in
+    (id,Some j.uj_val, j.uj_type)
 
 let typecheck_params_and_field ps fs =
   let env0 = Global.env () in
   let env1,newps =
     List.fold_left
       (fun (env,newps) (id,t) -> 
-         let tj = interp_type Evd.empty env t in
-         (push_named_assum (id,tj) env,(id,tj)::newps))
+         let decl = interp_decl Evd.empty env (id,true,t) in
+         (push_named_decl decl env,decl::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
-      (fun (env,newfs) (id,t) -> 
-         let ass = interp_type Evd.empty env t in
-         (push_named_assum (id,ass) env,(id,ass)::newfs)) (env1,[]) fs
+      (fun (env,newfs) d ->
+         let decl = interp_decl Evd.empty env d in
+         (push_named_decl decl env, decl::newfs))
+      (env1,[]) fs
+  in
+  newps, newfs
+
+type record_error =
+  | MissingProj of identifier * identifier list
+  | BadTypedProj of identifier * path_kind * env * Type_errors.type_error
+
+let warning_or_error coe err =
+  let st = match err with
+    | MissingProj (fi,projs) ->
+	let s,have = if List.length projs > 1 then "s","have" else "","has" in
+        [< 'sTR(string_of_id fi);
+	   'sTR" cannot be defined because the projection"; 'sTR s; 'sPC;
+           prlist_with_sep pr_coma pr_id projs; 'sPC; 'sTR have; 'sTR "n't." >]
+    | BadTypedProj (fi,k,ctx,te) ->
+        [<'sTR (string_of_id fi); 
+          'sTR" cannot be defined for the following reason:";
+	  'fNL; 'sTR "  "; hOV 2 (Himsg.explain_type_error k ctx te) >]
   in
-  List.rev(newps),List.rev(newfs)
-
-let mk_LambdaCit = List.fold_right (fun (x,a) b -> mkNamedLambda x a b)
-
-let warning_or_error coe st = 
   if coe then errorlabstrm "structure" st;
   pPNL (hOV 0 [< 'sTR"Warning: "; st >])
 
 (* We build projections *)
-let declare_projections idstruc coers params fields =
+let declare_projections idstruc coers paramdecls fields =
   let r = global_reference CCI idstruc in
-  let lp = List.length params in
-  let rp1 = applist (r,(rel_list 0 lp)) in
-  let rp2 = applist (r,(rel_list 1 lp)) in
+  let paramargs = List.rev (List.map (fun (id,_,_) -> mkVar id) paramdecls) in
+  let rp = applist (r, paramargs) in
   let x = Environ.named_hd (Global.env()) r Anonymous in
-  let args =  (* Rel 1 refers to "x" *)
-    (List.map (fun (id,_) -> mkVar id) params)@[mkRel 1] in
+  let proj_args = (* Rel 1 refers to "x" *) paramargs@[mkRel 1] in
   let (sp_projs,_,_) =
     List.fold_left2
-      (fun (sp_projs,ids_not_ok,subst) coe (fi,ti) -> 
-	 let fv_ti = global_vars ti in
+      (fun (sp_projs,ids_not_ok,subst) coe (fi,optci,ti) ->
+	 let fv_ti = match optci with
+	   | Some ci -> global_vars ci (* Type is then meaningless *)
+	   | None -> global_vars ti in
 	 let bad_projs = (list_intersect ids_not_ok fv_ti) in
 	 if bad_projs <> [] then begin
-	   let s,have =
-	     if List.length bad_projs > 1 then "s","have" else "","has" in
-	   (warning_or_error coe
-              [< 'sTR(string_of_id fi);
-		 'sTR" cannot be defined because the projection"; 'sTR s; 'sPC;
-                 prlist_with_sep pr_coma pr_id bad_projs;
-		 'sPC; 'sTR have; 'sTR "n't." >]);
+	   warning_or_error coe (MissingProj (fi,bad_projs));
            (None::sp_projs,fi::ids_not_ok,subst)
-         end else 
-	   let p = mkLambda (x, rp2, replace_vars subst ti) in
-	   let branch = mk_LambdaCit fields (mkVar fi) in
-	   let ci = Inductive.make_case_info
-		      (Global.lookup_mind_specif (destMutInd r))
-		      (Some PrintLet) [| RegularPat |] in
-	   let proj = mk_LambdaCit params 
-			(mkLambda (x, rp1,
-				   mkMutCase (ci, p, mkRel 1, [|branch|]))) in
+         end else
+	   let body = match optci with
+	     | Some ci -> replace_vars subst ci
+	     | None ->
+		 let p = mkLambda (x, rp, replace_vars subst ti) in
+		 let branch = it_mkNamedLambda_or_LetIn (mkVar fi) fields in
+		 let ci = Inductive.make_case_info
+			    (Global.lookup_mind_specif (destMutInd r))
+			    (Some PrintLet) [| RegularPat |] in
+		 mkMutCase (ci, p, mkRel 1, [|branch|]) in
+	   let proj =
+	     it_mkNamedLambda_or_LetIn (mkLambda (x, rp, body)) paramdecls in
 	   let ok = 
 	     try
-	       let cie =
-		 { const_entry_body = proj;
-		   const_entry_type = None } in
-	       (declare_constant fi (ConstantEntry cie,NeverDischarge,false); 
-		true)
-             with Type_errors.TypeError (k,ctx,te) ->
-               ((warning_or_error coe 
-                   [<'sTR (string_of_id fi); 
-                     'sTR" cannot be defined for the following reason:";
-		     'fNL; 'sTR "  ";
-		     hOV 2 (Himsg.explain_type_error k ctx te) >]);
-		false) in
+	       let cie = { const_entry_body = proj; const_entry_type = None} in
+	       declare_constant fi (ConstantEntry cie,NeverDischarge,false); 
+	       true
+             with Type_errors.TypeError (k,ctx,te) -> begin
+               warning_or_error coe (BadTypedProj (fi,k,ctx,te));
+	       false
+	     end in
 	   if not ok then 
 	     (None::sp_projs,fi::ids_not_ok,subst)
 	   else begin
              if coe then
 	       Class.try_add_new_coercion_record fi NeverDischarge idstruc;
              let constr_fi = global_reference CCI fi in
-             let constr_fip = applist (constr_fi,args)
+             let constr_fip = applist (constr_fi,proj_args)
              in (Some(path_of_const constr_fi)::sp_projs,
 		 ids_not_ok, (fi,constr_fip)::subst)
 	   end)
-      ([],[],[]) coers fields
+      ([],[],[]) coers (List.rev fields)
   in sp_projs
 
-(* Fields have names [idfs] and types [tyfs]; [coers] is a boolean list 
-   telling if the corresponding field must me a coercion *)
+let degenerate_decl env =
+  snd 
+    (List.fold_right
+       (fun (id,c,t) (ids,env) ->
+	  let d = match c with
+	    | None -> LocalAssum (subst_vars ids t)
+	    | Some c -> LocalDef (subst_vars ids c) in
+	  (id::ids, (id,d)::env))
+       env ([],[]))
+
+(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
+   list telling if the corresponding fields must me declared as coercion *)
 let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
-  let coers,fs = List.split cfs in     
-  let idps,typs = List.split ps in      
-  let idfs,tyfs = List.split fs in
-  if not (free_in_asts idstruc tyfs) then error "A record cannot be recursive";
-  let newps,newfs = typecheck_params_and_field ps fs in
-  let app_constructor = 
-    ope("APPLISTEXPL",
-        (nvar (string_of_id idstruc))::
-        List.map (fun id -> nvar(string_of_id id)) idps) in
-  let type_constructor = make_constructor fs app_constructor in 
-  let sp = build_mutual_give_path
-	     ps [(idstruc,s,[(idbuild,type_constructor)])] true in
-  let sp_projs = declare_projections idstruc coers newps newfs in
-
+  let coers,fs = List.split cfs in
+  let nparams = List.length ps in
+  let idps = List.map fst ps in
+  let allnames =  idstruc::idps@(List.map (fun (id,_,_) -> id) fs) in
+  if not (list_distinct allnames) then error "Two objects have the same name";
+  if occur_fields idstruc fs then error "A record cannot be recursive";
+  (* Now, younger decl in params and fields is on top *)
+  let params,fields = typecheck_params_and_field ps fs in
+  let args =  List.map mkVar idps in
+  let ind = applist (mkVar idstruc, args) in
+  let subst = List.rev (idstruc::idps) in
+  let named_type_constructor = it_mkNamedProd_or_LetIn ind fields in
+  let type_constructor = subst_vars subst named_type_constructor in
+  let mie_ind =
+    { mind_entry_nparams = nparams;
+      mind_entry_params = degenerate_decl params;
+      mind_entry_typename = idstruc;
+      mind_entry_arity = mkSort s;
+      mind_entry_consnames = [idbuild];
+     mind_entry_lc = [type_constructor] } in
+  let mie =
+    { mind_entry_finite = true;
+      mind_entry_inds = [mie_ind] } in
+  let sp = declare_mutual_with_eliminations mie in
+  let sp_projs = declare_projections idstruc coers params fields in
   let rsp = (sp,0) in
   if is_coe then Class.try_add_new_coercion idbuild NeverDischarge;
-  Recordops.add_new_struc (rsp,idbuild,List.length idps,List.rev sp_projs)
+  Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 88a3e120f..d6093fdc1 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Names
 open Term
+open Sign
 (*i*)
 
 (* [declare_projections id coers params fields] declare projections of
@@ -12,10 +13,8 @@ open Term
 
 val declare_projections :
   identifier -> bool list -> 
-   (identifier * types) list -> (identifier * types) list -> 
-      constant_path option list
+   named_context -> named_context -> constant_path option list
 
 val definition_structure :
    bool * identifier * (identifier * Coqast.t) list *
-  (bool * (identifier * Coqast.t)) list * identifier *
-  Coqast.t -> unit
+  (bool * (identifier * bool * Coqast.t)) list * identifier * sorts -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f5599792e..5714bbded 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -542,13 +542,21 @@ let _ =
 	    | VARG_CONSTANT sp -> Global.set_transparent sp
 	    |   _  -> bad_vernac_args "TRANSPARENT")
 	 id_list)
-    
+
+let warning_opaque s =
+  warning (
+    "This command turns the constants which depend on the definition/proof
+of "^s^" un-re-checkable until the next \"Transparent "^s^"\" command.")
+
 let _ =
   add "OPAQUE"
     (fun id_list () ->
        List.iter
 	 (function 
-	    | VARG_CONSTANT sp -> Global.set_opaque sp
+	    | VARG_CONSTANT sp ->
+		warning_opaque
+		  (string_of_qualid (Global.qualid_of_global (ConstRef sp)));
+		Global.set_opaque sp
 	    |   _  -> bad_vernac_args "OPAQUE")
 	 id_list)
 
@@ -1114,7 +1122,7 @@ let _ =
        | [VARG_STRING coe;
           VARG_IDENTIFIER struc; 
           VARG_BINDERLIST binders; 
-          VARG_CONSTR s; 
+          VARG_CONSTR sort; 
           VARG_VARGLIST namec; 
           VARG_VARGLIST cfs] -> 
            let ps = join_binders binders in
@@ -1122,8 +1130,13 @@ let _ =
 	     List.map
                (function 
 		  | (VARG_VARGLIST 
-                       [VARG_STRING str; VARG_IDENTIFIER id; VARG_CONSTR c]) ->
-		      (str = "COERCION",(id,c))
+                      [VARG_STRING str; VARG_STRING b; 
+		       VARG_IDENTIFIER id; VARG_CONSTR c]) ->
+		      let assum = match b with
+			| "ASSUM" -> true
+			| "DEF" -> false
+			| _ -> bad_vernac_args "RECORD" in
+		      (str = "COERCION", (id, assum, c))
 		  | _ -> bad_vernac_args "RECORD")
                cfs in
            let const = match namec with 
@@ -1131,6 +1144,7 @@ let _ =
              | [VARG_IDENTIFIER id] -> id 
              | _ -> bad_vernac_args "RECORD" in
            let iscoe = (coe = "COERCION") in
+	   let s = interp_sort sort in
 	   fun () -> Record.definition_structure (iscoe,struc,ps,cfs,const,s)
        | _ -> bad_vernac_args "RECORD")