dyck.mlw 2.14 KB
Newer Older
1

2 3 4 5 6 7
(** Checking that a word is a Dyck word

    Authors: Martin Clochard (École Normale Supérieure)
             Jean-Christophe Filliâtre (CNRS)
*)

8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
theory Dyck

  use export list.List
  use export list.Append

  type paren = L | R

  type word = list paren

  (* D -> eps | L D R D *)
  inductive dyck word =
  | Dyck_nil:
      dyck Nil
  | Dyck_ind:
      forall w1 w2. dyck w1 -> dyck w2 -> dyck (Cons L (w1 ++ Cons R w2))

  (* the first letter, if any, must be L *)
  lemma dyck_word_first:
    forall w: word. dyck w ->
    match w with Nil -> true | Cons c _ -> c = L end

end

module Check

33 34 35
  use Dyck
  use list.Length
  use ref.Ref
36 37 38

  exception Failure

39 40
  (* A fall of a word is a decomposition p ++ s with p a dyck word
     and s a word not starting by L. *)
41
  predicate fall (p s: word) = dyck p /\
42 43
    match s with Cons L _ -> false | _ -> true end

44
  let rec lemma same_prefix (p s s2: word) : unit
45 46 47 48 49 50 51
    requires { p ++ s = p ++ s2 }
    ensures { s = s2 }
    variant { p }
  = match p with Nil -> () | Cons _ q -> same_prefix q s s2 end

  (* Compute the fall decomposition, if it exists. As a side-effect,
     prove its unicity. *)
52
  let rec is_dyck_rec (ghost p: ref word) (w: word) : word
53 54 55
    ensures { w = !p ++ result && fall !p result &&
      (forall p2 s: word. w = p2 ++ s /\ fall p2 s -> p2 = !p && s = result) }
    writes { p }
56
    raises  { Failure -> forall p s: word. w = p ++ s -> not fall p s }
57 58 59
    variant { length w }
  =
    match w with
60 61
    | Cons L w0 ->
      let ghost p0 = ref Nil in
62
      match is_dyck_rec p0 w0 with
63 64 65 66 67
      | Cons _ w1 ->
        assert { forall p s p1 p2: word.
          dyck p /\ w = p ++ s /\ dyck p1 /\ dyck p2 /\
          p = Cons L (p1 ++ Cons R p2) ->
          w0 = p1 ++ (Cons R (p2 ++ s)) && p1 = !p0 && w1 = p2 ++ s };
68 69 70 71
        let ghost p1 = ref Nil in
        let w = is_dyck_rec p1 w1 in
        p := Cons L (!p0 ++ Cons R !p1);
        w
72 73
      | _ ->
        raise Failure
74
      end
75 76
    | _ ->
      p := Nil; w
77 78 79 80 81
    end

  let is_dyck (w: word) : bool
    ensures { result <-> dyck w }
  =
82
    try match is_dyck_rec (ref Nil) w with
83 84 85
      | Nil -> true
      | _ -> false
    end with Failure -> false end
86 87 88

end