Revision 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC, committed by Pierre-Yves Strub on 26 February 2018, 15:04:53 UTC
The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *)
1 parent 5115c89
ecRegexp.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
(* -------------------------------------------------------------------- *)
type split =
| Text of string
| Delim of string
(* -------------------------------------------------------------------- *)
module type CORE = sig
type error
type regexp
type subst
type match_
exception Error of error
val quote : string -> string
val regexp : string -> regexp
val subst : string -> subst
val exec : ?pos:int -> regexp -> string -> match_ option
val split : ?pos:int -> regexp -> string -> split list
val sub : regexp -> subst -> string -> string
val extract : regexp -> string -> (string option array) array
module Match : sig
val count : match_ -> int
val group : match_ -> int -> string option
val groups : match_ -> (string option) array
val offset : match_ -> int -> (int * int) option
end
end
(* -------------------------------------------------------------------- *)
module PcreCore : CORE = struct
type regexp = Pcre.regexp
type subst = Pcre.substitution
type match_ = Pcre.substrings
type error =
| PCREError of Pcre.error
| InvalidSubString of int
| InvalidBackRef
exception Error of error
let wrap (f : 'a -> 'b) (x : 'a) =
try f x
with Pcre.Error err -> raise (Error (PCREError err))
let quote (x : string) = (wrap Pcre.quote ) x
let regexp (x : string) = (wrap Pcre.regexp) x
let subst (x : string) = (wrap Pcre.subst ) x
let exec ?(pos = 0) (rex : regexp) (x : string) =
try Some (wrap (Pcre.exec ~pos ~rex) x)
with Not_found -> None
let split ?(pos = 0) (rex : regexp) (x : string) =
let convert = function
| Pcre.Text s -> Some (Text s)
| Pcre.Delim s -> Some (Delim s)
| _ -> None
in List.pmap convert (wrap (Pcre.full_split ~pos ~rex) x)
let sub (rex : regexp) (subst : subst) (x : string) =
try wrap (Pcre.replace ~rex ~itempl:subst) x
with Failure _ -> raise (Error InvalidBackRef)
let extract (rex : regexp) (x : string) =
try wrap (Pcre.extract_all_opt ~full_match:true ~rex) x
with Not_found -> [||]
module Match = struct
let count (m : match_) : int =
(wrap Pcre.num_of_subs) m
let group (m : match_) (i : int) : string option =
try Some (wrap (Pcre.get_substring m) i)
with
| Invalid_argument _ -> raise (Error (InvalidSubString i))
| Not_found -> None
let groups (m : match_) : (string option) array =
wrap (Pcre.get_opt_substrings ~full_match:true) m
let offset (m : match_) (i : int) : (int * int) option =
try Some (wrap (Pcre.get_substring_ofs m) i)
with
| Invalid_argument _ -> raise (Error (InvalidSubString i))
| Not_found -> None
end
end
(* -------------------------------------------------------------------- *)
module Core : CORE = PcreCore
(* -------------------------------------------------------------------- *)
include Core
type oregexp = [`C of regexp | `S of string]
type osubst = [`C of subst | `S of string]
(* -------------------------------------------------------------------- *)
let oregexp (rex : oregexp) =
match rex with
| `C rex -> rex
| `S rex -> Core.regexp rex
let osubst (subst : osubst) =
match subst with
| `C sst -> sst
| `S sst -> Core.subst sst
(* -------------------------------------------------------------------- *)
let exec ?(pos : int option) (rex : oregexp) (x : string) =
exec ?pos (oregexp rex) x
let match_ ?(pos : int option) (rex : oregexp) (x : string) =
is_some (exec ?pos rex x)
let split ?(pos : int option) (rex : oregexp) (x : string) =
split ?pos (oregexp rex) x
let split0 ?(pos : int option) (rex : oregexp) (x : string) =
let convert = function Text s -> Some s | Delim _ -> None in
List.pmap convert (split ?pos rex x)
let sub (rex : oregexp) (sst : osubst) (x : string) =
sub (oregexp rex) (osubst sst) x
let extract (rex : oregexp) (x : string) =
extract (oregexp rex) x
Computing file changes ...