Ajout d'un LetIn primitif.

Abstraction de constr via kind_of_constr dans une bonne partie du code.


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

8 files changed, 119 insertions, 51 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7da510029f..2a15741bf6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Options
-open Generic
+(*i open Generic i*)
 open Term
 open Declarations
 open Inductive
@@ -201,7 +201,7 @@ let collect_non_rec  =
 	    | _ -> [] (* nrec=[] for cofixpoints *)
         with Failure "list_chop" -> []
       in 
-      searchrec ((f,DOP2(Cast,def,body_of_type ar))::lnonrec) 
+      searchrec ((f,mkCast (def,body_of_type ar))::lnonrec) 
         (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
     with Failure "try_find_i" -> 
       (lnonrec, (lnamerec,ldefrec,larrec,nrec))
@@ -267,7 +267,7 @@ let build_recursive lnameargsardef =
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
-	 let ce = { const_entry_body = Cooked (Generic.replace_vars subst def);
+	 let ce = { const_entry_body = Cooked (replace_vars subst def);
 		    const_entry_type = None } in
 	 declare_constant f (ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
@@ -333,7 +333,7 @@ let build_corecursive lnameardef =
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
-	 let ce = { const_entry_body = Cooked (Generic.replace_vars subst def);
+	 let ce = { const_entry_body = Cooked (replace_vars subst def);
 		    const_entry_type = None } in
 	 declare_constant f (ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5253f9fb7e..96b594106c 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -43,7 +43,7 @@ let load_rcfile() =
 (* Puts dir in the path of ML and in the LoadPath *)
 let add_include s =
   Mltop.dir_ml_dir s;
-  add_path s
+  Library.add_path s
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 91ce37753d..987daed1b3 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Sign
-open Generic
+(*i open Generic i*)
 open Term
 open Declarations
 open Inductive
@@ -55,36 +55,63 @@ let modify_opers replfun absfun oper_alist =
          'sPC ; 'sTR"is broken - this function is an internal system" ;
          'sPC ; 'sTR"for internal system use only" >]
   in
-  let rec substrec = function
-    (* Hack pour ls sp dans l'annotation du Cases *)
-    | DOPN(MutCase(n,(spi,a,b,c,d)) as oper,cl) ->
-	let cl' = Array.map substrec cl in
-	(try
-	   match List.assoc (MutInd spi) oper_alist with
-	     | DO_ABSTRACT (MutInd spi',_) ->
-		 DOPN(MutCase(n,(spi',a,b,c,d)),cl')
-	     | _ -> raise Not_found
-	 with
-	   | Not_found -> DOPN(oper,cl'))
-    | DOPN(oper,cl) as c ->
-	let cl' = Array.map substrec cl in
-	(try
-	   (match List.assoc oper oper_alist with
-	      | NOT_OCCUR -> failure ()
-	      | DO_ABSTRACT (oper',modif) ->
-		  if List.length modif > Array.length cl then
-		    anomaly "found a reference with too few args"
-		  else 
-		    interp_modif absfun oper (oper',modif) (Array.to_list cl')
-	      | DO_REPLACE -> substrec (replfun (DOPN(oper,cl'))))
-	 with 
-	   | Not_found -> DOPN(oper,cl'))
-    | DOP1(i,c) -> DOP1(i,substrec c)
-    | DOPL(oper,cl) -> DOPL(oper,List.map substrec cl)
-    | DOP2(oper,c1,c2) -> DOP2(oper,substrec c1,substrec c2)
-    | DLAM(na,c) -> DLAM(na,substrec c)
-    | DLAMV(na,v) -> DLAMV(na,Array.map substrec v)
-    | x -> x
+  let rec substrec c =
+    let op, cl = splay_constr c in
+    let cl' = Array.map substrec cl in
+    match op with
+      (* Hack pour le sp dans l'annotation du Cases *)
+      | OpMutCase (n,(spi,a,b,c,d) as oper) ->
+	  (try
+	     match List.assoc (MutInd spi) oper_alist with
+	       | DO_ABSTRACT (MutInd spi',_) ->
+		   DOPN(MutCase(n,(spi',a,b,c,d)),cl')
+	       | _ -> raise Not_found
+	   with
+	     | Not_found -> DOPN(MutCase oper,cl'))
+
+      | OpMutInd spi ->
+	  (try
+	     (match List.assoc (MutInd spi) oper_alist with
+		| NOT_OCCUR -> failure ()
+		| DO_ABSTRACT (oper',modif) ->
+		    if List.length modif > Array.length cl then
+		      anomaly "found a reference with too few args"
+		    else 
+		      interp_modif absfun (MutInd spi) (oper',modif)
+			(Array.to_list cl')
+		| DO_REPLACE -> substrec (replfun (DOPN(MutInd spi,cl'))))
+	   with 
+	     | Not_found -> DOPN(MutInd spi,cl'))
+
+      | OpMutConstruct spi ->
+	  (try
+	     (match List.assoc (MutConstruct spi) oper_alist with
+		| NOT_OCCUR -> failure ()
+		| DO_ABSTRACT (oper',modif) ->
+		    if List.length modif > Array.length cl then
+		      anomaly "found a reference with too few args"
+		    else 
+		      interp_modif absfun (MutConstruct spi) (oper',modif)
+			(Array.to_list cl')
+		| DO_REPLACE -> substrec (replfun (DOPN(MutConstruct spi,cl'))))
+	   with 
+	     | Not_found -> DOPN(MutConstruct spi,cl'))
+
+      | OpConst sp ->
+	  (try
+	     (match List.assoc (Const sp) oper_alist with
+		| NOT_OCCUR -> failure ()
+		| DO_ABSTRACT (oper',modif) ->
+		    if List.length modif > Array.length cl then
+		      anomaly "found a reference with too few args"
+		    else 
+		      interp_modif absfun (Const sp) (oper',modif)
+			(Array.to_list cl')
+		| DO_REPLACE -> substrec (replfun (DOPN(Const sp,cl'))))
+	   with 
+	     | Not_found -> DOPN(Const sp,cl'))
+  
+    | _ -> gather_constr (op, cl')
   in 
   if oper_alist = [] then fun x -> x else substrec
 
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 9d0e9558a6..c37aa6ff1a 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Environ
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index d9dd3d9035..f33633517a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Options
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Indtypes
@@ -131,9 +131,9 @@ let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
      'sTR"The term"; 'bRK(1,1); pr; 'sPC;
      'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
      'sTR("cannot be applied to the "^term_string1); 'fNL; 
-     'sTR" "; v 0 appl; 'fNL;
-     'sTR (term_string2^" has type"); 'bRK(1,1); prterm_env ctx exptyp; 'sPC;
-     'sTR"which should be coercible to"; 'bRK(1,1); prterm_env ctx actualtyp >]
+     'sTR" "; v 0 appl; 'fNL; 'sTR (term_string2^" has type");
+     'bRK(1,1); prterm_env ctx actualtyp; 'sPC;
+     'sTR"which should be coercible to"; 'bRK(1,1); prterm_env ctx exptyp >]
 
 let explain_cant_apply_not_functional k ctx rator randl =
   let ctx = make_all_name_different ctx in
@@ -167,7 +167,43 @@ let explain_not_product k ctx c =
      'bRK(1,1); pr; 'fNL >]
 
 (* (co)fixpoints *)
-let explain_ill_formed_rec_body k ctx str lna i vdefs =
+let explain_ill_formed_rec_body k ctx err lna i vdefs =
+  let str = match err with
+
+  (* Fixpoint guard errors *)
+  | NotEnoughAbstractionInFixBody ->
+      [< 'sTR "Not enough abstractions in the definition" >]
+  | RecursionNotOnInductiveType ->
+      [< 'sTR "Recursive definition on a non inductive type" >]
+  | RecursionOnIllegalTerm ->
+      [< 'sTR "Recursive call applied to an illegal term" >]
+  | NotEnoughArgumentsForFixCall ->
+      [< 'sTR "Not enough arguments for the recursive call" >]
+
+  (* CoFixpoint guard errors *)
+  (* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
+  | CodomainNotInductiveType c ->
+      [< 'sTR "The codomain is"; 'sPC; prterm c; 'sPC;
+	 'sTR "which should be a coinductive type" >]
+  | NestedRecursiveOccurrences ->
+      [< 'sTR "Nested recursive occurrences" >]
+  | UnguardedRecursiveCall c ->
+      [< 'sTR "Unguarded recursive call" >]
+  | RecCallInTypeOfAbstraction c ->
+      [< 'sTR "Not allowed recursive call in the domain of an abstraction" >]
+  | RecCallInNonRecArgOfConstructor c ->
+      [< 'sTR "Not allowed recursive call in a non-recursive argument of constructor" >]
+  | RecCallInTypeOfDef c ->
+      [< 'sTR "Not allowed recursive call in the type of a recursive definition" >]
+  | RecCallInCaseFun c ->
+      [< 'sTR "Not allowed recursive call in a branch of cases" >]
+  | RecCallInCaseArg c -> 
+      [< 'sTR "Not allowed recursive call in the argument of cases" >]
+  | RecCallInCasePred c ->
+      [< 'sTR "Not allowed recursive call in the type of cases in" >]
+  | NotGuardedForm ->
+      [< 'sTR "Definition not in guarded form" >]
+in
   let pvd = prterm_env ctx vdefs.(i) in
   let s =
     match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 945ff63ef2..0395b94d95 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Declarations
@@ -37,9 +37,11 @@ let rec globalize bv = function
   | DOPN (MutConstruct ((sp,_),_) as op, _) ->
       let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
   | DOPN (op,v) -> DOPN (op, Array.map (globalize bv) v)
-  | DOPL (op,l) -> DOPL (op, List.map (globalize bv) l)
   | DLAM (na,c) -> DLAM (na, globalize (na::bv) c)
   | DLAMV (na,v) -> DLAMV (na, Array.map (globalize (na::bv)) v)
+  | CLam(n,t,c)   -> CLam (n, globalize bv t, globalize (n::bv) c)  
+  | CPrd(n,t,c)   -> CPrd (n, globalize bv t, globalize (n::bv) c)
+  | CLet(n,b,t,c) -> CLet (n,globalize bv b,globalize bv t,globalize (n::bv) c)
   | Rel _ | DOP0 _ as c -> c
 
 let check c = 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9801045a2e..f3169a066a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Declarations
 open Declare
@@ -127,14 +127,14 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
                  print_id_list bad_projs; 'sTR " were not defined" >]);
            (None::sp_projs,fi::ids_not_ok,subst)
          end else 
-	   let p = mkLambda x rp2 (replace_vars subst ti) in
+	   let p = mkLambda (x, rp2, replace_vars subst ti) in
 	   let branch = mk_LambdaCit newfs (VAR fi) in
 	   let ci = Inductive.make_case_info
 		      (Global.lookup_mind_specif (destMutInd r))
 		      (Some PrintLet) [| RegularPat |] in
 	   let proj = mk_LambdaCit newps 
-			(mkLambda x rp1 
-			   (mkMutCaseA ci p (Rel 1) [|branch|])) in
+			(mkLambda (x, rp1,
+				   mkMutCaseA ci p (Rel 1) [|branch|])) in
 	   let ok = 
 	     try
 	       let cie =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bad51033bf..c755419df4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -51,7 +51,7 @@ let real_error = function
    the file we parse seems a bit risky to me.  B.B.  *)
 
 let open_file_twice_if verbosely fname =
-  let longfname = find_file_in_path fname in
+  let longfname = find_file_in_path (Library.get_load_path ()) fname in
   let in_chan = open_in longfname in
   let verb_ch = if verbosely then Some (open_in longfname) else None in
   let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -104,9 +104,12 @@ let rec vernac interpfun input =
             (raw_compile_module verbosely only_spec mname)
             (make_suffix fname ".v")
 	    
-      | Node(_,"Time",l) ->
+      | Node(_,"VernacList",l) ->
+	  List.iter interp l
+
+      | Node(_,"Time",[v]) ->
 	  let tstart = System.get_time() in
-          List.iter interp l;
+          interp v;
 	  let tend = System.get_time() in
           mSGNL [< 'sTR"Finished transaction in " ;
                    System.fmt_time_difference tstart tend >]