diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm index bed306d..43a9d57 100644 --- a/src/Bergamot/Syntax.elm +++ b/src/Bergamot/Syntax.elm @@ -109,12 +109,21 @@ merge v1 v2 us = in case (ui1.term, ui2.term) of (Just t1, Just t2) -> - unify t1 t2 us - |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp) + if occurs ui1.equivalence us t2 || occurs ui2.equivalence us t1 + then Nothing + else + unify t1 t2 us + |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp) (Just t1, Nothing) -> - Just (reconcile newEq (Just t1) us) + if occurs ui2.equivalence us t1 + then Nothing + else + Just (reconcile newEq (Just t1) us) (Nothing, Just t2) -> - Just (reconcile newEq (Just t2) us) + if occurs ui1.equivalence us t2 + then Nothing + else + Just (reconcile newEq (Just t2) us) (Nothing, Nothing) -> Just (reconcile newEq Nothing us) (Just ui1, Nothing) -> Just (reconcile (Set.insert v2s ui1.equivalence) ui1.term us) @@ -128,13 +137,34 @@ set v t us = in case Dict.get vs 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 vs { equivalence = Set.singleton vs, term = Just t } us) + if occurs ui.equivalence us t + then Nothing + else + 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 -> + if occurs (Set.singleton vs) us t + then Nothing + else + Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us) + +occurs : Set String -> UnificationState -> Term UnificationVar -> Bool +occurs vars us t = + case t of + IntLit _ -> False + StringLit _ -> False + Call n ts -> List.any (occurs vars us) ts + Var (MkUnificationVar v) -> if Set.member v vars then True else + case Dict.get v us of + Just { term } -> + case term of + Just tp -> occurs vars us tp + Nothing -> False + _ -> False unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState) unifyList l1 l2 us =