Everything-I-Know-About-Types/bergamot-elm
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Make Metavariable and UnificationVar newtypes to help type safety

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-11-26 12:58:38 -08:00
parent 985be53367
commit a24fbad249
2 changed files with 63 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/Bergamot/Parser.elm
View File

@ -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

92
src/Bergamot/Syntax.elm
View File

@ -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