SHARE
TWEET

Untitled

a guest Sep 17th, 2019 104 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module Parsing
  2. import ParsingHelpers
  3. --import Data.List.Quantifiers
  4.  
  5. data Transition : (a -> a -> Type) -> a -> a -> Type where
  6.   IdTrans : (f x y) -> Transition f x y
  7.   StepTrans : (f x y) -> Transition f y z -> Transition f x z
  8.  
  9. rhs_head_transitive_closure : DecEq s => Grammar s -> List s -> List (Rule s)
  10. rhs_head_transitive_closure g vs =
  11.   transitive_closure check conv g vs
  12.   where
  13.     check : (v : s) -> Rule s -> Bool
  14.     check v x = decAsBool (decEq v (lhs x))
  15.     conv  : Rule s -> s
  16.     conv = rhs_head
  17.  
  18. record Item (s:Type) where
  19.   constructor Incomplete
  20.   origin : Nat
  21.   rule : Rule s
  22.   dot_point : Index (rhs rule)
  23.  
  24. record CompleteItem (s:Type) where
  25.   constructor Complete
  26.   origin : Nat
  27.   rule : Rule s
  28.  
  29. predict : DecEq s => Grammar s -> List s -> List (s, Item s)
  30. predict g = map new_item . rhs_head_transitive_closure g
  31.   where new_item : Rule s -> (s, Item s)
  32.         new_item rule = (rhs_head rule, Incomplete Z rule rhs_head_index)
  33.  
  34. zeros : List (Nat, s) -> List (s)
  35. zeros [] = []
  36. zeros ((Z, x) :: xs) = x :: zeros xs
  37. zeros ((S _, _) :: xs) = zeros xs
  38.  
  39. decr : List (Nat, s) -> List (Nat, s)
  40. decr [] = []
  41. decr ((Z,s) :: xs) = decr xs
  42. decr ((S x,s) :: xs) = (x, s) :: decr xs
  43.  
  44. process : Nat -> List (s, Item s) ->
  45.   (List (Nat, s), List (CompleteItem s), List (s, Item s))
  46. process m [] = ([],[],[])
  47. process m ((x, Incomplete n r dp) :: xs) = let (a,b,c) = process m xs
  48.   in case nexth dp of
  49.   Just dpn => (a, b, (nth dpn, Incomplete (n+m) r dpn)::c)
  50.   Nothing => ((n, lhs r)::a, (Complete (n+m) r)::b, c)
  51.  
  52. pitpull : DecEq s => List s -> List (s, Item s) -> List (s, Item s)
  53. pitpull xs st = transitive_closure check conv st xs
  54.   where check : s -> (s, Item s) -> Bool
  55.         check x y = decAsBool (decEq x (fst y))
  56.         conv : (s, Item s) -> s
  57.         conv (x, Incomplete Z r dp) = case nexth dp of
  58.           Just _ => x
  59.           Nothing => lhs r
  60.         conv (x, _) = x
  61.  
  62. shift : DecEq s => List (List (s, Item s))
  63.   -> (List (Nat, s))
  64.   -> {default (S Z) m : Nat}
  65.   -> (List (CompleteItem s), List (s, Item s))
  66. shift [] ss {m} = ([], [])
  67. shift (st::sts) ss {m} = let
  68.   (tt,c1,s1) = process m (pitpull (zeros ss) st)
  69.   (c2,s2) = shift sts (decr $ tt ++ ss) {m=S m}
  70.   in (c1++c2, s1++s2)
  71.  
  72. recognize : DecEq s => (g : Grammar s) -> (acc:s) -> (input:List s) -> Bool
  73. recognize g acc input = step [predict g [acc]] input
  74.   where step : List (List (s, Item s)) -> (List s) -> Bool
  75.         step sts [] = False
  76.         step ([]::_) _ = False
  77.         step sts (x :: []) = let
  78.           (c,_) = shift sts [(0, x)]
  79.           m = (length sts)
  80.           in any (\(Complete n r) => (m == n) && decAsBool(decEq acc (lhs r))) c
  81.         step sts (x :: ys) = let
  82.           (_,st) = shift sts [(0, x)]
  83.           st2 = predict g (map fst st)
  84.           in step ((st++st2)::sts) ys
  85.  
  86. mutual
  87.   data Generates : Grammar s -> s -> List s -> Type where
  88.     Put : Generates g s [s]
  89.     Derive : (ir:Index g) -> Seq g (rhs (nth ir)) xs
  90.       -> {auto x_is:lhs (nth ir) = x}
  91.       -> Generates g x xs
  92.  
  93.   data Seq : Grammar s -> List s -> List s -> Type where
  94.     Nil  : Seq g [] []
  95.     (::) : Generates g s xs -> Seq g ss ys -> {auto zs_is:(xs ++ ys = zs)}
  96.       -> Seq g (s::ss) zs
  97.  
  98. recognize_lemma : DecEq s => (Grammar s) -> (acc:s) -> (input:List s)
  99.   -> (recognize g acc input = True) -> Generates g acc input
  100. recognize_lemma g acc [] Refl impossible
  101. recognize_lemma g acc (k::rest) prf = ?aaaaaa
  102.  
  103.  
  104.  
  105. --x -- Some two fun little auxiliary proofs.
  106. --x next_ndex_empty_tail : Dec (xs=[]) -> Dec (next_ndex (Z {xs=xs}) = Nothing)
  107. --x next_ndex_empty_tail (Yes Refl) = Yes Refl
  108. --x next_ndex_empty_tail {xs = []} (No contra) = Yes Refl
  109. --x next_ndex_empty_tail {xs = (x :: xs)} (No contra) =
  110. --x   No (\assum => case assum of Refl impossible)
  111. --x
  112. --x next_ndex_is_next : (next_ndex (Z {xs=(x::(y::xs))}) = Just (S Z {xs=(x::(y::xs))}))
  113. --x next_ndex_is_next = Refl
  114.  
  115. -- Test grammar, with some symbols
  116. data Symbol = A | B | C | D
  117.  
  118. DecEq Symbol where
  119.   decEq A A = Yes Refl
  120.   decEq A B = No (\pf => case pf of Refl impossible)
  121.   decEq A C = No (\pf => case pf of Refl impossible)
  122.   decEq A D = No (\pf => case pf of Refl impossible)
  123.   decEq B B = Yes Refl
  124.   decEq B A = No (\pf => case pf of Refl impossible)
  125.   decEq B C = No (\pf => case pf of Refl impossible)
  126.   decEq B D = No (\pf => case pf of Refl impossible)
  127.   decEq C C = Yes Refl
  128.   decEq C A = No (\pf => case pf of Refl impossible)
  129.   decEq C B = No (\pf => case pf of Refl impossible)
  130.   decEq C D = No (\pf => case pf of Refl impossible)
  131.   decEq D D = Yes Refl
  132.   decEq D A = No (\pf => case pf of Refl impossible)
  133.   decEq D B = No (\pf => case pf of Refl impossible)
  134.   decEq D C = No (\pf => case pf of Refl impossible)
  135.  
  136. test_grammar : Grammar Symbol
  137. test_grammar = [
  138.   D ::= [A,B,C],
  139.   D ::= [B,C],
  140.   D ::= [B,C],
  141.   B ::= [A,C],
  142.   A ::= [B,C],
  143.   B ::= [C] ]
  144.  
  145. leaf_a : SPPF Parsing.test_grammar (Sym A) [A]
  146. leaf_a = Leaf
  147. leaf_b : SPPF Parsing.test_grammar (Sym B) [B]
  148. leaf_b = Leaf
  149. leaf_c : SPPF Parsing.test_grammar (Sym C) [C]
  150. leaf_c = Leaf
  151. leaf_d : SPPF Parsing.test_grammar (Sym D) [D]
  152. leaf_d = Leaf
  153.  
  154. generates_abc : SPPF Parsing.test_grammar (Sym D) [A,B,C]
  155. generates_abc = Branch ab leaf_c {rule=Z} {dot=(S Z)}
  156.   where ab : SPPF Parsing.test_grammar (Dot Z {rule=Z}) [A,B]
  157.         ab = (Branch leaf_a leaf_b {rule=Z} {dot=Z})
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top