diff options
| author |  Stephane Glondu <steph@glondu.net> | 2011-04-19 16:47:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:47:51 +0200 |
| commit | aa33547c764a229e22d323ca213d46ea221b903e (patch) | |
| tree | 3894cb190f34bc1d2deee4322a674db641562ee0 | |
| parent | 50dc9067e98ca001ad2e875011abab5da6fdb621 (diff) | |
| parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) | |
Remove non-DFSG contentsupstream/8.3.pl2+dfsg
62 files changed, 701 insertions, 355 deletions
@@ -73,6 +73,8 @@ toplevel/mltop.byteml coqdoc.sty ide/index_urls.txt doc/faq/html/ +doc/refman/csdp.cache +doc/refman/trace doc/refman/Reference-Manual.pdf doc/refman/Reference-Manual.ps doc/refman/cover.html @@ -1,3 +1,43 @@ +Changes from V8.3pl1 to V8.3pl2 +=============================== + +Coqdoc and documentation bugs + +- #2470 (use "membership" instead of "appartness") +- #2475 (documentation of the "f binders := t" notation for record fields) +- Documentation of module String on coq.inria.fr/stdlib + +Tactics + +- #2493 (dependent pairs injection failing because of Type cumulativity missing) +- Reduction "simpl" sometimes failing in presence of names redefined in modules + +Extraction + +- #2359 (Some unnecessary unsafe casts are now avoided (bug in the type checker)). +- #2469 (fix Extract Inlined Constant for Haskell and Scheme) +- #2476 (Fix indentation of default pattern in haskell case) +- #2477 (Avoid printing unused mutual fix components) +- #2478 (Add missing parenthesis around emulated pattern-match) +- #2482 (Extract Inductive on singleton inductives) +- #2484 (Avoid an assert failure with -dont-load-proofs) +- #2497 (malformed Haskell extraction of deeply-nested match expressions) +- #2515 (Allow extracting Ascii.ascii to native Char in Haskell) +- #2525 (Nicer error when a toplevel module has no body) +- Fix printing of haskell modular names + +Miscellaneous bug fixes + +- #2487 (compilation with camlp5 in strict mode) +- #2283, #2460 (new option "Set Default Timeout n / Unset Default Timeout") +- #2524 (In win32, the exit code of coqc should be correct now) +- Now, vm_compute is responsive to Ctrl-C interruption, as the rest of coqtop +- Fixed uncaught exception when vmcast used in Check +- coqdep complies with the -R visibility discipline +- Fixing printing of f when defined using "Notation f x := ..." +- Fixing Unset for options setting integer values +- Excluding admitted subgoals from Search/SearchAbout + Changes from V8.3 to V8.3pl1 ============================ @@ -49,6 +89,10 @@ Miscellaneous bug fixes - a few improvements in efficiency +Extraction + +- The pretty-printer for Haskell now produces layout-independant code + Changes from V8.2 to V8.3 ========================= diff --git a/Coq.bat b/Coq.bat deleted file mode 100755 index cdd7d50d..00000000 --- a/Coq.bat +++ /dev/null @@ -1,8 +0,0 @@ -@echo off -set COQBIN=%~0\..\bin -set COQLIB=%~0\..\lib -echo Using COQBIN= %COQBIN% -echo and COQLIB= %COQLIB% -echo Starting Coq -%~0\..\bin\coqtop.opt.exe -pause
\ No newline at end of file diff --git a/Coqide.bat b/Coqide.bat deleted file mode 100755 index f955a970..00000000 --- a/Coqide.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -set COQBIN=%~0\..\bin -set COQLIB=%~0\..\lib -echo Using COQBIN= %COQBIN% -echo and COQLIB= %COQLIB% -echo Starting Coqide -%~0\..\bin\coqide.opt.exe
\ No newline at end of file @@ -41,7 +41,7 @@ WHAT DO YOU NEED ? Should you need or prefer to compile Coq V8.3 yourself, you need: - - Objective Caml version 3.09.3 or later + - Objective Caml version 3.10.2 or later (available at http://caml.inria.fr/) For Objective Caml version >= 3.10.0, you also need to install @@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.09.3 (or later) +1- Check that you have the Objective Caml compiler version 3.10.2 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. diff --git a/INSTALL.ide b/INSTALL.ide index 2c2f86f5..e99002f0 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do: Else, read the rest of this document to compile your own CoqIde. REQUIREMENT: - - OCaml >= 3.09.3 with native threads support. + - OCaml >= 3.10.2 with native threads support. - make world must succeed. - The graphical toolkit GTK+ 2.x. See http://www.gtk.org. The official supported version is at least 2.10.x. @@ -9,9 +9,9 @@ INSTALLATION. The Coq package for Windows comes with an auto-installer. It will install Coq binaries and libraries under any directory you specify (C:\Program Files\Coq is the default path). It also creates shortcuts -in the Windows menus. Alternatively, you can launch Coq using Coq.bat -and Coqide.bat in the installation directory (C:\Program Files\Coq by -default). +in the Windows menus. Alternatively, you can launch Coq using coqide.exe +or coqtop.exe in the bin sub-directory of the installation +(C:\Program Files\Coq\bin by default). COMPILATION. ============ @@ -20,7 +20,7 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml for Windows (MinGW port), at least version 3.09.3. + 1- Install ocaml for Windows (MinGW port), at least version 3.10.2. See: http://caml.inria.fr 2- Install a shell environment with at least: @@ -52,4 +52,8 @@ COMPILATION. Good luck :-) + Alternatively, it is now possible (and even recommended ...) to build + Windows executables of coq from Linux thanks to a mingw cross-compiler. + If interested, please contact us for more details. + The Coq Team. @@ -10,6 +10,7 @@ <tools/coqdoc/main.{native,byte}> : use_str <checker/main.{native,byte}> : use_str, use_unix, use_gramlib <plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix +<tools/mkwinapp.{native,byte}> : use_unix ## tags for ide @@ -6,7 +6,7 @@ # ################################## -VERSION=8.3pl1 +VERSION=8.3pl2 VOMAGIC=08300 STATEMAGIC=58300 DATE=`LANG=C date +"%B %Y"` @@ -411,12 +411,12 @@ esac CAMLVERSION=`"$bytecamlc" -version` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012]) + 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$force_caml_version" = "yes" ]; then echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." else - echo " You need Objective-Caml 3.09.3 or later." + echo " You need Objective-Caml 3.10.2 or later." echo " Configuration script failed!" exit 1 fi;; @@ -491,11 +491,6 @@ if [ "$camlp5dir" != "" ]; then exit 1 fi camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then - echo "Error: Camlp5 found, but in strict mode!" - echo "Please compile Camlp5 in transitional mode." - exit 1 - fi else case $CAMLTAG in OCAML31*) @@ -510,11 +505,6 @@ else fi CAMLP4=camlp5 camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then - echo "Error: Camlp5 found, but in strict mode!" - echo "Please compile Camlp5 in transitional mode." - exit 1 - fi ;; *) CAMLP4=camlp4 @@ -1094,4 +1084,4 @@ echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure 13740 2010-12-23 12:37:18Z notin $ +# $Id: configure 14025 2011-04-19 07:19:00Z notin $ diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7ee85fe8..541fa1b9 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -452,13 +452,13 @@ through the <tt>Require Import</tt> command.</p> theories/FSets/FMapFullAVL.v </dd> -<!-- <dt> <b>Strings</b> + <dt> <b>Strings</b> Implementation of string as list of ascii characters </dt> <dd> theories/Strings/Ascii.v theories/Strings/String.v - </dd> --> + </dd> <dt> <b>Reals</b>: Formalization of real numbers @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 13431 2010-09-18 08:15:29Z herbelin $ *) +(* $Id: coq.ml 13751 2010-12-24 09:56:05Z letouzey $ *) open Vernac open Vernacexpr @@ -27,10 +27,6 @@ open Termops open Namegen open Ideutils -let prerr_endline s = if !debug then prerr_endline s else () - -let output = ref (Format.formatter_of_out_channel stdout) - let msg m = let b = Buffer.create 103 in Pp.msg_with (Format.formatter_of_buffer b) m; @@ -394,7 +390,7 @@ let compute_reset_info loc_ast = } let reset_initial () = - prerr_endline "Reset initial called"; flush stderr; + prerr_endline "Reset initial called"; Vernacentries.abort_refine Lib.reset_initial () let reset_to sp = @@ -412,7 +408,7 @@ let interp_with_options verbosely options s = let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in (* Temporary hack to make coqide.byte work (WTF???) - now with less screen * pollution *) - Pervasives.prerr_string " \r"; Pervasives.flush stderr; + (try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ()); match pe with | None -> assert false | Some((loc,vernac) as last) -> diff --git a/ide/coq_icon.rc b/ide/coq_icon.rc new file mode 100644 index 00000000..f873e7de --- /dev/null +++ b/ide/coq_icon.rc @@ -0,0 +1 @@ +large ICON ide/coq.ico diff --git a/ide/coqide.ml b/ide/coqide.ml index fdf33c39..ce4f0666 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *) +(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *) open Preferences open Vernacexpr @@ -200,7 +200,7 @@ let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; let crash_save i = (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*) - Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files"; + safe_prerr_endline "Trying to save all buffers in .crashcoqide files"; let count = ref 0 in List.iter (function {script=view; analyzed_view = av } -> @@ -212,12 +212,12 @@ let crash_save i = in try if try_export filename (view#buffer#get_text ()) then - Pervasives.prerr_endline ("Saved "^filename) - else Pervasives.prerr_endline ("Could not save "^filename) - with _ -> Pervasives.prerr_endline ("Could not save "^filename)) + safe_prerr_endline ("Saved "^filename) + else safe_prerr_endline ("Could not save "^filename) + with _ -> safe_prerr_endline ("Could not save "^filename)) ) session_notebook#pages; - Pervasives.prerr_endline "Done. Please report."; + safe_prerr_endline "Done. Please report."; if i <> 127 then exit i let ignore_break () = @@ -3202,7 +3202,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); "\nCoq is developed by the Coq Development Team\ \n(INRIA - CNRS - University Paris 11 and partners)\ \nWeb site: " ^ Coq_config.wwwcoq ^ - "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\ + "\nFeature wish or bug report: http://coq.inria.fr/bugs\ \n\ \nCredits for CoqIDE, the Integrated Development Environment for Coq:\ \n\ @@ -3332,10 +3332,10 @@ let start () = try GtkThread.main () with - | Sys.Break -> prerr_endline "Interrupted." ; flush stderr + | Sys.Break -> prerr_endline "Interrupted." | e -> - Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); - flush stderr; + safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); + flush_all (); crash_save 127 done diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 138bf5f6..8b7840e3 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: ideutils.ml 13751 2010-12-24 09:56:05Z letouzey $ *) open Preferences @@ -31,12 +31,16 @@ let set_location = ref (function s -> failwith "not ready") let pbar = GRange.progress_bar ~pulse_step:0.2 () +(* On a Win32 application with no console, writing to stderr raise + a Sys_error "bad file descriptor" *) +let safe_prerr_endline msg = try prerr_endline msg with _ -> () + let debug = Flags.debug let prerr_endline s = - if !debug then (prerr_endline s;flush stderr) + if !debug then try (prerr_endline s;flush stderr) with _ -> () let prerr_string s = - if !debug then (prerr_string s;flush stderr) + if !debug then try (prerr_string s;flush stderr) with _ -> () let lib_ide_file f = let coqlib = Envars.coqlib () in diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 9af4fb43..ade460c6 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ideutils.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ideutils.mli 13751 2010-12-24 09:56:05Z letouzey $ i*) val async : ('a -> unit) -> 'a -> unit val sync : ('a -> 'b) -> 'a -> 'b @@ -34,6 +34,7 @@ val is_char_start : char -> bool val lib_ide_file : string -> string val my_stat : string -> Unix.stats option +val safe_prerr_endline : string -> unit val prerr_endline : string -> unit val prerr_string : string -> unit val print_id : 'a -> unit diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml index f8984462..26f5b61b 100644 --- a/ide/utils/configwin_messages.ml +++ b/ide/utils/configwin_messages.ml @@ -30,9 +30,7 @@ let version = "1.2";; let html_config = "Configwin bindings configurator for html parameters" -let home = - try Sys.getenv "HOME" - with Not_found -> "" +let home = System.home let mCapture = "Capture";; let mType_key = "Type key" ;; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fd230539..1716cfad 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: constrextern.ml 13967 2011-04-08 14:08:43Z herbelin $ *) (*i*) open Pp @@ -343,6 +343,10 @@ let make_pat_notation loc ntn (terms,termlists as subst) = (fun (loc,p) -> CPatPrim (loc,p)) destPatPrim terms +let mkPat loc qid l = + (* Normally irrelevant test with v8 syntax, but let's do it anyway *) + if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l) + (* Better to use extern_rawconstr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try @@ -397,15 +401,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function (match keyrule with | NotationRule (sc,ntn) -> raise No_match | SynDefRule kn -> - let p = - let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in - if l = [] then - CPatAtom (loc,Some qid) - else - let l = - List.map (extern_cases_pattern_in_scope allscopes vars) l in - CPatCstr (loc,qid,l) in - insert_pat_alias loc p na) + let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in + let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in + insert_pat_alias loc (mkPat loc qid l) na) | PatCstr (_,f,l,_), Some n when List.length l > n -> raise No_match | PatCstr (loc,_,_,na),_ -> @@ -432,8 +430,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function insert_pat_delimiters loc (make_pat_notation loc ntn (l,ll)) key) | SynDefRule kn -> - let qid = shortest_qualid_of_syndef vars kn in - CPatAtom (loc,Some (Qualid (loc, qid))) in + let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in + let l = + List.map (fun (c,(scopt,scl)) -> + extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) + subst in + assert (substlist = []); + mkPat loc qid l in insert_pat_alias loc p na | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None) | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id))) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 98ef2791..cce2319b 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -14,6 +14,7 @@ for fast computation of bounded (31bits) integers */ #include <stdio.h> +#include <signal.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -157,6 +158,12 @@ sp is a local copy of the global variable extern_sp. */ #endif #endif +/* For signal handling, we highjack some code from the caml runtime */ + +extern intnat caml_signals_are_pending; +extern intnat caml_pending_signals[]; +extern void caml_process_pending_signals(void); + /* The interpreter itself */ value coq_interprete @@ -414,8 +421,13 @@ value coq_interprete realloc_coq_stack(Coq_stack_threshold); sp = coq_sp; } + /* We also check for signals */ + if (caml_signals_are_pending) { + /* If there's a Ctrl-C, we reset the vm */ + if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; } + caml_process_pending_signals(); + } Next; - /* Fall through CHECK_SIGNALS */ Instruct(APPTERM) { int nargs = *pc++; diff --git a/kernel/names.ml b/kernel/names.ml index 9f1becf7..e5a9f0fc 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 13486 2010-10-03 17:01:43Z herbelin $ *) +(* $Id: names.ml 13804 2011-01-27 00:41:34Z letouzey $ *) open Pp open Util @@ -223,7 +223,7 @@ type constructor = inductive * int let constant_of_kn kn = (kn,kn) let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_con mp dir l = ((mp,dir,l),(mp,dir,l)) +let make_con mp dir l = constant_of_kn (mp,dir,l) let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) let canonical_con con = snd con let user_con con = fst con @@ -235,6 +235,10 @@ let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ let eq_constant (_,kn1) (_,kn2) = kn1=kn2 let debug_string_of_con con = string_of_kn (fst con)^"'"^string_of_kn (snd con) +let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = + if lbl = l1 && lbl = l2 then con + else ((mp1,dp1,lbl),(mp2,dp2,lbl)) + let con_modpath con = modpath (fst con) let mind_modpath mind = modpath (fst mind) diff --git a/kernel/names.mli b/kernel/names.mli index f54df6ec..f57116f9 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: names.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: names.mli 13804 2011-01-27 00:41:34Z letouzey $ i*) (*s Identifiers *) @@ -139,6 +139,7 @@ val user_con : constant -> kernel_name val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * dir_path * label val eq_constant : constant -> constant -> bool +val con_with_label : constant -> label -> constant val string_of_con : constant -> string val con_label : constant -> label diff --git a/lib/envars.ml b/lib/envars.ml index efb2d3fa..b0db1a50 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -14,6 +14,13 @@ let coqbin () = then Filename.concat Coq_config.coqsrc "bin" else System.canonical_path_name (Filename.dirname Sys.executable_name) +(* On win32, we add coqbin to the PATH at launch-time (this used to be + done in a .bat script). *) + +let _ = + if Coq_config.arch = "win32" then + Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "") + let guess_coqlib () = let file = "states/initial.coq" in if Sys.file_exists (Filename.concat Coq_config.coqlib file) diff --git a/lib/system.ml b/lib/system.ml index 17d211f8..7744a79b 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: system.ml 13750 2010-12-24 09:55:54Z letouzey $ *) open Pp open Util @@ -19,12 +19,21 @@ let safe_getenv_def var def = Sys.getenv var with Not_found -> warning ("Environment variable "^var^" not found: using '"^def^"' ."); - flush Pervasives.stdout; + flush_all (); def let getenv_else s dft = try Sys.getenv s with Not_found -> dft -let home = (safe_getenv_def "HOME" ".") +(* On win32, the home directory is probably not in $HOME, but in + some other environment variable *) + +let home = + try Sys.getenv "HOME" with Not_found -> + try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> + try Sys.getenv "USERPROFILE" with Not_found -> + warning ("Cannot determine user home directory, using '.' ."); + flush_all (); + "." let safe_getenv n = safe_getenv_def n ("$"^n) diff --git a/library/goptions.ml b/library/goptions.ml index bfd3b272..8cf560d5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: goptions.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: goptions.ml 13922 2011-03-21 16:25:18Z letouzey $ *) (* This module manages customization parameters at the vernacular level *) @@ -305,19 +305,37 @@ let set_option_value locality check_and_cast key v = let bad_type_error () = error "Bad type of value for this option." -let set_int_option_value_gen locality = set_option_value locality - (fun v -> function - | (IntValue _) -> IntValue v - | _ -> bad_type_error ()) +let check_int_value v = function + | IntValue _ -> IntValue v + | _ -> bad_type_error () + +let check_bool_value v = function + | BoolValue _ -> BoolValue v + | _ -> bad_type_error () + +let check_string_value v = function + | StringValue _ -> StringValue v + | _ -> bad_type_error () + +let check_unset_value v = function + | BoolValue _ -> BoolValue false + | IntValue _ -> IntValue None + | _ -> bad_type_error () + +(* Nota: For compatibility reasons, some errors are treated as + warning. This allows a script to refer to an option that doesn't + exist anymore *) + +let set_int_option_value_gen locality = + set_option_value locality check_int_value let set_bool_option_value_gen locality key v = - try set_option_value locality (fun v -> function - | (BoolValue _) -> BoolValue v - | _ -> bad_type_error ()) key v + try set_option_value locality check_bool_value key v + with UserError (_,s) -> Flags.if_verbose msg_warning s +let set_string_option_value_gen locality = + set_option_value locality check_string_value +let unset_option_value_gen locality key = + try set_option_value locality check_unset_value key () with UserError (_,s) -> Flags.if_verbose msg_warning s -let set_string_option_value_gen locality = set_option_value locality - (fun v -> function - | (StringValue _) -> StringValue v - | _ -> bad_type_error ()) let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None diff --git a/library/goptions.mli b/library/goptions.mli index d2f98cd2..2962b5ca 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: goptions.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: goptions.mli 13922 2011-03-21 16:25:18Z letouzey $ i*) (* This module manages customization parameters at the vernacular level *) @@ -157,6 +157,7 @@ val get_ref_table : val set_int_option_value_gen : bool option -> option_name -> int option -> unit val set_bool_option_value_gen : bool option -> option_name -> bool -> unit val set_string_option_value_gen : bool option -> option_name -> string -> unit +val unset_option_value_gen : bool option -> option_name -> unit val set_int_option_value : option_name -> int option -> unit val set_bool_option_value : option_name -> bool -> unit diff --git a/myocamlbuild.ml b/myocamlbuild.ml index f062b50b..1994efac 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -64,8 +64,10 @@ let w32pref = "i586-mingw32msvc" let w32ocamlc = w32pref^"-ocamlc" let w32ocamlopt = w32pref^"-ocamlopt" let w32ocamlmklib = w32pref^"-ocamlmklib" +let w32res = w32pref^"-windres" let w32lib = "/usr/"^w32pref^"/lib/" let w32bin = "/usr/"^w32pref^"/bin/" +let w32ico = "ide/coq_icon.o" let _ = if w32 then begin Options.ocamlopt := A w32ocamlopt; @@ -167,6 +169,7 @@ let coqmktop = "scripts/coqmktop" type links = Both | Best | BestInPlace | Ide let all_binaries = + (if w32 then [ "mkwinapp", "tools/mkwinapp", Best ] else []) @ [ "coqtop", coqtop, Both; "coqide", coqide, Ide; "coqmktop", coqmktop, Both; @@ -365,18 +368,35 @@ let extra_rules () = begin "let ide = \""^ide_mods^"\"\n"], tolink)); +(** For windows, building coff object file from a .rc (for the icon) *) + + if w32 then rule ".rc.o" ~deps:["%.rc";"ide/coq.ico"] ~prod:"%.o" + (fun env _ -> + let rc = env "%.rc" and o = env "%.o" in + Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc; + A "--output-format";A "coff";A "--output"; Px o])); + (** Coqtop and coqide *) let mktop_rule f is_ide = let fo = f^".native" and fb = f^".byte" in let ideflag = if is_ide then A"-ide" else N in let depsall = [coqmktopbest;libcoqrun] in + let depsall = if w32 then w32ico::depsall else depsall in let depso = "coq_config.cmx" :: core_cmxa in let depsb = "coq_config.cmo" :: core_cma in let depideo = if is_ide then [ide_cmxa] else [] in let depideb = if is_ide then [ide_cma] else [] in - let w32ideflag = (*if is_ide then [A"-ccopt";A"\"-link -mwindows\""] else*) [] in - let w32flag = if not w32 then N else S ([A"-camlbin";A w32bin]@w32ideflag) in + let w32ideflag = + (* Uncomment the following line to make coqide a console-free win32 app. + For the moment we don't, some issue remain to be investigated. + In the meantime, coqide can be made console-free a posteriori via + the mkwinapp tool. *) + (*if is_ide then [A"-ccopt";A"\"-link -Wl,-subsystem,windows\""] else*) [] in + let w32flag = + if not w32 then N + else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]@w32ideflag) + in if opt then rule fo ~prod:fo ~deps:(depsall@depso@depideo) ~insert:`top (cmd [P coqmktopbest;w32flag;A"-boot";A"-opt";ideflag;incl fo;A"-o";Px fo]); rule fb ~prod:fb ~deps:(depsall@depsb@depideb) ~insert:`top diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index cf83c72a..3fc18219 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: prettyp.ml 13967 2011-04-08 14:08:43Z herbelin $ *) open Pp open Util @@ -460,13 +460,15 @@ let gallina_print_constant_with_infos sp = with_line_skip (print_name_infos (ConstRef sp)) let gallina_print_syntactic_def kn = - let sep = " := " - and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn + let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in let c = Topconstr.rawconstr_of_aconstr dummy_loc a in - str "Notation " ++ pr_qualid qid ++ - prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++ - Constrextern.without_symbols pr_lrawconstr c ++ fnl () + hov 2 + (hov 4 + (str "Notation " ++ pr_qualid qid ++ + prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ + spc () ++ str ":=") ++ + spc () ++ Constrextern.without_symbols pr_rawconstr c) ++ fnl () let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index f067fcf3..39477b0b 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: tacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *) open Util open Genarg @@ -55,7 +55,7 @@ let rec make_let e = function let add_clause s (pt,e) l = let p = make_patt pt in let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, w, make_let e pt)::l + (p, <:vala< w >>, make_let e pt)::l let rec extract_signature = function | [] -> [] @@ -72,7 +72,8 @@ let check_unicity s l = let make_clauses s l = check_unicity s l; let default = - (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in + (<:patt< _ >>,<:vala<None>>, + <:expr< failwith "Tactic extension: cannot occur" >>) in List.fold_right (add_clause s) l [default] let rec make_args = function diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 95eccfda..860110e5 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: vernacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: vernacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *) open Util open Genarg @@ -31,7 +31,7 @@ let rec make_let e = function let add_clause s (_,pt,e) l = let p = make_patt pt in let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, w, make_let e pt)::l + (p, <:vala<w>>, make_let e pt)::l let check_unicity s l = let l' = List.map (fun (_,l,_) -> extract_signature l) l in @@ -43,7 +43,8 @@ let check_unicity s l = let make_clauses s l = check_unicity s l; let default = - (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in + (<:patt< _ >>,<:vala<None>>, + <:expr< failwith "Vernac extension: cannot occur" >>) in List.fold_right (add_clause s) l [default] let mlexpr_of_clause = diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml index 9a62f39d..199c3087 100644 --- a/plugins/dp/dp_why.ml +++ b/plugins/dp/dp_why.ml @@ -181,6 +181,5 @@ let print_query fmt (decls,concl) = let output_file f q = let c = open_out f in let fmt = formatter_of_out_channel c in - fprintf fmt "include \"real.why\"@."; fprintf fmt "@[%a@]@." print_query q; close_out c diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 8dc512fa..9cea0562 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: common.ml 14010 2011-04-15 16:05:07Z letouzey $ i*) open Pp open Util @@ -43,6 +43,13 @@ let pr_binding = function | [] -> mt () | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l +(** By default, in module Format, you can do horizontal placing of blocks + even if they include newlines, as long as the number of chars in the + blocks are less that a line length. To avoid this awkward situation, + we attach a big virtual size to [fnl] newlines. *) + +let fnl () = stras (1000000,"") ++ fnl () + let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () @@ -509,8 +516,10 @@ let pp_ocaml_gen k mp rls olab = let pp_haskell_gen k mp rls = match rls with | [] -> assert false | s::rls' -> - (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^ - (if upperkind k then "" else "_") ^ pseudo_qualify rls' + let str = pseudo_qualify rls' in + let str = if is_upper str && not (upperkind k) then ("_"^str) else str in + let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in + prf ^ str (* Main name printing function for a reference *) @@ -542,4 +551,38 @@ let pp_module mp = add_visible (Mod,s) l; s | _ -> pp_ocaml_gen Mod mp (List.rev ls) None +(** Special hack for constants of type Ascii.ascii : if an + [Extract Inductive ascii => char] has been declared, then + the constants are directly turned into chars *) + +let mk_ind path s = + make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s) +let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" + +let check_extract_ascii () = + try + let char_type = match lang () with + | Ocaml -> "char" + | Haskell -> "Char" + | _ -> raise Not_found + in + find_custom (IndRef (ind_ascii,0)) = char_type + with Not_found -> false + +let is_list_cons l = + List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l + +let is_native_char = function + | MLcons(_,ConstructRef ((kn,0),1),l) -> + kn = ind_ascii && check_extract_ascii () && is_list_cons l + | _ -> false + +let pp_native_char c = + let rec cumul = function + | [] -> 0 + | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) + | _ -> assert false + in + let l = match c with MLcons(_,_,l) -> l | _ -> assert false in + str ("'"^Char.escaped (Char.chr (cumul l))^"'") diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 619cddfb..f6ff76ba 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: common.mli 14010 2011-04-15 16:05:07Z letouzey $ i*) open Names open Libnames @@ -14,6 +14,12 @@ open Miniml open Mlutil open Pp +(** By default, in module Format, you can do horizontal placing of blocks + even if they include newlines, as long as the number of chars in the + blocks are less that a line length. To avoid this awkward situation, + we attach a big virtual size to [fnl] newlines. *) + +val fnl : unit -> std_ppcmds val fnl2 : unit -> std_ppcmds val space_if : bool -> std_ppcmds val sec_space_if : bool -> std_ppcmds @@ -57,3 +63,14 @@ type reset_kind = AllButExternal | Everything val reset_renaming_tables : reset_kind -> unit val set_keywords : Idset.t -> unit + +(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) + +val mk_ind : string -> string -> mutual_inductive + +(** Special hack for constants of type Ascii.ascii : if an + [Extract Inductive ascii => char] has been declared, then + the constants are directly turned into chars *) + +val is_native_char : ml_ast -> bool +val pp_native_char : ml_ast -> std_ppcmds diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index c5929392..7d4cd770 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: extract_env.ml 14012 2011-04-15 16:45:27Z letouzey $ i*) open Term open Declarations @@ -49,11 +49,12 @@ let environment_until dir_opt = | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] | [] -> [] | d :: l -> - match (Global.lookup_module (MPfile d)).mod_expr with - | Some meb -> - if dir_opt = Some d then [MPfile d, meb] - else (MPfile d, meb) :: (parse l) - | _ -> assert false + let mb = Global.lookup_module (MPfile d) in + (* If -dont-load-proof has been used, mod_expr is None, + we try with mod_type *) + let meb = Option.default mb.mod_type mb.mod_expr in + if dir_opt = Some d then [MPfile d, meb] + else (MPfile d, meb) :: (parse l) in parse (Library.loaded_libraries ()) @@ -327,10 +328,17 @@ and extract_seb env mp all = function | SEBwith (_,_) -> anomaly "Not available yet" and extract_module env mp all mb = - (* [mb.mod_expr <> None ], since we look at modules from outside. *) - (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) - { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr); - ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } + (* A module has an empty [mod_expr] when : + - it is a module variable (for instance X inside a Module F [X:SIG]) + - it is a module assumption (Declare Module). + Since we look at modules from outside, we shouldn't have variables. + But a Declare Module at toplevel seems legal (cf #2525). For the + moment we don't support this situation. *) + match mb.mod_expr with + | None -> error_no_module_expr mp + | Some me -> + { ml_mod_expr = extract_seb env mp all me; + ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false @@ -397,13 +405,20 @@ let print_one_decl struc mp decl = (*s Extraction of a ml struct to a file. *) let formatter dry file = - if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) - else match file with - | None -> !Pp_control.std_ft - | Some cout -> - let ft = Pp_control.with_output_to cout in - Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ()); - ft + let ft = + if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) + else Pp_control.with_output_to (Option.default stdout file) + in + (* We never want to see ellipsis ... in extracted code *) + Format.pp_set_max_boxes ft max_int; + (* We reuse the width information given via "Set Printing Width" *) + (match Pp_control.get_margin () with + | None -> () + | Some i -> + Format.pp_set_margin ft i; + Format.pp_set_max_indent ft (i-10)); + (* note: max_indent should be < margin above, otherwise it's ignored *) + ft let print_structure_to_file (fn,si,mo) dry struc = let d = descr () in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5329c675..b9a3a736 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: extraction.ml 13795 2011-01-22 14:43:06Z glondu $ i*) (*i*) open Util @@ -394,6 +394,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Third pass: we determine special cases. *) let ind_info = try + let ip = (kn, 0) in + let r = IndRef ip in + if is_custom r then raise (I Standard); if not mib.mind_finite then raise (I Coinductive); if mib.mind_ntypes <> 1 then raise (I Standard); let p = packets.(0) in @@ -405,9 +408,6 @@ and extract_ind env kn = (* kn is supposed to be in long form *) then raise (I Singleton); if l = [] then raise (I Standard); if not mib.mind_record then raise (I Standard); - let ip = (kn, 0) in - let r = IndRef ip in - if is_custom r then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match kind_of_term t with diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 1c47ad81..17a38136 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: haskell.ml 14010 2011-04-15 16:05:07Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -106,7 +106,7 @@ let rec pp_type par vl t = let expr_needs_par = function | MLlam _ -> true - | MLcase _ -> true + | MLcase _ -> false (* now that we use the case ... of { ... } syntax *) | _ -> false @@ -129,16 +129,17 @@ let rec pp_expr par env args = let pp_id = pr_id (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in - hv 0 - (apply - (pp_par par' - (hv 0 - (hov 5 - (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ - spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2))) + let pp_def = + str "let {" ++ cut () ++ + hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}") + in + apply + (pp_par par' + (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) | MLglob r -> apply (pp_global Term r) + | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c | MLcons (_,r,[]) -> assert (args=[]); pp_global Cons r | MLcons (_,r,[a]) -> @@ -153,13 +154,16 @@ let rec pp_expr par env args = if ids <> [] then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 in - hov 2 (str (find_custom_match pv) ++ fnl () ++ + apply + (pp_par par' + (hov 2 + (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv - ++ pp_expr true env [] t) + ++ pp_expr true env [] t))) | MLcase (info,t, pv) -> apply (pp_par par' - (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ - fnl () ++ str " " ++ pp_pat env info pv))) + (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++ + fnl () ++ pp_pat env info pv))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -176,12 +180,11 @@ and pp_pat env info pv = let pp_one_pat (name,ids,t) = let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let par = expr_needs_par t in - hov 2 (pp_global Cons name ++ + hov 2 (str " " ++ pp_global Cons name ++ (match ids with | [] -> mt () | _ -> (str " " ++ - prlist_with_sep - (fun () -> (spc ())) pr_id (List.rev ids))) ++ + prlist_with_sep spc pr_id (List.rev ids))) ++ str " ->" ++ spc () ++ pp_expr par env' [] t) in let factor_br, factor_set = try match info.m_same with @@ -198,18 +201,18 @@ and pp_pat env info pv = prvecti (fun i x -> if Intset.mem i factor_set then mt () else (pp_one_pat pv.(i) ++ - if i = last && Intset.is_empty factor_set then mt () else - fnl () ++ str " ")) pv + if i = last && Intset.is_empty factor_set then str "}" else + (str ";" ++ fnl ()))) pv ++ if Intset.is_empty factor_set then mt () else let par = expr_needs_par factor_br in match info.m_same with | BranchFun _ -> let ids, env' = push_vars [anonymous_name] env in - pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br + hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br ++ str "}") | BranchCst _ -> - str "_ ->" ++ spc () ++ pp_expr par env [] factor_br + hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}") | BranchNone -> mt () (*s names of the functions ([ids]) are already pushed in [env], @@ -218,12 +221,12 @@ and pp_pat env info pv = and pp_fix par env i (ids,bl) args = pp_par par (v 0 - (v 2 (str "let" ++ fnl () ++ - prvect_with_sep fnl + (v 1 (str "let {" ++ fnl () ++ + prvect_with_sep (fun () -> str ";" ++ fnl ()) (fun (fi,ti) -> pp_function env (pr_id fi) ti) - (array_map2 (fun a b -> a,b) ids bl)) ++ - fnl () ++ - hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) + (array_map2 (fun a b -> a,b) ids bl) ++ + str "}") ++ + fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args)) and pp_function env f t = let bl,t' = collect_lams t in @@ -262,12 +265,12 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.length cv = 0 then "type " else "data ") ++ - pp_global Type (IndRef ip) ++ str " " ++ - prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ - (if pl = [] then mt () else str " ") ++ - if Array.length cv = 0 then str "= () -- empty inductive" + pp_global Type (IndRef ip) ++ + prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++ + if Array.length cv = 0 then str " () -- empty inductive" else - (v 0 (str "= " ++ + (fnl () ++ str " " ++ + v 0 (str " " ++ prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) @@ -309,15 +312,23 @@ let pp_decl = function in hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () | Dfix (rv, defs, typs) -> - let max = Array.length rv in - let rec iter i = - if i = max then mt () - else - let e = pp_global Term rv.(i) in - e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () - ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 () - ++ iter (i+1) - in iter 0 + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + prvecti + (fun i r -> + let void = is_inline_custom r || + (not (is_custom r) && defs.(i) = MLexn "UNUSED") + in + if void then mt () + else + names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++ + (if is_custom r then + (names.(i) ++ str " = " ++ str (find_custom r)) + else + (pp_function (empty_env ()) names.(i) defs.(i))) + ++ fnl2 ()) + rv | Dterm (r, a, t) -> if is_inline_custom r then mt () else diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index d467f508..c242e4ab 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i*) (*i*) open Pp @@ -110,22 +110,17 @@ let rec type_occurs alpha t = let rec mgu = function | Tmeta m, Tmeta m' when m.id = m'.id -> () - | Tmeta m, t when m.contents=None -> - if type_occurs m.id t then raise Impossible - else m.contents <- Some t - | t, Tmeta m when m.contents=None -> - if type_occurs m.id t then raise Impossible - else m.contents <- Some t - | Tmeta {contents=Some u}, t -> mgu (u, t) - | t, Tmeta {contents=Some u} -> mgu (t, u) + | Tmeta m, t | t, Tmeta m -> + (match m.contents with + | Some u -> mgu (u, t) + | None when type_occurs m.id t -> raise Impossible + | None -> m.contents <- Some t) | Tarr(a, b), Tarr(a', b') -> mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when r = r' -> List.iter mgu (List.combine l l') - | Tvar i, Tvar j when i = j -> () - | Tvar' i, Tvar' j when i = j -> () | Tdummy _, Tdummy _ -> () - | Tunknown, Tunknown -> () + | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *) | _ -> raise Impossible let needs_magic p = try mgu p; false with Impossible -> true @@ -828,6 +823,23 @@ let is_atomic = function let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false +(** Program creates a let-in named "program_branch_NN" for each branch of match. + Unfolding them leads to more natural code (and more dummy removal) *) + +let is_program_branch = function + | Id id -> + let s = string_of_id id in + let br = "program_branch_" in + let n = String.length br in + (try + ignore (int_of_string (String.sub s n (String.length s - n))); + String.sub s 0 n = br + with _ -> false) + | Tmp _ | Dummy -> false + +let expand_linear_let o id e = + o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e + (*S The main simplification function. *) (* Some beta-iota reductions + simplifications. *) @@ -844,7 +856,7 @@ let rec simpl o = function if (is_atomic c) || (is_atomic e) || (let n = nb_occur_match e in - (n = 0 || (n=1 && (is_tmp id || is_imm_apply e || o.opt_lin_let)))) + (n = 0 || (n=1 && expand_linear_let o id e))) then simpl o (ast_subst c e) else diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 313fc58d..23ec108a 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: modutil.ml 14006 2011-04-14 23:09:56Z letouzey $ i*) open Names open Declarations @@ -289,10 +289,10 @@ let reset_needed, add_needed, found_needed, is_needed = (fun r -> Refset'.mem (base_r r) !needed)) let declared_refs = function - | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|] - | Dtype (r,_,_) -> [|r|] - | Dterm (r,_,_) -> [|r|] - | Dfix (rv,_,_) -> rv + | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)] + | Dtype (r,_,_) -> [r] + | Dterm (r,_,_) -> [r] + | Dfix (rv,_,_) -> Array.to_list rv (* Computes the dependencies of a declaration, except in case of custom extraction. *) @@ -308,18 +308,25 @@ let compute_deps_decl = function if not (is_custom r) then ast_iter_references add_needed add_needed add_needed u | Dfix _ as d -> - (* Todo Later : avoid dependencies when Extract Constant *) decl_iter_references add_needed add_needed add_needed d let rec depcheck_se = function | [] -> [] - | ((l,SEdecl d) as t)::se -> - let se' = depcheck_se se in - let rv = declared_refs d in - if not (array_exists is_needed rv) then - (Array.iter remove_info_axiom rv; se') - else - (Array.iter found_needed rv; compute_deps_decl d; t::se') + | ((l,SEdecl d) as t) :: se -> + let se' = depcheck_se se in + let refs = declared_refs d in + let refs' = List.filter is_needed refs in + if refs' = [] then + (List.iter remove_info_axiom refs; se') + else begin + List.iter found_needed refs'; + (* Hack to avoid extracting unused part of a Dfix *) + match d with + | Dfix (rv,trms,tys) when (List.for_all is_custom refs') -> + let trms' = Array.create (Array.length rv) (MLexn "UNUSED") in + ((l,SEdecl (Dfix (rv,trms',tys))) :: se') + | _ -> (compute_deps_decl d; t::se') + end | _ -> raise NoDepCheck let rec depcheck_struct = function diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index f136fab5..81eea9e2 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: ocaml.ml 14010 2011-04-15 16:05:07Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -120,9 +120,6 @@ let find_projections = function Record l -> l | _ -> raise NoRecord (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) -let mk_ind path s = - make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s) - let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false @@ -160,26 +157,6 @@ let expr_needs_par = function | MLcase (_,_,pv) -> not (is_ifthenelse pv) | _ -> false - -(** Special hack for constants of type Ascii.ascii : if an - [Extract Inductive ascii => char] has been declared, then - the constants are directly turned into chars *) - -let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" - -let check_extract_ascii () = - try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false - -let is_list_cons l = - List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l - -let pp_char l = - let rec cumul = function - | [] -> 0 - | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) - | _ -> assert false - in str ("'"^Char.escaped (Char.chr (cumul l))^"'") - let rec pp_expr par env args = let par' = args <> [] || par and apply st = pp_apply st par args in @@ -214,10 +191,7 @@ let rec pp_expr par env args = let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) with _ -> apply (pp_global Term r)) - | MLcons(_,ConstructRef ((kn,0),1),l) - when kn = ind_ascii && check_extract_ascii () & is_list_cons l -> - assert (args=[]); - pp_char l + | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c | MLcons ({c_kind = Coinductive},r,[]) -> assert (args=[]); pp_par par (str "lazy " ++ pp_global Cons r) @@ -247,9 +221,12 @@ let rec pp_expr par env args = if ids <> [] then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 in - hov 2 (str (find_custom_match pv) ++ fnl () ++ + apply + (pp_par par' + (hov 2 + (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv - ++ pp_expr true env [] t) + ++ pp_expr true env [] t))) | MLcase (info, t, pv) -> let expr = if info.m_kind = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) @@ -291,7 +268,7 @@ let rec pp_expr par env args = (try pp_ifthenelse par' env expr pv with Not_found -> v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ - str " | " ++ pp_pat env info pv)))) + pp_pat env info pv)))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -355,19 +332,19 @@ and pp_pat env info pv = prvecti (fun i x -> if Intset.mem i factor_set then mt () else let s1,s2 = pp_one_pat env info x in - hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ - if i = last && Intset.is_empty factor_set then mt () else - fnl () ++ str " | ") pv + hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++ + if i = last && Intset.is_empty factor_set then mt () else fnl ()) + pv ++ if Intset.is_empty factor_set then mt () else let par = expr_needs_par factor_br in match info.m_same with | BranchFun _ -> let ids, env' = push_vars [anonymous_name] env in - hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br) + hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + hov 2 (pp_expr par env' [] factor_br)) | BranchCst _ -> - hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br)) | BranchNone -> mt () and pp_function env t = @@ -379,11 +356,11 @@ and pp_function env t = if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv) + v 0 (pp_pat env' i pv) else pr_binding (List.rev bl) ++ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv) + v 0 (pp_pat env' i pv) | _ -> pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ @@ -412,17 +389,24 @@ let pp_Dfix (rv,c,t) = let names = Array.map (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv in - let rec pp sep letand i = - if i >= Array.length rv then mt () - else if is_inline_custom rv.(i) then pp sep letand (i+1) + let rec pp init i = + if i >= Array.length rv then + (if init then failwith "empty phrase" else mt ()) else - let def = - if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) - else pp_function (empty_env ()) c.(i) + let void = is_inline_custom rv.(i) || + (not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED") in - sep () ++ pp_val names.(i) t.(i) ++ - str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) - in pp mt "let rec " 0 + if void then pp init (i+1) + else + let def = + if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) + else pp_function (empty_env ()) c.(i) + in + (if init then mt () else fnl2 ()) ++ + pp_val names.(i) t.(i) ++ + str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ + pp false (i+1) + in pp true 0 (*s Pretty-printing of inductive types declaration. *) @@ -439,7 +423,7 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps = let pl = rename_tvars keywords pl in let pp_constructor i typs = (if i=0 then mt () else fnl ()) ++ - hov 5 (str " | " ++ cnames.(i) ++ + hov 3 (str "| " ++ cnames.(i) ++ (if typs = [] then mt () else str " of ") ++ prlist_with_sep (fun () -> spc () ++ str "* ") (pp_type true pl) typs) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 06098591..cb980cba 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: scheme.ml 14006 2011-04-14 23:09:56Z letouzey $ i*) (*s Production of Scheme syntax. *) @@ -101,9 +101,12 @@ let rec pp_expr env args = if ids <> [] then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 in - hov 2 (str (find_custom_match pv) ++ fnl () ++ + apply + (paren + (hov 2 + (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv - ++ pp_expr env [] t) + ++ pp_expr env [] t))) | MLcase (info,t, pv) -> let e = if info.m_kind <> Coinductive then pp_expr env [] t @@ -163,24 +166,29 @@ let pp_decl = function | Dind _ -> mt () | Dtype _ -> mt () | Dfix (rv, defs,_) -> - let ppv = Array.map (pp_global Term) rv in - prvect_with_sep fnl - (fun (pi,ti) -> - hov 2 - (paren (str "define " ++ pi ++ spc () ++ - (pp_expr (empty_env ()) [] ti)) - ++ fnl ())) - (array_map2 (fun p b -> (p,b)) ppv defs) ++ - fnl () + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + prvecti + (fun i r -> + let void = is_inline_custom r || + (not (is_custom r) && defs.(i) = MLexn "UNUSED") + in + if void then mt () + else + hov 2 + (paren (str "define " ++ names.(i) ++ spc () ++ + (if is_custom r then str (find_custom r) + else pp_expr (empty_env ()) [] defs.(i))) + ++ fnl ()) ++ fnl ()) + rv | Dterm (r, a, _) -> if is_inline_custom r then mt () else - if is_custom r then - hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ - str (find_custom r))) ++ fnl () ++ fnl () - else - hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ - pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ + (if is_custom r then str (find_custom r) + else pp_expr (empty_env ()) [] a))) + ++ fnl2 () let rec pp_structure_elem = function | (l,SEdecl d) -> pp_decl d diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 085c0a44..b2b5e6f5 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: table.ml 14012 2011-04-15 16:45:27Z letouzey $ i*) open Names open Term @@ -310,6 +310,12 @@ let error_module_clash mp1 mp2 = pr_long_mp mp2 ++ str " have the same ML name.\n" ++ str "This is not supported yet. Please do some renaming first.") +let error_no_module_expr mp = + err (str "The module " ++ pr_long_mp mp + ++ str " has no body, it probably comes from\n" + ++ str "some Declare Module outside any Module Type.\n" + ++ str "This situation is currently unsupported by the extraction.") + let error_unknown_module m = err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index ff4780a1..2eafe1d8 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: table.mli 14012 2011-04-15 16:45:27Z letouzey $ i*) open Names open Libnames @@ -29,6 +29,7 @@ val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a +val error_no_module_expr : module_path -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index f6f8695b..866e6a10 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_cases.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: subtac_cases.ml 14003 2011-04-14 23:09:41Z letouzey $ *) open Cases open Util @@ -1741,7 +1741,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in + let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = let bref = RVar (dummy_loc, branch_name) in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index bae89329..67bf7043 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *) +(* $Id: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *) open Util open Names @@ -1203,7 +1203,7 @@ and match_current pb tomatch = let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); - uj_type = substl inst typ } + uj_type = prod_applist typ inst } and compile_branch current names deps pb arsign eqn cstr = let sign, pb = build_branch current deps names pb arsign eqn cstr in diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a41cdd6f..b9fd307c 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *) open Pp open Util @@ -305,7 +305,7 @@ let evar_clenv_unique_resolver = clenv_unique_resolver let connect_clenv gls clenv = { clenv with - evd = evars_reset_evd gls.sigma clenv.evd; + evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd; env = Global.env_of_context gls.it.evar_hyps } (* [clenv_fchain mv clenv clenv'] diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 77442584..5d61e727 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *) open Pp open Util @@ -507,7 +507,9 @@ let empty = { metas=Metamap.empty } -let evars_reset_evd evd d = {d with evars = evd.evars} +let evars_reset_evd ?(with_conv_pbs=false) evd d = + {d with evars = evd.evars; + conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs} let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (EvarMap.find d.evars evk).evar_source diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ce4e1b28..c68cfffe 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*) (*i*) open Util @@ -177,7 +177,7 @@ val existential_opt_value : evar_map -> existential -> constr option val subst_evar_defs_light : substitution -> evar_map -> evar_map (* spiwack: this function seems to somewhat break the abstraction. *) -val evars_reset_evd : evar_map -> evar_map -> evar_map +val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map (* spiwack: [is_undefined_evar] should be considered a candidate diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1c17ff88..b8dc719b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *) +(* $Id: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *) open Pp open Util @@ -634,7 +634,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in let cj = match k with | VMcast when not (occur_existential cty || occur_existential tval) -> - ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj + (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj + with Reduction.NotConvertible -> + error_actual_type_loc loc env !evdref cj tval) + | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval) in let v = mkCast (cj.uj_val, k, tval) in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 49ccb80c..68a67402 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *) open Pp open Util @@ -216,8 +216,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - let (mp,dp,_) = repr_con kn in - Some (EvalConst (make_con mp dp (label_of_id id))) in + Some (EvalConst (con_with_label kn (label_of_id id))) in match refi with | None -> None | Some ref -> @@ -481,7 +480,6 @@ let reduce_mind_case_use_function func env sigma mia = | CoFix (bodynum,(names,_,_) as cofix) -> let build_cofix_name = if isConst func then - let (mp,dp,_) = repr_con (destConst func) in let minargs = List.length mia.mcargs in fun i -> if i = bodynum then Some (minargs,func) @@ -492,7 +490,8 @@ let reduce_mind_case_use_function func env sigma mia = mutual inductive, try to reuse the global name if the block was indeed initially built as a global definition *) - let kn = make_con mp dp (label_of_id id) in + let kn = con_with_label (destConst func) (label_of_id id) + in try match constant_opt_value env kn with | None -> None (* TODO: check kn is correct *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 171db848..42111213 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pfedit.ml 13981 2011-04-08 16:59:26Z herbelin $ *) open Pp open Util @@ -344,8 +344,7 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic sign typ tac = - let id = id_of_string ("temporary_proof"^string_of_int (next())) in +let build_constant_by_tactic id sign typ tac = start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ()); try by tac; @@ -357,5 +356,6 @@ let build_constant_by_tactic sign typ tac = raise e let build_by_tactic typ tac = + let id = id_of_string ("temporary_proof"^string_of_int (next())) in let sign = Decls.clear_proofs (Global.named_context ()) in - (build_constant_by_tactic sign typ tac).const_entry_body + (build_constant_by_tactic id sign typ tac).const_entry_body diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 1b284f8d..8df26706 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pfedit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pfedit.mli 13981 2011-04-08 16:59:26Z herbelin $ i*) (*i*) open Util @@ -202,6 +202,6 @@ val mutate : (pftreestate -> pftreestate) -> unit (* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) -val build_constant_by_tactic : named_context_val -> types -> tactic -> +val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> Entries.definition_entry val build_by_tactic : types -> tactic -> constr diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 7185b140..cc8e5a1a 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqc.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coqc.ml 14015 2011-04-15 17:48:45Z letouzey $ *) (* Afin de rendre Coq plus portable, ce programme Caml remplace le script coqc. @@ -84,7 +84,11 @@ let compile command args files = Unix.create_process_env command (Array.of_list args') environment Unix.stdin Unix.stdout Unix.stderr in - ignore (Unix.waitpid [] pid) + let status = snd (Unix.waitpid [] pid) in + let errcode = + match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c + in + exit errcode | _ -> Unix.execvpe command (Array.of_list args') environment @@ -196,4 +200,4 @@ let main () = (* List.iter (compile coqtopname args) cfiles*) Unix.handle_unix_error (compile coqtopname args) cfiles -let _ = Printexc.print main (); exit 0 +let _ = Printexc.print main () diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index afd13b4c..66f15fbe 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: class_tactics.ml4 13902 2011-03-10 15:50:24Z msozeau $ *) open Pp open Util @@ -85,7 +85,7 @@ let evars_to_goals p evm = if goals = [] then None else let goals = List.rev goals in - let evm' = evars_reset_evd evm' evm in + let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in Some (goals, evm') (** Typeclasses instance search tactic / eauto *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 7a774cc9..411ccc0e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *) +(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *) open Pp open Util @@ -888,8 +888,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = with | Some w -> let w_type = type_of env sigma w in - if Evarconv.e_conv env evdref w_type a then - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + if Evarconv.e_cumul env evdref w_type a then + applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." | None -> anomaly "Not enough components to build the dependent tuple" diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 569cf356..771047fd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *) +(* $Id: tactics.ml 13981 2011-04-08 16:59:26Z herbelin $ *) open Pp open Util @@ -3469,7 +3469,7 @@ let abstract_subproof id tac gl = try flush_and_check_evars (project gl) concl with Uninstantiated_evar _ -> error "\"abstract\" cannot handle existentials." in - let const = Pfedit.build_constant_by_tactic secsign concl + let const = Pfedit.build_constant_by_tactic id secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out index 7bce6671..848abd00 100644 --- a/test-suite/output/Extraction_matchs_2413.out +++ b/test-suite/output/Extraction_matchs_2413.out @@ -9,8 +9,8 @@ let test2 b = (** val wrong_id : 'a1 hole -> 'a2 hole **) let wrong_id = function - | Hole -> Hole - | Hole2 -> Hole2 +| Hole -> Hole +| Hole2 -> Hole2 (** val test3 : 'a1 option -> 'a1 option **) let test3 o = @@ -18,35 +18,35 @@ let test3 o = (** val test4 : indu -> indu **) let test4 = function - | A m -> A (S m) - | x -> x +| A m -> A (S m) +| x -> x (** val test5 : indu -> indu **) let test5 = function - | A m -> A (S m) - | _ -> B +| A m -> A (S m) +| _ -> B (** val test6 : indu' -> indu' **) let test6 = function - | A' m -> A' (S m) - | E' -> B' - | F' -> B' - | _ -> C' +| A' m -> A' (S m) +| E' -> B' +| F' -> B' +| _ -> C' (** val test7 : indu -> nat option **) let test7 = function - | A m -> Some m - | _ -> None +| A m -> Some m +| _ -> None (** val decode_cond_mode : (word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1 -> opcode -> 'a2) -> 'a2 decoder_result **) let decode_cond_mode condition f w g = match condition w with - | Some oc -> - (match f w with - | DecUndefined -> DecUndefined - | DecUnpredictable -> DecUnpredictable - | DecInst i -> DecInst (g i oc) - | DecError m -> DecError m) - | None -> DecUndefined + | Some oc -> + (match f w with + | DecUndefined -> DecUndefined + | DecUnpredictable -> DecUnpredictable + | DecInst i -> DecInst (g i oc) + | DecError m -> DecError m) + | None -> DecUndefined diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index cf0449f8..49f595d7 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -8,7 +8,7 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *) +(* $Id: FMapAVL.v 13768 2011-01-06 13:55:35Z glondu $ *) (** * FMapAVL *) @@ -78,9 +78,9 @@ Definition empty := Leaf. Definition is_empty m := match m with Leaf => true | _ => false end. -(** * Appartness *) +(** * Membership *) -(** The [mem] function is deciding appartness. It exploits the [bst] property +(** The [mem] function is deciding membership. It exploits the [bst] property to achieve logarithmic complexity. *) Fixpoint mem x m : bool := @@ -705,7 +705,7 @@ Proof. destruct m; simpl; intros; try discriminate; red; intuition_in. Qed. -(** * Appartness *) +(** * Membership *) Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true. Proof. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index c41df7c2..96580749 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -82,9 +82,9 @@ Definition empty := Leaf. Definition is_empty s := match s with Leaf => true | _ => false end. -(** ** Appartness *) +(** ** Membership *) -(** The [mem] function is deciding appartness. It exploits the +(** The [mem] function is deciding membership. It exploits the binary search tree invariant to achieve logarithmic complexity. *) Fixpoint mem x s := @@ -792,7 +792,7 @@ Proof. split; auto. try discriminate. intro H; elim (H x); auto. Qed. -(** * Appartness *) +(** * Membership *) Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s. Proof. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 9bc8965d..3093fa6c 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coqdep.ml 13983 2011-04-08 17:57:56Z herbelin $ *) open Printf open Coqdep_lexer @@ -41,8 +41,8 @@ let add_coqlib_known phys_dir log_dir f = match get_extension f [".vo"] with | (basename,".vo") -> let name = log_dir@[basename] in - Hashtbl.add coqlibKnown [basename] (); - Hashtbl.add coqlibKnown name () + let paths = suffixes name in + List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () let sort () = @@ -199,7 +199,8 @@ let coqdep () = let coqlib = Envars.coqlib () in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; - add_dir add_coqlib_known (coqlib//"user-contrib") [] + let user = coqlib//"user-contrib" in + if Sys.file_exists user then add_rec_dir add_coqlib_known user [] end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0961e398..851b7089 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -397,8 +397,7 @@ let rec add_directory recur add_file phys_dir log_dir = | S_DIR when recur -> if List.mem phys_f !norecdir_list then () else - let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in - add_directory recur add_file phys_f log_dir' + add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f | _ -> () done diff --git a/tools/mkwinapp.ml b/tools/mkwinapp.ml new file mode 100644 index 00000000..226302fb --- /dev/null +++ b/tools/mkwinapp.ml @@ -0,0 +1,92 @@ +(* OCaml-Win32 + * mkwinapp.ml + * Copyright (c) 2002-2004 by Harry Chomsky + * + * This library is free software; you can redistribute it and/or + * modify it under the terms of the GNU Library General Public + * License as published by the Free Software Foundation; either + * version 2 of the License, or (at your option) any later version. + * + * This library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + * Library General Public License for more details. + * + * You should have received a copy of the GNU Library General Public + * License along with this library; if not, write to the Free + * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + *) + +(********************************************************************* + * This program alters an .exe file to make it use the "windows subsystem" + * instead of the "console subsystem". In other words, when Windows runs + * the program, it will not create a console for it. + *) + +(* Pierre Letouzey 23/12/2010 : modification to allow selecting the + subsystem to use instead of just setting the windows subsystem *) + +(* This tool can be run directly via : + ocaml unix.cma mkwinapp.ml [-set|-unset] <filename> +*) + +exception Invalid_file_format + +let input_word ic = + let lo = input_byte ic in + let hi = input_byte ic in + (hi lsl 8) + lo + +let find_pe_header ic = + seek_in ic 0x3C; + let peheader = input_word ic in + seek_in ic peheader; + if input_char ic <> 'P' then + raise Invalid_file_format; + if input_char ic <> 'E' then + raise Invalid_file_format; + peheader + +let find_optional_header ic = + let peheader = find_pe_header ic in + let coffheader = peheader + 4 in + seek_in ic (coffheader + 16); + let optsize = input_word ic in + if optsize < 96 then + raise Invalid_file_format; + let optheader = coffheader + 20 in + seek_in ic optheader; + let magic = input_word ic in + if magic <> 0x010B && magic <> 0x020B then + raise Invalid_file_format; + optheader + +let change flag ic oc = + let optheader = find_optional_header ic in + seek_out oc (optheader + 64); + for i = 1 to 4 do + output_byte oc 0 + done; + output_byte oc (if flag then 2 else 3) + +let usage () = + print_endline "Alters a Win32 executable file to use the Windows subsystem or not."; + print_endline "Usage: mkwinapp [-set|-unset] <filename>"; + print_endline "Giving no option is equivalent to -set"; + exit 1 + +let main () = + let n = Array.length Sys.argv - 1 in + if not (n = 1 || n = 2) then usage (); + let flag = + if n = 1 then true + else if Sys.argv.(1) = "-set" then true + else if Sys.argv.(1) = "-unset" then false + else usage () + in + let filename = Sys.argv.(n) in + let f = Unix.openfile filename [Unix.O_RDWR] 0 in + let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in + change flag ic oc + +let _ = main () diff --git a/toplevel/search.ml b/toplevel/search.ml index 0bd552af..574983cd 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: search.ml 13853 2011-02-24 07:57:31Z glondu $ *) open Pp open Util @@ -197,7 +197,8 @@ let filter_by_module_from_list = function | l, outside -> filter_by_module l (not outside) let filter_subproof gr _ _ = - not (string_string_contains (name_of_reference gr) "_subproof") + not (string_string_contains (name_of_reference gr) "_subproof") && + not (string_string_contains (name_of_reference gr) "_admitted") let (&&&&&) f g x y z = f x y z && g x y z diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9464d763..afc5057e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *) +(* $Id: vernac.ml 13923 2011-03-21 16:25:20Z letouzey $ *) (* Parsing of vernacular. *) @@ -52,8 +52,51 @@ let real_error = function | Error_in_file (_, _, e) -> e | e -> e +(** Timeout handling *) + +(** A global default timeout, controled by option "Set Default Timeout n". + Use "Unset Default Timeout" to deactivate it (or set it to 0). *) + +let default_timeout = ref None + +let _ = + Goptions.declare_int_option + { Goptions.optsync = true; + Goptions.optname = "the default timeout"; + Goptions.optkey = ["Default";"Timeout"]; + Goptions.optread = (fun () -> !default_timeout); + Goptions.optwrite = ((:=) default_timeout) } + +(** When interpreting a command, the current timeout is initially + the default one, but may be modified locally by a Timeout command. *) + +let current_timeout = ref None + +(** Installing and de-installing a timer. + Note: according to ocaml documentation, Unix.alarm isn't available + for native win32. *) + let timeout_handler _ = raise Timeout +let set_timeout n = + let psh = + Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + ignore (Unix.alarm n); + Some psh + +let default_set_timeout () = + match !current_timeout with + | Some n -> set_timeout n + | None -> None + +let restore_timeout = function + | None -> () + | Some psh -> + (* stop alarm *) + ignore(Unix.alarm 0); + (* restore handler *) + Sys.set_signal Sys.sigalrm psh + (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. Note: we could use only one thanks to seek_in, but seeking on and on in @@ -185,25 +228,21 @@ let rec vernac_com interpfun (loc,com) = | VernacTimeout(n,v) -> if not !just_parsing then begin - let psh = - Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - ignore (Unix.alarm n); - let stop() = - (* stop alarm *) - ignore(Unix.alarm 0); - (* restore handler *) - Sys.set_signal Sys.sigalrm psh in - try interp v; stop() - with e -> stop(); raise e + current_timeout := Some n; + interp v end | v -> if not !just_parsing then - States.with_heavy_rollback interpfun - Cerrors.process_vernac_interp_error v - + let psh = default_set_timeout () in + try + States.with_heavy_rollback interpfun + Cerrors.process_vernac_interp_error v; + restore_timeout psh + with e -> restore_timeout psh; raise e in try + current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); interp com with e -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d74711c2..7710cb95 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 13492 2010-10-04 21:20:01Z herbelin $ i*) +(*i $Id: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -1013,9 +1013,7 @@ let vernac_set_option locality key = function | BoolValue b -> set_bool_option_value_gen locality key b let vernac_unset_option locality key = - try set_bool_option_value_gen locality key false - with _ -> - set_int_option_value_gen locality key None + unset_option_value_gen locality key let vernac_add_option key lv = let f = function |