why3/examples/coma/re.coma

use int.Int
use seq.Seq
use seq.FreeMonoid

(** {Logical definition of Regular Expressions} *)

type char

type regexp =
  | Empty
  | Epsilon
  | Char    char
  | Alt     regexp regexp
  | Concat  regexp regexp
  | Star    regexp


predicate re_g (r r1: regexp)

axiom re_g_alt :
  forall r r1 r2: regexp.
  r = Alt r1 r2 -> re_g r r1 /\ re_g r r2

axiom re_g_concat :
  forall r r1 r2: regexp.
  r = Concat r1 r2 -> re_g r r1 /\ re_g r r2

axiom re_g_star :
  forall r r1: regexp.
  r = Star r1 -> re_g r r1

-- lemma re_g_trans :
--   forall r1 r2 r3: regexp. re_g r1 r2 -> re_g r2 r3 -> re_g r1 r3

type word = seq char

inductive mem (w: word) (r: regexp) =
  | mem_eps:
      mem empty Epsilon
  | mem_char:
      forall c: char. mem (singleton c) (Char c)
  | mem_altl:
      forall w: word, r1 r2: regexp. mem w r1 -> mem w (Alt r1 r2)
  | mem_altr:
      forall w: word, r1 r2: regexp. mem w r2 -> mem w (Alt r1 r2)
  | mem_concat:
      forall w1 w2: word, r1 r2: regexp.
      mem w1 r1 -> mem w2 r2 -> mem (w1 ++ w2) (Concat r1 r2)
  | mems1:
      forall r: regexp. mem empty (Star r)
  | mems2:
      forall w1 w2: word, r: regexp.
      mem w1 r -> mem w2 (Star r) -> mem (w1 ++ w2) (Star r)

lemma mem_star_nonempty: forall w: word. forall r: regexp.
  mem w (Star r) ->
  w <> empty ->
    exists k: int.
      0 < k <= length w /\
      mem w[..k] r /\
      mem w[k..] (Star r)

lemma split_concat: forall w: word. forall r1 r2: regexp.
  mem w (Concat r1 r2) ->
    exists k: int.
      0 <= k <= length w /\
      mem w[..k] r1 /\ mem w[k..] r2

lemma concat_split: forall w: word. forall r1 r2: regexp. forall i j k: int.
  0 <= i <= k <= j <= length w ->
    mem w[i..k] r1 ->
    mem w[k..j] r2 ->
    mem w[i..j] (Concat r1 r2)

lemma extseq: forall w: word. w[0..length w] = w

(** {Coma Part} *)
use coma.Std

let unRe (r: regexp)
    (empty {r = Empty})
    (eps {r = Epsilon})
    (char (c: char) {r = Char c})
    (alt (r1 r2: regexp) {r = Alt r1 r2})
    (cat (r1 r2: regexp) {r = Concat r1 r2})
    (star (r1: regexp) {r = Star r1})
= any

predicate cons (w: word) (r: regexp) (ck: int -> bool) (i: int) =
  [@inline:trivial]
  exists j. i <= j <= length w /\ mem w[i..j] r /\ ck j

let accept_nonterm (r: regexp) (w: word) {} (ret (b: bool) {b <-> mem w r})
= a {r} {0} {fun j -> j = n}
    (fun (i: int) (h) -> if {i = n} (ret {true}) h)
    (ret {false})
  [ a (r: regexp) (i: int) (ck: int -> bool) {0 <= i <= n}
      (k (j: int) {mem w[i..j] r} {i <= j <= n} (h {not ck j}))
      (o {not cons w r ck i})
    = unRe {r} empty eps char alt cat star
      [ empty -> o
      | eps   -> k {i} o
      | char (c: char) ->
          if {i < n && w[i] = c} (k {i+1} o) o
      | alt (r1 r2: regexp) ->
          a {r1} {i} {ck} k (-> a {r2} {i} {ck} k o)
      | cat (r1 r2: regexp) ->
          a {r1} {i} {cons w r2 ck}
          (fun (j: int) (h) -> a {r2} {j} {ck} k h) o
      | star (r1: regexp) ->
          k {i} (-> a {r1} {i} {fun j -> i < j && cons w r ck j}
                     (fun (j: int) (h) -> if {i < j} (-> a {r} {j} {ck} k h) h)
                     o)
      ]
  ]
  [ n: int = length w ]

predicate v (n old_i i: int) (old_r r: regexp) =
  (n-i) < (n-old_i) || (old_i=i /\ re_g old_r r)

-- variant lexico : n-i, r
let accept_terminates (r: regexp) (w: word) {} (ret (b: bool) {b <-> mem w r})
= a {r} {0} {fun j -> j = n}
    (fun (i: int) (h) -> if {i = n} (ret {true}) h)
    ({not mem w[0..n] r} ret {false})
  [ a (r: regexp) (i: int) (ck: int -> bool) {0 <= i <= n}
      (k (j: int) {mem w[i..j] r} {i <= j <= n} (h {not ck j}))
      (o {not cons w r ck i})
    = (fun (r__: regexp) (i__: int) ->
        unRe {r} empty eps char alt cat star
        [ empty -> o
        | eps   -> k {i} o
        | char (c: char) ->
            if {i < n && w[i] = c} (k {i+1} o) o
        | alt (r1 r2: regexp) ->
            arec {r1} {i} {ck} k (-> arec {r2} {i} {ck} k o)
        | cat (r1 r2: regexp) ->
            arec {r1} {i} {cons w r2 ck}
            (fun (j: int) (h) -> arec {r2} {j} {ck} k h) o
        | star (r1: regexp) ->
            k {i} (-> arec {r1} {i} {fun j -> i < j && cons w r ck j}
                       (fun (j: int) (h) -> if {i < j} (-> arec {r} {j} {ck} k h) h)
                       o)
        ]
        [ arec (r_: regexp) (i_: int) (ck_: int -> bool) (k_ (j: int) (h)) (o_)
        -> { v n i__ i_ r__ r_ } a {r_} {i_} {ck_} k_ o_ ]) {r} {i}
  ]
  [ n: int = length w ]