# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223318473 14400
# Node ID a0b8b550e265c5a3abc4e6c9c4d2183b72c781d1
# Parent  fd505bcb5632a86d8e046fc2776cd3118606a1d4
Add 'Or' to regexp matcher

diff -r fd505bcb5632 -r a0b8b550e265 src/MoreDep.v
--- a/src/MoreDep.v	Mon Oct 06 14:33:11 2008 -0400
+++ b/src/MoreDep.v	Mon Oct 06 14:41:13 2008 -0400
@@ -353,7 +353,9 @@
 | Char : forall ch : ascii,
   regexp (fun s => s = String ch "")
 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
-  regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
+  regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
+| Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
+  regexp (fun s => P1 s \/ P2 s).
 
 Open Scope specif_scope.
 
@@ -465,6 +467,7 @@
     match r with
       | Char ch => string_dec s (String ch "")
       | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
+      | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
     end); crush;
   match goal with
     | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
@@ -475,3 +478,9 @@
 Example hi := Concat (Char "h"%char) (Char "i"%char).
 Eval simpl in matches hi "hi".
 Eval simpl in matches hi "bye".
+
+Example a_b := Or (Char "a"%char) (Char "b"%char).
+Eval simpl in matches a_b "".
+Eval simpl in matches a_b "a".
+Eval simpl in matches a_b "aa".
+Eval simpl in matches a_b "b".