Haskell - Etat des variables dans l'expression analysée (La variable est-elle liée ou non?)

Question

Salut, donc j'ai une fonction qui prend une chaîne et calcule la valeur, int ou bool. La chaîne peut être i.e.: "* let X = 3 in + X 1 2", qui représentent "(let X = 3 in (X + 1)) * 2". Ce qui me donnera 8 ou faux si je demande un bool. Assez simple. Mais je veux aussi vérifier l'état des variables liées dans l'analyseur. C'est à dire. si j'utilise une chaîne comme celle-ci "* let X = 3 in + X 1 X" comme entrée, elle représentera "(let X = 3 in (X + 1)) * X" ce qui rendra le dernier X non lié. Cela me donnera alors une erreur en disant que la variable A est non liée ou quelque chose. Si quelqu'un pouvait me donner des idées sur comment je pourrais le faire, je serais très reconnaissant!

expample de chaîne analysable:

((let X = 3 in (X + 1)) * 2)

me donner:

(Mul (Let (Vari X) (Lit (Single 3)) (Sum (Vari X) (Lit (Single 1)))) (Vari X))

Alors ma question est basiclly comment je peux vérifier si la chaîne analysable a toutes les variables non liées .

data Number = Single Int | Many Int Number deriving (Eq, Show) 

data Expr = Vari Chara | Lit Number | Sub Expr | Sum Expr Expr | Mul Expr Expr | Let Expr Expr Expr | If Expr Expr Expr deriving (Eq, Show) 

Answer 1

Recopiez l'expression analysée en maintenant un ensemble de variables liées. Chaque fois que vous rencontrez un Let, enregistrez-le, chaque fois que vous rencontrez un Var, vérifiez qu'il est dans votre ensemble, et chaque fois que vous rencontrez quelque chose d'autre, vérifiez ses sous-expressions.

checkVars' :: Set String -> Expr -> Bool 
checkVars' bound (Var v) = S.member v set 
checkVars' bound (Let var val expr) = checkVars' bound val && checkVars' (insert var bound) expr 
checkVars' bound (Mul expr1 expr2) = checkVars' bound expr1 && checkVars' bound expr2 
-- Similar for other ctors... 

checkVars :: Expr -> Bool 
checkVars = checkVars' S.empty 

Vous pouvez également travailler dans le sens opposé, la construction d'un ensemble de variables libres du bas vers le haut, et la suppression des variables chaque fois que vous les voyez liés par Let. (Cela se sent plus naturel.)

freeVars :: Expr -> Set String 
freeVars (Var v) = S.singleton v 
freeVars (Let var val expr) = S.union (freeVars val) $ S.delete var $ freeVars expr 
freeVars (Add expr1 expr2) = S.union expr1 expr2 
-- etc. 

checkVars :: Expr -> Bool 
checkVars = S.null . freeVars 

-- With recursion-schemes 
data ExprF a = Add a a 
      | Mul a a 
      | Let String a a 
      | Var String 
      | Lit Int 
      deriving (Eq, Show, Read, Functor, Foldable, Traversable) 

type Expr = Fix ExprF 

freeVars :: Expr -> Set String 
freeVars = cata go -- -XLambdaCase, anyone? 
    where go :: ExprF (Set String) -> Set String 
     go (Var var) = S.singleton var 
     go (Let var val expr) = S.union val $ S.delete var expr 
     go e = foldl S.union S.empty e -- Handle everything else 

Answer 2

Je recommande d'utiliser une représentation sans nom localement pour les variables (telles que celles fournies par the extraordinarily useful bound library) dans une syntaxe avec une liaison. Dans une représentation localement sans nom, les variables liées sont représentées à l'aide d'indices de Bruijn, et les variables non liées sont représentées à l'aide d'un nom. Cela vous épargne beaucoup d'effort quand il s'agit de choses comme l'alpha-équivalence et la capture-évitant la substitution, et de répondre à la question "cette variable est-elle liée?" devient très simple.

Généralement, une représentation localement sans nom est la sortie d'une opération de vérification de portée sur un arbre de syntaxe de surface. Nous pouvons régler le code de @HNTW's answer pour produire un terme contrôlé au lieu d'un Bool:

data Scoped a = SVar a 
       | SLet (Scoped a) (Scope() Scoped a) -- The expression being let-bound, and the subexpression with the new variable in scope 
       | SLit Number 
       | SSub (Scoped a) 
       | SSum (Scoped a) (Scoped a) 
       | SMul (Scoped a) (Scoped a) 
       | SIf (Scoped a) (Scoped a) (Scoped a) 
       deriving (Functor, Foldable, Traversable) 

instance Applicative Scoped where 
    pure = SVar 
    (<*>) = ap 

instance Monad Scoped where 
    return = SVar 
    SVar a >>= g = g a 
    SLet expr scope >>= g = SLet (expr >>= g) (scope >>>= g) 
    SLit x >>= g = SLit x 
    SSub x >>= g = SSub (x >>= g) 
    SSum x y >>= g = SSum (x >>= g) (y >>= g) 
    SMul x y >>= g = SMul (x >>= g) (y >>= g) 
    SIf cond t f >>= g = SIf (cond >>= g) (t >>= g) (f >>= g) 

scoped :: Expr -> Scoped Char 
scoped (Var x) = SVar x 
scoped (Let name expr sub) = SLet (scope expr) (abstract1 name $ scoped sub) 
scoped (Lit x) = SLit x 
scoped (Sub s) = SSub (scoped s) 
scoped (Sum x y) = SSum (scoped x) (scoped y) 
scoped (Mul x y) = SMul (scoped x) (scoped y) 
scoped (If cond t f) = SIf (scoped cond) (scoped t) (scoped f) 

bound vues une expression comme « contenant » des noms a. L'instance Monad effectue une substitution ((>>=) :: Scoped a -> (a -> Scoped b) -> Scoped b prend une fonction mappant les noms a aux termes Scoped b et les regroupe), et la bibliothèque bound utilise cette opération de substitution pour implémenter des outils tels que abstract1, qui lie une variable dans une sous-expression, produisant une nouvelle sous-expression sous une forme localement sans nom.

(Il ne serait pas déraisonnable de supprimer le type séparé Expr et de produire un Scoped Char directement comme sortie de votre analyseur.Les instances Foldable et Traversable permettent de trouver toutes les variables non liées dans une expression.

unboundVariables :: Scoped a -> [a] 
unboundVariables = toList 

de isClosedbound Combinator fait exactement ce que vous vouliez: il retourne False si l'expression a des variables libres.

Si, pendant que vous marchez dans un champ, vous devez savoir si une variable particulière est liée ou libre, vous pouvez soit motif match sur B et F constructeurs de Var, ou the supplied Prisms:

isBound :: Var b f -> Bool 
isBound = is _B 

Pour plus d'informations sur le fonctionnement de bound, voir this blog post ou these slides.