Execution and compilation hangs indefintely

[freddi301]

module Parser

import public Data.List.Quantifiers
import Data.List

public export
Parser : Type -> Type -> Type
Parser token result = List token -> Maybe (result, List token)

export
next : Parser token token
next [] = Nothing
next (head :: tail) = Just (head, tail)

export
exactly : Eq token => token -> Parser token token
exactly token [] = Nothing
exactly token (head :: tail) = if head == token then Just (head, tail) else Nothing

export
predicatively : (token -> Bool) -> Parser token token
predicatively predicate [] = Nothing
predicatively predicate (head :: tail) = if predicate head then Just (head, tail) else Nothing

export
repeatedly : {default 0 min : Nat} -> {default Nothing max : Maybe Nat} -> Parser token result -> Parser token (List result)
repeatedly {min} {max} parser tokens = outcome where
  collect : List result -> List token -> (List result, List token)
  collect items tokens with (the Bool $ case max of Nothing => True; (Just m) => length items < m)
    _ | False = (items, tokens)
    _ | True with (parser tokens)
      _ | Nothing = (items, tokens)
      _ | Just (item, remaining_tokens) = collect (snoc items item) remaining_tokens
  outcome = 
    let (items, remaining_tokens) = collect [] tokens in
    if (length items >= min) then Just (items, remaining_tokens) else Nothing

export
optionally : Parser token result -> Parser token (Maybe result)
optionally parser tokens with (repeatedly {max = Just 1} parser tokens)
  _ | Just ([], remaining_tokens) = Just (Nothing, remaining_tokens) 
  _ | Just ([item], remaining_tokens) = Just (Just item, remaining_tokens) 
  _ | _ = Nothing

export
sequentially : All (Parser token) results -> Parser token (HList results)
sequentially [] tokens = Just ([], tokens)
sequentially (parser :: remaining_parsers) tokens with (parser tokens)
  _ | Just (item, remaining_tokens) with (sequentially remaining_parsers remaining_tokens)
    _ | Just (items, more_tokens) = Just (item :: items, more_tokens)
    _ | Nothing = Nothing
  _ | Nothing = Nothing

export
alternatively : All (Parser token) results -> (choice : (All (\item => Maybe (item, List token)) results) -> Maybe result) -> Parser token result
-- alternatively parsers choice tokens = choice ((\parser => parser tokens) <$> parsers)

export
alternativelyFirst : List (Parser token result) -> Parser token result
alternativelyFirst [] tokens = Nothing
alternativelyFirst (parser :: remaining_parsers) tokens with (parser tokens)
  _ | Just (item, remaining_tokens) = Just (item, remaining_tokens)
  _ | Nothing = alternativelyFirst remaining_parsers tokens

export
mapped : (resultX -> resultY) -> Parser token resultX -> Parser token resultY
mapped mapper parser tokens with (parser tokens)
  _ | Just (item, remaining_tokens) = Just (mapper item, remaining_tokens)
  _ | Nothing = Nothing

export
flatMapped : (resultX -> Maybe resultY) -> Parser token resultX -> Parser token resultY
flatMapped mapper parser tokens with (parser tokens)
  _ | Just (item, remaining_tokens) with (mapper item)
    _ | Just mapped = Just (mapped, remaining_tokens)
    _ | Nothing = Nothing
  _ | Nothing = Nothing

test_1 : sequentially [exactly 1, exactly 2, exactly 3] [1, 2, 3, 4] = Just ([1, 2, 3], [4])
test_1 = Refl

test_2 : repeatedly (exactly True) [True, True, True] = Just ([True, True, True], [])
test_2 = Refl

test_3_parser = repeatedly (alternativelyFirst [exactly ',', predicatively isAlpha])
test_3 : test_3_parser (unpack "a,b,c") = Just (['a', ',', 'b', ',', 'c'], [])
test_3 = Refl

test_4_parser = mapped pack $ repeatedly $ predicatively isAlpha
test_4 : test_4_parser (unpack "aaaa,bbbb") = Just ("aaaa", unpack ",bbbb")
test_4 = Refl

test_5_parser = repeatedly $ repeatedly {max = Just 3} $ predicatively isAlpha
-- test_5 : test_5_parser (unpack "aaabbbccc") = Just ([unpack "aaa", unpack "bbb", unpack "ccc"], [])
-- test_5 = Refl
test_5_value = test_5_parser (unpack "aaabbbccc")

-- test_6_parser = repeatedly $ alternativelyFirst [
--   mapped pack $ repeatedly $ predicatively isAlpha,
--   mapped (const ",") $ exactly ','
-- ]
-- test_6 : test_6_parser (unpack "aaaa,bbbb") = Just (["aaaa", ",", "bbbb"], [])
-- test_6 = Refl

Steps to Reproduce

Load this file with repl then

• try to get read test_5_value
• uncomment test_5 and reload file

Expected Behavior

It prints test_5_value It compiles

Observed Behavior

Execution hangs indefinetly if try to get test_5_value Compilation hangs indefinitely if test_5 is decommmented

[mjustus]

Is this still the case after #3281?

[freddi301]

Sorry for opening a useless issue, i just noticed that the code is not total, there is an infite loop in the repeat combinator. I wrongly assumed that computation wont happen over values inside aun unapplied function (like in javascript). closing!

[mjustus]

No worries and thank you for confirming!