metavariables made unique in type checking

2 files changed, 13 insertions, 3 deletions

diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs
index c586aae8c..eee489100 100644
--- a/src/PGF/Expr.hs
+++ b/src/PGF/Expr.hs
@@ -10,7 +10,10 @@ module PGF.Expr(Tree(..), Literal(..),
                 Value(..), Env, eval, apply,

 

                 -- helpers

-                pStr,pFactor

+                pStr,pFactor,

+

+                -- refresh metavariables

+                newMetas

                ) where

 

 import PGF.CId

@@ -250,4 +253,11 @@ apply :: Value -> Value -> Value
 apply (VClosure env (EAbs x e)) v = eval (Map.insert x v env) e

 apply v0                        v = VApp v0 v

 

-

+--- use composOp and state monad...

+newMetas :: Expr -> Expr

+newMetas = fst . metas 0 where

+  metas i exp = case exp of

+    EAbs x e -> let (f,j) = metas i e in (EAbs x f, j)

+    EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k)

+    EMeta _  -> (EMeta i, i+1)

+    _        -> (exp,i)

diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs
index 1c0d04fd4..1a2ba334a 100644
--- a/src/PGF/TypeCheck.hs
+++ b/src/PGF/TypeCheck.hs
@@ -28,7 +28,7 @@ import Data.List (partition,sort,groupBy)
 import Debug.Trace
 
 typecheck :: PGF -> Tree -> [Tree]
-typecheck pgf t = case inferExpr pgf (tree2expr t) of
+typecheck pgf t = case inferExpr pgf (newMetas (tree2expr t)) of
   Ok t  -> [expr2tree t]
   Bad s -> trace s []