Revision a52f3279764e0095d59a4d8c7063342b2fa83178 authored by Pierre-Yves Strub on 13 July 2018, 18:34:30 UTC, committed by Pierre-Yves Strub on 13 July 2018, 18:35:17 UTC
This tactic tries to prove goal of the form "islossless M.f". It uses random/lossless solve DB for pruning goals related to the losslessness of samplings or call to abstract procs.
1 parent de5cd4a
ecRegexp.mli
(* --------------------------------------------------------------------
* 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
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
type error
type regexp
type subst
type match_
type split =
| Text of string
| Delim of string
exception Error of error
type oregexp = [`C of regexp | `S of string]
type osubst = [`C of subst | `S of string]
(* -------------------------------------------------------------------- *)
val quote : string -> string
val regexp : string -> regexp
val subst : string -> subst
(* -------------------------------------------------------------------- *)
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
(* -------------------------------------------------------------------- *)
val exec : ?pos:int -> oregexp -> string -> match_ option
val match_ : ?pos:int -> oregexp -> string -> bool
val split : ?pos:int -> oregexp -> string -> split list
val split0 : ?pos:int -> oregexp -> string -> string list
val sub : oregexp -> osubst -> string -> string
val extract : oregexp -> string -> (string option array) array
Computing file changes ...
