From 7f7f543f592cfab8b8031a5f90255c6e5a8d0e51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Tue, 26 Sep 2023 10:09:23 +0200
Subject: [PATCH 01/24] Fix quasiquotation syntax error

---
 src/compiler/GF/CompileInParallel.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/compiler/GF/CompileInParallel.hs b/src/compiler/GF/CompileInParallel.hs
index ed498a6903..de11a7a7d4 100644
--- a/src/compiler/GF/CompileInParallel.hs
+++ b/src/compiler/GF/CompileInParallel.hs
@@ -61,7 +61,7 @@ parallelBatchCompile jobs opts rootfiles0 =
 
         usesPresent (_,paths) = take 1 libs==["present"]
           where
-            libs = [p|path<-paths,
+            libs = [p | path<-paths,
                       let (d,p0) = splitAt n path
                           p = dropSlash p0,
                       d==lib_dir,p `elem` all_modes]
@@ -175,7 +175,7 @@ batchCompile1 lib_dir (opts,filepaths) =
                    " from being compiled."
        else return (maximum ts,(cnc,gr))
 
-splitEither es = ([x|Left x<-es],[y|Right y<-es])
+splitEither es = ([x | Left x<-es],[y | Right y<-es])
 
 canonical path = liftIO $ D.canonicalizePath path `catch` const (return path)
 

From ea5c77ca4f1ecb19923bc40a3aa4927d0b3dac5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Thu, 28 Sep 2023 02:10:32 +0200
Subject: [PATCH 02/24] Add more missing spaces

---
 src/compiler/GF/CompileInParallel.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/compiler/GF/CompileInParallel.hs b/src/compiler/GF/CompileInParallel.hs
index de11a7a7d4..987c4a9c1d 100644
--- a/src/compiler/GF/CompileInParallel.hs
+++ b/src/compiler/GF/CompileInParallel.hs
@@ -171,7 +171,7 @@ batchCompile1 lib_dir (opts,filepaths) =
                    <+>length (nub (map (dropFileName.fst) ds))<+>"directories."
      let n = length es
      if n>0
-       then fail $ "Errors prevented "++show n++" module"++['s'|n/=1]++
+       then fail $ "Errors prevented "++show n++" module"++['s' | n/=1] ++
                    " from being compiled."
        else return (maximum ts,(cnc,gr))
 

From 1ada0a9e977701d4f562056b55093def8a99f6ae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 16:40:16 +0200
Subject: [PATCH 03/24] Prepare for making the info needed available

---
 src/compiler/GF/Compile/TypeCheck/Abstract.hs | 11 ++-
 src/compiler/GF/Compile/TypeCheck/TC.hs       | 86 ++++++++++++-------
 src/compiler/GF/Compile/Update.hs             | 18 ++--
 3 files changed, 75 insertions(+), 40 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index c766602597..083e7373ad 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -30,6 +30,7 @@ import GF.Grammar.Unify
 import GF.Compile.TypeCheck.TC
 
 import GF.Text.Pretty
+import Debug.Trace (traceM)
 --import Control.Monad (foldM, liftM, liftM2)
 
 -- | invariant way of creating TCEnv from context
@@ -61,9 +62,11 @@ notJustMeta (c,k) = case (c,k) of
 
 grammar2theory :: SourceGrammar -> Theory
 grammar2theory gr (m,f) = case lookupFunType gr m f of
-  Ok t -> return $ type2val t
+  Ok t -> case lookupAbsDef gr m f of -- TODO: Don't lookup twice
+            Ok (n, Just eqs) -> return (type2val t, eqs)
+            _ -> return (type2val t, [])
   Bad s -> case lookupCatContext gr m f of
-    Ok cont -> return $ cont2val cont
+    Ok cont -> return (cont2val cont,[]) 
     _ -> Bad s
 
 checkContext :: SourceGrammar -> Context -> [Message]
@@ -74,7 +77,11 @@ checkTyp gr typ = err (\x -> [pp x]) ppConstrs $ justTypeCheck gr typ vType
 
 checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message]
 checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do
+  traceM . render $ "\nchecking def: " <+> pp fun <+> ":" <+> pp typ
+                   $$ "with equation:" <+> pp fun <+> hsep [ppPatt Unqualified 2 p | p <- fst eq] <+> "=>" <+> snd eq
   (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ)
+  traceM . render $ "\ngot branches" {- <+> pp (show $ snd b) -} <+> ": with :" <+> pp (vcat $ fst b)
+        $$ "with constraints:" <+> vcat [ppValue Unqualified 0 a <+> " = " <+> ppValue Unqualified 0 b | (a,b) <- cs]
   (constrs,_) <- unifyVal cs
   return $ filter notJustMeta constrs
 
diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index c0df83394d..a953f128ea 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -30,6 +30,7 @@ import Control.Monad
 --import Data.List (sortBy)
 import Data.Maybe
 import GF.Text.Pretty
+import Debug.Trace (traceM)
 
 data AExp =
      AVr   Ident Val
@@ -54,9 +55,9 @@ data AExp =
 type ALabelling = (Label, AExp)
 type AAssign = (Label, (Val, AExp))
 
-type Theory = QIdent -> Err Val
+type Theory = QIdent -> Err (Val, [Equation])
 
-lookupConst :: Theory -> QIdent -> Err Val
+lookupConst :: Theory -> QIdent -> Err (Val, [Equation])
 lookupConst th f = th f
 
 lookupVar :: Env -> Ident -> Err Val
@@ -68,20 +69,36 @@ type TCEnv = (Int,Env,Env)
 --emptyTCEnv :: TCEnv
 --emptyTCEnv = (0,[],[])
 
-whnf :: Val -> Err Val
-whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
+whnf :: Theory -> Val -> Err Val
+whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
          case v of
   VApp u w -> do
-    u' <- whnf u
-    w' <- whnf w
-    app u' w'
-  VClos env e -> eval env e
-  _ -> return v
+    u' <- whnf th u
+    w' <- whnf th w
+    v' <- app u' w'
+    traceM . render $ "\nwhnf: Normalized app" <+> vcat 
+      ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' 
+      , ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w' 
+      , ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' 
+      ]
+    return v
+  VClos env e -> do
+    e' <- eval env e
+    traceM . render $ "\nwhnf: Normalized Closure" <+> vcat 
+      ["" <+> ppTerm Unqualified 0 e <+> "to" <+> ppValue Unqualified 0 e' ]
+    return e'
+  _ -> do
+    traceM . render $ "\nwhnf: unchanged" <+> ppValue Unqualified 0 v
+    return v
 
 app :: Val -> Val -> Err Val
 app u v = case u of
   VClos env (Abs _ x e) -> eval ((x,v):env) e
-  _ -> return $ VApp u v
+  _ -> do
+    traceM . render $ "\napp: Unchanged app:" <+> 
+      (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
+       $$ take 100 (show u))
+    return $ VApp u v
 
 eval :: Env -> Term -> Err Val
 eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
@@ -95,20 +112,20 @@ eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
                    return (VRecType xs)
   _ -> return $ VClos env e
 
-eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
-eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
+eqVal :: Theory -> Int -> Val -> Val -> Err [(Val,Val)]
+eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
                 do
-  w1 <- whnf u1
-  w2 <- whnf u2
+  w1 <- whnf th u1
+  w2 <- whnf th u2
   let v = VGen k
   case (w1,w2) of
-    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
+    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (eqVal th k a1 a2)
     (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
-      eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
+      eqVal th (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
     (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
       liftM2 (++)
-        (eqVal k     (VClos            env1  a1) (VClos            env2  a2))
-        (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
+        (eqVal th k     (VClos            env1  a1) (VClos            env2  a2))
+        (eqVal th (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
     (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
     (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
     --- thus ignore qualifications; valid because inheritance cannot
@@ -121,14 +138,16 @@ checkType th tenv e = checkExp th tenv e vType
 
 checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkExp th tenv@(k,rho,gamma) e ty = do
-  typ <- whnf ty
+  typ <- whnf th ty
+  traceM . render $ "\ncheckExp: Normalized" <+> vcat ["" <+> ppValue Unqualified 0 ty , ppValue Unqualified 0 typ]
   let v = VGen k
+  traceM . render $ "\ncheckExp: checking" <+> vcat ["" <+> e , pp (take 30 $ show e)]
   case e of
     Meta m -> return $ (AMeta m typ,[])
 
     Abs _ x t -> case typ of
       VClos env (Prod _ y a b) -> do
-                           a' <- whnf $ VClos env a ---
+                           a' <- whnf th $ VClos env a ---
                            (t',cs) <- checkExp th
                                           (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
                            return (AAbs x a' t', cs)
@@ -164,7 +183,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
     P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)])
                 return (AP r' l typ,cs)
 
-    Glue x y -> do cs1 <- eqVal k valAbsFloat typ
+    Glue x y -> do cs1 <- eqVal th k valAbsFloat typ
                    (x,cs2) <- checkExp th tenv x typ
                    (y,cs3) <- checkExp th tenv y typ
                    return (AGlue x y,cs1++cs2++cs3)
@@ -173,7 +192,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
 checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkInferExp th tenv@(k,_,_) e typ = do
   (e',w,cs1) <- inferExp th tenv e
-  cs2 <- eqVal k w typ
+  cs2 <- eqVal th k w typ
   return (e',cs1 ++ cs2)
 
 inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)])
@@ -181,8 +200,8 @@ inferExp th tenv@(k,rho,gamma) e = case e of
    Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
    Q (m,c) | m == cPredefAbs && isPredefCat c
                      -> return (ACn (m,c) vType, vType, [])
-           | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
-   QC c -> mkAnnot (ACn c) $ noConstr $ lookupConst th c ----
+           | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ fmap fst $ lookupConst th (m,c)
+   QC c -> mkAnnot (ACn c) $ noConstr $ fmap fst $ lookupConst th c ----
    EInt i -> return (AInt i, valAbsInt, [])
    EFloat i -> return (AFloat i, valAbsFloat, [])
    K i -> return (AStr i, valAbsString, [])
@@ -202,11 +221,11 @@ inferExp th tenv@(k,rho,gamma) e = case e of
     return (ALet (x,(val1,e1)) e2, val2, cs1++cs2)
    App f t -> do
     (f',w,csf) <- inferExp th tenv f
-    typ <- whnf w
+    typ <- whnf th w
     case typ of
       VClos env (Prod _ x a b) -> do
         (a',csa) <- checkExp th tenv t (VClos env a)
-        b' <- whnf $ VClos ((x,VClos rho t):env) b
+        b' <- whnf th $ VClos ((x,VClos rho t):env) b
         return $ (AApp f' a' b', b', csf ++ csa)
       _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
    _ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e))
@@ -222,7 +241,7 @@ checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
   val <- eval rho typ
   cs2 <- case lookup lbl typs of
            Nothing   -> return []
-           Just val0 -> eqVal k val val0
+           Just val0 -> eqVal th k val val0
   (aexp,cs3) <- checkExp th tenv exp val
   return ((lbl,(val,aexp)),cs1++cs2++cs3)
 checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
@@ -243,10 +262,11 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
 
   chB tenv@(k,rho,gamma) ps ty = case ps of
     p:ps2 -> do
-      typ <- whnf ty
+      typ <- whnf th ty
+      traceM . render $ "\ncheckBranch: Normalized " <+> vcat [ppValue Unqualified 0 ty , ppValue Unqualified 0 typ]
       case typ of
         VClos env (Prod _ y a b) -> do
-          a' <- whnf $ VClos env a
+          a' <- whnf th $ VClos env a
           (p', sigma, binds, cs1) <- checkP tenv p y a'
           let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
           ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
@@ -297,18 +317,18 @@ checkPatt th tenv exp val = do
      K s    -> return (AStr s, valAbsString, [])
 
      Q c  -> do
-       typ <- lookupConst th c
+       (typ, _eqn) <- lookupConst th c
        return $ (ACn c typ, typ, [])
      QC c  -> do
-       typ <- lookupConst th c
+       (typ, _eqn) <- lookupConst th c
        return $ (ACn c typ, typ, []) ----
      App f t -> do
        (f',w,csf) <- checkExpP tenv f val
-       typ <- whnf w
+       typ <- whnf th w
        case typ of
          VClos env (Prod _ x a b) -> do
            (a',_,csa) <- checkExpP tenv t (VClos env a)
-           b' <- whnf $ VClos ((x,VClos rho t):env) b
+           b' <- whnf th $ VClos ((x,VClos rho t):env) b
            return $ (AApp f' a' b', b', csf ++ csa)
          _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
      _ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp))
diff --git a/src/compiler/GF/Compile/Update.hs b/src/compiler/GF/Compile/Update.hs
index 7bbe1d8dc2..836d9652f3 100644
--- a/src/compiler/GF/Compile/Update.hs
+++ b/src/compiler/GF/Compile/Update.hs
@@ -38,10 +38,11 @@ buildAnyTree m = go Map.empty
       case Map.lookup c map of
         Just i  -> case unifyAnyInfo m i j of
           Ok k  -> go (Map.insert c k map) is
-          Bad _ -> fail $ render ("conflicting information in module"<+>m $$
+          Bad msg -> fail $ render ("conflicting information in module"<+>m $$
                                   nest 4 (ppJudgement Qualified (c,i)) $$
                                   "and" $+$
-                                  nest 4 (ppJudgement Qualified (c,j)))
+                                  nest 4 (ppJudgement Qualified (c,j)) $+$
+                                  msg)
         Nothing -> go (Map.insert c j map) is
 
 extendModule :: FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
@@ -203,7 +204,7 @@ unifyAnyInfo m i j = case (i,j) of
     liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
   (ResValue (L l1 t1), ResValue (L l2 t2))
       | t1==t2    -> return (ResValue (L l1 t1))
-      | otherwise -> fail ""
+      | otherwise -> fail "non-matching ResValue"
   (_, ResOverload ms t) | elem m ms ->
     return $ ResOverload ms t
   (ResOper mt1 m1, ResOper mt2 m2) ->
@@ -222,7 +223,7 @@ unifyAnyInfo m i j = case (i,j) of
   _ -> fail "informations"
 
 -- | this is what happens when matching two values in the same module
-unifyMaybeL :: Eq a => Maybe (L a) -> Maybe (L a) -> Err (Maybe (L a))
+unifyMaybeL :: (Eq a, Show a) => Maybe (L a) -> Maybe (L a) -> Err (Maybe (L a))
 unifyMaybeL = unifyMaybeBy unLoc
 
 unifAbsArrity :: Maybe Int -> Maybe Int -> Err (Maybe Int)
@@ -230,5 +231,12 @@ unifAbsArrity = unifyMaybe
 
 unifAbsDefs :: Maybe [L Equation] -> Maybe [L Equation] -> Err (Maybe [L Equation])
 unifAbsDefs (Just xs) (Just ys) = return (Just (xs ++ ys))
+-- unifAbsDefs Nothing ys          = return ys
+-- unifAbsDefs xs Nothing          = return xs
 unifAbsDefs Nothing   Nothing   = return Nothing
-unifAbsDefs _         _         = fail ""
+unifAbsDefs Nothing   (Just ys) = fail $ "Can't unify Nothing with def " ++ render (pp ys)
+unifAbsDefs xs        Nothing   = fail $ "Can't unify def " ++ show xs ++ " with Nothing"
+-- Cannot use def with data. Hint: replace data with fun for $name
+
+instance (Pretty a, Pretty b) => Pretty (a,b) where
+  pp (a,b) = "(" <+> pp a <+> ", " <+> pp b <+> ")"

From 5df3fb9d8a2c01b9fc88cd69486db7b6953b80f3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 17:34:46 +0200
Subject: [PATCH 04/24] Make VApp take a list of args

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 27 +++++++++++++++----------
 src/compiler/GF/Grammar/Printer.hs      |  2 +-
 src/compiler/GF/Grammar/Unify.hs        |  2 +-
 src/compiler/GF/Grammar/Values.hs       |  2 +-
 4 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index a953f128ea..a48bee6702 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -74,17 +74,16 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
          case v of
   VApp u w -> do
     u' <- whnf th u
-    w' <- whnf th w
-    v' <- app u' w'
-    traceM . render $ "\nwhnf: Normalized app" <+> vcat 
-      ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' 
-      , ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w' 
-      , ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' 
-      ]
+    w' <- mapM (whnf th) w
+    v' <- foldM app u' w'
+    traceM . render $ "\nwhnf: Normalized app" <+> vcat (
+      ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
+      zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
+      [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
     return v
   VClos env e -> do
     e' <- eval env e
-    traceM . render $ "\nwhnf: Normalized Closure" <+> vcat 
+    traceM . render $ "\nwhnf: Normalized Closure" <+> vcat
       ["" <+> ppTerm Unqualified 0 e <+> "to" <+> ppValue Unqualified 0 e' ]
     return e'
   _ -> do
@@ -94,11 +93,17 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
 app :: Val -> Val -> Err Val
 app u v = case u of
   VClos env (Abs _ x e) -> eval ((x,v):env) e
+  VApp u' v' -> do
+    let val = VApp u' (v' ++ [v])
+    traceM . render $ "\napp: Extended app:" <+>
+      (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
+       $$ take 150 (show val))
+    return val
   _ -> do
-    traceM . render $ "\napp: Unchanged app:" <+> 
+    traceM . render $ "\napp: Unchanged app:" <+>
       (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
        $$ take 100 (show u))
-    return $ VApp u v
+    return $ VApp u [v]
 
 eval :: Env -> Term -> Err Val
 eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
@@ -119,7 +124,7 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
   w2 <- whnf th u2
   let v = VGen k
   case (w1,w2) of
-    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (eqVal th k a1 a2)
+    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (fmap concat $ zipWithM (eqVal th k) a1 a2)
     (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
       eqVal th (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
     (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs
index 74fd511b78..e113de182e 100644
--- a/src/compiler/GF/Grammar/Printer.hs
+++ b/src/compiler/GF/Grammar/Printer.hs
@@ -276,7 +276,7 @@ ppPatt q d (PTilde t)   = prec d 2 ('~' <> ppTerm q 6 t)
 
 ppValue :: TermPrintQual -> Int -> Val -> Doc
 ppValue q d (VGen i x)    = x <> "{-" <> i <> "-}" ---- latter part for debugging
-ppValue q d (VApp u v)    = prec d 4 (ppValue q 4 u <+> ppValue q 5 v)
+ppValue q d (VApp u v)    = prec d 4 (ppValue q 4 u <+> hsep (ppValue q 5 <$> v))
 ppValue q d (VCn (_,c))   = pp c
 ppValue q d (VClos env e) = case e of
                               Meta _ -> ppTerm q d e <> ppEnv env
diff --git a/src/compiler/GF/Grammar/Unify.hs b/src/compiler/GF/Grammar/Unify.hs
index 3a7f0edef4..9585524131 100644
--- a/src/compiler/GF/Grammar/Unify.hs
+++ b/src/compiler/GF/Grammar/Unify.hs
@@ -108,7 +108,7 @@ occCheck s u = case u of
 val2term :: Val -> Term
 val2term v = case v of
   VClos g e   -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e
-  VApp f c    -> App (val2term f) (val2term c)
+  VApp f cs   -> foldl App (val2term f) (map val2term cs)
   VCn c       -> Q c
   VGen i x    -> Vr x
   VRecType xs -> RecType (map (\(l,v) -> (l,val2term v)) xs)
diff --git a/src/compiler/GF/Grammar/Values.hs b/src/compiler/GF/Grammar/Values.hs
index c8fcb3945f..3658329134 100644
--- a/src/compiler/GF/Grammar/Values.hs
+++ b/src/compiler/GF/Grammar/Values.hs
@@ -29,7 +29,7 @@ import GF.Grammar.Predef
 
 -- values used in TC type checking
 
-data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term
+data Val = VGen Int Ident | VApp Val [Val] | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term
   deriving (Eq,Show)
 
 type Env = [(Ident,Val)]

From 0b2011c725051876496cb6c12369af8935d8b0eb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 18:01:16 +0200
Subject: [PATCH 05/24] Add unused unifyMaybeWith

---
 src/compiler/GF/Data/Operations.hs | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/compiler/GF/Data/Operations.hs b/src/compiler/GF/Data/Operations.hs
index e9b95f8abb..05ca6e9f6b 100644
--- a/src/compiler/GF/Data/Operations.hs
+++ b/src/compiler/GF/Data/Operations.hs
@@ -24,7 +24,7 @@ module GF.Data.Operations (
                  liftErr,
 
      -- ** Checking
-     checkUnique, unifyMaybeBy, unifyMaybe,
+     checkUnique, unifyMaybeBy, unifyMaybe, unifyMaybeWith,
 
          -- ** Monadic operations on lists and pairs
      mapPairsM, pairM,
@@ -89,16 +89,21 @@ checkUnique ss = ["overloaded" +++ show s | s <- nub overloads] where
   overloaded s = length (filter (==s) ss) > 1
 
 -- | this is what happens when matching two values in the same module
-unifyMaybe :: (Eq a, Fail.MonadFail m) => Maybe a -> Maybe a -> m (Maybe a)
+unifyMaybe :: (Eq a, Fail.MonadFail m, Show a) => Maybe a -> Maybe a -> m (Maybe a)
 unifyMaybe = unifyMaybeBy id
 
-unifyMaybeBy :: (Eq b, Fail.MonadFail m) => (a->b) -> Maybe a -> Maybe a -> m (Maybe a)
+unifyMaybeBy :: (Eq b, Fail.MonadFail m, Show a) => (a->b) -> Maybe a -> Maybe a -> m (Maybe a)
 unifyMaybeBy f (Just p1) (Just p2)
   | f p1==f p2                     = return (Just p1)
-  | otherwise                      = fail ""
+  | otherwise                      = fail $ "non-matching values: " ++ show p1 ++ " and " ++ show p2
 unifyMaybeBy _ Nothing   mp2       = return mp2
 unifyMaybeBy _ mp1       _         = return mp1
 
+unifyMaybeWith :: Applicative m => (a -> a -> m a) -> Maybe a -> Maybe a -> m (Maybe a)
+unifyMaybeWith f (Just p1) (Just p2) = Just <$> f p1 p2
+unifyMaybeWith _ Nothing   mp2       = pure mp2
+unifyMaybeWith _ mp1       _         = pure mp1
+
 -- printing
 
 indent :: Int -> String -> String

From 50686387e26a06d9959628386e424c55209f5f5a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 18:02:15 +0200
Subject: [PATCH 06/24] Add def-equations to VCn

---
 src/compiler/GF/Compile/TypeCheck/Abstract.hs |  6 +++---
 src/compiler/GF/Compile/TypeCheck/TC.hs       | 10 +++++-----
 src/compiler/GF/Grammar/Printer.hs            |  2 +-
 src/compiler/GF/Grammar/Unify.hs              |  2 +-
 src/compiler/GF/Grammar/Values.hs             |  8 ++++----
 5 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index 083e7373ad..c10e6eab08 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -63,10 +63,10 @@ notJustMeta (c,k) = case (c,k) of
 grammar2theory :: SourceGrammar -> Theory
 grammar2theory gr (m,f) = case lookupFunType gr m f of
   Ok t -> case lookupAbsDef gr m f of -- TODO: Don't lookup twice
-            Ok (n, Just eqs) -> return (type2val t, eqs)
-            _ -> return (type2val t, [])
+            Ok (Just n, Just eqs) -> return (type2val t, Just (n, eqs))
+            _ -> return (type2val t, Nothing)
   Bad s -> case lookupCatContext gr m f of
-    Ok cont -> return (cont2val cont,[]) 
+    Ok cont -> return (cont2val cont,Nothing) 
     _ -> Bad s
 
 checkContext :: SourceGrammar -> Context -> [Message]
diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index a48bee6702..dc22e5bbdc 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -55,9 +55,9 @@ data AExp =
 type ALabelling = (Label, AExp)
 type AAssign = (Label, (Val, AExp))
 
-type Theory = QIdent -> Err (Val, [Equation])
+type Theory = QIdent -> Err (Val, Maybe (Int, [Equation]))
 
-lookupConst :: Theory -> QIdent -> Err (Val, [Equation])
+lookupConst :: Theory -> QIdent -> Err (Val, Maybe (Int, [Equation]))
 lookupConst th f = th f
 
 lookupVar :: Env -> Ident -> Err Val
@@ -109,8 +109,8 @@ eval :: Env -> Term -> Err Val
 eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
              case e of
   Vr x    -> lookupVar env x
-  Q c   -> return $ VCn c
-  QC c  -> return $ VCn c ---- == Q ?
+  Q c   -> return $ VCn c Nothing -- TODO
+  QC c  -> return $ VCn c Nothing ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
   App f a -> join $ liftM2 app (eval env f) (eval env a)
   RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
@@ -132,7 +132,7 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
         (eqVal th k     (VClos            env1  a1) (VClos            env2  a2))
         (eqVal th (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
     (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
-    (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
+    (VCn (_, i) _, VCn (_,j) _) -> return [(w1,w2) | i /= j]
     --- thus ignore qualifications; valid because inheritance cannot
     --- be qualified. Simplifies annotation. AR 17/3/2005
     _ -> return [(w1,w2) | w1 /= w2]
diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs
index e113de182e..4ce8c4fa4f 100644
--- a/src/compiler/GF/Grammar/Printer.hs
+++ b/src/compiler/GF/Grammar/Printer.hs
@@ -277,7 +277,7 @@ ppPatt q d (PTilde t)   = prec d 2 ('~' <> ppTerm q 6 t)
 ppValue :: TermPrintQual -> Int -> Val -> Doc
 ppValue q d (VGen i x)    = x <> "{-" <> i <> "-}" ---- latter part for debugging
 ppValue q d (VApp u v)    = prec d 4 (ppValue q 4 u <+> hsep (ppValue q 5 <$> v))
-ppValue q d (VCn (_,c))   = pp c
+ppValue q d (VCn (_,c) _)   = pp c
 ppValue q d (VClos env e) = case e of
                               Meta _ -> ppTerm q d e <> ppEnv env
                               _      -> ppTerm q d e ---- ++ prEnv env ---- for debugging
diff --git a/src/compiler/GF/Grammar/Unify.hs b/src/compiler/GF/Grammar/Unify.hs
index 9585524131..b17e84de67 100644
--- a/src/compiler/GF/Grammar/Unify.hs
+++ b/src/compiler/GF/Grammar/Unify.hs
@@ -109,7 +109,7 @@ val2term :: Val -> Term
 val2term v = case v of
   VClos g e   -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e
   VApp f cs   -> foldl App (val2term f) (map val2term cs)
-  VCn c       -> Q c
+  VCn c _     -> Q c
   VGen i x    -> Vr x
   VRecType xs -> RecType (map (\(l,v) -> (l,val2term v)) xs)
   VType       -> typeType
diff --git a/src/compiler/GF/Grammar/Values.hs b/src/compiler/GF/Grammar/Values.hs
index 3658329134..3fb88b9185 100644
--- a/src/compiler/GF/Grammar/Values.hs
+++ b/src/compiler/GF/Grammar/Values.hs
@@ -29,7 +29,7 @@ import GF.Grammar.Predef
 
 -- values used in TC type checking
 
-data Val = VGen Int Ident | VApp Val [Val] | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term
+data Val = VGen Int Ident | VApp Val [Val] | VCn QIdent (Maybe (Int, [Equation])) | VRecType [(Label,Val)] | VType | VClos Env Term
   deriving (Eq,Show)
 
 type Env = [(Ident,Val)]
@@ -42,13 +42,13 @@ type MetaSubst = [(MetaId,Val)]
 -- for TC
 
 valAbsInt :: Val
-valAbsInt = VCn (cPredefAbs, cInt)
+valAbsInt = VCn (cPredefAbs, cInt) Nothing
 
 valAbsFloat :: Val
-valAbsFloat = VCn (cPredefAbs, cFloat)
+valAbsFloat = VCn (cPredefAbs, cFloat) Nothing
 
 valAbsString :: Val
-valAbsString = VCn (cPredefAbs, cString)
+valAbsString = VCn (cPredefAbs, cString) Nothing
 
 vType :: Val
 vType = VType

From 59f5f62390f467cc60e316eb77d8ba9f733fd5a4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 18:04:23 +0200
Subject: [PATCH 07/24] Add theory to eval

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index dc22e5bbdc..e16284b9d4 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -75,14 +75,14 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
   VApp u w -> do
     u' <- whnf th u
     w' <- mapM (whnf th) w
-    v' <- foldM app u' w'
+    v' <- foldM (app th) u' w'
     traceM . render $ "\nwhnf: Normalized app" <+> vcat (
       ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
       zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
       [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
     return v
   VClos env e -> do
-    e' <- eval env e
+    e' <- eval th env e
     traceM . render $ "\nwhnf: Normalized Closure" <+> vcat
       ["" <+> ppTerm Unqualified 0 e <+> "to" <+> ppValue Unqualified 0 e' ]
     return e'
@@ -90,9 +90,9 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
     traceM . render $ "\nwhnf: unchanged" <+> ppValue Unqualified 0 v
     return v
 
-app :: Val -> Val -> Err Val
-app u v = case u of
-  VClos env (Abs _ x e) -> eval ((x,v):env) e
+app :: Theory -> Val -> Val -> Err Val
+app th u v = case u of
+  VClos env (Abs _ x e) -> eval th ((x,v):env) e
   VApp u' v' -> do
     let val = VApp u' (v' ++ [v])
     traceM . render $ "\napp: Extended app:" <+>
@@ -105,15 +105,15 @@ app u v = case u of
        $$ take 100 (show u))
     return $ VApp u [v]
 
-eval :: Env -> Term -> Err Val
-eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
+eval :: Theory -> Env -> Term -> Err Val
+eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
              case e of
   Vr x    -> lookupVar env x
   Q c   -> return $ VCn c Nothing -- TODO
   QC c  -> return $ VCn c Nothing ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
-  App f a -> join $ liftM2 app (eval env f) (eval env a)
-  RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
+  App f a -> join $ liftM2 (app th) (eval th env f) (eval th env a)
+  RecType xs -> do xs <- mapM (\(l,e) -> eval th env e >>= \e -> return (l,e)) xs
                    return (VRecType xs)
   _ -> return $ VClos env e
 
@@ -161,7 +161,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
     Let (x, (mb_typ, e1)) e2 -> do
       (val,e1,cs1) <- case mb_typ of
                         Just typ -> do (_,cs1) <- checkType th tenv typ
-                                       val <- eval rho typ
+                                       val <- eval th rho typ
                                        (e1,cs2) <- checkExp th tenv e1 val
                                        return (val,e1,cs1++cs2)
                         Nothing  -> do (e1,val,cs) <- inferExp th tenv e1
@@ -217,7 +217,7 @@ inferExp th tenv@(k,rho,gamma) e = case e of
    Let (x, (mb_typ, e1)) e2 -> do
     (val1,e1,cs1) <- case mb_typ of
                        Just typ -> do (_,cs1) <- checkType th tenv typ
-                                      val <- eval rho typ
+                                      val <- eval th rho typ
                                       (e1,cs2) <- checkExp th tenv e1 val
                                       return (val,e1,cs1++cs2)
                        Nothing  -> do (e1,val,cs) <- inferExp th tenv e1
@@ -243,7 +243,7 @@ checkLabelling th tenv (lbl,typ) = do
 checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
 checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
   (atyp,cs1) <- checkType th tenv typ
-  val <- eval rho typ
+  val <- eval th rho typ
   cs2 <- case lookup lbl typs of
            Nothing   -> return []
            Just val0 -> eqVal th k val val0

From 8460a5464497bdef49030cb652d1026c12bca16c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 18:09:11 +0200
Subject: [PATCH 08/24] Add defEqns to VCn in eval

Makes it availale for evaluating an VApp
---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index e16284b9d4..f46efb0252 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -109,8 +109,12 @@ eval :: Theory -> Env -> Term -> Err Val
 eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
              case e of
   Vr x    -> lookupVar env x
-  Q c   -> return $ VCn c Nothing -- TODO
-  QC c  -> return $ VCn c Nothing ---- == Q ?
+  Q c   -> do
+    (_ty, defEqns) <- lookupConst th c
+    return $ VCn c defEqns
+  QC c  -> do
+    (_ty, defEqns) <- lookupConst th c
+    return $ VCn c defEqns ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
   App f a -> join $ liftM2 (app th) (eval th env f) (eval th env a)
   RecType xs -> do xs <- mapM (\(l,e) -> eval th env e >>= \e -> return (l,e)) xs

From cf7d10e15908147b0a4f015ccded3f73138fbb3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Fri, 29 Sep 2023 22:35:59 +0200
Subject: [PATCH 09/24] Add code for pattern matching def equations

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 50 ++++++++++++++++++++++++-
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index f46efb0252..1e227a7980 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -92,19 +92,65 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
 
 app :: Theory -> Val -> Val -> Err Val
 app th u v = case u of
-  VClos env (Abs _ x e) -> eval th ((x,v):env) e
+  VClos env (Abs _ x e) -> do 
+    traceM "app: VClos"
+    evalDef th =<< eval th ((x,v):env) e
   VApp u' v' -> do
     let val = VApp u' (v' ++ [v])
     traceM . render $ "\napp: Extended app:" <+>
       (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
        $$ take 150 (show val))
-    return val
+    evalDef th val
   _ -> do
     traceM . render $ "\napp: Unchanged app:" <+>
       (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
        $$ take 100 (show u))
     return $ VApp u [v]
 
+evalDef :: Theory -> Val -> Err Val
+evalDef th e = case e of
+  VApp (VCn c (Just (n, eqs))) xs | length xs == n -> do
+    traceM . render $ ("\nevalDef:" <+>) $ "Found def:" <+> snd c
+            $$ "with equations:" <+> vcat
+              [ snd c <+> hsep [ppPatt Unqualified 2 p | p <- pat] <+> "=>" <+> val
+              | (pat, val) <- eqs
+              ]
+            $$ ("applied to:" <+> (ppValue Unqualified 0 e))
+            $$ "raw equations:" <+> vcat
+              [ snd c <+> hsep [showsPrec 11 p "" | p <- pat] <+> "=>" <+> val | (pat, val) <- eqs ]
+            $$ ("applied to:" <+> (show (VApp (VCn c Nothing) xs)))
+    e' <- tryMatchEqns eqs xs
+    traceM . render $ ("\nevalDef:" <+>) $ "Evaluated:" <+> show e'
+    case e' of
+      Just (VClos env tm) -> eval th env tm
+      _ -> return e
+  _ -> return e
+
+tryMatchEqns :: [Equation] -> [Val] -> Err (Maybe Val)
+tryMatchEqns ((pts,repl):eqs) xs = do
+  me' <- tryMatchEqn [] pts xs repl
+  case me' of
+    Nothing -> tryMatchEqns eqs xs
+    Just e' -> return $ Just e'
+tryMatchEqns [] xs = return Nothing
+
+tryMatchEqn :: Env -> [Patt] -> [Val] -> Term -> Err (Maybe Val)
+tryMatchEqn env [] [] repl = return $ Just $ VClos env repl -- TODO: eval?
+tryMatchEqn env (PW: ps) (v: vs) repl = do
+  traceM . render $ "Matching wildcard" <+> ppValue Unqualified 0 v
+  tryMatchEqn env ps vs repl
+tryMatchEqn env (PV c: ps) (v: vs) repl = do
+  traceM . render $ "Matching variable" <+> c <+> ":" <+> ppValue Unqualified 0 v
+  tryMatchEqn ((c,v):env) ps vs repl -- TODO: Is this sound?
+tryMatchEqn env (PP (q,p) pp: ps) (VApp (VCn (r,f) _) tt: vs) repl 
+  | p == f && length pp == length tt = tryMatchEqn env (pp ++ ps) (tt ++ vs) repl
+-- tryMatchEqn env (p: ps) (v: vs) repl = _
+tryMatchEqn env (a:_) (b:_) _ = do
+  traceM . render $ ("\ntryMatchEqn:" <+>) $ "Failed to match" <+> a <+> "with" <+> ppValue Unqualified 0 b
+    $$ "raw:" <+> (show a $$ show b) 
+  return Nothing
+tryMatchEqn env _ _ _ = Bad "tryMatchEqn: Non-matching length"
+
 eval :: Theory -> Env -> Term -> Err Val
 eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
              case e of

From 6351724e1ada487c43c6e05e9bd3317e69ad6fdc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 09:09:38 +0200
Subject: [PATCH 10/24] Add more debug tracing

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 1e227a7980..7f48d81351 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -75,6 +75,9 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
   VApp u w -> do
     u' <- whnf th u
     w' <- mapM (whnf th) w
+    traceM . render $ "\nwhnf: Normalized app 2" <+> vcat (
+      ("" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ) :
+      zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w')
     v' <- foldM (app th) u' w'
     traceM . render $ "\nwhnf: Normalized app" <+> vcat (
       ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
@@ -94,17 +97,19 @@ app :: Theory -> Val -> Val -> Err Val
 app th u v = case u of
   VClos env (Abs _ x e) -> do 
     traceM "app: VClos"
-    evalDef th =<< eval th ((x,v):env) e
+    val <- eval th ((x,v):env) e
+    traceM "app: VClos 2"
+    evalDef th val
   VApp u' v' -> do
     let val = VApp u' (v' ++ [v])
     traceM . render $ "\napp: Extended app:" <+>
       (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
-       $$ take 150 (show val))
+       $$ take 300 (show val))
     evalDef th val
   _ -> do
     traceM . render $ "\napp: Unchanged app:" <+>
       (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
-       $$ take 100 (show u))
+       $$ take 300 (show u))
     return $ VApp u [v]
 
 evalDef :: Theory -> Val -> Err Val
@@ -124,7 +129,9 @@ evalDef th e = case e of
     case e' of
       Just (VClos env tm) -> eval th env tm
       _ -> return e
-  _ -> return e
+  _ -> do
+    traceM "evalDef: not yet"
+    return e
 
 tryMatchEqns :: [Equation] -> [Val] -> Err (Maybe Val)
 tryMatchEqns ((pts,repl):eqs) xs = do
@@ -162,10 +169,14 @@ eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
     (_ty, defEqns) <- lookupConst th c
     return $ VCn c defEqns ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
-  App f a -> join $ liftM2 (app th) (eval th env f) (eval th env a)
+  App f a -> do 
+    traceM "eval: App"
+    join $ liftM2 (app th) (eval th env f) (eval th env a)
   RecType xs -> do xs <- mapM (\(l,e) -> eval th env e >>= \e -> return (l,e)) xs
                    return (VRecType xs)
-  _ -> return $ VClos env e
+  _ -> do
+    traceM . render . ("eval:" <+>) $ "not evaling: " <+> show e --  $$ "in context" <+> env
+    return $ VClos env e
 
 eqVal :: Theory -> Int -> Val -> Val -> Err [(Val,Val)]
 eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $

From c6661a07358dffb99eae146872d76713315f1792 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 09:28:02 +0200
Subject: [PATCH 11/24] Fix typo

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 7f48d81351..d62580592f 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -83,7 +83,7 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
       ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
       zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
       [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
-    return v
+    return v'
   VClos env e -> do
     e' <- eval th env e
     traceM . render $ "\nwhnf: Normalized Closure" <+> vcat

From 8c7eee8b04c39560d3d160e33143c1e1788fe2c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 09:54:44 +0200
Subject: [PATCH 12/24] More compact Show for identifiers

---
 src/compiler/GF/Infra/Ident.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/compiler/GF/Infra/Ident.hs b/src/compiler/GF/Infra/Ident.hs
index ad47d91cdc..143503d8d3 100644
--- a/src/compiler/GF/Infra/Ident.hs
+++ b/src/compiler/GF/Infra/Ident.hs
@@ -61,7 +61,10 @@ data Ident =
 -- (It is also possible to use regular Haskell 'String's, with somewhat
 -- reduced performance and increased memory use.)
 newtype RawIdent = Id { rawId2utf8 :: UTF8.ByteString }
-  deriving (Eq, Ord, Show, Read)
+  deriving (Eq, Ord, Read)
+
+instance Show RawIdent where
+  showsPrec d (Id s) = showParen (d >= 11) $ showString "Id " . showsPrec 11 s 
 
 pack = UTF8.fromString
 unpack = UTF8.toString

From 94850213c0f782e1c16db940baad86b3f2f69bb8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 10:54:47 +0200
Subject: [PATCH 13/24] Add new type for unevaluated closures

Note: This removes some whnf calls. It might be a regression
---
 src/compiler/GF/Compile/TypeCheck/Abstract.hs |   5 +-
 src/compiler/GF/Compile/TypeCheck/TC.hs       | 105 ++++++++++--------
 src/compiler/GF/Grammar/Printer.hs            |   4 +
 src/compiler/GF/Grammar/Values.hs             |   5 +-
 4 files changed, 72 insertions(+), 47 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index c10e6eab08..39b2373517 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -42,6 +42,9 @@ initTCEnv gamma =
 type2val :: Type -> Val
 type2val = VClos []
 
+type2nval :: Type -> NotVal
+type2nval = NVClos []
+
 cont2exp :: Context -> Term
 cont2exp c = mkProd c eType [] -- to check a context
 
@@ -79,7 +82,7 @@ checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message]
 checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do
   traceM . render $ "\nchecking def: " <+> pp fun <+> ":" <+> pp typ
                    $$ "with equation:" <+> pp fun <+> hsep [ppPatt Unqualified 2 p | p <- fst eq] <+> "=>" <+> snd eq
-  (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ)
+  (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2nval typ)
   traceM . render $ "\ngot branches" {- <+> pp (show $ snd b) -} <+> ": with :" <+> pp (vcat $ fst b)
         $$ "with constraints:" <+> vcat [ppValue Unqualified 0 a <+> " = " <+> ppValue Unqualified 0 b | (a,b) <- cs]
   (constrs,_) <- unifyVal cs
diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index d62580592f..ccf23eae2f 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -16,6 +16,7 @@ module GF.Compile.TypeCheck.TC (
     AExp(..),
     Theory,
     checkExp,
+    checkNExp,
     inferExp,
     checkBranch,
     eqVal,
@@ -69,29 +70,29 @@ type TCEnv = (Int,Env,Env)
 --emptyTCEnv :: TCEnv
 --emptyTCEnv = (0,[],[])
 
-whnf :: Theory -> Val -> Err Val
+whnf :: Theory -> NotVal -> Err Val
 whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
          case v of
-  VApp u w -> do
-    u' <- whnf th u
-    w' <- mapM (whnf th) w
-    traceM . render $ "\nwhnf: Normalized app 2" <+> vcat (
-      ("" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ) :
-      zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w')
-    v' <- foldM (app th) u' w'
-    traceM . render $ "\nwhnf: Normalized app" <+> vcat (
-      ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
-      zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
-      [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
-    return v'
-  VClos env e -> do
+  -- VApp u w -> do
+  --   u' <- whnf th u
+  --   w' <- mapM (whnf th) w
+  --   traceM . render $ "\nwhnf: Normalized app 2" <+> vcat (
+  --     ("" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ) :
+  --     zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w')
+  --   v' <- foldM (app th) u' w'
+  --   traceM . render $ "\nwhnf: Normalized app" <+> vcat (
+  --     ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
+  --     zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
+  --     [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
+  --   return v'
+  NVClos env e -> do
     e' <- eval th env e
     traceM . render $ "\nwhnf: Normalized Closure" <+> vcat
       ["" <+> ppTerm Unqualified 0 e <+> "to" <+> ppValue Unqualified 0 e' ]
     return e'
-  _ -> do
-    traceM . render $ "\nwhnf: unchanged" <+> ppValue Unqualified 0 v
-    return v
+  -- _ -> do
+  --   traceM . render $ "\nwhnf: unchanged" <+> ppValue Unqualified 0 v
+  --   return v
 
 app :: Theory -> Val -> Val -> Err Val
 app th u v = case u of
@@ -127,13 +128,13 @@ evalDef th e = case e of
     e' <- tryMatchEqns eqs xs
     traceM . render $ ("\nevalDef:" <+>) $ "Evaluated:" <+> show e'
     case e' of
-      Just (VClos env tm) -> eval th env tm
+      Just (NVClos env tm) -> eval th env tm
       _ -> return e
   _ -> do
     traceM "evalDef: not yet"
     return e
 
-tryMatchEqns :: [Equation] -> [Val] -> Err (Maybe Val)
+tryMatchEqns :: [Equation] -> [Val] -> Err (Maybe NotVal)
 tryMatchEqns ((pts,repl):eqs) xs = do
   me' <- tryMatchEqn [] pts xs repl
   case me' of
@@ -141,8 +142,8 @@ tryMatchEqns ((pts,repl):eqs) xs = do
     Just e' -> return $ Just e'
 tryMatchEqns [] xs = return Nothing
 
-tryMatchEqn :: Env -> [Patt] -> [Val] -> Term -> Err (Maybe Val)
-tryMatchEqn env [] [] repl = return $ Just $ VClos env repl -- TODO: eval?
+tryMatchEqn :: Env -> [Patt] -> [Val] -> Term -> Err (Maybe NotVal)
+tryMatchEqn env [] [] repl = return $ Just $ NVClos env repl
 tryMatchEqn env (PW: ps) (v: vs) repl = do
   traceM . render $ "Matching wildcard" <+> ppValue Unqualified 0 v
   tryMatchEqn env ps vs repl
@@ -178,20 +179,27 @@ eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
     traceM . render . ("eval:" <+>) $ "not evaling: " <+> show e --  $$ "in context" <+> env
     return $ VClos env e
 
+eqNVal :: Theory -> Int -> NotVal -> NotVal -> Err [(Val,Val)]
+eqNVal th k u1 u2 = do
+  w1 <- whnf th u1
+  w2 <- whnf th u2
+  eqVal th k w1 w2
+
 eqVal :: Theory -> Int -> Val -> Val -> Err [(Val,Val)]
 eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
                 do
-  w1 <- whnf th u1
-  w2 <- whnf th u2
+  -- w1 <- whnf th u1
+  -- w2 <- whnf th u2
+  let (w1,w2) = (u1,u2)
   let v = VGen k
   case (w1,w2) of
     (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (fmap concat $ zipWithM (eqVal th k) a1 a2)
     (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
-      eqVal th (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
+      eqNVal th (k+1) (NVClos ((x1,v x1):env1) e1) (NVClos ((x2,v x1):env2) e2)
     (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
       liftM2 (++)
-        (eqVal th k     (VClos            env1  a1) (VClos            env2  a2))
-        (eqVal th (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
+        (eqNVal th k     (NVClos            env1  a1) (NVClos            env2  a2))
+        (eqNVal th (k+1) (NVClos ((x1,v x1):env1) e1) (NVClos ((x2,v x1):env2) e2))
     (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
     (VCn (_, i) _, VCn (_,j) _) -> return [(w1,w2) | i /= j]
     --- thus ignore qualifications; valid because inheritance cannot
@@ -202,10 +210,13 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
 checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)])
 checkType th tenv e = checkExp th tenv e vType
 
-checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
-checkExp th tenv@(k,rho,gamma) e ty = do
+checkNExp :: Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)])
+checkNExp th tenv@(k,rho,gamma) e ty = do
   typ <- whnf th ty
-  traceM . render $ "\ncheckExp: Normalized" <+> vcat ["" <+> ppValue Unqualified 0 ty , ppValue Unqualified 0 typ]
+  traceM . render $ "\ncheckExp: Normalized" <+> vcat ["" <+> ppNValue Unqualified 0 ty , ppValue Unqualified 0 typ]
+  checkExp th tenv e typ
+checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
+checkExp th tenv@(k,rho,gamma) e typ = do
   let v = VGen k
   traceM . render $ "\ncheckExp: checking" <+> vcat ["" <+> e , pp (take 30 $ show e)]
   case e of
@@ -213,9 +224,9 @@ checkExp th tenv@(k,rho,gamma) e ty = do
 
     Abs _ x t -> case typ of
       VClos env (Prod _ y a b) -> do
-                           a' <- whnf th $ VClos env a ---
-                           (t',cs) <- checkExp th
-                                          (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
+                           a' <- whnf th $ NVClos env a ---
+                           (t',cs) <- checkNExp th
+                                          (k+1,(x,v x):rho, (x,a'):gamma) t (NVClos ((y,v x):env) b)
                            return (AAbs x a' t', cs)
       _ -> Bad (render ("function type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ))
 
@@ -233,7 +244,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
     Prod _ x a b -> do
       testErr (typ == vType) "expected Type"
       (a',csa) <- checkType th tenv a
-      (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
+      (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b -- TODO: Valid VClos?
       return (AProd x a' b', csa ++ csb)
 
     R xs ->
@@ -287,11 +298,12 @@ inferExp th tenv@(k,rho,gamma) e = case e of
     return (ALet (x,(val1,e1)) e2, val2, cs1++cs2)
    App f t -> do
     (f',w,csf) <- inferExp th tenv f
-    typ <- whnf th w
+    -- typ <- whnf th w
+    let typ = w
     case typ of
       VClos env (Prod _ x a b) -> do
-        (a',csa) <- checkExp th tenv t (VClos env a)
-        b' <- whnf th $ VClos ((x,VClos rho t):env) b
+        (a',csa) <- checkNExp th tenv t (NVClos env a)
+        b' <- whnf th $ NVClos ((x,VClos rho t):env) b -- Valid VClos?
         return $ (AApp f' a' b', b', csf ++ csa)
       _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
    _ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e))
@@ -317,7 +329,7 @@ checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
     Just val -> do (aexp,cs) <- checkExp th tenv exp val
                    return ((lbl,(val,aexp)),cs)
 
-checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)])
+checkBranch :: Theory -> TCEnv -> Equation -> NotVal -> Err (([Term],AExp),[(Val,Val)])
 checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
                                   chB tenv' ps' ty
  where
@@ -326,25 +338,26 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
   tenv' = (k, rho2++rho, gamma) ---- k' ?
   (k,rho,gamma) = tenv
 
+  chB :: (Int, [(Ident, Val)], [(Ident, Val)]) -> [Term] -> NotVal -> Err (([Term], AExp), [(Val, Val)])
   chB tenv@(k,rho,gamma) ps ty = case ps of
     p:ps2 -> do
       typ <- whnf th ty
-      traceM . render $ "\ncheckBranch: Normalized " <+> vcat [ppValue Unqualified 0 ty , ppValue Unqualified 0 typ]
+      traceM . render $ "\ncheckBranch: Normalized " <+> vcat [ppNValue Unqualified 0 ty , ppValue Unqualified 0 typ]
       case typ of
         VClos env (Prod _ y a b) -> do
-          a' <- whnf th $ VClos env a
+          a' <- whnf th $ NVClos env a
           (p', sigma, binds, cs1) <- checkP tenv p y a'
           let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
-          ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
+          ((ps',exp),cs2) <- chB tenv' ps2 (NVClos ((y,p'):env) b)
           return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
         _ -> Bad (render ("Product expected for definiens" <+> ppTerm Unqualified 0 t <+> "instead of" <+> ppValue Unqualified 0 typ))
     [] -> do
-      (e,cs) <- checkExp th tenv t ty
+      (e,cs) <- checkNExp th tenv t ty
       return (([],e),cs)
   checkP env@(k,rho,gamma) t x a = do
      (delta,cs) <- checkPatt th env t a
      let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
-     return (VClos sigma t, sigma, delta, cs)
+     return (VClos sigma t, sigma, delta, cs) -- TODO: Valid VClos?
 
   ps2ts k = foldr p2t ([],0,[],k)
   p2t p (ps,i,g,k) = case p of
@@ -375,6 +388,7 @@ checkPatt th tenv exp val = do
      _ -> [] -- no other cases are possible
 
 --- ad hoc, to find types of variables
+   checkExpP :: (a, Env, c) -> Term -> Val -> Err (AExp, Val, [a2])
    checkExpP tenv@(k,rho,gamma) exp val = case exp of
      Meta m -> return $ (AMeta m val, val, [])
      Vr x   -> return $ (AVr   x val, val, [])
@@ -390,11 +404,12 @@ checkPatt th tenv exp val = do
        return $ (ACn c typ, typ, []) ----
      App f t -> do
        (f',w,csf) <- checkExpP tenv f val
-       typ <- whnf th w
+      --  typ <- whnf th w
+       let typ = w -- Already normalized
        case typ of
          VClos env (Prod _ x a b) -> do
-           (a',_,csa) <- checkExpP tenv t (VClos env a)
-           b' <- whnf th $ VClos ((x,VClos rho t):env) b
+           (a',_,csa) <- checkExpP tenv t (VClos env a) -- TODO: Valid VClos?
+           b' <- whnf th $ NVClos ((x,VClos rho t):env) b -- TODO: Valid VClos?
            return $ (AApp f' a' b', b', csf ++ csa)
          _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
      _ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp))
diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs
index 4ce8c4fa4f..32883ae24a 100644
--- a/src/compiler/GF/Grammar/Printer.hs
+++ b/src/compiler/GF/Grammar/Printer.hs
@@ -17,6 +17,7 @@ module GF.Grammar.Printer
            , ppTerm
            , ppPatt
            , ppValue
+           , ppNValue
            , ppConstrs
            , ppQIdent
            , ppMeta
@@ -284,6 +285,9 @@ ppValue q d (VClos env e) = case e of
 ppValue q d (VRecType xs) = braces (hsep (punctuate ',' [l <> '=' <> ppValue q 0 v | (l,v) <- xs]))
 ppValue q d VType         = pp "Type"
 
+ppNValue :: TermPrintQual -> Int -> NotVal -> Doc
+ppNValue q d (NVClos env e) = ppValue q d (VClos env e)
+
 ppConstrs :: Constraints -> [Doc]
 ppConstrs = map (\(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w))
 
diff --git a/src/compiler/GF/Grammar/Values.hs b/src/compiler/GF/Grammar/Values.hs
index 3fb88b9185..e6d95e0581 100644
--- a/src/compiler/GF/Grammar/Values.hs
+++ b/src/compiler/GF/Grammar/Values.hs
@@ -14,7 +14,7 @@
 
 module GF.Grammar.Values (
                -- ** Values used in TC type checking
-               Val(..), Env,
+               Val(..), NotVal(..), Env,
                -- ** Annotated tree used in editing
                Binds, Constraints, MetaSubst,
                -- ** For TC
@@ -32,6 +32,9 @@ import GF.Grammar.Predef
 data Val = VGen Int Ident | VApp Val [Val] | VCn QIdent (Maybe (Int, [Equation])) | VRecType [(Label,Val)] | VType | VClos Env Term
   deriving (Eq,Show)
 
+data NotVal = NVClos Env Term
+  deriving (Show)
+
 type Env = [(Ident,Val)]
 
 type Binds = [(Ident,Val)]

From 87c658c4e28add502259c9bd5c4f9078684a570a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 11:16:48 +0200
Subject: [PATCH 14/24] dbg: Print raw constraints and not just ppValue

---
 src/compiler/GF/Grammar/Printer.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs
index 32883ae24a..53bdf8a8bf 100644
--- a/src/compiler/GF/Grammar/Printer.hs
+++ b/src/compiler/GF/Grammar/Printer.hs
@@ -289,7 +289,8 @@ ppNValue :: TermPrintQual -> Int -> NotVal -> Doc
 ppNValue q d (NVClos env e) = ppValue q d (VClos env e)
 
 ppConstrs :: Constraints -> [Doc]
-ppConstrs = map (\(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w))
+ppConstrs = map $ \(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w)
+  $$ braces(show v <+> "<>" <+> show w)
 
 ppEnv :: Env -> Doc
 ppEnv e = hcat (map (\(x,t) -> braces (x <> ":=" <> ppValue Unqualified 0 t)) e)

From 485082c6cd6a329ce6afd8eeeb52407088458bc4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 21:41:16 +0200
Subject: [PATCH 15/24] One fewer false Val

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index ccf23eae2f..174bc783b2 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -244,7 +244,8 @@ checkExp th tenv@(k,rho,gamma) e typ = do
     Prod _ x a b -> do
       testErr (typ == vType) "expected Type"
       (a',csa) <- checkType th tenv a
-      (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b -- TODO: Valid VClos?
+      aWhnf <- whnf th (NVClos rho a)
+      (b',csb) <- checkType th (k+1, (x,v x):rho, (x,aWhnf):gamma) b
       return (AProd x a' b', csa ++ csb)
 
     R xs ->

From 47309e94dd0a010a591bec06ef00cb16a194fdeb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 21:43:34 +0200
Subject: [PATCH 16/24] Normalize constant types on lookup

Not that this is not cached (but should be a simple oper
---
 src/compiler/GF/Compile/TypeCheck/Abstract.hs |  6 +++---
 src/compiler/GF/Compile/TypeCheck/TC.hs       | 11 ++++++++---
 src/compiler/GF/Grammar/Values.hs             |  2 +-
 3 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index 39b2373517..ee223482c3 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -39,8 +39,8 @@ initTCEnv gamma =
 
 -- interface to TC type checker
 
-type2val :: Type -> Val
-type2val = VClos []
+type2val :: Type -> NotVal
+type2val = NVClos []
 
 type2nval :: Type -> NotVal
 type2nval = NVClos []
@@ -48,7 +48,7 @@ type2nval = NVClos []
 cont2exp :: Context -> Term
 cont2exp c = mkProd c eType [] -- to check a context
 
-cont2val :: Context -> Val
+cont2val :: Context -> NotVal
 cont2val = type2val . cont2exp
 
 -- some top-level batch-mode checkers for the compiler
diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 174bc783b2..cdf39741a4 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -56,10 +56,15 @@ data AExp =
 type ALabelling = (Label, AExp)
 type AAssign = (Label, (Val, AExp))
 
-type Theory = QIdent -> Err (Val, Maybe (Int, [Equation]))
+type Theory = QIdent -> Err (NotVal, Maybe (Int, [Equation]))
+
+lookupConst :: HasCallStack => Theory -> QIdent -> Err (Val, Maybe (Int, [Equation]))
+lookupConst th f = do
+  (nv,info) <- th f
+  -- checkWhnf (pp (snd f)) th v
+  v <- whnf th nv
+  return (v, info)
 
-lookupConst :: Theory -> QIdent -> Err (Val, Maybe (Int, [Equation]))
-lookupConst th f = th f
 
 lookupVar :: Env -> Ident -> Err Val
 lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,VClos [] (Meta 0)):g)
diff --git a/src/compiler/GF/Grammar/Values.hs b/src/compiler/GF/Grammar/Values.hs
index e6d95e0581..fae0c017b4 100644
--- a/src/compiler/GF/Grammar/Values.hs
+++ b/src/compiler/GF/Grammar/Values.hs
@@ -32,7 +32,7 @@ import GF.Grammar.Predef
 data Val = VGen Int Ident | VApp Val [Val] | VCn QIdent (Maybe (Int, [Equation])) | VRecType [(Label,Val)] | VType | VClos Env Term
   deriving (Eq,Show)
 
-data NotVal = NVClos Env Term
+data NotVal = NVClos Env Term | NVVal Val
   deriving (Show)
 
 type Env = [(Ident,Val)]

From e73ce33c96b7a6065e5d8117038779e728ca1b0b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 21:44:37 +0200
Subject: [PATCH 17/24] Add more debug printing

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 57 ++++++++++++++++++++-----
 1 file changed, 47 insertions(+), 10 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index cdf39741a4..50a0e341db 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -32,6 +32,7 @@ import Control.Monad
 import Data.Maybe
 import GF.Text.Pretty
 import Debug.Trace (traceM)
+import GHC.Stack (HasCallStack)
 
 data AExp =
      AVr   Ident Val
@@ -65,6 +66,18 @@ lookupConst th f = do
   v <- whnf th nv
   return (v, info)
 
+checkWhnf :: HasCallStack => Doc -> Theory -> Val -> Err ()
+checkWhnf ctx th v = do
+  v' <- whnf th (unVal v)
+  when (v /= v') $ error . render $ ("Not whnf:" <+>) $
+     ctx <+> ":" <+> (ppVal v <+> "<>" <+> ppVal v')
+     $$ show v $$ show v'
+
+ppVal = ppValue Unqualified 0
+
+unVal :: Val -> NotVal
+unVal (VClos e t) = NVClos e t
+unVal v = NVVal v
 
 lookupVar :: Env -> Ident -> Err Val
 lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,VClos [] (Meta 0)):g)
@@ -90,6 +103,7 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
   --     zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
   --     [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
   --   return v'
+  NVVal v -> return v
   NVClos env e -> do
     e' <- eval th env e
     traceM . render $ "\nwhnf: Normalized Closure" <+> vcat
@@ -101,7 +115,7 @@ whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
 
 app :: Theory -> Val -> Val -> Err Val
 app th u v = case u of
-  VClos env (Abs _ x e) -> do 
+  VClos env (Abs _ x e) -> do
     traceM "app: VClos"
     val <- eval th ((x,v):env) e
     traceM "app: VClos 2"
@@ -155,12 +169,12 @@ tryMatchEqn env (PW: ps) (v: vs) repl = do
 tryMatchEqn env (PV c: ps) (v: vs) repl = do
   traceM . render $ "Matching variable" <+> c <+> ":" <+> ppValue Unqualified 0 v
   tryMatchEqn ((c,v):env) ps vs repl -- TODO: Is this sound?
-tryMatchEqn env (PP (q,p) pp: ps) (VApp (VCn (r,f) _) tt: vs) repl 
+tryMatchEqn env (PP (q,p) pp: ps) (VApp (VCn (r,f) _) tt: vs) repl
   | p == f && length pp == length tt = tryMatchEqn env (pp ++ ps) (tt ++ vs) repl
 -- tryMatchEqn env (p: ps) (v: vs) repl = _
 tryMatchEqn env (a:_) (b:_) _ = do
   traceM . render $ ("\ntryMatchEqn:" <+>) $ "Failed to match" <+> a <+> "with" <+> ppValue Unqualified 0 b
-    $$ "raw:" <+> (show a $$ show b) 
+    $$ "raw:" <+> (show a $$ show b)
   return Nothing
 tryMatchEqn env _ _ _ = Bad "tryMatchEqn: Non-matching length"
 
@@ -175,7 +189,7 @@ eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
     (_ty, defEqns) <- lookupConst th c
     return $ VCn c defEqns ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
-  App f a -> do 
+  App f a -> do
     traceM "eval: App"
     join $ liftM2 (app th) (eval th env f) (eval th env a)
   RecType xs -> do xs <- mapM (\(l,e) -> eval th env e >>= \e -> return (l,e)) xs
@@ -190,12 +204,13 @@ eqNVal th k u1 u2 = do
   w2 <- whnf th u2
   eqVal th k w1 w2
 
-eqVal :: Theory -> Int -> Val -> Val -> Err [(Val,Val)]
+eqVal :: HasCallStack => Theory -> Int -> Val -> Val -> Err [(Val,Val)]
 eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
                 do
   -- w1 <- whnf th u1
   -- w2 <- whnf th u2
   let (w1,w2) = (u1,u2)
+  traceM . render $ "\neqVal comparing:" <+> vcat ["" <+> ppValue Unqualified 0 w1 , ppValue Unqualified 0 w2]
   let v = VGen k
   case (w1,w2) of
     (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (fmap concat $ zipWithM (eqVal th k) a1 a2)
@@ -209,18 +224,27 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
     (VCn (_, i) _, VCn (_,j) _) -> return [(w1,w2) | i /= j]
     --- thus ignore qualifications; valid because inheritance cannot
     --- be qualified. Simplifies annotation. AR 17/3/2005
-    _ -> return [(w1,w2) | w1 /= w2]
+    _ -> do
+      when (w1 /= w2) $ do
+        traceM . render $ "\neqVal not equal" <+> vcat 
+          ["" <+> ppValue Unqualified 0 w1 , ppValue Unqualified 0 w2
+          ,pp $ show w1 , pp $ show w2
+          ]
+        error "not equal"
+      return [(w1,w2) | w1 /= w2]
 -- invariant: constraints are in whnf
 
 checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)])
 checkType th tenv e = checkExp th tenv e vType
 
-checkNExp :: Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)])
+checkNExp :: HasCallStack => Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)])
 checkNExp th tenv@(k,rho,gamma) e ty = do
   typ <- whnf th ty
+  checkWhnf (pp "checkNExp:") th typ
   traceM . render $ "\ncheckExp: Normalized" <+> vcat ["" <+> ppNValue Unqualified 0 ty , ppValue Unqualified 0 typ]
   checkExp th tenv e typ
-checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
+
+checkExp :: HasCallStack => Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkExp th tenv@(k,rho,gamma) e typ = do
   let v = VGen k
   traceM . render $ "\ncheckExp: checking" <+> vcat ["" <+> e , pp (take 30 $ show e)]
@@ -272,14 +296,20 @@ checkExp th tenv@(k,rho,gamma) e typ = do
                    return (AGlue x y,cs1++cs2++cs3)
     _ -> checkInferExp th tenv e typ
 
-checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp :: HasCallStack => Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkInferExp th tenv@(k,_,_) e typ = do
   (e',w,cs1) <- inferExp th tenv e
+  checkWhnf (pp "checkInferExp w:") th w
+  checkWhnf (pp "checkInferExp typ:") th typ
   cs2 <- eqVal th k w typ
   return (e',cs1 ++ cs2)
 
 inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)])
-inferExp th tenv@(k,rho,gamma) e = case e of
+inferExp th tenv@(k,rho,gamma) e = do
+  traceM . render $ ("\ninferExp:" <+>) 
+    $ "Inferring type of:" <+> vcat ["" <+> ppTerm Unqualified 0 e , pp $ show e]
+    $$ "In context:" <+> show tenv
+  case e of
    Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
    Q (m,c) | m == cPredefAbs && isPredefCat c
                      -> return (ACn (m,c) vType, vType, [])
@@ -363,6 +393,9 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
   checkP env@(k,rho,gamma) t x a = do
      (delta,cs) <- checkPatt th env t a
      let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
+     traceM . render $ ("\ncheckP:" <+>) 
+        $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos sigma t)]
+        $$ "In context:" <+> show tenv
      return (VClos sigma t, sigma, delta, cs) -- TODO: Valid VClos?
 
   ps2ts k = foldr p2t ([],0,[],k)
@@ -414,8 +447,12 @@ checkPatt th tenv exp val = do
        let typ = w -- Already normalized
        case typ of
          VClos env (Prod _ x a b) -> do
+           traceM . render $ ("\ncheckPatt:" <+>) 
+              $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos env t)]
+              --  $$ "In context:" <+> show tenv
            (a',_,csa) <- checkExpP tenv t (VClos env a) -- TODO: Valid VClos?
            b' <- whnf th $ NVClos ((x,VClos rho t):env) b -- TODO: Valid VClos?
+           checkWhnf (pp "checkPatt") th b'
            return $ (AApp f' a' b', b', csf ++ csa)
          _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
      _ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp))

From fc8856b2edab5b35f02994c4f6dcf0951643f16c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 21:55:05 +0200
Subject: [PATCH 18/24] Remove the last unnormalized values

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 50a0e341db..6a08530bda 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -339,7 +339,8 @@ inferExp th tenv@(k,rho,gamma) e = do
     case typ of
       VClos env (Prod _ x a b) -> do
         (a',csa) <- checkNExp th tenv t (NVClos env a)
-        b' <- whnf th $ NVClos ((x,VClos rho t):env) b -- Valid VClos?
+        rhoT <- whnf th $ NVClos rho t -- New whnf
+        b' <- whnf th $ NVClos ((x,rhoT):env) b
         return $ (AApp f' a' b', b', csf ++ csa)
       _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
    _ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e))
@@ -393,10 +394,11 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
   checkP env@(k,rho,gamma) t x a = do
      (delta,cs) <- checkPatt th env t a
      let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
-     traceM . render $ ("\ncheckP:" <+>) 
-        $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos sigma t)]
-        $$ "In context:" <+> show tenv
-     return (VClos sigma t, sigma, delta, cs) -- TODO: Valid VClos?
+    --  traceM . render $ ("\ncheckP:" <+>) 
+    --     $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos sigma t)]
+    --     $$ "In context:" <+> show tenv
+     sigmaT <- whnf th $ NVClos sigma t -- New whnf
+     return (sigmaT, sigma, delta, cs)
 
   ps2ts k = foldr p2t ([],0,[],k)
   p2t p (ps,i,g,k) = case p of
@@ -447,11 +449,12 @@ checkPatt th tenv exp val = do
        let typ = w -- Already normalized
        case typ of
          VClos env (Prod _ x a b) -> do
-           traceM . render $ ("\ncheckPatt:" <+>) 
-              $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos env t)]
-              --  $$ "In context:" <+> show tenv
-           (a',_,csa) <- checkExpP tenv t (VClos env a) -- TODO: Valid VClos?
-           b' <- whnf th $ NVClos ((x,VClos rho t):env) b -- TODO: Valid VClos?
+          --  traceM . render $ ("\ncheckPatt:" <+>) 
+          --     $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos env t)]
+           envA <- whnf th $ NVClos env a -- New whnf
+           (a',_,csa) <- checkExpP tenv t envA
+           rhoT <- whnf th $ NVClos rho t -- New whnf
+           b' <- whnf th $ NVClos ((x,rhoT):env) b
            checkWhnf (pp "checkPatt") th b'
            return $ (AApp f' a' b', b', csf ++ csa)
          _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))

From bab61ccb1118fa4b60143859d8510a84181f9784 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 22:05:03 +0200
Subject: [PATCH 19/24] Remove crash on non-matching values

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 6a08530bda..f9b21e81f0 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -230,7 +230,6 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
           ["" <+> ppValue Unqualified 0 w1 , ppValue Unqualified 0 w2
           ,pp $ show w1 , pp $ show w2
           ]
-        error "not equal"
       return [(w1,w2) | w1 /= w2]
 -- invariant: constraints are in whnf
 

From 23f600c5541acd8712a2597d3a476eb54d932a90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 22:05:34 +0200
Subject: [PATCH 20/24] Disable most debug logging

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index f9b21e81f0..02e39cf6b1 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -31,9 +31,11 @@ import Control.Monad
 --import Data.List (sortBy)
 import Data.Maybe
 import GF.Text.Pretty
-import Debug.Trace (traceM)
+-- import Debug.Trace (traceM)
 import GHC.Stack (HasCallStack)
 
+traceM _ = return ()
+
 data AExp =
      AVr   Ident Val
    | ACn   QIdent Val

From e2528e7848ed71d4baa9aca3ab0a81687c1dfefe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 22:08:40 +0200
Subject: [PATCH 21/24] Remove more debug printing

---
 src/compiler/GF/Compile/TypeCheck/Abstract.hs | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index ee223482c3..ad163e9a6d 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -30,7 +30,6 @@ import GF.Grammar.Unify
 import GF.Compile.TypeCheck.TC
 
 import GF.Text.Pretty
-import Debug.Trace (traceM)
 --import Control.Monad (foldM, liftM, liftM2)
 
 -- | invariant way of creating TCEnv from context
@@ -80,11 +79,7 @@ checkTyp gr typ = err (\x -> [pp x]) ppConstrs $ justTypeCheck gr typ vType
 
 checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message]
 checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do
-  traceM . render $ "\nchecking def: " <+> pp fun <+> ":" <+> pp typ
-                   $$ "with equation:" <+> pp fun <+> hsep [ppPatt Unqualified 2 p | p <- fst eq] <+> "=>" <+> snd eq
   (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2nval typ)
-  traceM . render $ "\ngot branches" {- <+> pp (show $ snd b) -} <+> ": with :" <+> pp (vcat $ fst b)
-        $$ "with constraints:" <+> vcat [ppValue Unqualified 0 a <+> " = " <+> ppValue Unqualified 0 b | (a,b) <- cs]
   (constrs,_) <- unifyVal cs
   return $ filter notJustMeta constrs
 

From 6fa91e38e62a4ade8360be6f1e3b798dfe67d483 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 22:09:48 +0200
Subject: [PATCH 22/24] Remove more debugging junk

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 02e39cf6b1..053534fec4 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -31,8 +31,6 @@ import Control.Monad
 --import Data.List (sortBy)
 import Data.Maybe
 import GF.Text.Pretty
--- import Debug.Trace (traceM)
-import GHC.Stack (HasCallStack)
 
 traceM _ = return ()
 
@@ -61,14 +59,14 @@ type AAssign = (Label, (Val, AExp))
 
 type Theory = QIdent -> Err (NotVal, Maybe (Int, [Equation]))
 
-lookupConst :: HasCallStack => Theory -> QIdent -> Err (Val, Maybe (Int, [Equation]))
+lookupConst ::  Theory -> QIdent -> Err (Val, Maybe (Int, [Equation]))
 lookupConst th f = do
   (nv,info) <- th f
   -- checkWhnf (pp (snd f)) th v
   v <- whnf th nv
   return (v, info)
 
-checkWhnf :: HasCallStack => Doc -> Theory -> Val -> Err ()
+checkWhnf ::  Doc -> Theory -> Val -> Err ()
 checkWhnf ctx th v = do
   v' <- whnf th (unVal v)
   when (v /= v') $ error . render $ ("Not whnf:" <+>) $
@@ -206,7 +204,7 @@ eqNVal th k u1 u2 = do
   w2 <- whnf th u2
   eqVal th k w1 w2
 
-eqVal :: HasCallStack => Theory -> Int -> Val -> Val -> Err [(Val,Val)]
+eqVal ::  Theory -> Int -> Val -> Val -> Err [(Val,Val)]
 eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
                 do
   -- w1 <- whnf th u1
@@ -238,14 +236,14 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
 checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)])
 checkType th tenv e = checkExp th tenv e vType
 
-checkNExp :: HasCallStack => Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)])
+checkNExp ::  Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)])
 checkNExp th tenv@(k,rho,gamma) e ty = do
   typ <- whnf th ty
   checkWhnf (pp "checkNExp:") th typ
   traceM . render $ "\ncheckExp: Normalized" <+> vcat ["" <+> ppNValue Unqualified 0 ty , ppValue Unqualified 0 typ]
   checkExp th tenv e typ
 
-checkExp :: HasCallStack => Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
+checkExp ::  Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkExp th tenv@(k,rho,gamma) e typ = do
   let v = VGen k
   traceM . render $ "\ncheckExp: checking" <+> vcat ["" <+> e , pp (take 30 $ show e)]
@@ -297,7 +295,7 @@ checkExp th tenv@(k,rho,gamma) e typ = do
                    return (AGlue x y,cs1++cs2++cs3)
     _ -> checkInferExp th tenv e typ
 
-checkInferExp :: HasCallStack => Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp ::  Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkInferExp th tenv@(k,_,_) e typ = do
   (e',w,cs1) <- inferExp th tenv e
   checkWhnf (pp "checkInferExp w:") th w

From 5ea706b91b8e12b94ff17398d7dfcc297d8d7e8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 22:12:09 +0200
Subject: [PATCH 23/24] Remove debug logging

---
 src/compiler/GF/Compile/TypeCheck/TC.hs | 65 ++-----------------------
 1 file changed, 4 insertions(+), 61 deletions(-)

diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index 053534fec4..4cf36ac81b 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -32,7 +32,6 @@ import Control.Monad
 import Data.Maybe
 import GF.Text.Pretty
 
-traceM _ = return ()
 
 data AExp =
      AVr   Ident Val
@@ -91,66 +90,28 @@ type TCEnv = (Int,Env,Env)
 whnf :: Theory -> NotVal -> Err Val
 whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug
          case v of
-  -- VApp u w -> do
-  --   u' <- whnf th u
-  --   w' <- mapM (whnf th) w
-  --   traceM . render $ "\nwhnf: Normalized app 2" <+> vcat (
-  --     ("" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ) :
-  --     zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w')
-  --   v' <- foldM (app th) u' w'
-  --   traceM . render $ "\nwhnf: Normalized app" <+> vcat (
-  --     ["" <+> ppValue Unqualified 0 u <+> "to" <+> ppValue Unqualified 0 u' ] ++
-  --     zipWith (\w w' -> ppValue Unqualified 0 w <+> "to" <+> ppValue Unqualified 0 w') w w' ++
-  --     [ ppValue Unqualified 0 v <+> "to" <+> ppValue Unqualified 0 v' ])
-  --   return v'
   NVVal v -> return v
-  NVClos env e -> do
-    e' <- eval th env e
-    traceM . render $ "\nwhnf: Normalized Closure" <+> vcat
-      ["" <+> ppTerm Unqualified 0 e <+> "to" <+> ppValue Unqualified 0 e' ]
-    return e'
-  -- _ -> do
-  --   traceM . render $ "\nwhnf: unchanged" <+> ppValue Unqualified 0 v
-  --   return v
+  NVClos env e -> eval th env e
 
 app :: Theory -> Val -> Val -> Err Val
 app th u v = case u of
   VClos env (Abs _ x e) -> do
-    traceM "app: VClos"
     val <- eval th ((x,v):env) e
-    traceM "app: VClos 2"
     evalDef th val
   VApp u' v' -> do
     let val = VApp u' (v' ++ [v])
-    traceM . render $ "\napp: Extended app:" <+>
-      (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
-       $$ take 300 (show val))
     evalDef th val
   _ -> do
-    traceM . render $ "\napp: Unchanged app:" <+>
-      (ppValue Unqualified 0 u <+> "applied to" <+> ppValue Unqualified 0 v
-       $$ take 300 (show u))
     return $ VApp u [v]
 
 evalDef :: Theory -> Val -> Err Val
 evalDef th e = case e of
   VApp (VCn c (Just (n, eqs))) xs | length xs == n -> do
-    traceM . render $ ("\nevalDef:" <+>) $ "Found def:" <+> snd c
-            $$ "with equations:" <+> vcat
-              [ snd c <+> hsep [ppPatt Unqualified 2 p | p <- pat] <+> "=>" <+> val
-              | (pat, val) <- eqs
-              ]
-            $$ ("applied to:" <+> (ppValue Unqualified 0 e))
-            $$ "raw equations:" <+> vcat
-              [ snd c <+> hsep [showsPrec 11 p "" | p <- pat] <+> "=>" <+> val | (pat, val) <- eqs ]
-            $$ ("applied to:" <+> (show (VApp (VCn c Nothing) xs)))
     e' <- tryMatchEqns eqs xs
-    traceM . render $ ("\nevalDef:" <+>) $ "Evaluated:" <+> show e'
     case e' of
       Just (NVClos env tm) -> eval th env tm
       _ -> return e
   _ -> do
-    traceM "evalDef: not yet"
     return e
 
 tryMatchEqns :: [Equation] -> [Val] -> Err (Maybe NotVal)
@@ -163,18 +124,14 @@ tryMatchEqns [] xs = return Nothing
 
 tryMatchEqn :: Env -> [Patt] -> [Val] -> Term -> Err (Maybe NotVal)
 tryMatchEqn env [] [] repl = return $ Just $ NVClos env repl
-tryMatchEqn env (PW: ps) (v: vs) repl = do
-  traceM . render $ "Matching wildcard" <+> ppValue Unqualified 0 v
+tryMatchEqn env (PW: ps) (v: vs) repl =
   tryMatchEqn env ps vs repl
-tryMatchEqn env (PV c: ps) (v: vs) repl = do
-  traceM . render $ "Matching variable" <+> c <+> ":" <+> ppValue Unqualified 0 v
+tryMatchEqn env (PV c: ps) (v: vs) repl =
   tryMatchEqn ((c,v):env) ps vs repl -- TODO: Is this sound?
 tryMatchEqn env (PP (q,p) pp: ps) (VApp (VCn (r,f) _) tt: vs) repl
   | p == f && length pp == length tt = tryMatchEqn env (pp ++ ps) (tt ++ vs) repl
 -- tryMatchEqn env (p: ps) (v: vs) repl = _
 tryMatchEqn env (a:_) (b:_) _ = do
-  traceM . render $ ("\ntryMatchEqn:" <+>) $ "Failed to match" <+> a <+> "with" <+> ppValue Unqualified 0 b
-    $$ "raw:" <+> (show a $$ show b)
   return Nothing
 tryMatchEqn env _ _ _ = Bad "tryMatchEqn: Non-matching length"
 
@@ -190,12 +147,10 @@ eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
     return $ VCn c defEqns ---- == Q ?
   Sort c  -> return $ VType --- the only sort is Type
   App f a -> do
-    traceM "eval: App"
     join $ liftM2 (app th) (eval th env f) (eval th env a)
   RecType xs -> do xs <- mapM (\(l,e) -> eval th env e >>= \e -> return (l,e)) xs
                    return (VRecType xs)
   _ -> do
-    traceM . render . ("eval:" <+>) $ "not evaling: " <+> show e --  $$ "in context" <+> env
     return $ VClos env e
 
 eqNVal :: Theory -> Int -> NotVal -> NotVal -> Err [(Val,Val)]
@@ -210,7 +165,6 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
   -- w1 <- whnf th u1
   -- w2 <- whnf th u2
   let (w1,w2) = (u1,u2)
-  traceM . render $ "\neqVal comparing:" <+> vcat ["" <+> ppValue Unqualified 0 w1 , ppValue Unqualified 0 w2]
   let v = VGen k
   case (w1,w2) of
     (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (fmap concat $ zipWithM (eqVal th k) a1 a2)
@@ -225,11 +179,6 @@ eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2
     --- thus ignore qualifications; valid because inheritance cannot
     --- be qualified. Simplifies annotation. AR 17/3/2005
     _ -> do
-      when (w1 /= w2) $ do
-        traceM . render $ "\neqVal not equal" <+> vcat 
-          ["" <+> ppValue Unqualified 0 w1 , ppValue Unqualified 0 w2
-          ,pp $ show w1 , pp $ show w2
-          ]
       return [(w1,w2) | w1 /= w2]
 -- invariant: constraints are in whnf
 
@@ -240,13 +189,11 @@ checkNExp ::  Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)])
 checkNExp th tenv@(k,rho,gamma) e ty = do
   typ <- whnf th ty
   checkWhnf (pp "checkNExp:") th typ
-  traceM . render $ "\ncheckExp: Normalized" <+> vcat ["" <+> ppNValue Unqualified 0 ty , ppValue Unqualified 0 typ]
   checkExp th tenv e typ
 
 checkExp ::  Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
 checkExp th tenv@(k,rho,gamma) e typ = do
   let v = VGen k
-  traceM . render $ "\ncheckExp: checking" <+> vcat ["" <+> e , pp (take 30 $ show e)]
   case e of
     Meta m -> return $ (AMeta m typ,[])
 
@@ -304,10 +251,7 @@ checkInferExp th tenv@(k,_,_) e typ = do
   return (e',cs1 ++ cs2)
 
 inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)])
-inferExp th tenv@(k,rho,gamma) e = do
-  traceM . render $ ("\ninferExp:" <+>) 
-    $ "Inferring type of:" <+> vcat ["" <+> ppTerm Unqualified 0 e , pp $ show e]
-    $$ "In context:" <+> show tenv
+inferExp th tenv@(k,rho,gamma) e =
   case e of
    Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
    Q (m,c) | m == cPredefAbs && isPredefCat c
@@ -378,7 +322,6 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
   chB tenv@(k,rho,gamma) ps ty = case ps of
     p:ps2 -> do
       typ <- whnf th ty
-      traceM . render $ "\ncheckBranch: Normalized " <+> vcat [ppNValue Unqualified 0 ty , ppValue Unqualified 0 typ]
       case typ of
         VClos env (Prod _ y a b) -> do
           a' <- whnf th $ NVClos env a

From 9bc6a07245b1b0e6254dd22faa2d59c1d7a06f17 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= <anka.213@gmail.com>
Date: Sat, 30 Sep 2023 22:13:00 +0200
Subject: [PATCH 24/24] Remove more debug info

---
 src/compiler/GF/Grammar/Printer.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs
index 53bdf8a8bf..b587dcd8df 100644
--- a/src/compiler/GF/Grammar/Printer.hs
+++ b/src/compiler/GF/Grammar/Printer.hs
@@ -290,7 +290,6 @@ ppNValue q d (NVClos env e) = ppValue q d (VClos env e)
 
 ppConstrs :: Constraints -> [Doc]
 ppConstrs = map $ \(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w)
-  $$ braces(show v <+> "<>" <+> show w)
 
 ppEnv :: Env -> Doc
 ppEnv e = hcat (map (\(x,t) -> braces (x <> ":=" <> ppValue Unqualified 0 t)) e)