From a24fbad2494adbb4433d2e8caf18ce28bf8c3570 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 26 Nov 2023 12:58:38 -0800 Subject: [PATCH] Make Metavariable and UnificationVar newtypes to help type safety Signed-off-by: Danila Fedorin --- src/Bergamot/Parser.elm | 16 +++---- src/Bergamot/Syntax.elm | 92 ++++++++++++++++++++++++----------------- 2 files changed, 63 insertions(+), 45 deletions(-) diff --git a/src/Bergamot/Parser.elm b/src/Bergamot/Parser.elm index f653d14..81f706a 100644 --- a/src/Bergamot/Parser.elm +++ b/src/Bergamot/Parser.elm @@ -1,6 +1,6 @@ module Bergamot.Parser exposing (..) -import Bergamot.Syntax exposing (Term(..), Metavariable) +import Bergamot.Syntax exposing (Term(..), Metavariable(..)) import Bergamot.Rules exposing (Rule, RuleEnv) import Parser exposing (Parser, Trailing(..), (|.), (|=)) @@ -16,12 +16,14 @@ name = Parser.variable , reserved = Set.empty } -variable : Parser String -variable = Parser.variable - { start = \c -> c == '?' - , inner = \c -> Char.isAlphaNum c || c == '_' - , reserved = Set.empty - } +variable : Parser Metavariable +variable = + Parser.succeed MkMetavariable + |= Parser.variable + { start = \c -> c == '?' + , inner = \c -> Char.isAlphaNum c || c == '_' + , reserved = Set.empty + } term : Parser (Term Metavariable) term = Parser.lazy (\() -> Parser.oneOf diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm index 06c6325..ca0f4de 100644 --- a/src/Bergamot/Syntax.elm +++ b/src/Bergamot/Syntax.elm @@ -1,5 +1,5 @@ module Bergamot.Syntax exposing - ( Term(..), Metavariable, UnificationVar + ( Term(..), Metavariable(..), UnificationVar(..) , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars , unify, unifyList, UnificationState, emptyUnificationState , reify @@ -12,8 +12,14 @@ import Tuple import Debug type alias Name = String -type alias Metavariable = String -type alias UnificationVar = String +type Metavariable = MkMetavariable String +type UnificationVar = MkUnificationVar String + +unMetavariable : Metavariable -> String +unMetavariable (MkMetavariable s) = s + +unUnificationVar : UnificationVar -> String +unUnificationVar (MkUnificationVar s) = s type Term a = IntLit Int @@ -23,7 +29,7 @@ type Term a type alias InstantiationState = { counter : Int - , vars : Dict Metavariable UnificationVar + , vars : Dict String UnificationVar } emptyInstantiationState = { counter = 0, vars = Dict.empty } @@ -33,12 +39,15 @@ resetVars is = { is | vars = Dict.empty } metavariable : Metavariable -> InstantiationState -> (UnificationVar, InstantiationState) metavariable mv is = - case Dict.get mv is.vars of + case Dict.get (unMetavariable 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 } + v = MkUnificationVar ("var" ++ (String.fromInt is.counter)) + isp = + { counter = is.counter + 1 + , vars = Dict.insert (unMetavariable mv) v is.vars + } in (v, isp) instantiateList : List (Term Metavariable) -> InstantiationState -> (List (Term UnificationVar), InstantiationState) @@ -58,51 +67,58 @@ instantiate mt is = Var mv -> Tuple.mapFirst Var (metavariable mv is) type alias UnificationInfo = - { equivalence : Set UnificationVar + { equivalence : Set String , term : Maybe (Term UnificationVar) } -type alias UnificationState = Dict UnificationVar UnificationInfo +type alias UnificationState = Dict String UnificationInfo emptyUnificationState = Dict.empty -reconcile : Set UnificationVar -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState +reconcile : Set String -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState reconcile eq mt us = let newValue = { equivalence = eq, term = mt } in Set.foldl (\v -> Dict.insert v newValue) us eq merge : UnificationVar -> UnificationVar -> UnificationState -> Maybe UnificationState 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) + let + v1s = unUnificationVar v1 + v2s = unUnificationVar v2 + in + case (Dict.get v1s us, Dict.get v2s 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 v2s ui1.equivalence) ui1.term us) + (Nothing, Just ui2) -> Just (reconcile (Set.insert v1s ui2.equivalence) ui2.term us) + (Nothing, Nothing) -> Just (reconcile (Set.fromList [v1s,v2s]) Nothing us) set : UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState) 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) + let + vs = unUnificationVar v + 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) unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState) unifyList l1 l2 us = @@ -136,7 +152,7 @@ reify t us = StringLit s -> StringLit s Call n ts -> Call n (List.map (\tp -> reify tp us) ts) Var v -> - case Dict.get v us of + case Dict.get (unUnificationVar v) us of Just ui -> case ui.term of Just tp -> reify tp us