<commit_before>module Prelude.Maybe

import Builtins
import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Interfaces
import Prelude.Foldable

%access public export
%default total

||| An optional value. This can be used to represent the possibility of
||| failure, where a function may return a value, or not.
data Maybe : (a : Type) -> Type where
    ||| No value stored
    Nothing : Maybe a
    ||| A value of type `a` is stored
    Just : (x : a) -> Maybe a

-- Used hints for erasure analysis
%used Just x

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

isNothing : Maybe a -> Bool
isNothing Nothing  = True
isNothing (Just j) = False

isJust : Maybe a -> Bool
isJust Nothing  = False
isJust (Just j) = True

||| Proof that some `Maybe` is actually `Just`
data IsJust : Maybe a -> Type where
  ItIsJust : IsJust (Just x)

--------------------------------------------------------------------------------
-- Misc
--------------------------------------------------------------------------------

maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
maybe n j Nothing  = n
maybe n j (Just x) = j x

||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
||| in the case that the `Maybe` value is `Nothing`.
fromMaybe : (Lazy a) -> Maybe a -> a
fromMaybe def Nothing  = def
fromMaybe def (Just j) = j

||| Returns `Just` the given value if the conditional is `True`
||| and `Nothing` if the conditional is `False`.
toMaybe : Bool -> Lazy a -> Maybe a
toMaybe True  j = Just j
toMaybe False j = Nothing

justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
justInjective Refl = Refl<commit_msg>Add decision procedure for IsJust<commit_after>module Prelude.Maybe

import Builtins
import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Interfaces
import Prelude.Foldable
import Prelude.Uninhabited

%access public export
%default total

||| An optional value. This can be used to represent the possibility of
||| failure, where a function may return a value, or not.
data Maybe : (a : Type) -> Type where
    ||| No value stored
    Nothing : Maybe a
    ||| A value of type `a` is stored
    Just : (x : a) -> Maybe a

-- Used hints for erasure analysis
%used Just x

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

isNothing : Maybe a -> Bool
isNothing Nothing  = True
isNothing (Just j) = False

isJust : Maybe a -> Bool
isJust Nothing  = False
isJust (Just j) = True

||| Proof that some `Maybe` is actually `Just`
data IsJust : Maybe a -> Type where
  ItIsJust : IsJust (Just x)

Uninhabited (IsJust Nothing) where
  uninhabited ItIsJust impossible

||| Decide whether a 'Maybe' is 'Just'
isItJust : (v : Maybe a) -> Dec (IsJust v)
isItJust (Just x) = Yes ItIsJust
isItJust Nothing = No absurd

--------------------------------------------------------------------------------
-- Misc
--------------------------------------------------------------------------------

maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
maybe n j Nothing  = n
maybe n j (Just x) = j x

||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
||| in the case that the `Maybe` value is `Nothing`.
fromMaybe : (Lazy a) -> Maybe a -> a
fromMaybe def Nothing  = def
fromMaybe def (Just j) = j

||| Returns `Just` the given value if the conditional is `True`
||| and `Nothing` if the conditional is `False`.
toMaybe : Bool -> Lazy a -> Maybe a
toMaybe True  j = Just j
toMaybe False j = Nothing

justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
justInjective Refl = Refl
{'fraction_non_alphanumeric': 0.25348477026329375, 'fraction_numerical': 0.0, 'mean_word_length': 1.7877697841726619, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 36, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1530742', 'n_tokens_mistral': 1086, 'n_tokens_neox': 1071, 'n_words': 480}