Skip to content

Instantly share code, notes, and snippets.

@abailly
Last active April 1, 2020 18:52
Show Gist options
  • Save abailly/acfdab8aa967ba6a2f4f78a14298447b to your computer and use it in GitHub Desktop.
Save abailly/acfdab8aa967ba6a2f4f78a14298447b to your computer and use it in GitHub Desktop.
||| A proof of the validity of matching algorithm for
||| regular expressions
|||
||| From https://arxiv.org/abs/2003.06458
module re
%default total
infix 7 .|
infix 6 ..
||| Representation of Regular expressions
data R : Type where
R_0 : R
R_1 : R
R_char : Char -> R
(.|) : R -> R -> R
(..) : R -> R -> R
R_star : R -> R
||| Matching algorithms
data R_match : List Char -> R -> Type where
R_match_zero : R_match s R_0
R_match_unit : R_match [] R_1
R_match_char : {c : Char} -> R_match (c :: _) (R_char c)
R_match_plus1 : {s : List Char} -> {r1, r2 : R} -> R_match s r1 -> R_match s (r1 .| r2)
R_match_plus2 : {s : List Char} -> {r1, r2 : R} -> R_match s r2 -> R_match s (r1 .| r2)
R_match_times : {s1, s2 : List Char} -> {r1, r2 : R} ->
R_match s1 r1 -> R_match s2 r2 -> R_match (s1 ++ s2) (r1 .. r2)
R_match_star1 : {r : R} -> R_match [] (R_star r)
R_match_star2 : {s1, s2 : List Char} -> {r : R} ->
R_match s1 r ->
R_match s2 (R_star r) -> R_match (s1 ++ s2) (R_star r)
data R_match_partial : (whole : List Char) -> (r : R) -> Type where
R_match_here : (matched, rest : List Char) -> (r_match : R_match matched r) -> R_match_partial (matched ++ rest) r
||| A proof that the list `ls` can be split in 2 parts
data Split : (ls : List a) -> Type where
IsSplit : (prefix : List a) -> (suffix : List a) -> Split (prefix ++ suffix)
prepend : (x : a) -> Split xs -> Split (x :: xs)
prepend x (IsSplit prefix suffix) = IsSplit (x :: prefix) suffix
splits : (ls : List Char) -> List (Split ls)
splits [] = [] -- we could have a split [] [] but it's better to stop recursion with emnpty list
splits (x :: xs) =
let subsplits = splits xs
in IsSplit [x] xs :: map (prepend x) subsplits
mutual
check_partial : (re : R) -> (Either String (R_match_partial s re), List Char) -> Split s -> (Either String (R_match_partial s re), List Char)
check_partial _ r@(Right _, _) _ = r
check_partial re (Left err, _) (IsSplit pref suff) with (accept pref re)
check_partial re (Left err, _) (IsSplit pref suff) | (Left l) = (Left l, suff)
check_partial re (Left err, _) (IsSplit pref suff) | (Right x) = (Right (R_match_here pref suff x), suff)
accept_partial : (r : R) -> (s : List Char)
-> Either String (R_match_partial s r)
accept_partial r s =
let subs = splits s
in fst $ foldl (check_partial r) (Left "no match", the (List Char) []) subs
accept : (s : List Char) -> (r : R) -> Either String (R_match s r)
accept s R_0 = Right R_match_zero
accept [] R_1 = Right R_match_unit
accept s R_1 = Left $ "'" ++ pack s ++ "' is not empty"
accept [y] (R_char x) with (decEq x y)
accept [y] (R_char x) | (Yes prf) = rewrite prf in Right R_match_char
accept [y] (R_char x) | (No contra) = Left $ show y ++ " does not match " ++ show x
accept [] (R_char x) = Left $ "empty string cannot match char " ++ show x
accept s (x .| y) with (accept s x)
accept s (x .| y) | (Left l) with (accept s y)
accept s (x .| y) | (Left l) | (Left z) = Left l
accept s (x .| y) | (Left l) | (Right r) = Right (R_match_plus2 r)
accept s (x .| y) | (Right r) = Right (R_match_plus1 r)
accept s (x .. y) with (accept_partial x s)
accept s (x .. y) | (Left l) = Left l
accept (matched ++ rest) (x .. y) | (Right (R_match_here matched rest r_match)) with (accept rest y)
accept (matched ++ rest) (x .. y) | (Right (R_match_here matched rest r_match)) | (Left l) = Left l
accept (matched ++ rest) (x .. y) | (Right (R_match_here matched rest r_match)) | (Right r) = Right $ R_match_times r_match r
-- empty string matches <re>*
accept [] (R_star x) = Right $ R_match_star1
-- non empty string matches <re>* if a prefix matches <re>
-- and the rest matches <re>*
accept s (R_star x) with (accept_partial x s)
accept s (R_star x) | (Left l) = Left l
accept (matched ++ []) (R_star x) | (Right (R_match_here matched [] r_match)) = Right $ R_match_star2 r_match R_match_star1
accept (matched ++ rest) (R_star x) | (Right (R_match_here matched rest r_match)) with (accept rest (R_star x))
accept (matched ++ rest) (R_star x) | (Right (R_match_here matched rest r_match)) | with_pat = ?op_rhs
accept s _ = Left $ "failed to match " ++ pack s
-- namespace Test
-- test_empty : accept R_1 [] = Right R_match_unit
-- test_empty = Refl
-- test_seq_match_1 : accept (R_char 'a' .. R_char 'b') ['a','b'] = Right (R_match_times {s1=['a']} {s2=['b']} R_match_char R_match_char)
-- test_seq_match_1 = Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment