------------------------------------------------------------------------
-- The Agda standard library
--
-- Example use case for a trie: a wee generic lexer
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module README.Data.Trie.NonDependent where
------------------------------------------------------------------------
-- Introduction
-- A Trie is a tree of values indexed by words in a finite language. It
-- allows users to quickly compute the Brzozowski derivative of that
-- little mapping from words to values.
-- In the most general case, values can depend upon the list of characters
-- that constitutes the path leading to them. Here however we consider a
-- non-dependent case (cf. README.Trie.Dependent for a dependent use case).
-- We can recognize keywords by storing the list of characters they
-- correspond to as paths in a Trie and the constructor they are decoded
-- to as the tree's values.
-- E.g.
-- [ . ] is a root
-- [ -- m --> ] is an m-labeled edge and is followed when reading 'm'
-- [ (X) ] is a value leaf storing constructor X
-- --> -- m --> -- m --> -- a --> (LEMMA)
-- /
-- -- l --> -- e --> -- t --> (LET)
-- /
-- / -- u --> -- t --> -- u --> -- a --> -- l --> (MUTUAL)
-- / /
-- .< -- m --> -- o --> -- d --> -- u --> -- l --> -- e --> (MODULE)
-- \
-- -- w --> -- h --> -- e --> -- r --> -- e --> (WHERE)
-- \
-- --> -- n --> (WHEN)
-- after reading 'w', we get the derivative:
-- . -- h --> -- e --> -- r --> -- e --> (WHERE)
-- \
-- --> -- n --> (WHEN)
open import Level
open import Data.Unit
open import Data.Bool
open import Data.Char as Char
import Data.Char.Properties as Char
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Fresh as List# using (List#; []; _∷#_)
open import Data.Maybe as Maybe
open import Data.Product.Base as Product using (_×_; ∃; proj₁; _,_)
open import Data.String.Base as String using (String)
open import Data.String.Properties as String using (_≟_)
open import Data.These as These
open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
open import Relation.Nary
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary.Decidable using (¬?)
open import Data.Trie Char.<-strictTotalOrder
open import Data.Tree.AVL.Value
------------------------------------------------------------------------
-- Generic lexer
record Lexer t : Set (suc t) where
field
-- Our lexer is parametrised over the type of tokens
Tok : Set t
-- Keywords are distinguished strings associated to tokens
Keyword : Set t
Keyword = String × Tok
-- Two keywords are considered distinct if the strings are not equal
Distinct : Rel Keyword 0ℓ
Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋
field
-- We ask users to provide us with a fresh list of keywords to guarantee
-- that no two keywords share the same string representation
keywords : List# Keyword Distinct
-- Some characters are special: they are separators, breaking a string
-- into a list of tokens. Some are associated to a token value
-- (e.g. parentheses) others are not (e.g. space)
breaking : Char → ∃ λ b → if b then Maybe Tok else Lift _ ⊤
-- Finally, strings which are not decoded as keywords are coerced
-- using a function to token values.
default : String → Tok
module _ {t} (L : Lexer t) where
open Lexer L
tokenize : String → List Tok
tokenize = start ∘′ String.toList where
mutual
-- A Trie is defined for an alphabet of strictly ordered letters (here
-- we have picked Char for letters and decided to use the strict total
-- order induced by their injection into ℕ as witnessed by the statement
-- open import Data.Trie Char.strictTotalOrder earlier in this file).
-- It is parametrised by a set of Values indexed over list of letters.
-- Because we focus on the non-dependent case, we pick the constant
-- family of Value uniformly equal to Tok. It is trivially compatible
-- with the notion of equality underlying the strict total order on Chars.
Keywords : Set _
Keywords = Trie (const _ Tok) _
-- We build a trie from the association list so that we may easily
-- compute the successive derivatives obtained by eating the
-- characters one by one
init : Keywords
init = fromList $ List.map (Product.map₁ String.toList) $ proj₁ $ List#.toList keywords
-- Kickstart the tokeniser with an empty accumulator and the initial
-- trie.
start : List Char → List Tok
start = loop [] init
-- The main loop
loop : (acc : List Char) → -- chars read so far in this token
(toks : Keywords) → -- keyword candidates left at this point
(input : List Char) → -- list of chars to tokenize
List Tok
-- Empty input: finish up, check whether we have a non-empty accumulator
loop acc toks [] = push acc []
-- At least one character
loop acc toks (c ∷ cs) = case breaking c of λ where
-- if we are supposed to break on this character, we do
(true , m) → push acc $ maybe′ _∷_ id m $ start cs
-- otherwise we see whether it leads to a recognized keyword
(false , _) → case lookupValue toks (c ∷ []) of λ where
-- if so we can forget about the current accumulator and
-- restart the tokenizer on the rest of the input
(just tok) → tok ∷ start cs
-- otherwise we record the character we read in the accumulator,
-- compute the derivative of the map of keyword candidates and
-- keep going with the rest of the input
nothing → loop (c ∷ acc) (lookupTrie toks c) cs
-- Grab the accumulator and, unless it is empty, push it on top of
-- the decoded list of tokens
push : List Char → List Tok → List Tok
push [] ts = ts
push cs ts = default (String.fromList (List.reverse cs)) ∷ ts
------------------------------------------------------------------------
-- Concrete instance
-- A small set of keywords for a language with expressions of the form
-- `let x = e in b`.
module LetIn where
data TOK : Set where
LET EQ IN : TOK
LPAR RPAR : TOK
ID : String → TOK
keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋)
keywords = ("let" , LET)
∷# ("=" , EQ)
∷# ("in" , IN)
∷# []
-- Breaking characters: spaces (thrown away) and parentheses (kept)
breaking : Char → ∃ (λ b → if b then Maybe TOK else Lift 0ℓ ⊤)
breaking c = if isSpace c then true , nothing else parens c where
parens : Char → _
parens '(' = true , just LPAR
parens ')' = true , just RPAR
parens _ = false , _
default : String → TOK
default = ID
letIn : Lexer 0ℓ
letIn = record { LetIn }
open import Agda.Builtin.Equality
-- A test case:
open LetIn
_ : tokenize letIn "fix f x = let b = fix f in (f b) x"
≡ ID "fix"
∷ ID "f"
∷ ID "x"
∷ EQ
∷ LET
∷ ID "b"
∷ EQ
∷ ID "fix"
∷ ID "f"
∷ IN
∷ LPAR
∷ ID "f"
∷ ID "b"
∷ RPAR
∷ ID "x"
∷ []
_ = refl