diff options
57 files changed, 479 insertions, 315 deletions
@@ -1,4 +1,4 @@ -FLG -rectypes -thread +FLG -rectypes -thread -safe-string S ltac B ltac diff --git a/configure.ml b/configure.ml index 82ce931d67..dfc6724a2d 100644 --- a/configure.ml +++ b/configure.ml @@ -264,6 +264,10 @@ module Prefs = struct let debug = ref true let profile = ref false let annotate = ref false + (* Note, disabling this should be OK, but be careful with the + sharing invariants. + *) + let safe_string = ref true let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false @@ -386,6 +390,9 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot" else "" +let coq_safe_string = + if !Prefs.safe_string then "-safe-string" else "" + let cflags = "-Wall -Wno-unused -g -O2" (** * Architecture *) @@ -1118,7 +1125,7 @@ let write_makefile f = pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; pr "# Caml flags\n"; - pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag; + pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_safe_string; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; pr "# Flags for GCC\n"; diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index da5b425794..241ec35861 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -68,7 +68,7 @@ : ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} ######################################################################## -# Coquelicot +# CompCert ######################################################################## : ${CompCert_CI_BRANCH:=master} : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} diff --git a/dev/doc/api.txt b/dev/doc/api.txt new file mode 100644 index 0000000000..5827257b53 --- /dev/null +++ b/dev/doc/api.txt @@ -0,0 +1,10 @@ +Recommendations in using the API: + +The type of terms: constr (see kernel/constr.ml and kernel/term.ml) + +- On type constr, the canonical equality on CIC (up to + alpha-conversion and cast removal) is Constr.equal +- The type constr is abstract, use mkRel, mkSort, etc. to build + elements in constr; use "kind_of_term" to analyze the head of a + constr; use destRel, destSort, etc. when the head constructor is + known diff --git a/dev/doc/style.txt b/dev/doc/style.txt index 27695a09b1..2ee3dadd77 100644 --- a/dev/doc/style.txt +++ b/dev/doc/style.txt @@ -1,75 +1,142 @@ - -<< L'uniformité du style est plus importante que le style lui-même. >> -(Kernigan & Pike, The Practice of Programming) - -Mode Emacs -========== - Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ - - avec le réglage suivant : (setq tuareg-in-indent 2) - -Types récursifs et filtrages -============================ - Une barre de séparation y compris sur le premier constructeur - -type t = - | A - | B of machin - -match expr with - | A -> ... - | B x -> ... - -Remarque : à partir de la 8.2 environ, la tendance est à utiliser le -format suivant qui permet de limiter l'escalade d'indentation tout en -produisant un aspect visuel intéressant de bloc : - -type t = -| A -| B of machin - -match expr with -| A -> ... -| B x -> ... - -let f expr = match expr with -| A -> ... -| B x -> ... - -let f expr = function -| A -> ... -| B x -> ... - -Le deuxième cas est obtenu sous tuareg avec les réglages - - (setq tuareg-with-indent 0) - (setq tuareg-function-indent 0) - (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien - /// pour les let mais pas pour les let-in - -Conditionnelles -=============== - if condition then - premier-cas - else - deuxieme-cas - - Si effets de bord dans les branches, utilisez begin ... end et non des - parenthèses i.e. - - if condition then begin - instr1; - instr2 - end else begin - instr3; - instr4 - end - - Si la première branche lève une exception, évitez le else i.e. - - if condition then if condition then error "machin"; - error "machin" -----> suite +<< Style uniformity is more important than style itself >> + (Kernigan & Pike, The Practice of Programming) + +OCaml Style: +- Spacing and indentation + - indent your code (using tuareg default) + - no strong constraints in formatting "let in"; possible styles are: + "let x = ... in" + "let x = + ... in" + "let + x = ... + in" + - but: no extra indentation before a "in" coming on next line, + otherwise, it first shifts further and further on the right, + reducing the amount of space available; second, it is not robust to + insertion of a new "let" + - it is established usage to have space around "|" as in + "match c with + | [] | [a] -> ... + | a::b::l -> ..." + - in a one-line "match", it is preferred to have no "|" in front of + the first case (this saves spaces for the match to hold in the line) + - from about 8.2, the tendency is to use the following format which + limit excessive indentation while providing an interesting "block" aspect + type t = + | A + | B of machin + + let f expr = match expr with + | A -> ... + | B x -> ... + + let f expr = function + | A -> ... + | B x -> ... + - add spaces around = and == (make the code "breaths") + - the common usage is to write "let x,y = ... in ..." rather than + "let (x,y) = ... in ..." + - parenthesizing with either "(" and ")" or with "begin" and "end" is + common practice + - preferred layout for conditionals: + if condition then + premier-cas else - suite - - + deuxieme-cas + - in case of effects in branches, use "begin ... end" rather than + parentheses + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + - if the first branch raises an exception, avoid the "else", i.e.: + if condition then if condition then error "foo"; + error "foo" -----> bar + else + bar + - it is the usage not to use ;; to end OCaml sentences (however, + inserting ";;" can be useful for debugging syntax errors crossing + the boundary of functions) + - relevant options in tuareg: + (setq tuareg-in-indent 2) + (setq tuareg-with-indent 0) + (setq tuareg-function-indent 0) + (setq tuareg-let-always-indent nil) + +- Coding methodology + - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C), + Out_of_memory, Stack_overflow, etc. + at least, use "try with e when Errors.noncritical e -> ..." + (to be detailed, Pierre L. ?) + - do not abuse of fancy combinators: sometimes what a "let rec" loop + does is more readable and simpler to grasp than what a "fold" does + - do not break abstractions: if an internal property is hidden + behind an interface, do no rely on it in code which uses this + interface (e.g. do not use List.map thinking it is left-to-right, + use map_left) + - in particular, do not use "=" on abstract types: there is no + reason a priori that it is the intended equality on this type; use the + "equal" function normally provided with the abstract type + - avoid polymorphically typed "=" whose implementation is not + optimized in OCaml and which has moreover no reason to be the + intended implementation of the equality when it comes to be + instantiated on a particular type (e.g. use List.mem_f, + List.assoc_f, rather than List.mem, List.assoc, etc, unless it is + absolutely clear that "=" will implement the intended equality, and + with the right complexity) + - any new general-purpose enough combinator on list should be put in + cList.ml, on type option in cOpt.ml, etc. + - unless of a good reason not to so, follow the style of the + surrounding code in the same file as much as possible, + the general guidelines are otherwise "let spacing breaths" (we + have large screen nowadays), "make your code easy to read and + to understand" + - document what is tricky, but do not overdocument, sometimes the + choice of names and the structuration of the code is a better + documentation than a long discourse; use of unicode in comments is + welcome if it can make comments more readable (then + "toggle-enable-multibyte-characters" can help when using the + debugger in emacs) + - all of initial "open File", or of small-scope File.(...), or + per-ident File.foo are common practices + +- Choice of variable names + - be consistent when naming from one function to another + - be consistent with the naming adopted in the functions from the + same file, or with the naming used elsewhere by similar functions + - use variable names which express meaning + - keep "cst" for constants and avoid it for constructors which is + otherwise a source of confusion + - for constructors, use "cstr" in type constructor (resp. "cstru" in + constructor puniverse); avoid "constr" for "constructor" which + could be think as the name of an arbitrary Constr.t + - for inductive types, use "ind" in the type inductive (resp "indu" + in inductive puniverse) + - for env, use "env" + - for evar_map, use "sigma", with tolerance into "evm" and "evd" + - for named_context or rel_context, use "ctxt" or "ctx" (or "sign") + - for formal/actual indices of inductive types: "realdecls", "realargs" + - for formal/actual parameters of inductive types: "paramdecls", "paramargs" + - for terms, use e.g. c, b, a, ... + - if a term is known to be a function: f, ... + - if a term is known to be a type: t, u, typ, ... + - for a declaration, use d or "decl" + - for errors, exceptions, use e + +- Common OCaml pitfalls + - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in + "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in + parentheses are needed around the "try" and the inner "match" + - even if stream are lazy, the Pp.(++) combinator is strict and + forces the evaluation of its arguments (use a "lazy" or a "fun () ->") + to make it lazy explicitly + - in "if ... then ... else ... ++ ...", the default parenthesizing + is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..." + - in "let myspecialfun = mygenericfun args", be sure that it does no + do side-effect; prefer otherwise "let mygenericfun arg = + mygenericfun args arg" to ensure that the function is evaluated at + runtime diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c37367de5b..16c822b6a5 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -477,15 +477,15 @@ names. \item{\tt Show Intro.}\comindex{Show Intro}\\ If the current goal begins by at least one product, this command prints the name of the first product, as it would be generated by -an anonymous {\tt Intro}. The aim of this command is to ease the +an anonymous {\tt intro}. The aim of this command is to ease the writing of more robust scripts. For example, with an appropriate {\ProofGeneral} macro, it is possible to transform any anonymous {\tt - Intro} into a qualified one such as {\tt Intro y13}. + intro} into a qualified one such as {\tt intro y13}. In the case of a non-product goal, it prints nothing. \item{\tt Show Intros.}\comindex{Show Intros}\\ This command is similar to the previous one, it simulates the naming -process of an {\tt Intros}. +process of an {\tt intros}. \item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials} \\ It displays diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 8605dda3a0..33ca2c629b 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -82,14 +82,14 @@ let make_var = function | ExtNonTerminal (_, p) -> Some p | _ -> assert false -let declare_tactic loc s c cl = match cl with +let declare_tactic loc tacname ~level classification clause = match clause with | [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in let vars = List.map make_var rem in let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in - let entry = mlexpr_of_string s in + let entry = mlexpr_of_string tacname in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in let name = mlexpr_of_string name in @@ -117,13 +117,14 @@ let declare_tactic loc s c cl = match cl with | _ -> (** Otherwise we add parsing and printing rules to generate a call to a TacML tactic. *) - let entry = mlexpr_of_string s in + let entry = mlexpr_of_string tacname in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let gl = mlexpr_of_clause cl in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in + let gl = mlexpr_of_clause clause in + let level = mlexpr_of_int level in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in declare_str_items loc [ <:str_item< do { - Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); + Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); Mltop.declare_cache_obj $obj$ $plugin_name$; } >> ] @@ -134,20 +135,17 @@ EXTEND GLOBAL: str_item; str_item: [ [ "TACTIC"; "EXTEND"; s = tac_name; + level = OPT [ "AT"; "LEVEL"; level = INT -> level ]; c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ]; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> - declare_tactic loc s c l ] ] + let level = match level with Some i -> int_of_string i | None -> 0 in + declare_tactic loc s ~level c l ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ]; - "->"; "["; e = Pcaml.expr; "]" -> - (match l with - | ExtNonTerminal _ :: _ -> - (* En attendant la syntaxe de tacticielles *) - failwith "Tactic syntax must start with an identifier" - | _ -> (l,c,e)) + "->"; "["; e = Pcaml.expr; "]" -> (l,c,e) ] ] ; tacargs: diff --git a/ide/coqide.ml b/ide/coqide.ml index 450bfcdfb1..eec829f345 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -887,8 +887,8 @@ let alpha_items menu_name item_name l = | [] -> () | [s] -> mk_item s | s::_ as ll -> - let name = item_name^" "^(String.make 1 s.[0]) in - let label = "_@..." in label.[1] <- s.[0]; + let name = Printf.sprintf "%s %c" item_name s.[0] in + let label = Printf.sprintf "_%c..." s.[0] in item name ~label menu_name; List.iter mk_item ll in diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 06a1327320..c3a2807967 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -294,18 +294,20 @@ let coqtop_path () = match cmd_coqtop#get with | Some s -> s | None -> - let prog = String.copy Sys.executable_name in try - let pos = String.length prog - 6 in - let i = Str.search_backward (Str.regexp_string "coqide") prog pos + let old_prog = Sys.executable_name in + let pos = String.length old_prog - 6 in + let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos in - String.blit "coqtop" 0 prog i 6; - if Sys.file_exists prog then prog + let new_prog = Bytes.of_string old_prog in + Bytes.blit_string "coqtop" 0 new_prog i 6; + let new_prog = Bytes.to_string new_prog in + if Sys.file_exists new_prog then new_prog else let in_macos_bundle = Filename.concat - (Filename.dirname prog) - (Filename.concat "../Resources/bin" (Filename.basename prog)) + (Filename.dirname new_prog) + (Filename.concat "../Resources/bin" (Filename.basename new_prog)) in if Sys.file_exists in_macos_bundle then in_macos_bundle else "coqtop" with Not_found -> "coqtop" @@ -357,7 +359,7 @@ let stat f = let maxread = 4096 -let read_string = String.create maxread +let read_string = Bytes.create maxread let read_buffer = Buffer.create maxread (** Read the content of file [f] and add it to buffer [b]. @@ -368,7 +370,7 @@ let read_file name buf = let len = ref 0 in try while len := input ic read_string 0 maxread; !len > 0 do - Buffer.add_substring buf read_string 0 !len + Buffer.add_subbytes buf read_string 0 !len done; close_in ic with e -> close_in ic; raise e @@ -381,8 +383,9 @@ let read_file name buf = let io_read_all chan = Buffer.clear read_buffer; let read_once () = - let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in - Buffer.add_substring read_buffer read_string 0 len + (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *) + let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in + Buffer.add_subbytes read_buffer read_string 0 len in begin try while true do read_once () done diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index b020f89457..9f549b0c0f 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -173,32 +173,33 @@ let cook_notation df sc = (* - all single quotes in terminal tokens are doubled *) (* - characters < 32 are represented by '^A, '^B, '^C, etc *) (* The output is decoded in function Index.prepare_entry of coqdoc *) - let ntn = String.make (String.length df * 5) '_' in + let ntn = Bytes.make (String.length df * 5) '_' in let j = ref 0 in let l = String.length df - 1 in let i = ref 0 in + let open Bytes in (* Bytes.set *) while !i <= l do assert (df.[!i] != ' '); if df.[!i] == '_' && (Int.equal !i l || df.[!i+1] == ' ') then (* Next token is a non-terminal *) - (ntn.[!j] <- 'x'; incr j; incr i) + (set ntn !j 'x'; incr j; incr i) else begin (* Next token is a terminal *) - ntn.[!j] <- '\''; incr j; + set ntn !j '\''; incr j; while !i <= l && df.[!i] != ' ' do if df.[!i] < ' ' then let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i) else begin - if df.[!i] == '\'' then (ntn.[!j] <- '\''; incr j); - ntn.[!j] <- df.[!i]; incr j; incr i + if df.[!i] == '\'' then (set ntn !j '\''; incr j); + set ntn !j df.[!i]; incr j; incr i end done; - ntn.[!j] <- '\''; incr j + set ntn !j '\''; incr j end; - if !i <= l then (ntn.[!j] <- '_'; incr j; incr i) + if !i <= l then (set ntn !j '_'; incr j; incr i) done; - let df = String.sub ntn 0 !j in + let df = Bytes.sub_string ntn 0 !j in match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df let dump_notation_location posl df (((path,secpath),_),sc) = diff --git a/intf/misctypes.mli b/intf/misctypes.mli index e4f595ac4a..33dc2a335c 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -28,7 +28,7 @@ and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list - | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) + | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ad7a41a347..f2c3b402b3 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -24,33 +24,45 @@ type reloc_info = type patch = reloc_info * int let patch_char4 buff pos c1 c2 c3 c4 = - String.unsafe_set buff pos c1; - String.unsafe_set buff (pos + 1) c2; - String.unsafe_set buff (pos + 2) c3; - String.unsafe_set buff (pos + 3) c4 + Bytes.unsafe_set buff pos c1; + Bytes.unsafe_set buff (pos + 1) c2; + Bytes.unsafe_set buff (pos + 2) c3; + Bytes.unsafe_set buff (pos + 3) c4 let patch buff (pos, n) = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) +(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) let patch_int buff patches = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) - let buff = String.copy buff in + let buff = Bytes.of_string buff in let () = List.iter (fun p -> patch buff p) patches in - buff + (* Note: we follow the apporach suggested by Gabriel Scherer in + PR#136 here, and use unsafe as we own buff. + + The crux of the question that avoids defining emitcodes just as a + Byte.t is the call to hcons in to_memory below. Even if disabling + this optimization has no visible time impact, test data shows + that the optimization is indeed triggered quite often so we + choose ugliness over altering the semantics. + + Handle with care. + *) + Bytes.unsafe_to_string buff (* Buffering of bytecode *) -let out_buffer = ref(String.create 1024) +let out_buffer = ref(Bytes.create 1024) and out_position = ref 0 let out_word b1 b2 b3 b4 = let p = !out_position in - if p >= String.length !out_buffer then begin - let len = String.length !out_buffer in + if p >= Bytes.length !out_buffer then begin + let len = Bytes.length !out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 = if len = Sys.max_string_length then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in - let new_buffer = String.create new_len in - String.blit !out_buffer 0 new_buffer 0 len; + let new_buffer = Bytes.create new_len in + Bytes.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; patch_char4 !out_buffer p (Char.unsafe_chr b1) @@ -94,10 +106,10 @@ let extend_label_table needed = let backpatch (pos, orig) = let displ = (!out_position - orig) asr 2 in - !out_buffer.[pos] <- Char.unsafe_chr displ; - !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8); - !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16); - !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24) + Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) let define_label lbl = if lbl >= Array.length !label_table then extend_label_table lbl; @@ -305,7 +317,7 @@ let init () = label_table := Array.make 16 (Label_undefined []); reloc_info := [] -type emitcodes = string +type emitcodes = String.t let length = String.length @@ -369,9 +381,8 @@ let to_memory (init_code, fun_code, fv) = init(); emit init_code; emit fun_code; - let code = String.create !out_position in - String.unsafe_blit !out_buffer 0 code 0 !out_position; (** Later uses of this string are all purely functional *) + let code = Bytes.sub_string !out_buffer 0 !out_position in let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> diff --git a/kernel/names.ml b/kernel/names.ml index 1f138581cc..ee8d838da1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -50,17 +50,20 @@ struct | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_soft s; + String.hcons s + let of_string s = let () = check_soft s in - let s = String.copy s in String.hcons s let of_string_soft s = let () = check_soft ~warn:false s in - let s = String.copy s in String.hcons s - let to_string id = String.copy id + let to_string id = id let print id = str id diff --git a/kernel/names.mli b/kernel/names.mli index 6b0a80625b..be9b9422b7 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -43,6 +43,7 @@ sig (** Check that a string may be converted to an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df3044..965ed67b07 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -491,12 +491,12 @@ let str_encode expr = let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in - let buf = String.create 2 in + let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do - String.blit s (2*i) buf 0 2; - Buffer.add_char mshl_expr (bin_of_hex buf) + Bytes.blit_string s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; - Marshal.from_string (Buffer.contents mshl_expr) 0 + Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 (** Retroknowledge, to be removed when we switch to primitive integers *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 130f1eb039..f147ea3433 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -136,7 +136,7 @@ let dump (otab,_) = let disch_table = Array.make n a_discharge in let f2t_map = ref FMap.empty in Int.Map.iter (fun n (d,cu) -> - let c, u = Future.split2 ~greedy:true cu in + let c, u = Future.split2 cu in Future.sink u; Future.sink c; opaque_table.(n) <- c; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3a0d1a2a5e..22b7eebcb4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -76,8 +76,7 @@ let inline_side_effects env body ctx side_eff = let cbl = List.filter not_exists cbl in let cname c = let name = string_of_con c in - for i = 0 to String.length name - 1 do - if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done; + let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in Name (id_of_string name) in let rec sub c i x = match kind_of_term x with | Const (c', _) when eq_constant c c' -> mkRel i @@ -191,7 +190,7 @@ let infer_declaration ~trust env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> let body, uctx, signatures = inline_side_effects env body uctx side_eff in let valid_signatures = check_signatures trust signatures in @@ -416,7 +415,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~greedy:true ~pure:true body + const_entry_body = Future.chain ~pure:true body (fun (b_ctx, _) -> b_ctx, []) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -498,7 +497,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~greedy:true ~pure:true + const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in (body, ctx'), []); diff --git a/lib/cThread.ml b/lib/cThread.ml index 4f60a69745..9f642b3cec 100644 --- a/lib/cThread.ml +++ b/lib/cThread.ml @@ -36,7 +36,7 @@ let really_read_fd fd s off len = let really_read_fd_2_oc fd oc len = let i = ref 0 in let size = 4096 in - let s = String.create size in + let s = Bytes.create size in while !i < len do let len = len - !i in let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in @@ -55,11 +55,13 @@ let thread_friendly_really_read_line ic = try let fd = Unix.descr_of_in_channel ic in let b = Buffer.create 1024 in - let s = String.make 1 '\000' in - while s <> "\n" do + let s = Bytes.make 1 '\000' in + let endl = Bytes.of_string "\n" in + (* Bytes.equal is in 4.03.0 *) + while Bytes.compare s endl <> 0 do let n = thread_friendly_read_fd fd s ~off:0 ~len:1 in if n = 0 then raise End_of_file; - if s <> "\n" then Buffer.add_string b s; + if Bytes.compare s endl <> 0 then Buffer.add_bytes b s; done; Buffer.contents b with Unix.Unix_error _ -> raise End_of_file @@ -67,15 +69,15 @@ let thread_friendly_really_read_line ic = let thread_friendly_input_value ic = try let fd = Unix.descr_of_in_channel ic in - let header = String.create Marshal.header_size in + let header = Bytes.create Marshal.header_size in really_read_fd fd header 0 Marshal.header_size; let body_size = Marshal.data_size header 0 in let desired_size = body_size + Marshal.header_size in if desired_size <= Sys.max_string_length then begin - let msg = String.create desired_size in - String.blit header 0 msg 0 Marshal.header_size; + let msg = Bytes.create desired_size in + Bytes.blit header 0 msg 0 Marshal.header_size; really_read_fd fd msg Marshal.header_size body_size; - Marshal.from_string msg 0 + Marshal.from_bytes msg 0 end else begin (* Workaround for 32 bit systems and data > 16M *) let name, oc = diff --git a/lib/cThread.mli b/lib/cThread.mli index 7302dfb558..36477a1160 100644 --- a/lib/cThread.mli +++ b/lib/cThread.mli @@ -19,8 +19,8 @@ val prepare_in_channel_for_thread_friendly_io : in_channel -> thread_ic val thread_friendly_input_value : thread_ic -> 'a val thread_friendly_read : - thread_ic -> string -> off:int -> len:int -> int + thread_ic -> Bytes.t -> off:int -> len:int -> int val thread_friendly_really_read : - thread_ic -> string -> off:int -> len:int -> unit + thread_ic -> Bytes.t -> off:int -> len:int -> unit val thread_friendly_really_read_line : thread_ic -> string diff --git a/lib/cUnix.ml b/lib/cUnix.ml index cb436511fb..2542b9751b 100644 --- a/lib/cUnix.ml +++ b/lib/cUnix.ml @@ -91,15 +91,15 @@ let rec waitpid_non_intr pid = let run_command ?(hook=(fun _ ->())) c = let result = Buffer.create 127 in let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in - let buff = String.make 127 ' ' in - let buffe = String.make 127 ' ' in + let buff = Bytes.make 127 ' ' in + let buffe = Bytes.make 127 ' ' in let n = ref 0 in let ne = ref 0 in while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0 do - let r = String.sub buff 0 !n in (hook r; Buffer.add_string result r); - let r = String.sub buffe 0 !ne in (hook r; Buffer.add_string result r); + let r = Bytes.sub buff 0 !n in (hook r; Buffer.add_bytes result r); + let r = Bytes.sub buffe 0 !ne in (hook r; Buffer.add_bytes result r); done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) diff --git a/lib/cUnix.mli b/lib/cUnix.mli index f03719c3d2..c6bcf63475 100644 --- a/lib/cUnix.mli +++ b/lib/cUnix.mli @@ -46,7 +46,7 @@ val file_readable_p : string -> bool is called on each elements read on stdout or stderr. *) val run_command : - ?hook:(string->unit) -> string -> Unix.process_status * string + ?hook:(bytes->unit) -> string -> Unix.process_status * string (** [sys_command] launches program [prog] with arguments [args]. It behaves like [Sys.command], except that we rely on diff --git a/lib/future.ml b/lib/future.ml index ea0382a63d..b60b32bb61 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -191,9 +191,9 @@ let transactify f x = let purify_future f x = if is_over x then f x else purify f x let compute x = purify_future (compute ~pure:false) x let force ~pure x = purify_future (force ~pure) x -let chain ?(greedy=true) ~pure x f = +let chain ~pure x f = let y = chain ~pure x f in - if is_over x && greedy then ignore(force ~pure y); + if is_over x then ignore(force ~pure y); y let force x = force ~pure:false x @@ -204,13 +204,13 @@ let join kx = let sink kx = if is_val kx then ignore(join kx) -let split2 ?greedy x = - chain ?greedy ~pure:true x (fun x -> fst x), - chain ?greedy ~pure:true x (fun x -> snd x) +let split2 x = + chain ~pure:true x (fun x -> fst x), + chain ~pure:true x (fun x -> snd x) -let map2 ?greedy f x l = +let map2 f x l = CList.map_i (fun i y -> - let xi = chain ?greedy ~pure:true x (fun x -> + let xi = chain ~pure:true x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in diff --git a/lib/future.mli b/lib/future.mli index c780faf324..2a025ae844 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -113,8 +113,9 @@ val is_exn : 'a computation -> bool val peek_val : 'a computation -> 'a option val uuid : 'a computation -> UUID.t -(* [chain greedy pure c f] chains computation [c] with [f]. - * The [greedy] and [pure] parameters are tricky: +(* [chain pure c f] chains computation [c] with [f]. + * [chain] forces immediately the new computation if the old one is_over (Exn or Val). + * The [pure] parameter is tricky: * [pure]: * When pure is true, the returned computation will not keep a copy * of the global state. @@ -124,10 +125,8 @@ val uuid : 'a computation -> UUID.t * one forces c' and then c''. * [join c; chain ~pure:false c g] is invalid and fails at runtime. * [force c; chain ~pure:false c g] is correct. - * [greedy]: - * The [greedy] parameter forces immediately the new computation if - * the old one is_over (Exn or Val). Defaults to true. *) -val chain : ?greedy:bool -> pure:bool -> + *) +val chain : pure:bool -> 'a computation -> ('a -> 'b) -> 'b computation (* Forcing a computation *) @@ -143,9 +142,9 @@ val join : 'a computation -> 'a val sink : 'a computation -> unit (*** Utility functions ************************************************* ***) -val split2 : ?greedy:bool -> +val split2 : ('a * 'b) computation -> 'a computation * 'b computation -val map2 : ?greedy:bool -> +val map2 : ('a computation -> 'b -> 'c) -> 'a list computation -> 'b list -> 'c list diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 890ffe0a18..ab8dc0798c 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -58,7 +58,7 @@ let with_fp chan out_function flush_function = (* Output on a channel ch *) let with_output_to ch = - let ft = with_fp ch (output ch) (fun () -> flush ch) in + let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in set_gp ft deep_gp; ft diff --git a/lib/util.ml b/lib/util.ml index 9fb0d48ee8..0d2425f271 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -161,11 +161,11 @@ let iraise = Exninfo.iraise let open_utf8_file_in fname = let is_bom s = - Int.equal (Char.code s.[0]) 0xEF && - Int.equal (Char.code s.[1]) 0xBB && - Int.equal (Char.code s.[2]) 0xBF + Int.equal (Char.code (Bytes.get s 0)) 0xEF && + Int.equal (Char.code (Bytes.get s 1)) 0xBB && + Int.equal (Char.code (Bytes.get s 2)) 0xBF in let in_chan = open_in fname in - let s = " " in + let s = Bytes.make 3 ' ' in if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; in_chan diff --git a/library/nameops.ml b/library/nameops.ml index 6020db33d9..098f5112fd 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -61,7 +61,7 @@ let make_ident sa = function if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) else sa ^ "_" ^ (string_of_int n) in Id.of_string s - | None -> Id.of_string (String.copy sa) + | None -> Id.of_string sa let root_of_id id = let suffixstart = cut_ident true id in @@ -92,20 +92,20 @@ let increment_subscript id = add (carrypos-1) end else begin - let newid = String.copy id in - String.fill newid (carrypos+1) (len-1-carrypos) '0'; - newid.[carrypos] <- Char.chr (Char.code c + 1); + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); newid end else begin - let newid = id^"0" in + let newid = Bytes.of_string (id^"0") in if carrypos < len-1 then begin - String.fill newid (carrypos+1) (len-1-carrypos) '0'; - newid.[carrypos+1] <- '1' + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' end; newid end - in Id.of_string (add (len-1)) + in Id.of_bytes (add (len-1)) let has_subscript id = let id = Id.to_string id in @@ -113,9 +113,9 @@ let has_subscript id = let forget_subscript id = let numstart = cut_ident false id in - let newid = String.make (numstart+1) '0' in + let newid = Bytes.make (numstart+1) '0' in String.blit (Id.to_string id) 0 newid 0 numstart; - (Id.of_string newid) + (Id.of_bytes newid) let add_suffix id s = Id.of_string (Id.to_string id ^ s) let add_prefix s id = Id.of_string (s ^ Id.to_string id) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 02a720d2d9..72bd11e030 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -240,18 +240,19 @@ let unfreeze tt = (token_tree := tt) (* The string buffering machinery *) -let buff = ref (String.create 80) +let buff = ref (Bytes.create 80) let store len x = - if len >= String.length !buff then - buff := !buff ^ String.create (String.length !buff); - !buff.[len] <- x; + let open Bytes in + if len >= length !buff then + buff := cat !buff (create (length !buff)); + set !buff len x; succ len let rec nstore n len cs = if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len -let get_buff len = String.sub !buff 0 len +let get_buff len = Bytes.sub_string !buff 0 len (* The classical lexer: idents, numbers, quoted strings, comments *) @@ -382,6 +383,7 @@ let push_char c = real_push_char c let push_string s = Buffer.add_string current_comment s +let push_bytes s = Buffer.add_bytes current_comment s let null_comment s = let rec null i = @@ -716,13 +718,13 @@ let strip s = in if len == String.length s then s else - let s' = String.create len in + let s' = Bytes.create len in let rec loop i i' = if i == String.length s then s' else if s.[i] == ' ' then loop (i + 1) i' - else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end + else begin Bytes.set s' i' s.[i]; loop (i + 1) (i' + 1) end in - loop 0 0 + Bytes.to_string (loop 0 0) let terminal s = let s = strip s in diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index de97ba97c3..0a591e786f 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -91,10 +91,7 @@ let begins_with_CoqXX s = let unquote s = if lang () != Scheme then s - else - let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done; - s + else String.map (fun c -> if c == '\'' then '~' else c) s let rec qualify delim = function | [] -> assert false diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index a6309e61f9..8d0cc4a0db 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -40,11 +40,7 @@ let preamble _ comment _ usf = (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) let pr_id id = - let s = Id.to_string id in - for i = 0 to String.length s - 1 do - if s.[i] == '\'' then s.[i] <- '~' - done; - str s + str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id) let paren = pp_par true diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 5e7d810c93..d6a334c5fe 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -773,9 +773,7 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = String.copy (string_of_modfile mp) in - if s.[0] != s0.[0] then s.[0] <- s0.[0]; - s + String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp) let add_blacklist_entries l = blacklist_table := diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 685c07c9a8..fa01baab75 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -325,8 +325,9 @@ GEXTEND Gram l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> let loc0,pat = pat in let f c pat = - let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in - IntroAction (IntroApplyOn (c,(loc,pat))) in + let loc1 = Constrexpr_ops.constr_loc c in + let loc = Loc.merge loc0 loc1 in + IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in !@loc, List.fold_right f l pat ] ] ; simple_intropattern_closed: diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 2514ededb0..58123f63ef 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -257,7 +257,7 @@ let string_of_call ck = (Pptactic.pr_glob_tactic (Global.env ()) te) ) in - for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = String.map (fun c -> if c = '\n' then ' ' else c) s in let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in CString.strip s diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 75edf150e3..cd8c9e471e 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -302,9 +302,9 @@ let cons_production_parameter = function | TacTerm _ -> None | TacNonTerm (_, _, id) -> Some id -let add_glob_tactic_notation local n prods forml ids tac = +let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { - tacgram_level = n; + tacgram_level = level; tacgram_prods = prods; } in let tacobj = { @@ -360,7 +360,7 @@ let extend_atomic_tactic name entries = in List.iteri add_atomic entries -let add_ml_tactic_notation name prods = +let add_ml_tactic_notation name ~level prods = let len = List.length prods in let iter i prods = let open Tacexpr in @@ -372,10 +372,12 @@ let add_ml_tactic_notation name prods = let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in let tac = TacML (Loc.ghost, entry, List.map map ids) in - add_glob_tactic_notation false 0 prods true ids tac + add_glob_tactic_notation false ~level prods true ids tac in List.iteri iter (List.rev prods); - extend_atomic_tactic name prods + (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at + tactic_expr level 0) *) + if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) (** Ltac quotations *) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 969c118fb5..0695044736 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -45,7 +45,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 1a8f26b264..3f83f104e9 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -248,8 +248,8 @@ and intern_intro_pattern_action lf ist = function | IntroInjection l -> IntroInjection (List.map (intern_intro_pattern lf ist) l) | IntroWildcard | IntroRewrite _ as x -> x - | IntroApplyOn (c,pat) -> - IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat) + | IntroApplyOn ((loc,c),pat) -> + IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat) and intern_or_and_intro_pattern lf ist = function | IntroAndPattern l -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index aa646aa517..155cb31d85 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -520,7 +520,7 @@ let rec intropattern_ids (loc,pat) = match pat with List.flatten (List.map intropattern_ids (List.flatten ll)) | IntroAction (IntroInjection l) -> List.flatten (List.map intropattern_ids l) - | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat + | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat | IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _) | IntroForthcoming _ -> [] @@ -913,14 +913,14 @@ and interp_intro_pattern_action ist env sigma = function | IntroInjection l -> let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l - | IntroApplyOn (c,ipat) -> + | IntroApplyOn ((loc,c),ipat) -> let c = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) } in let sigma,ipat = interp_intro_pattern ist env sigma ipat in - sigma, IntroApplyOn (c,ipat) + sigma, IntroApplyOn ((loc,c),ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x and interp_or_and_intro_pattern ist env sigma = function @@ -1422,7 +1422,14 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") + | VFun (_, _, _,vars,_) -> + let numargs = List.length vars in + Tacticals.New.tclZEROMSG + (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ + Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ + Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ + pr_enum pr_name vars ++ Pp.str ".") + | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in tactic_of_value ist tac diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index b09bdda65c..fe3a9f3b2a 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -51,8 +51,8 @@ let rec subst_intro_pattern subst = function | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x and subst_intro_pattern_action subst = function - | IntroApplyOn (t,pat) -> - IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat) + | IntroApplyOn ((loc,t),pat) -> + IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat) | IntroOrAndPattern l -> IntroOrAndPattern (subst_intro_or_and_pattern subst l) | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a2ffe12e93..88ea08c840 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -500,8 +500,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) - ++ fnl ()) in + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -1129,6 +1128,10 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in + let () = if !debug_unification then + let open Pp in + Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 + ++ cut () ++ print_constr t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 7b2c5695fd..360843711c 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function | IntroInjection pl -> str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ str "]" - | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c + | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c | IntroRewrite true -> str "->" | IntroRewrite false -> str "<-" diff --git a/stm/stm.ml b/stm/stm.ml index e698d1c72e..e56db4090a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1618,9 +1618,9 @@ end = struct (* {{{ *) Future.from_val (Option.get (Global.body_of_constant_body c)) in let uc = Future.chain - ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in - let pr = Future.chain ~greedy:true ~pure:true pr discharge in - let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in + ~pure:true uc Univ.hcons_universe_context_set in + let pr = Future.chain ~pure:true pr discharge in + let pr = Future.chain ~pure:true pr Constr.hcons in Future.sink pr; let extra = Future.join uc in u.(bucket) <- uc; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6205bd1092..84d09d8330 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1815,24 +1815,37 @@ let find_matching_clause unifier clause = with NotExtensibleClause -> failwith "Cannot apply" in find clause +exception UnableToApply + let progress_with_clause flags innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in - if List.is_empty ordered_metas then error "Statement without assumptions."; + if List.is_empty ordered_metas then raise UnableToApply; let f mv = try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause) with Failure _ -> None in try List.find_map f ordered_metas - with Not_found -> error "Unable to unify." + with Not_found -> raise UnableToApply + +let explain_unable_to_apply_lemma loc env sigma thm innerclause = + user_err ~loc (hov 0 + (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++ + Pp.quote (Printer.pr_lconstr_env env sigma thm) ++ spc() ++ + str "on hypothesis of type" ++ brk(1,1) ++ + Pp.quote (Printer.pr_lconstr_env innerclause.env innerclause.evd (clenv_type innerclause)) ++ + str ".")) -let apply_in_once_main flags innerclause env sigma (d,lbind) = +let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e' = CErrors.push e in try aux (clenv_push_prod clause) - with NotExtensibleClause -> iraise e + with NotExtensibleClause -> + match e with + | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause + | _ -> iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -1852,7 +1865,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in + let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause (fun id -> Tacticals.New.tclTHENLIST [ @@ -2467,7 +2480,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id = intro_decomp_eq loc l' thin tac id | IntroRewrite l2r -> rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) - | IntroApplyOn (f,(loc,pat)) -> + | IntroApplyOn ((loc',f),(loc,pat)) -> let naming,tac_ipat = prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in let doclear = @@ -2479,7 +2492,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id = let Sigma (c, sigma, p) = f.delayed env sigma in Sigma ((c, NoBindings), sigma, p) } in - apply_in_delayed_once false true true with_evars naming id (None,(loc,f)) + apply_in_delayed_once false true true with_evars naming id (None,(loc',f)) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros_loc loc with_evars dft destopt = function diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out new file mode 100644 index 0000000000..ae3fd7acc7 --- /dev/null +++ b/test-suite/output/ltac_missing_args.out @@ -0,0 +1,21 @@ +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: +missing arguments for variables y and _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v new file mode 100644 index 0000000000..8ecd97aa56 --- /dev/null +++ b/test-suite/output/ltac_missing_args.v @@ -0,0 +1,19 @@ +Ltac foo x := idtac x. +Ltac bar x := fun y _ => idtac x y. +Ltac baz := foo. +Ltac qux := bar. +Ltac mydo tac := tac (). +Ltac rec x := rec. + +Goal True. + Fail foo. + Fail bar. + Fail bar True. + Fail baz. + Fail qux. + Fail mydo ltac:(fun _ _ => idtac). + Fail let tac := (fun _ => idtac) in tac. + Fail (fun _ => idtac). + Fail rec True. + Fail let rec tac x := tac in tac True. +Abort.
\ No newline at end of file diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index fb1a7ab1c1..9b58c524e4 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -572,7 +572,8 @@ Proof. intros A P (x & Hp & Huniq); split. - intro; exists x; auto. - intros (x0 & HPx0 & HQx0) x1 HPx1. - replace x1 with x0 by (transitivity x; [symmetry|]; auto). + assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto). + destruct H. assumption. Qed. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 9fc00e80c1..2cc2ecbc20 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -103,7 +103,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P of an [a] of type [A], a of a proof [h] that [a] satisfies [P], and a proof [h'] that [a] satisfies [Q]. Then [(proj1_sig (sig_of_sig2 y))] is the witness [a], - [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and + [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and [(proj3_sig y)] is the proof of [(Q a)]. *) Section Subset_projections2. @@ -190,6 +190,23 @@ Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). +(** η Principles *) +Definition sigT_eta {A P} (p : { a : A & P a }) + : p = existT _ (projT1 p) (projT2 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig_eta {A P} (p : { a : A | P a }) + : p = exist _ (proj1_sig p) (proj2_sig p). +Proof. destruct p; reflexivity. Defined. + +Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a }) + : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) + : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). +Proof. destruct p; reflexivity. Defined. + (** [sumbool] is a boolean type equipped with the justification of their value *) @@ -263,10 +280,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 56e03e965c..a10c180ccf 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -360,13 +360,12 @@ Module NoRetractToModalProposition. Section Paradox. Variable M : Prop -> Prop. -Hypothesis unit : forall A:Prop, A -> M A. -Hypothesis join : forall A:Prop, M (M A) -> M A. Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B. Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x). Proof. - eauto. + intros A P h x. + eapply incr in h; eauto. Qed. (** ** The universe of modal propositions *) @@ -470,7 +469,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem paradox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + exact bool. + exact p2b. @@ -480,8 +479,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End Paradox. @@ -516,7 +513,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem mparadox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => P). + exact bool. + exact p2b. @@ -526,8 +523,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End MParadox. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index ef2709b472..8b0aa6691e 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -1,4 +1,5 @@ Berardi.vo +PropExtensionalityFacts.vo ChoiceFacts.vo ClassicalChoice.vo ClassicalDescription.vo diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4842a89151..4dfb7af6aa 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -125,12 +125,9 @@ let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in let pdir = if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) - else String.copy ldir + else ldir in - for i = 0 to le - 1 do - if pdir.[i] = '.' then pdir.[i] <- '/'; - done; - pdir + String.map (fun c -> if c = '.' then '/' else c) pdir let standard opt = print "byte:\n"; @@ -524,10 +521,10 @@ let variables is_install opt (args,defs) = List.iter (fun c -> print " \\ -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; - print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n"; - print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n"; - print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n"; - print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n"; + print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n"; + print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n"; + print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n"; + print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n"; print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; @@ -767,9 +764,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other begin print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; print "\t mkdir $@ || rm -rf $@/*\n"; - print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; end; if !some_vfile then begin @@ -885,7 +882,7 @@ let check_overlapping_include (_,inc_i,inc_r) = *) let merlin targets (ml_inc,_,_) = print ".merlin:\n"; - print "\t@echo 'FLG -rectypes' > .merlin\n" ; + print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ; List.iter (fun c -> printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c) lib_dirs ; diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index f817ed5a2a..3d92c9356b 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -26,12 +26,7 @@ let norm_char c = if !latin1 then norm_char_latin1 c else Char.uppercase c -let norm_string s = - let u = String.copy s in - for i = 0 to String.length s - 1 do - u.[i] <- norm_char s.[i] - done; - u +let norm_string = String.map (fun s -> norm_char s) let compare_char c1 c2 = match norm_char c1, norm_char c2 with | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2 diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 9be791a8de..34108eff42 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -197,7 +197,7 @@ let prepare_entry s = function let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in let sc = String.sub s (h+1) (i-h-1) in - let ntn = String.make (String.length s - i) ' ' in + let ntn = Bytes.make (String.length s - i) ' ' in let k = ref 0 in let j = ref (i+1) in let quoted = ref false in @@ -205,22 +205,22 @@ let prepare_entry s = function while !j <= l do if not !quoted then begin (match s.[!j] with - | '_' -> ntn.[!k] <- ' '; incr k - | 'x' -> ntn.[!k] <- '_'; incr k + | '_' -> Bytes.set ntn !k ' '; incr k + | 'x' -> Bytes.set ntn !k '_'; incr k | '\'' -> quoted := true | _ -> assert false) end else if s.[!j] = '\'' then if (!j = l || s.[!j+1] = '_') then quoted := false - else (incr j; ntn.[!k] <- s.[!j]; incr k) + else (incr j; Bytes.set ntn !k s.[!j]; incr k) else begin - ntn.[!k] <- s.[!j]; + Bytes.set ntn !k s.[!j]; incr k end; incr j done; - let ntn = String.sub ntn 0 !k in + let ntn = Bytes.sub_string ntn 0 !k in if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" | _ -> s diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index d7bdf907a2..b8e69d6c6d 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -72,10 +72,13 @@ let really_read_fd fd s off len = let raw_input_line fd = try let b = Buffer.create 80 in - let s = String.make 1 '\000' in - while s <> "\n" do + let s = Bytes.make 1 '\000' in + let endl = Bytes.of_string "\n" in + let endr = Bytes.of_string "\r" in + while Bytes.compare s endl <> 0 do really_read_fd fd s 0 1; - if s <> "\n" && s <> "\r" then Buffer.add_string b s; + if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0 + then Buffer.add_bytes b s; done; Buffer.contents b with Unix.Unix_error _ -> raise End_of_file diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e9771cfa40..0dfd06726a 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -20,7 +20,7 @@ let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x type input_buffer = { mutable prompt : unit -> string; - mutable str : string; (* buffer of already read characters *) + mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) mutable tokens : Gram.coq_parsable; (* stream of tokens *) @@ -28,9 +28,9 @@ type input_buffer = { (* Double the size of the buffer. *) -let resize_buffer ibuf = - let nstr = String.create (2 * String.length ibuf.str + 1) in - String.blit ibuf.str 0 nstr 0 (String.length ibuf.str); +let resize_buffer ibuf = let open Bytes in + let nstr = create (2 * length ibuf.str + 1) in + blit ibuf.str 0 nstr 0 (length ibuf.str); ibuf.str <- nstr (* Delete all irrelevant lines of the input buffer. Keep the last line @@ -40,7 +40,7 @@ let resynch_buffer ibuf = match ibuf.bols with | ll::_ -> let new_len = ibuf.len - ll in - String.blit ibuf.str ll ibuf.str 0 new_len; + Bytes.blit ibuf.str ll ibuf.str 0 new_len; ibuf.len <- new_len; ibuf.bols <- []; ibuf.start <- ibuf.start + ll @@ -65,8 +65,8 @@ let prompt_char ic ibuf count = try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; - if ibuf.len == String.length ibuf.str then resize_buffer ibuf; - ibuf.str.[ibuf.len] <- c; + if ibuf.len == Bytes.length ibuf.str then resize_buffer ibuf; + Bytes.set ibuf.str ibuf.len c; ibuf.len <- ibuf.len + 1; Some c with End_of_file -> @@ -75,7 +75,7 @@ let prompt_char ic ibuf count = (* Reinitialize the char stream (after a Drop) *) let reset_input_buffer ic ibuf = - ibuf.str <- ""; + ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf)); @@ -109,19 +109,19 @@ let dotted_location (b,e) = else (String.make (e-b-1) '.', " ") -let blanch_utf8_string s bp ep = - let s' = String.make (ep-bp) ' ' in +let blanch_utf8_string s bp ep = let open Bytes in + let s' = make (ep-bp) ' ' in let j = ref 0 in for i = bp to ep - 1 do - let n = Char.code s.[i] in + let n = Char.code (get s i) in (* Heuristic: assume utf-8 chars are printed using a single fixed-size char and therefore contract all utf-8 code into one space; in any case, preserve tabulation so that its effective interpretation in terms of spacing is preserved *) - if s.[i] == '\t' then s'.[!j] <- '\t'; + if get s i == '\t' then set s' !j '\t'; if n < 0x80 || 0xC0 <= n then incr j done; - String.sub s' 0 !j + Bytes.sub_string s' 0 !j let print_highlight_location ib loc = let (bp,ep) = Loc.unloc loc in @@ -132,17 +132,17 @@ let print_highlight_location ib loc = | ([],(bl,el)) -> let shift = blanch_utf8_string ib.str bl bp in let span = String.length (blanch_utf8_string ib.str bp ep) in - (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++ + (str"> " ++ str(Bytes.sub_string ib.str bl (el-bl-1)) ++ fnl () ++ str"> " ++ str(shift) ++ str(String.make span '^')) | ((b1,e1)::ml,(bn,en)) -> let (d1,s1) = dotted_location (b1,bp) in let (dn,sn) = dotted_location (ep,en) in let l1 = (str"> " ++ str d1 ++ str s1 ++ - str(String.sub ib.str bp (e1-bp))) in + str(Bytes.sub_string ib.str bp (e1-bp))) in let li = prlist (fun (bi,ei) -> - (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in - let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++ + (str"> " ++ str(Bytes.sub_string ib.str bi (ei-bi)))) ml in + let ln = (str"> " ++ str(Bytes.sub_string ib.str bn (ep-bn)) ++ str sn ++ str dn) in (l1 ++ li ++ ln) in @@ -220,7 +220,7 @@ let top_buffer = ^ emacs_prompt_endstring() in { prompt = pr; - str = ""; + str = Bytes.empty; len = 0; bols = []; tokens = Gram.parsable (Stream.of_list []); diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index e40353e0f9..d248f2f706 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -15,7 +15,7 @@ open Pp type input_buffer = { mutable prompt : unit -> string; - mutable str : string; (** buffer of already read characters *) + mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f914f83b9b..b73321c005 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -108,7 +108,7 @@ let verbose_phrase verbch loc = let s = Bytes.create len in seek_in ch (fst loc); really_input ch s 0 len; - Feedback.msg_notice (str s) + Feedback.msg_notice (str (Bytes.to_string s)) | None -> () exception End_of_input @@ -126,7 +126,7 @@ let chan_beautify = ref stdout let beautify_suffix = ".beautified" let set_formatter_translator ch = - let out s b e = output ch s b e in + let out s b e = output_substring ch s b e in Format.set_formatter_output_functions out (fun () -> flush ch); Format.set_max_boxes max_int @@ -161,13 +161,11 @@ let pr_new_syntax po loc chan_beautify ocom = let pp_cmd_header loc com = let shorten s = try (String.sub s 0 30)^"..." with _ -> s in - let noblank s = - for i = 0 to Bytes.length s - 1 do - match s.[i] with - | ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~' - | _ -> () - done; - s + let noblank s = String.map (fun c -> + match c with + | ' ' | '\n' | '\t' | '\r' -> '~' + | x -> x + ) s in let (start,stop) = Loc.unloc loc in let safe_pr_vernac x = diff --git a/vernac/command.ml b/vernac/command.ml index 049f58aa26..4b4f4d2711 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -81,7 +81,7 @@ let red_constant_entry n ce sigma = function let Sigma (c, _, _) = redfun.e_redfun env sigma c in c in - { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out + { ce with const_entry_body = Future.chain ~pure:true proof_out (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } let warn_implicits_in_term = diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 55f33be399..798a238c74 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function (* Try all combinations... not optimal *) let env = Global.env() in { const with const_entry_body = - Future.chain ~greedy:true ~pure:true const.const_entry_body + Future.chain ~pure:true const.const_entry_body (fun ((body, ctx), eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8b7d654572..3afe04b37b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -517,9 +517,6 @@ let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> save_proof ?proof e - (* A stupid macro that should be replaced by ``Exact c. Save.'' all along - the theories [??] *) - let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) |