diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm index 15cc4fe..01cafbc 100644 --- a/src/Bergamot/Syntax.elm +++ b/src/Bergamot/Syntax.elm @@ -1,4 +1,4 @@ -module Bergamot.Syntax exposing (Term(..)) +module Bergamot.Syntax exposing (Term(..), instantiate, emptyInstantiationState, unify, emptyUnificationState) import Set exposing (Set) import Dict exposing (Dict) @@ -21,6 +21,8 @@ type alias InstantiationState = , vars : Dict Metavariable UnificationVar } +emptyInstantiationState = { counter = 0, vars = Dict.empty } + metavariable : Metavariable -> InstantiationState -> (UnificationVar, InstantiationState) metavariable mv is = case Dict.get mv is.vars of @@ -54,6 +56,8 @@ type alias UnificationInfo = type alias UnificationState = Dict UnificationVar UnificationInfo +emptyUnificationState = Dict.empty + reconcile : Set UnificationVar -> Maybe (Term UnificationVar) -> UnificationState -> UnificationState reconcile eq mt us = let newValue = { equivalence = eq, term = mt }