2023-11-25 22:51:53 -08:00
|
|
|
module Bergamot.Syntax exposing (Term(..))
|
|
|
|
|
|
|
|
import Set exposing (Set)
|
|
|
|
import Dict exposing (Dict)
|
|
|
|
import Maybe exposing (Maybe)
|
|
|
|
import Tuple
|
|
|
|
import Debug
|
|
|
|
|
|
|
|
type alias Name = String
|
2023-11-25 23:08:21 -08:00
|
|
|
type alias Metavariable = String
|
2023-11-25 22:53:08 -08:00
|
|
|
type alias UnificationVar = String
|
2023-11-25 22:51:53 -08:00
|
|
|
|
|
|
|
type Term a
|
|
|
|
= IntLit Int
|
|
|
|
| StringLit String
|
|
|
|
| Call Name (List (Term a))
|
|
|
|
| Var a
|
|
|
|
|
2023-11-25 23:08:21 -08:00
|
|
|
type alias InstantiationState =
|
|
|
|
{ counter : Int
|
|
|
|
, vars : Dict Metavariable UnificationVar
|
|
|
|
}
|
|
|
|
|
|
|
|
metavariable : Metavariable -> InstantiationState -> (UnificationVar, InstantiationState)
|
|
|
|
metavariable mv is =
|
|
|
|
case Dict.get mv is.vars of
|
|
|
|
Just v -> (v, is)
|
|
|
|
Nothing ->
|
|
|
|
let
|
|
|
|
v = "var" ++ (String.fromInt is.counter)
|
|
|
|
isp = { counter = is.counter + 1, vars = Dict.insert mv v is.vars }
|
|
|
|
in (v, isp)
|
|
|
|
|
|
|
|
instantiateList : List (Term Metavariable) -> InstantiationState -> (List (Term UnificationVar), InstantiationState)
|
|
|
|
instantiateList ml is =
|
|
|
|
case ml of
|
|
|
|
mt :: mts ->
|
|
|
|
instantiate mt is
|
|
|
|
|> \(t, isp) -> Tuple.mapFirst (\ts -> t :: ts) (instantiateList mts isp)
|
|
|
|
[] -> ([], is)
|
|
|
|
|
|
|
|
instantiate : Term Metavariable -> InstantiationState -> (Term UnificationVar, InstantiationState)
|
|
|
|
instantiate mt is =
|
|
|
|
case mt of
|
|
|
|
IntLit i -> (IntLit i, is)
|
|
|
|
StringLit s -> (StringLit s, is)
|
|
|
|
Call n mts -> Tuple.mapFirst (Call n) (instantiateList mts is)
|
|
|
|
Var mv -> Tuple.mapFirst Var (metavariable mv is)
|
|
|
|
|
2023-11-25 22:51:53 -08:00
|
|
|
type alias UnificationInfo =
|
2023-11-25 22:53:08 -08:00
|
|
|
{ equivalence : Set UnificationVar
|
|
|
|
, term : Maybe (Term UnificationVar)
|
2023-11-25 22:51:53 -08:00
|
|
|
}
|
|
|
|
|
2023-11-25 22:53:08 -08:00
|
|
|
type alias UnificationState = Dict UnificationVar UnificationInfo
|
2023-11-25 22:51:53 -08:00
|
|
|
|
2023-11-25 22:53:08 -08:00
|
|
|
reconcile : Set UnificationVar -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState
|
2023-11-25 22:51:53 -08:00
|
|
|
reconcile eq mt us =
|
|
|
|
let newValue = { equivalence = eq, term = mt }
|
|
|
|
in Set.foldl (\v -> Dict.insert v newValue) us eq
|
|
|
|
|
2023-11-25 22:53:08 -08:00
|
|
|
merge : UnificationVar -> UnificationVar -> UnificationState -> Maybe UnificationState
|
2023-11-25 22:51:53 -08:00
|
|
|
merge v1 v2 us =
|
|
|
|
case (Dict.get v1 us, Dict.get v2 us) of
|
|
|
|
(Just ui1, Just ui2) ->
|
|
|
|
let
|
|
|
|
newEq = Set.union ui1.equivalence ui2.equivalence
|
|
|
|
in
|
|
|
|
case (ui1.term, ui2.term) of
|
|
|
|
(Just t1, Just t2) ->
|
|
|
|
unify t1 t2 us
|
|
|
|
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
|
|
|
|
(Just t1, Nothing) ->
|
|
|
|
Just (reconcile newEq (Just t1) us)
|
|
|
|
(Nothing, Just t2) ->
|
|
|
|
Just (reconcile newEq (Just t2) us)
|
|
|
|
(Nothing, Nothing) ->
|
|
|
|
Just (reconcile newEq Nothing us)
|
|
|
|
(Just ui1, Nothing) -> Just (reconcile (Set.insert v2 ui1.equivalence) ui1.term us)
|
|
|
|
(Nothing, Just ui2) -> Just (reconcile (Set.insert v1 ui2.equivalence) ui2.term us)
|
|
|
|
(Nothing, Nothing) -> Just (reconcile (Set.fromList [v1,v2]) Nothing us)
|
|
|
|
|
2023-11-25 22:53:08 -08:00
|
|
|
set : UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState)
|
2023-11-25 22:51:53 -08:00
|
|
|
set v t us =
|
|
|
|
case Dict.get v us of
|
|
|
|
Just ui ->
|
|
|
|
case ui.term of
|
|
|
|
Just tp ->
|
|
|
|
unify t tp us
|
|
|
|
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
|
|
|
|
Nothing ->
|
|
|
|
Just (t, reconcile ui.equivalence (Just t) us)
|
|
|
|
Nothing -> Just (t, Dict.insert v { equivalence = Set.singleton v, term = Just t } us)
|
|
|
|
|
2023-11-25 22:53:08 -08:00
|
|
|
unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
|
2023-11-25 22:51:53 -08:00
|
|
|
unifyList l1 l2 us =
|
|
|
|
case (l1, l2) of
|
|
|
|
(t1 :: ts1, t2 :: ts2) ->
|
|
|
|
unify t1 t2 us
|
2023-11-25 23:08:05 -08:00
|
|
|
|> Maybe.andThen (\(t, usp) -> Maybe.map (Tuple.mapFirst (\ts -> t :: ts)) (unifyList ts1 ts2 usp))
|
2023-11-25 22:51:53 -08:00
|
|
|
([], []) -> Just ([], us)
|
|
|
|
_ -> Nothing
|
|
|
|
|
2023-11-25 22:53:08 -08:00
|
|
|
unify : Term UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState)
|
2023-11-25 22:51:53 -08:00
|
|
|
unify t1 t2 us =
|
|
|
|
case (t1, t2) of
|
|
|
|
(IntLit i1, IntLit i2) -> if i1 == i2 then Just (t1, us) else Nothing
|
|
|
|
(StringLit s1, StringLit s2) -> if s1 == s2 then Just (t1, us) else Nothing
|
|
|
|
(Call n1 ts1, Call n2 ts2) ->
|
|
|
|
if n1 == n2
|
|
|
|
then Maybe.map (Tuple.mapFirst (Call n1)) (unifyList ts1 ts2 us)
|
|
|
|
else Nothing
|
|
|
|
(Var v1, Var v2) ->
|
|
|
|
merge v1 v2 us
|
|
|
|
|> Maybe.map (\usp -> (Var v1, usp))
|
|
|
|
(Var v1, _) -> set v1 t2 us
|
|
|
|
(_, Var v2) -> set v2 t1 us
|
|
|
|
_ -> Nothing
|