Merge branch '863-forward-propagation-strategy-accept-optionnal-arguments' into ...
[why3.git] / examples / dyck.mlw
blob35141b3600cdad6c31e5562b3a1601e5eb9abd25
2 (** Checking that a word is a Dyck word
4     Authors: Martin Clochard (École Normale Supérieure)
5              Jean-Christophe Filliâtre (CNRS)
6 *)
8 theory Dyck
10   use export list.List
11   use export list.Append
13   type paren = L | R
15   type word = list paren
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))
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
29 end
31 module Check
33   use Dyck
34   use list.Length
35   use ref.Ref
37   exception Failure
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
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
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
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
87 end