Rename the 'Metavariable' type to 'UnificationVar'
'metavariable' is inaccurate. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
bfa9deb0b0
commit
a9163c0797
|
@ -7,7 +7,7 @@ import Tuple
|
||||||
import Debug
|
import Debug
|
||||||
|
|
||||||
type alias Name = String
|
type alias Name = String
|
||||||
type alias Metavariable = String
|
type alias UnificationVar = String
|
||||||
|
|
||||||
type Term a
|
type Term a
|
||||||
= IntLit Int
|
= IntLit Int
|
||||||
|
@ -16,18 +16,18 @@ type Term a
|
||||||
| Var a
|
| Var a
|
||||||
|
|
||||||
type alias UnificationInfo =
|
type alias UnificationInfo =
|
||||||
{ equivalence : Set Metavariable
|
{ equivalence : Set UnificationVar
|
||||||
, term : Maybe (Term Metavariable)
|
, term : Maybe (Term UnificationVar)
|
||||||
}
|
}
|
||||||
|
|
||||||
type alias UnificationState = Dict Metavariable UnificationInfo
|
type alias UnificationState = Dict UnificationVar UnificationInfo
|
||||||
|
|
||||||
reconcile : Set Metavariable -> Maybe (Term Metavariable) -> UnificationState -> UnificationState
|
reconcile : Set UnificationVar -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState
|
||||||
reconcile eq mt us =
|
reconcile eq mt us =
|
||||||
let newValue = { equivalence = eq, term = mt }
|
let newValue = { equivalence = eq, term = mt }
|
||||||
in Set.foldl (\v -> Dict.insert v newValue) us eq
|
in Set.foldl (\v -> Dict.insert v newValue) us eq
|
||||||
|
|
||||||
merge : Metavariable -> Metavariable -> UnificationState -> Maybe UnificationState
|
merge : UnificationVar -> UnificationVar -> UnificationState -> Maybe UnificationState
|
||||||
merge v1 v2 us =
|
merge v1 v2 us =
|
||||||
case (Dict.get v1 us, Dict.get v2 us) of
|
case (Dict.get v1 us, Dict.get v2 us) of
|
||||||
(Just ui1, Just ui2) ->
|
(Just ui1, Just ui2) ->
|
||||||
|
@ -48,7 +48,7 @@ merge v1 v2 us =
|
||||||
(Nothing, Just ui2) -> Just (reconcile (Set.insert v1 ui2.equivalence) ui2.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)
|
(Nothing, Nothing) -> Just (reconcile (Set.fromList [v1,v2]) Nothing us)
|
||||||
|
|
||||||
set : Metavariable -> Term Metavariable -> UnificationState -> Maybe (Term Metavariable, UnificationState)
|
set : UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState)
|
||||||
set v t us =
|
set v t us =
|
||||||
case Dict.get v us of
|
case Dict.get v us of
|
||||||
Just ui ->
|
Just ui ->
|
||||||
|
@ -60,7 +60,7 @@ set v t us =
|
||||||
Just (t, reconcile ui.equivalence (Just t) us)
|
Just (t, reconcile ui.equivalence (Just t) us)
|
||||||
Nothing -> Just (t, Dict.insert v { equivalence = Set.singleton v, term = Just t } us)
|
Nothing -> Just (t, Dict.insert v { equivalence = Set.singleton v, term = Just t } us)
|
||||||
|
|
||||||
unifyList : List (Term Metavariable) -> List (Term Metavariable) -> UnificationState -> Maybe (List (Term Metavariable), UnificationState)
|
unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
|
||||||
unifyList l1 l2 us =
|
unifyList l1 l2 us =
|
||||||
case (l1, l2) of
|
case (l1, l2) of
|
||||||
(t1 :: ts1, t2 :: ts2) ->
|
(t1 :: ts1, t2 :: ts2) ->
|
||||||
|
@ -69,7 +69,7 @@ unifyList l1 l2 us =
|
||||||
([], []) -> Just ([], us)
|
([], []) -> Just ([], us)
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
|
|
||||||
unify : Term Metavariable -> Term Metavariable -> UnificationState -> Maybe (Term Metavariable, UnificationState)
|
unify : Term UnificationVar -> Term UnificationVar -> UnificationState -> Maybe (Term UnificationVar, UnificationState)
|
||||||
unify t1 t2 us =
|
unify t1 t2 us =
|
||||||
case (t1, t2) of
|
case (t1, t2) of
|
||||||
(IntLit i1, IntLit i2) -> if i1 == i2 then Just (t1, us) else Nothing
|
(IntLit i1, IntLit i2) -> if i1 == i2 then Just (t1, us) else Nothing
|
||||||
|
|
Loading…
Reference in New Issue
Block a user