PatternMatching.fs

[<RequireQualifiedAccess>]
type Type =
    | Unit
    | Bool
    | Int
    | Sum of (string * Type list) list

[<RequireQualifiedAccess>]
type Pattern =
    | Variable of string
    | Wildcard
    | Or of Pattern * Pattern
    | Unit
    | Bool of bool
    | Int of int
    | Constructor of string * Pattern list
    | As of Pattern * string

type Expression =
    | Unit
    | Bool of bool
    | Int of int
    | Variable of string
    | Constructor of string * Expression list * Type
    | Match of Expression * (Pattern * Expression option * Expression) list

[<RequireQualifiedAccess>]
type State =
    | Satisfied
    | Unit
    | Int of int list
    | Bool of bool option
    | Sum of (string * State list) list

let list_equal equals list_a list_b =
    (List.length list_a = List.length list_b) && List.forall2 equals list_a list_b

let tuple_equal equals_fst equals_snd (tuple_a_fst, tuple_a_snd) (tuple_b_fst, tuple_b_snd) =
    equals_fst tuple_a_fst tuple_b_fst && equals_snd tuple_a_snd tuple_b_snd

let rec type_equal type_a type_b =
    match type_a, type_b with
    | Type.Unit, Type.Unit
    | Type.Bool, Type.Bool
    | Type.Int, Type.Int -> true
    | Type.Sum constructors_a, Type.Sum constructors_b ->
        list_equal
            (tuple_equal (=) (list_equal type_equal))
            (List.sortBy fst constructors_a)
            (List.sortBy fst constructors_b)
    | (Type.Unit | Type.Bool | Type.Int | Type.Sum _), (Type.Unit | Type.Bool | Type.Int | Type.Sum _) -> false


// TODO: should error when a given type doesn't even have a possible valid pattern, like a function type
let rec get_type_binds type_ pattern =
    match type_, pattern with
    | _, Pattern.Variable ident -> [ (ident, type_) ]
    | _, Pattern.Wildcard -> []
    | _, Pattern.Or(pattern_a, pattern_b) ->
        let binds_a = get_type_binds type_ pattern_a
        let binds_b = get_type_binds type_ pattern_b

        if list_equal (tuple_equal (=) type_equal) (List.sortBy fst binds_a) (List.sortBy fst binds_b) then
            binds_a
        else
            failwith "TODO: both sides of the or pattern need to have the same binds"
    | _, Pattern.As(pattern, ident) ->
        let binds = get_type_binds type_ pattern

        if List.exists (fst >> (=) ident) binds then
            failwith "TODO: error about repeated bind name in same pattern"
        else
            (ident, type_) :: binds
    | Type.Sum constructors, Pattern.Constructor(ident, patterns) ->
        let types =
            List.tryFind (fst >> (=) ident) constructors
            |> Option.map snd
            |> function
                | None -> failwith "TODO: error about not finding "
                | Some types when List.length types <> List.length patterns ->
                    failwith
                        "TODO: error about the different length of the types the constructors carries and the pattern, a way to improve this would be checking the length problem in the same iteration that goes check if the pattern is valid with a given type, this way, more accurate error can be given"
                | Some types -> types

        let binds = List.map2 get_type_binds types patterns |> List.concat

        binds
        |> List.map fst
        |> List.fold
            (fun set key ->
                if Set.contains key set then
                    failwith "TODO: error about repeated bind name in same pattern"
                else
                    Set.add key set)
            Set.empty
        |> ignore

        binds
    | Type.Int, Pattern.Int _
    | Type.Bool, Pattern.Bool _
    | Type.Unit, Pattern.Unit _ -> []
    | (Type.Sum _ | Type.Int | Type.Bool | Type.Unit),
      (Pattern.Variable _ | Pattern.Wildcard | Pattern.Or _ | Pattern.Unit | Pattern.Bool _ | Pattern.Int _ | Pattern.Constructor _) ->
        failwith "TODO: error about pattern not being valid for given expression/type"


let rec get_next_state state pattern =
    match state, pattern with
    | State.Satisfied, _ ->
        printfn "TODO: warning about unreachable branch"
        State.Satisfied
    | _, (Pattern.Variable _ | Pattern.Wildcard) -> State.Satisfied
    | _, Pattern.Or(pattern_a, pattern_b) ->
        let next_state = get_next_state state pattern_a
        get_next_state next_state pattern_b
    | _, (Pattern.As(pattern, _)) -> get_next_state state pattern
    | State.Unit, (Pattern.Unit) -> State.Satisfied
    | State.Bool None, Pattern.Bool boolean -> State.Bool(Some boolean)
    | State.Bool(Some state_boolean), Pattern.Bool pattern_boolean ->
        if state_boolean = pattern_boolean then
            printfn "TODO: warning about unreachable branch"
            state
        else
            State.Satisfied
    | State.Int previous_integers, Pattern.Int integer ->
        if List.contains integer previous_integers then
            printfn "TODO: warning about unreachable branch"
            state
        else
            State.Int(integer :: previous_integers)
    | State.Sum constructors_states, Pattern.Constructor(ident, constructor_patterns) ->
        let next_constructors_states =
            constructors_states
            |> List.choose (fun ((constructor_ident, constructor_states) as element) ->

                if constructor_ident = ident then

                    List.map2 get_next_state constructor_states constructor_patterns
                    |> function
                        | states when states |> List.forall ((=) State.Satisfied) -> None
                        | states -> Some(constructor_ident, states)

                else
                    Some element

            )

        next_constructors_states
        |> List.isEmpty
        |> function
            | true -> State.Satisfied
            | false -> State.Sum next_constructors_states

    | (State.Satisfied | State.Unit | State.Int _ | State.Bool _ | State.Sum _),
      (Pattern.Variable _ | Pattern.Wildcard | Pattern.Or _ | Pattern.Unit | Pattern.Bool _ | Pattern.Int _ | Pattern.Constructor _ | Pattern.As _) ->
        failwith "should not happen"


let rec get_initial_state type_ =
    match type_ with
    | Type.Unit -> State.Unit
    | Type.Int -> State.Int []
    | Type.Bool -> State.Bool None
    | Type.Sum constructors ->
        constructors
        |> List.map (fun (ident, types) -> (ident, List.map get_initial_state types))
        |> State.Sum


let rec type_of env expression =
    match expression with
    | Unit -> Type.Unit
    | Bool _ -> Type.Bool
    | Int _ -> Type.Int
    | Variable ident ->
        // TODO: change for a safe lookup
        Map.find ident env
    | Constructor(_, _, type_) ->
        // TODO: check if the type actually matches the constructor
        type_
    | Match(to_match, branches) ->
        let to_match_type = type_of env to_match

        let folder (expected_type, state) (pattern, guard, body) =
            let new_env =
                get_type_binds to_match_type pattern
                |> List.fold (fun env (ident, type_) -> Map.add ident type_ env) env

            check_guard new_env guard

            let body_type = type_of new_env body

            check_match_body expected_type body_type

            let next_state = get_next_state state pattern

            let next_state' = if Option.isSome guard then state else next_state

            Some body_type, next_state'

        let (expected_type, state) =
            List.fold folder (None, get_initial_state to_match_type) branches

        match state with
        | State.Satisfied -> ()
        | _ ->
            printfn
                "TODO: warning about non exhaustive patterns, i can use the current state informing the previous patterns matched and the type to give information about what is left"

        Option.get expected_type


and check_guard env guard =
    guard
    |> Option.map (type_of env)
    |> Option.map (type_equal Type.Bool)
    |> function
        | Some false -> failwith "TODO: guard expression must have type Bool"
        | _ -> ()

and check_match_body expected_type body_type =
    expected_type
    |> Option.map (type_equal body_type)
    |> function
        | Some false -> failwith "TODO: body expression has the wrong type"
        | _ -> ()

TODO: fix the bug on product types