work on checking equations

grammars/logic/Logic.gf

@@ -81,7 +81,7 @@ def
   ImplE _ _ (ImplI _ _ b) a = b a ;
   NegE _ (NegI _ b) a = b a ;
   UnivE _ _ (UnivI _ _ b) a = b a ;
-  ExistE _ _ _ (ExistI _ _ a b) d = d a b ;
+  ExistE _ _ _ (ExistI A B a b) d = d a b ;
 
   -- Hypo and Pron are identities
   Hypo _ a = a ;

src/GF/Grammar/PrGrammar.hs

@@ -162,7 +162,7 @@ prBinds bi = if null bi
    prValDecl (x,t) = prParenth (prt_ x +++ ":" +++ prt_ t)
 
 instance Print Val where
-  prt (VGen i x) = prt x ---- ++ "-$" ++ show i ---- latter part for debugging
+  prt (VGen i x) = prt x ++ "{-" ++ show i ++ "-}" ---- latter part for debugging
   prt (VApp u v) = prt u +++ prv1 v
   prt (VCn mc) = prQIdent_ mc
   prt (VClos env e) = case e of

src/GF/Grammar/TC.hs

@@ -19,6 +19,7 @@ data AExp =
    | AAbs  Ident Val AExp 
    | AProd Ident AExp AExp 
    | AEqs  [([Exp],AExp)] ---
+   | AData Val
   deriving (Eq,Show)
 
 type Theory = QIdent -> Err Val
@@ -55,6 +56,7 @@ eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
              case e of
   Vr x    -> lookupVar env x
   Q m c   -> return $ VCn (m,c)
+  QC m c  -> return $ VCn (m,c) ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
   App f a -> join $ liftM2 app (eval env f) (eval env a)
   _ -> return $ VClos env e
@@ -86,6 +88,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
   let v = VGen k
   case e of
     Meta m -> return $ (AMeta m typ,[])
+    EData -> return $ (AData typ,[])
 
     Abs x t -> case typ of
       VClos env (Prod y a b) -> do
@@ -141,14 +144,14 @@ inferExp th tenv@(k,rho,gamma) e = case e of
      IC "String" -> return $ const $ Q cPredefAbs cString
      _ -> Bad s
 
-
+---- this is an unreliable function which should be rewritten (AR)
 checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
 checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ 
                                   chB tenv' ps' ty 
  where 
 
-  (ps',_,rho2,_) = ps2ts k ps
-  tenv' = (k,rho2++rho, gamma)
+  (ps',_,rho2,k') = ps2ts k ps
+  tenv' = (k, rho2++rho, gamma) ---- k' ?
   (k,rho,gamma) = tenv
 
   chB tenv@(k,rho,gamma) ps ty = case ps of
@@ -172,9 +175,11 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
 
   ps2ts k = foldr p2t ([],0,[],k) 
   p2t p (ps,i,g,k) = case p of
+     PW      -> (meta (MetaSymb i) : ps, i+1,g,k) 
      PV IW   -> (meta (MetaSymb i) : ps, i+1,g,k) 
      PV x    -> (vr x   : ps, i, upd x k g,k+1)
-----     PL s    -> (cn s : ps, i, g, k)
+     PString s -> (K s : ps, i, g, k)
+     PInt i -> (EInt i : ps, i, g, k)
      PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k') 
                     where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
      _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"

src/GF/Grammar/TypeCheck.hs

@@ -13,6 +13,7 @@ import TC
 import Unify ---
 
 import Monad (foldM, liftM, liftM2)
+import List (nub) ---
 
 -- top-level type checking functions; TC should not be called directly.
 
@@ -74,7 +75,8 @@ computeVal gr v = case v of
 splitConstraints :: Constraints -> (Constraints,MetaSubst)
 splitConstraints cs = csmsu where
 
-  csmsu     = unif (csf,msf)  -- alternative: filter first
+  csmsu     = (nub [(a,b) | (a,b) <- csf,a /= b],msf)
+  csmsu0    = unif (csf,msf)  -- alternative: filter first
   (csf,msf) = foldr mkOne ([],[]) cs
 
   csmsf     = foldr mkOne ([],msu) csu

src/GF/Source/GrammarToSource.hs

@@ -152,6 +152,7 @@ trt trm = case trm of
     Alts (t, tt) -> P.EPre (trt t) [P.Alt (trt v) (trt c) | (v,c) <- tt]
     FV ts -> P.EVariants $ map trt ts
     Strs tt -> P.EStrs $ map trt tt
+    EData -> P.EData
     _ -> error $ "not yet" +++ show trm ----
 
 trp :: Patt -> P.Patt