    ------------------------------------------------------------------------
    -- 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