https://github.com/EasyCrypt/easycrypt
Revision 3ffc3beb6838ddcc61710a1327ef58b4714fce53 authored by Alley Stoughton on 06 October 2021, 15:00:49 UTC, committed by Pierre-Yves Strub on 07 October 2021, 06:39:26 UTC
1 parent 0656ac7
Raw File
Tip revision: 3ffc3beb6838ddcc61710a1327ef58b4714fce53 authored by Alley Stoughton on 06 October 2021, 15:00:49 UTC
Some lemmas for floor and ceil, in particular letting one rewrite
Tip revision: 3ffc3be
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
back to top