examples/dyck.mlw

   1
   2 (** Checking that a word is a Dyck word
   3
   4     Authors: Martin Clochard (École Normale Supérieure)
   5              Jean-Christophe Filliâtre (CNRS)
   6 *)
   7
   8 theory Dyck
   9
  10   use export list.List
  11   use export list.Append
  12
  13   type paren = L | R
  14
  15   type word = list paren
  16
  17   (* D -> eps | L D R D *)
  18   inductive dyck word =
  19   | Dyck_nil:
  20       dyck Nil
  21   | Dyck_ind:
  22       forall w1 w2. dyck w1 -> dyck w2 -> dyck (Cons L (w1 ++ Cons R w2))
  23
  24   (* the first letter, if any, must be L *)
  25   lemma dyck_word_first:
  26     forall w: word. dyck w ->
  27     match w with Nil -> true | Cons c _ -> c = L end
  28
  29 end
  30
  31 module Check
  32
  33   use Dyck
  34   use list.Length
  35   use ref.Ref
  36
  37   exception Failure
  38
  39   (* A fall of a word is a decomposition p ++ s with p a dyck word
  40      and s a word not starting by L. *)
  41   predicate fall (p s: word) = dyck p /\
  42     match s with Cons L _ -> false | _ -> true end
  43
  44   let rec lemma same_prefix (p s s2: word) : unit
  45     requires { p ++ s = p ++ s2 }
  46     ensures { s = s2 }
  47     variant { p }
  48   = match p with Nil -> () | Cons _ q -> same_prefix q s s2 end
  49
  50   (* Compute the fall decomposition, if it exists. As a side-effect,
  51      prove its unicity. *)
  52   let rec is_dyck_rec (ghost p: ref word) (w: word) : word
  53     ensures { w = !p ++ result && fall !p result &&
  54       (forall p2 s: word. w = p2 ++ s /\ fall p2 s -> p2 = !p && s = result) }
  55     writes { p }
  56     raises  { Failure -> forall p s: word. w = p ++ s -> not fall p s }
  57     variant { length w }
  58   =
  59     match w with
  60     | Cons L w0 ->
  61       let ghost p0 = ref Nil in
  62       match is_dyck_rec p0 w0 with
  63       | Cons _ w1 ->
  64         assert { forall p s p1 p2: word.
  65           dyck p /\ w = p ++ s /\ dyck p1 /\ dyck p2 /\
  66           p = Cons L (p1 ++ Cons R p2) ->
  67           w0 = p1 ++ (Cons R (p2 ++ s)) && p1 = !p0 && w1 = p2 ++ s };
  68         let ghost p1 = ref Nil in
  69         let w = is_dyck_rec p1 w1 in
  70         p := Cons L (!p0 ++ Cons R !p1);
  71         w
  72       | _ ->
  73         raise Failure
  74       end
  75     | _ ->
  76       p := Nil; w
  77     end
  78
  79   let is_dyck (w: word) : bool
  80     ensures { result <-> dyck w }
  81   =
  82     try match is_dyck_rec (ref Nil) w with
  83       | Nil -> true
  84       | _ -> false
  85     end with Failure -> false end
  86
  87 end
  88