Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg

8 files changed, 106 insertions, 23 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index a1860329..a8e0133e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: command.ml 10067 2007-08-09 17:13:16Z msozeau $ *)
 
 open Pp
 open Util
@@ -657,6 +657,58 @@ let build_scheme lnamedepindsort =
   let _ = List.fold_right2 declare listdecl lrecnames [] in
   if_verbose ppnl (recursive_message Fixpoint lrecnames)
 
+let rec get_concl n t = 
+  if n = 0 then t
+  else
+    match kind_of_term t with
+	Prod (_,_,t) -> get_concl (pred n) t
+      | _ -> raise (Invalid_argument "get_concl")
+
+let cut_last l = 
+  let rec aux acc = function
+      hd :: [] -> List.rev acc, hd
+    | hd :: tl -> aux (hd :: acc) tl
+    | [] -> raise (Invalid_argument "cut_last")
+  in aux [] l
+	
+let build_combined_scheme name schemes =
+  let env = Global.env () in
+  let defs = 
+    List.map (fun x -> 
+		let refe = Ident x in
+		let qualid = qualid_of_reference refe in
+		let cst = Nametab.locate_constant (snd qualid) in
+		  qualid, cst, Typeops.type_of_constant env cst)
+      schemes
+  in
+  let (qid, c, t) = List.hd defs in
+  let nargs = 
+    let (_, arity, _) = destProd t in
+      nb_prod arity
+  in
+  let prods = nb_prod t - nargs in
+  let defs, (qid, c, t) = cut_last defs in
+  let (args, concl) = decompose_prod_n prods t in
+  let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in
+  let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+  let relargs = rel_vect 0 prods in
+  let concl_typ, concl_bod = 
+    List.fold_right
+      (fun (cst, x) (acct, accb) -> 
+	 mkApp (coqand, [| x; acct |]),
+	 mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |])) 
+      concls (concl, mkApp (mkConst c, relargs))
+  in
+  let ctx = List.map (fun (x, y) -> x, None, y) args in
+  let typ = it_mkProd_wo_LetIn concl_typ ctx in
+  let body = it_mkLambda_or_LetIn concl_bod ctx in
+  let ce = { const_entry_body = body;
+             const_entry_type = Some typ;
+             const_entry_opaque = false;
+	     const_entry_boxed = Options.boxed_definitions() } in
+  let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in
+    if_verbose ppnl (recursive_message Fixpoint [snd name])
+
 (* 4| Goal declaration *)
 
 let start_proof id kind c hook =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index e043f354..d15e90cb 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: command.mli 10067 2007-08-09 17:13:16Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -53,6 +53,8 @@ val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
 
 val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
+val build_combined_scheme : identifier located -> identifier located list -> unit
+
 val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3dcb1f58..13f1f1da 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml 9333 2006-11-02 13:59:14Z barras $ *)
+(* $Id: metasyntax.ml 10192 2007-10-08 00:33:39Z letouzey $ *)
 
 open Pp
 open Util
@@ -28,7 +28,7 @@ open Notation
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
+let cache_token (_,s) = Compat.using Pcoq.lexer ("", s)
 
 let (inToken, outToken) =
   declare_object {(default_object "TOKEN") with
@@ -739,7 +739,9 @@ let set_entry_type etyps (x,typ) =
 
 let check_rule_productivity l = 
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
-    error "A notation must include at least one symbol"
+    error "A notation must include at least one symbol";
+  if (match l with SProdList _ :: _ -> true | _ -> false) then
+    error "A recursive notation must start with at least one symbol"
 
 let is_not_printable = function
   | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4e6058be..2185d2a0 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mltop.ml4 9397 2006-11-21 21:50:54Z herbelin $ *)
+(* $Id: mltop.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
 
 open Util
 open Pp
@@ -98,7 +98,7 @@ let dir_ml_load s =
                 str s; str" to Coq code." >])
 (* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
-      ifdef Byte then
+      IFDEF Byte THEN
         let _,gname = where_in_path !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
@@ -108,7 +108,7 @@ let dir_ml_load s =
 	    [Filename.dirname gname]
 	with | Dynlink.Error a ->
           errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
-      else ()
+      ELSE () END
     | Native ->
 	errorlabstrm "Mltop.no_load_object"
           [< str"Loading of ML object file forbidden in a native Coq" >]
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 39106bbf..fdd30711 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 9432 2006-12-12 09:07:36Z courtieu $ *)
+(* $Id: toplevel.ml 10087 2007-08-24 10:39:30Z herbelin $ *)
 
 open Pp
 open Util
@@ -139,16 +139,16 @@ let print_highlight_location ib loc =
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file s inlibrary fname (bp,ep) =
+let print_location_in_file s inlibrary fname loc =
   let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
-  if (bp,ep) = dummy_loc then 
+  if loc = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
     if inlibrary then
       (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
-       str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
+       str" characters " ++ Cerrors.print_loc loc ++ fnl ())
     else
-    let (bp,ep) = unloc (bp,ep) in
+    let (bp,ep) = unloc loc in
     let ic = open_in fname in
     let rec line_of_pos lin bol cnt =
       if cnt < bp then
@@ -172,15 +172,16 @@ let print_command_location ib dloc =
            str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
     | None -> (mt ())
 
-let valid_loc dloc (b,e) =
-  (b,e) <> dummy_loc
+let valid_loc dloc loc =
+  loc <> dummy_loc
   & match dloc with
-    | Some (bd,ed) -> bd<=b & e<=ed
+    | Some dloc ->
+	let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
     | _ -> true
 	  
-let valid_buffer_loc ib dloc (b,e) =
-  valid_loc dloc (b,e) & 
-  let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
+let valid_buffer_loc ib dloc loc =
+  valid_loc dloc loc & 
+  let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
     otherwise. We trap all exceptions to prevent the error message printing
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb719a21..dd6d7e25 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 9874 2007-06-04 13:46:11Z soubiran $ i*)
+(*i $Id: vernacentries.ml 10067 2007-08-09 17:13:16Z msozeau $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -359,6 +359,8 @@ let vernac_cofixpoint = build_corecursive
 
 let vernac_scheme = build_scheme
 
+let vernac_combined_scheme = build_combined_scheme
+
 (**********************)
 (* Modules            *)
 
@@ -1137,6 +1139,7 @@ let interp c = match c with
   | VernacFixpoint (l,b) -> vernac_fixpoint l b
   | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
   | VernacScheme l -> vernac_scheme l
+  | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
 
   (* Modules *)
   | VernacDeclareModule (export,(_,id),bl,mtyo) -> 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 4c671787..9f51841d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacexpr.ml 9481 2007-01-11 19:17:56Z herbelin $ i*)
+(*i $Id: vernacexpr.ml 10067 2007-08-09 17:13:16Z msozeau $ i*)
 
 open Util
 open Names
@@ -199,6 +199,7 @@ type vernac_expr =
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
   | VernacScheme of (lident * bool * lreference * sort_expr) list
+  | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
   | VernacRecord of bool (* = Record or Structure *)
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 0e17df28..b067ba1f 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: whelp.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: whelp.ml4 10105 2007-08-30 16:53:32Z herbelin $ *)
 
 open Options
 open Pp
@@ -32,8 +32,30 @@ open Tacmach
 (* Coq interface to the Whelp query engine developed at 
    the University of Bologna *)
 
+let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080"
+let getter_server_name = ref "http://mowgli.cs.unibo.it:58081"
+
+open Goptions
+
+let _ =
+  declare_string_option 
+    { optsync  = false;
+      optname  = "Whelp server";
+      optkey   = (SecondaryTable ("Whelp","Server"));
+      optread  = (fun () -> !whelp_server_name);
+      optwrite = (fun s -> whelp_server_name := s) }
+
+let _ =
+  declare_string_option 
+    { optsync  = false;
+      optname  = "Whelp getter";
+      optkey   = (SecondaryTable ("Whelp","Getter"));
+      optread  = (fun () -> !getter_server_name);
+      optwrite = (fun s -> getter_server_name := s) }
+
+
 let make_whelp_request req c =
-  "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
+  !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
 
 let b = Buffer.create 16