From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- toplevel/command.ml | 54 ++++++++++++++++++++++++++++++++++++++++++++++- toplevel/command.mli | 4 +++- toplevel/metasyntax.ml | 8 ++++--- toplevel/mltop.ml4 | 6 +++--- toplevel/toplevel.ml | 23 ++++++++++---------- toplevel/vernacentries.ml | 5 ++++- toplevel/vernacexpr.ml | 3 ++- toplevel/whelp.ml4 | 26 +++++++++++++++++++++-- 8 files changed, 106 insertions(+), 23 deletions(-) (limited to 'toplevel') 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¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req + !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req let b = Buffer.create 16 -- cgit v1.2.3