Merge branch 'master' into concrete-new

resolves GrammaticalFramework/gf-core/#97

gf.cabal

@@ -178,7 +178,7 @@ library
     GF.Command.TreeOperations
     GF.Compile.CFGtoPGF
     GF.Compile.CheckGrammar
-    GF.Compile.Compute.ConcreteNew
+    GF.Compile.Compute.Concrete
     GF.Compile.Compute.Predef
     GF.Compile.Compute.Value
     GF.Compile.ExampleBased
@@ -207,7 +207,6 @@ library
     GF.Compile.TypeCheck.Concrete
     GF.Compile.TypeCheck.ConcreteNew
     GF.Compile.TypeCheck.Primitives
-    GF.Compile.TypeCheck.RConcrete
     GF.Compile.TypeCheck.TC
     GF.Compile.Update
     GF.Data.BacktrackM

src/compiler/GF/Command/CommonCommands.hs

@@ -15,6 +15,7 @@ import GF.Command.Abstract --(isOpt,valStrOpts,prOpt)
 import GF.Text.Pretty
 import GF.Text.Transliterations
 import GF.Text.Lexing(stringOp,opInEnv)
+import Data.Char (isSpace)
 
 import qualified PGF as H(showCId,showExpr,toATree,toTrie,Trie(..))
 
@@ -170,7 +171,8 @@ commonCommands = fmap (mapCommandExec liftSIO) $ Map.fromList [
        restrictedSystem $ syst ++ " <" ++ tmpi ++ " >" ++ tmpo
        fmap fromString $ restricted $ readFile tmpo,
        -}
-       fmap fromString . restricted . readShellProcess syst $ toString arg,
+       fmap (fromStrings . lines) . restricted . readShellProcess syst . unlines . map (dropWhile (=='\n')) $ toStrings $ arg,
+
      flags = [
        ("command","the system command applied to the argument")
        ],

src/compiler/GF/Command/SourceCommands.hs

@@ -18,8 +18,8 @@ import GF.Grammar.Parser (runP, pExp)
 import GF.Grammar.ShowTerm
 import GF.Grammar.Lookup (allOpers,allOpersTo)
 import GF.Compile.Rename(renameSourceTerm)
-import qualified GF.Compile.Compute.ConcreteNew as CN(normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(normalForm,resourceValues)
-import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType)
+import GF.Compile.TypeCheck.Concrete as TC(inferLType,ppType)
 import GF.Infra.Dependencies(depGraph)
 import GF.Infra.CheckM(runCheck)
 
@@ -259,7 +259,7 @@ checkComputeTerm os sgr t =
      ((t,_),_) <- runCheck $ do t <- renameSourceTerm sgr mo t
                                 inferLType sgr [] t
      let opts = modifyFlags (\fs->fs{optTrace=isOpt "trace" os})
-         t1 = CN.normalForm (CN.resourceValues opts sgr) (L NoLoc identW) t
+         t1 = normalForm (resourceValues opts sgr) (L NoLoc identW) t
          t2 = evalStr t1
      checkPredefError t2
   where

src/compiler/GF/Compile/CheckGrammar.hs

@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/11/11 23:24:33 $ 
+-- > CVS $Date: 2005/11/11 23:24:33 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.31 $
 --
@@ -27,9 +27,9 @@ import GF.Infra.Ident
 import GF.Infra.Option
 
 import GF.Compile.TypeCheck.Abstract
-import GF.Compile.TypeCheck.RConcrete
+import GF.Compile.TypeCheck.Concrete(computeLType,checkLType,inferLType,ppType)
-import qualified GF.Compile.TypeCheck.ConcreteNew as CN
+import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
-import qualified GF.Compile.Compute.ConcreteNew as CN
+import qualified GF.Compile.Compute.Concrete as CN(normalForm,resourceValues)
 
 import GF.Grammar
 import GF.Grammar.Lexer
@@ -74,9 +74,9 @@ checkRestrictedInheritance cwd sgr (name,mo) = checkInModule cwd mo NoLoc empty
      let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
      let incld c   = Set.member c (Set.fromList incl)
      let illegal c = Set.member c (Set.fromList excl)
-     let illegals = [(f,is) | 
+     let illegals = [(f,is) |
            (f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
-     case illegals of 
+     case illegals of
        [] -> return ()
        cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
                          nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
@@ -92,12 +92,12 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
 
   -- check that all abstract constants are in concrete; build default lin and lincats
   jsc <- foldM checkAbs jsc (Map.toList jsa)
-  
+
   return (cm,cnc{jments=jsc})
   where
    checkAbs js i@(c,info) =
      case info of
-       AbsFun (Just (L loc ty)) _ _ _ 
+       AbsFun (Just (L loc ty)) _ _ _
            -> do let mb_def = do
                        let (cxt,(_,i),_) = typeForm ty
                        info <- lookupIdent i js
@@ -136,11 +136,11 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
            checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
            return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
        _ -> return js
-     
+
    checkCnc js (c,info) =
      case info of
        CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
-                             Ok (_,AbsFun (Just (L _ ty)) _ _ _) -> 
+                             Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
                                         do (cont,val) <- linTypeOfType gr cm ty
                                            let linty = (snd (valCat ty),cont,val)
                                            return $ Map.insert c (CncFun (Just linty) d mn mf) js
@@ -159,14 +159,14 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
        _ -> return $ Map.insert c info js
 
 
--- | General Principle: only Just-values are checked. 
+-- | General Principle: only Just-values are checked.
 -- A May-value has always been checked in its origin module.
 checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
 checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
   checkReservedId c
   case info of
-    AbsCat (Just (L loc cont)) -> 
+    AbsCat (Just (L loc cont)) ->
-      mkCheck loc "the category" $ 
+      mkCheck loc "the category" $
         checkContext gr cont
 
     AbsFun (Just (L loc typ0)) ma md moper -> do
@@ -181,7 +181,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
 
     CncCat mty mdef mref mpr mpmcfg -> do
       mty  <- case mty of
-                Just (L loc typ) -> chIn loc "linearization type of" $ 
+                Just (L loc typ) -> chIn loc "linearization type of" $
                                      (if False --flag optNewComp opts
                                         then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
                                                 typ  <- computeLType gr [] typ
@@ -191,19 +191,19 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
                                                 return (Just (L loc typ)))
                 Nothing          -> return Nothing
       mdef <- case (mty,mdef) of
-                (Just (L _ typ),Just (L loc def)) -> 
+                (Just (L _ typ),Just (L loc def)) ->
                     chIn loc "default linearization of" $ do
                        (def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
                        return (Just (L loc def))
                 _ -> return Nothing
       mref <- case (mty,mref) of
-                (Just (L _ typ),Just (L loc ref)) -> 
+                (Just (L _ typ),Just (L loc ref)) ->
                     chIn loc "reference linearization of" $ do
                        (ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr)
                        return (Just (L loc ref))
                 _ -> return Nothing
       mpr  <- case mpr of
-                (Just (L loc t)) -> 
+                (Just (L loc t)) ->
                     chIn loc "print name of" $ do
                        (t,_) <- checkLType gr [] t typeStr
                        return (Just (L loc t))
@@ -212,13 +212,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
 
     CncFun mty mt mpr mpmcfg -> do
       mt <- case (mty,mt) of
-              (Just (cat,cont,val),Just (L loc trm)) -> 
+              (Just (cat,cont,val),Just (L loc trm)) ->
                   chIn loc "linearization of" $ do
                      (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
                      return (Just (L loc trm))
               _ -> return mt
       mpr  <- case mpr of
-                (Just (L loc t)) -> 
+                (Just (L loc t)) ->
                     chIn loc "print name of" $ do
                        (t,_) <- checkLType gr [] t typeStr
                        return (Just (L loc t))
@@ -251,16 +251,16 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
     ResOverload os tysts -> chIn NoLoc "overloading" $ do
       tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts  -- return explicit ones
       tysts0 <- lookupOverload gr (m,c)  -- check against inherited ones too
-      tysts1 <- mapM (uncurry $ flip (checkLType gr [])) 
+      tysts1 <- mapM (uncurry $ flip (checkLType gr []))
                   [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
       --- this can only be a partial guarantee, since matching
       --- with value type is only possible if expected type is given
-      checkUniq $ 
+      checkUniq $
         sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
       return (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (L loc pcs)) _ -> do
-      ts <- chIn loc "parameter type" $ 
+      ts <- chIn loc "parameter type" $
               liftM concat $ mapM mkPar pcs
       return (ResParam (Just (L loc pcs)) (Just ts))
 
@@ -274,9 +274,9 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
        return $ map (mkApp (QC (m,f))) vs
 
    checkUniq xss = case xss of
-     x:y:xs 
+     x:y:xs
       | x == y    -> checkError $ "ambiguous for type" <+>
-                                  ppType (mkFunType (tail x) (head x))  
+                                  ppType (mkFunType (tail x) (head x))
       | otherwise -> checkUniq $ y:xs
      _ -> return ()
 
@@ -294,7 +294,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
        t' <- compAbsTyp ((x,Vr x):g) t
        return $ Prod b x a' t'
      Abs _ _ _ -> return t
-     _ -> composOp (compAbsTyp g) t  
+     _ -> composOp (compAbsTyp g) t
 
 
 -- | for grammars obtained otherwise than by parsing ---- update!!

src/compiler/GF/Compile/Compute/Concrete.hs

@@ -1,3 +1,588 @@
-module GF.Compile.Compute.Concrete{-(module M)-} where
+-- | Functions for computing the values of terms in the concrete syntax, in
---import GF.Compile.Compute.ConcreteLazy as M -- New
+-- | preparation for PMCFG generation.
---import GF.Compile.Compute.ConcreteStrict as M -- Old, inefficient
+module GF.Compile.Compute.Concrete
+           (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
+            normalForm,
+            Value(..), Bind(..), Env, value2term, eval, vapply
+           ) where
+import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
+
+import GF.Grammar hiding (Env, VGen, VApp, VRecType)
+import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
+import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
+import GF.Grammar.PatternMatch(matchPattern,measurePatt)
+import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
+import GF.Compile.Compute.Value hiding (Error)
+import GF.Compile.Compute.Predef(predef,predefName,delta)
+import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
+import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
+import GF.Data.Utilities(mapFst,mapSnd)
+import GF.Infra.Option
+import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
+import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
+--import Data.Char (isUpper,toUpper,toLower)
+import GF.Text.Pretty
+import qualified Data.Map as Map
+import Debug.Trace(trace)
+
+-- * Main entry points
+
+normalForm :: GlobalEnv -> L Ident -> Term -> Term
+normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
+
+nfx env@(GE _ _ _ loc) t = do
+  v <- eval env [] t
+  case value2term loc [] v of
+    Left i  -> fail ("variable #"++show i++" is out of scope")
+    Right t -> return t
+
+eval :: GlobalEnv -> Env -> Term -> Err Value
+eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
+  where
+    cenv = CE gr rvs opts loc (map fst env)
+
+--apply env = apply' env
+
+--------------------------------------------------------------------------------
+
+-- * Environments
+
+type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
+
+data GlobalEnv = GE Grammar ResourceValues Options GLocation
+data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
+                       opts::Options,
+                       gloc::GLocation,local::LocalScope}
+type GLocation = L Ident
+type LocalScope = [Ident]
+type Stack = [Value]
+type OpenValue = Stack->Value
+
+geLoc     (GE _ _ _ loc) = loc
+geGrammar (GE gr _ _ _)  = gr
+
+ext b env = env{local=b:local env}
+extend bs env = env{local=bs++local env}
+global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
+
+var :: CompleteEnv -> Ident -> Err OpenValue
+var env x = maybe unbound pick' (elemIndex x (local env))
+  where
+    unbound = fail ("Unknown variable: "++showIdent x)
+    pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
+    err i vs = bug $ "Stack problem: "++showIdent x++": "
+                    ++unwords (map showIdent (local env))
+                    ++" => "++show (i,length vs)
+    ok v = --trace ("var "++show x++" = "++show v) $
+           v
+
+pick :: Int -> Stack -> Maybe Value
+pick 0 (v:_) = Just v
+pick i (_:vs) = pick (i-1) vs
+pick i vs = Nothing -- bug $ "pick "++show (i,vs)
+
+resource env (m,c) =
+--  err bug id $
+    if isPredefCat c
+    then value0 env =<< lockRecType c defLinType -- hmm
+    else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
+  where e = fail $ "Not found: "++render m++"."++showIdent c
+
+-- | Convert operators once, not every time they are looked up
+resourceValues :: Options -> SourceGrammar -> GlobalEnv
+resourceValues opts gr = env
+  where
+    env = GE gr rvs opts (L NoLoc identW)
+    rvs = Map.mapWithKey moduleResources (moduleMap gr)
+    moduleResources m = Map.mapWithKey (moduleResource m) . jments
+    moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
+                                  let loc = L l c
+                                      qloc = L l (Q (m,c))
+                                  eval (GE gr rvs opts loc) [] (traceRes qloc t)
+
+    traceRes = if flag optTrace opts
+               then traceResource
+               else const id
+
+-- * Tracing
+
+-- | Insert a call to the trace function under the top-level lambdas
+traceResource (L l q) t =
+  case termFormCnc t of
+    (abs,body) -> mkAbs abs (mkApp traceQ [args,body])
+      where
+        args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
+        lstr = render (l<>":"<>ppTerm Qualified 0 q)
+        traceQ = Q (cPredef,cTrace)
+
+-- * Computing values
+
+-- | Computing the value of a top-level term
+value0 :: CompleteEnv -> Term -> Err Value
+value0 env = eval (global env) []
+
+-- | Computing the value of a term
+value :: CompleteEnv -> Term -> Err OpenValue
+value env t0 =
+  -- Each terms is traversed only once by this function, using only statically
+  -- available information. Notably, the values of lambda bound variables
+  -- will be unknown during the term traversal phase.
+  -- The result is an OpenValue, which is a function that may be applied many
+  -- times to different dynamic values, but without the term traversal overhead
+  -- and without recomputing other statically known information.
+  -- For this to work, there should be no recursive calls under lambdas here.
+  -- Whenever we need to construct the OpenValue function with an explicit
+  -- lambda, we have to lift the recursive calls outside the lambda.
+  -- (See e.g. the rules for Let, Prod and Abs)
+{-
+  trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
+                                      brackets (fsep (map ppIdent (local env))),
+                                      ppTerm Unqualified 10 t0]) $
+--}
+  errIn (render t0) $
+  case t0 of
+    Vr x   -> var env x
+    Q x@(m,f)
+      | m == cPredef -> if f==cErrorType                -- to be removed
+                        then let p = identS "P"
+                             in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
+                        else if f==cPBool
+                               then const # resource env x
+                               else const . flip VApp [] # predef f
+      | otherwise    -> const # resource env x --valueResDef (fst env) x
+    QC x   -> return $ const (VCApp x [])
+    App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
+    Let (x,(oty,t)) body -> do vb <- value (ext x env) body
+                               vt <- value env t
+                               return $ \ vs -> vb (vt vs:vs)
+    Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
+    Prod bt x t1 t2 ->
+       do vt1 <- value env t1
+          vt2 <- value (ext x env) t2
+          return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
+    Abs bt x t -> do vt <- value (ext x env) t
+                     return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
+    EInt n -> return $ const (VInt n)
+    EFloat f -> return $ const (VFloat f)
+    K s -> return $ const (VString s)
+    Empty -> return $ const (VString "")
+    Sort s | s == cTok -> return $ const (VSort cStr)        -- to be removed
+           | otherwise -> return $ const (VSort s)
+    ImplArg t -> (VImplArg.) # value env t
+    Table p res -> liftM2 VTblType # value env p <# value env res
+    RecType rs -> do lovs <- mapPairsM (value env) rs
+                     return $ \vs->VRecType $ mapSnd ($vs) lovs
+    t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
+    FV ts   -> ((vfv .) # sequence) # mapM (value env) ts
+    R as    -> do lovs <- mapPairsM (value env.snd) as
+                  return $ \ vs->VRec $ mapSnd ($vs) lovs
+    T i cs  -> valueTable env i cs
+    V ty ts -> do pvs <- paramValues env ty
+                  ((VV ty pvs .) . sequence) # mapM (value env) ts
+    C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
+    S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
+    P t l   -> --maybe (bug $ "project "++show l++" from "++show v) id $
+               do ov <- value env t
+                  return $ \ vs -> let v = ov vs
+                                   in maybe (VP v l) id (proj l v)
+    Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
+    Strs ts    -> ((VStrs.) # sequence) # mapM (value env) ts
+    Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
+    ELin c r -> (unlockVRec (gloc env) c.) # value env r
+    EPatt p  -> return $ const (VPatt p) -- hmm
+    EPattType ty -> do vt <- value env ty
+                       return (VPattType . vt)
+    Typed t ty -> value env t
+    t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
+
+vconcat vv@(v1,v2) =
+    case vv of
+      (VString "",_) -> v2
+      (_,VString "") -> v1
+      (VApp NonExist _,_) -> v1
+      (_,VApp NonExist _) -> v2
+      _ -> VC v1 v2
+
+proj l v | isLockLabel l = return (VRec [])
+                ---- a workaround 18/2/2005: take this away and find the reason
+                ---- why earlier compilation destroys the lock field
+proj l v =
+    case v of
+      VFV vs -> liftM vfv (mapM (proj l) vs)
+      VRec rs -> lookup l rs
+--    VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
+      VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
+      _ -> return (ok1 VP v l)
+
+ok1 f v1@(VError {}) _ = v1
+ok1 f v1 v2 = f v1 v2
+
+ok2 f v1@(VError {}) _ = v1
+ok2 f _ v2@(VError {}) = v2
+ok2 f v1 v2 = f v1 v2
+
+ok2p f (v1@VError {},_) = v1
+ok2p f (_,v2@VError {}) = v2
+ok2p f vv = f vv
+
+unlockVRec loc c0 v0 = v0
+{-
+unlockVRec loc c0 v0 = unlockVRec' c0 v0
+  where
+    unlockVRec' ::Ident -> Value -> Value
+    unlockVRec' c v =
+        case v of
+    --    VClosure env t -> err bug (VClosure env) (unlockRecord c t)
+          VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
+          VRec rs        -> plusVRec rs lock
+    --    _              -> VExtR v (VRec lock) -- hmm
+          _              -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
+    --    _              -> bugloc loc $ "unlock non-record "++show v0
+      where
+        lock = [(lockLabel c,VRec [])]
+-}
+
+-- suspicious, but backwards compatible
+plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
+  where ls2 = map fst rs2
+
+extR t vv =
+    case vv of
+      (VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
+      (v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
+      (VRecType rs1, VRecType rs2) ->
+          case intersect (map fst rs1) (map fst rs2) of
+            [] -> VRecType (rs1 ++ rs2)
+            ls -> error $ "clash"<+>show ls
+      (VRec     rs1, VRec     rs2) -> plusVRec rs1 rs2
+      (v1          , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
+      (VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
+--    (v1,v2) -> ok2 VExtR v1 v2 -- hmm
+      (v1,v2) -> error $ "not records" $$ show v1 $$ show v2
+  where
+    error explain = ppbug $ "The term" <+> t
+                            <+> "is not reducible" $$ explain
+
+glue env (v1,v2) = glu v1 v2
+  where
+    glu v1 v2 =
+        case (v1,v2) of
+          (VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
+          (v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
+          (VString s1,VString s2) -> VString (s1++s2)
+          (v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
+             where glx v2 = glu v1 v2
+          (v1@(VAlts {}),v2) ->
+           --err (const (ok2 VGlue v1 v2)) id $
+             err bug id $
+             do y' <- strsFromValue v2
+                x' <- strsFromValue v1
+                return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
+          (VC va vb,v2) -> VC va (glu vb v2)
+          (v1,VC va vb) -> VC (glu v1 va) vb
+          (VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
+          (v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
+          (v1@(VApp NonExist _),_) -> v1
+          (_,v2@(VApp NonExist _)) -> v2
+--        (v1,v2) -> ok2 VGlue v1 v2
+          (v1,v2) -> if flag optPlusAsBind (opts env)
+                       then VC v1 (VC (VApp BIND []) v2)
+                       else let loc  = gloc env
+                                vt v = case value2term loc (local env) v of
+                                         Left i  -> Error ('#':show i)
+                                         Right t -> t
+                                originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
+                                                               (Glue (vt v1) (vt v2)))
+                                term = render $ pp  $ Glue (vt v1) (vt v2)
+                            in error $ unlines
+                                [originalMsg
+                                ,""
+                                ,"There was a problem in the expression `"++term++"`, either:"
+                                ,"1) You are trying to use + on runtime arguments, possibly via an oper."
+                                ,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
+                                ,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
+                                ]
+
+
+-- | to get a string from a value that represents a sequence of terminals
+strsFromValue :: Value -> Err [Str]
+strsFromValue t = case t of
+  VString s   -> return [str s]
+  VC s t -> do
+    s' <- strsFromValue s
+    t' <- strsFromValue t
+    return [plusStr x y | x <- s', y <- t']
+{-
+  VGlue s t -> do
+    s' <- strsFromValue s
+    t' <- strsFromValue t
+    return [glueStr x y | x <- s', y <- t']
+-}
+  VAlts d vs -> do
+    d0 <- strsFromValue d
+    v0 <- mapM (strsFromValue . fst) vs
+    c0 <- mapM (strsFromValue . snd) vs
+  --let vs' = zip v0 c0
+    return [strTok (str2strings def) vars |
+              def  <- d0,
+              vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
+                                                          vv <- sequence v0]
+           ]
+  VFV ts -> concat # mapM strsFromValue ts
+  VStrs ts -> concat # mapM strsFromValue ts
+
+  _ -> fail ("cannot get Str from value " ++ show t)
+
+vfv vs = case nub vs of
+           [v] -> v
+           vs -> VFV vs
+
+select env vv =
+    case vv of
+      (v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
+      (VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
+      (v1@(VV pty vs rs),v2) ->
+         err (const (VS v1 v2)) id $
+         do --ats <- allParamValues (srcgr env) pty
+            --let vs = map (value0 env) ats
+            i <- maybeErr "no match" $ findIndex (==v2) vs
+            return (ix (gloc env) "select" rs i)
+      (VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
+      (v1@(VT _ _ cs),v2) ->
+                 err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
+                 match (gloc env) cs v2
+      (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
+      (v1,v2) -> ok2 VS v1 v2
+
+match loc cs v =
+  case value2term loc [] v of
+    Left i  -> bad ("variable #"++show i++" is out of scope")
+    Right t -> err bad return (matchPattern cs t)
+  where
+    bad = fail . ("In pattern matching: "++)
+
+valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
+valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
+
+valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
+valueTable env i cs =
+    case i of
+      TComp ty -> do pvs <- paramValues env ty
+                     ((VV ty pvs .) # sequence) # mapM (value env.snd) cs
+      _ -> do ty <- getTableType i
+              cs' <- mapM valueCase cs
+              err (dynamic cs' ty) return (convert cs' ty)
+  where
+    dynamic cs' ty _ = cases cs' # value env ty
+
+    cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
+      where
+        keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
+                   VT wild (vty vs) (mapSnd ($vs) cs')
+
+    wild = case i of TWild _ -> True; _ -> False
+
+    convertv cs' vty =
+      case value2term (gloc env) [] vty of
+        Left i    -> fail ("variable #"++show i++" is out of scope")
+        Right pty -> convert' cs' =<< paramValues'' env pty
+
+    convert cs' ty = convert' cs' =<< paramValues' env ty
+
+    convert' cs' ((pty,vs),pvs) =
+      do sts  <- mapM (matchPattern cs') vs
+         return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
+                                           (mapFst ($vs) sts)
+
+    valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
+                         pvs <- linPattVars p'
+                         vt <- value (extend pvs env) t
+                         return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
+
+    inlinePattMacro p =
+        case p of
+          PM qc -> do r <- resource env qc
+                      case r of
+                        VPatt p' -> inlinePattMacro p'
+                        _ -> ppbug $ hang "Expected pattern macro:" 4
+                                          (show r)
+          _ -> composPattOp inlinePattMacro p
+
+
+paramValues env ty = snd # paramValues' env ty
+
+paramValues' env ty = paramValues'' env =<< nfx (global env) ty
+
+paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
+                           pvs <- mapM (eval (global env) []) ats
+                           return ((pty,ats),pvs)
+
+push' p bs xs = if length bs/=length xs
+                then bug $ "push "++show (p,bs,xs)
+                else push bs xs
+
+push :: Env -> LocalScope -> Stack -> Stack
+push bs [] vs = vs
+push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
+  where  err = bug $ "Unbound pattern variable "++showIdent x
+
+apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
+apply' env t [] = value env t
+apply' env t vs =
+  case t of
+    QC x                   -> return $ \ svs -> VCApp x (map ($svs) vs)
+{-
+    Q x@(m,f) | m==cPredef -> return $
+                              let constr = --trace ("predef "++show x) .
+                                           VApp x
+                              in \ svs -> maybe constr id (Map.lookup f predefs)
+                                          $ map ($svs) vs
+              | otherwise  -> do r <- resource env x
+                                 return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
+-}
+    App t1 t2              -> apply' env t1 . (:vs) =<< value env t2
+    _                      -> do fv <- value env t
+                                 return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
+
+vapply :: GLocation -> Value -> [Value] -> Value
+vapply loc v [] = v
+vapply loc v vs =
+  case v of
+    VError {} -> v
+--  VClosure env (Abs b x t) -> beta gr env b x t vs
+    VAbs bt _ (Bind f) -> vbeta loc bt f vs
+    VApp pre vs1 -> delta' pre (vs1++vs)
+      where
+        delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
+                                  in vtrace loc v1 vr
+        delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
+        --msg = const (VApp pre (vs1++vs))
+        msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
+    VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
+    VFV fs -> vfv [vapply loc f vs|f<-fs]
+    VCApp f vs0 -> VCApp f (vs0++vs)
+    VMeta i env vs0 -> VMeta i env (vs0++vs)
+    VGen i vs0 -> VGen i (vs0++vs)
+    v -> bug $ "vapply "++show v++" "++show vs
+
+vbeta loc bt f (v:vs) =
+  case (bt,v) of
+    (Implicit,VImplArg v) -> ap v
+    (Explicit,         v) -> ap v
+  where
+    ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
+    ap v         = vapply loc (f v) vs
+
+vary (VFV vs) = vs
+vary v = [v]
+varyList = mapM vary
+
+{-
+beta env b x t (v:vs) =
+  case (b,v) of
+    (Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
+    (Explicit,         v) -> apply' (ext (x,v) env) t vs
+-}
+
+vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
+  where
+    pv v = case v of
+             VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
+             _ -> ppV v
+    pf (_,VString n) = pp n
+    pf (_,v) = ppV v
+    pa (_,v) = ppV v
+    ppV v = case value2term' True loc [] v of
+              Left i  -> "variable #" <> pp i <+> "is out of scope"
+              Right t -> ppTerm Unqualified 10 t
+
+-- | Convert a value back to a term
+value2term :: GLocation -> [Ident] -> Value -> Either Int Term
+value2term = value2term' False
+value2term' stop loc xs v0 =
+  case v0 of
+    VApp pre vs    -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
+    VCApp f vs     -> liftM  (foldl App (QC f))   (mapM v2t vs)
+    VGen j vs      -> liftM2 (foldl App) (var j)  (mapM v2t vs)
+    VMeta j env vs -> liftM  (foldl App (Meta j)) (mapM v2t vs)
+    VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
+    VAbs  bt   x f -> liftM  (Abs  bt x)         (v2t' x f)
+    VInt n         -> return (EInt n)
+    VFloat f       -> return (EFloat f)
+    VString s      -> return (if null s then Empty else K s)
+    VSort s        -> return (Sort s)
+    VImplArg v     -> liftM  ImplArg (v2t v)
+    VTblType p res -> liftM2 Table (v2t p) (v2t res)
+    VRecType rs    -> liftM  RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
+    VRec as        -> liftM  R       (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
+    VV t _ vs      -> liftM  (V t)   (mapM v2t vs)
+    VT wild v cs   -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
+    VFV vs         -> liftM  FV (mapM v2t vs)
+    VC v1 v2       -> liftM2 C (v2t v1) (v2t v2)
+    VS v1 v2       -> liftM2 S (v2t v1) (v2t v2)
+    VP v l         -> v2t v >>= \t -> return (P t l)
+    VPatt p        -> return (EPatt p)
+    VPattType v    -> v2t v >>= return . EPattType
+    VAlts v vvs    -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
+    VStrs vs       -> liftM  Strs (mapM v2t vs)
+--  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
+--  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
+    VError err     -> return (Error err)
+
+  where
+    v2t = v2txs xs
+    v2txs = value2term' stop loc
+    v2t' x f = v2txs (x:xs) (bind f (gen xs))
+
+    var j
+      | j<length xs = Right (Vr (reverse xs !! j))
+      | otherwise   = Left  j
+
+
+    pushs xs e = foldr push e xs
+    push x (env,xs) = ((x,gen xs):env,x:xs)
+    gen xs = VGen (length xs) []
+
+    nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
+      where (env',xs') = pushs (pattVars p) ([],xs)
+
+    bind (Bind f) x = if stop
+                      then VSort (identS "...") -- hmm
+                      else f x
+
+
+linPattVars p =
+    if null dups
+    then return pvs
+    else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
+  where
+    allpvs = allPattVars p
+    pvs = nub allpvs
+    dups = allpvs \\ pvs
+
+pattVars = nub . allPattVars
+allPattVars p =
+    case p of
+      PV i    -> [i]
+      PAs i p -> i:allPattVars p
+      _       -> collectPattOp allPattVars p
+
+---
+ix loc fn xs i =
+    if i<n
+    then xs !! i
+    else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
+  where n = length xs
+
+infixl 1 #,<# --,@@
+
+f # x = fmap f x
+mf <# mx  = ap mf mx
+--m1 @@ m2 = (m1 =<<) . m2
+
+both f (x,y) = (,) # f x <# f y
+
+bugloc loc s = ppbug $ ppL loc s
+
+bug msg = ppbug msg
+ppbug doc = error $ render $ hang "Internal error in Compute.Concrete:" 4 doc

src/compiler/GF/Compile/Compute/ConcreteNew.hs

@@ -1,588 +0,0 @@
--- | Functions for computing the values of terms in the concrete syntax, in
--- | preparation for PMCFG generation.
-module GF.Compile.Compute.ConcreteNew
-           (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
-            normalForm,
-            Value(..), Bind(..), Env, value2term, eval, vapply
-           ) where
-import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
-
-import GF.Grammar hiding (Env, VGen, VApp, VRecType)
-import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
-import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
-import GF.Grammar.PatternMatch(matchPattern,measurePatt)
-import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
-import GF.Compile.Compute.Value hiding (Error)
-import GF.Compile.Compute.Predef(predef,predefName,delta)
-import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
-import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
-import GF.Data.Utilities(mapFst,mapSnd)
-import GF.Infra.Option
-import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
-import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
---import Data.Char (isUpper,toUpper,toLower)
-import GF.Text.Pretty
-import qualified Data.Map as Map
-import Debug.Trace(trace)
-
--- * Main entry points
-
-normalForm :: GlobalEnv -> L Ident -> Term -> Term
-normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
-
-nfx env@(GE _ _ _ loc) t = do
-  v <- eval env [] t
-  case value2term loc [] v of
-    Left i  -> fail ("variable #"++show i++" is out of scope")
-    Right t -> return t
-
-eval :: GlobalEnv -> Env -> Term -> Err Value
-eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
-  where
-    cenv = CE gr rvs opts loc (map fst env)
-
---apply env = apply' env
-
---------------------------------------------------------------------------------
-
--- * Environments
-
-type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
-
-data GlobalEnv = GE Grammar ResourceValues Options GLocation
-data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
-                       opts::Options,
-                       gloc::GLocation,local::LocalScope}
-type GLocation = L Ident
-type LocalScope = [Ident]
-type Stack = [Value]
-type OpenValue = Stack->Value
-
-geLoc     (GE _ _ _ loc) = loc
-geGrammar (GE gr _ _ _)  = gr
-
-ext b env = env{local=b:local env}
-extend bs env = env{local=bs++local env}
-global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
-
-var :: CompleteEnv -> Ident -> Err OpenValue
-var env x = maybe unbound pick' (elemIndex x (local env))
-  where
-    unbound = fail ("Unknown variable: "++showIdent x)
-    pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
-    err i vs = bug $ "Stack problem: "++showIdent x++": "
-                    ++unwords (map showIdent (local env))
-                    ++" => "++show (i,length vs)
-    ok v = --trace ("var "++show x++" = "++show v) $
-           v
-
-pick :: Int -> Stack -> Maybe Value
-pick 0 (v:_) = Just v
-pick i (_:vs) = pick (i-1) vs
-pick i vs = Nothing -- bug $ "pick "++show (i,vs)
-
-resource env (m,c) =
---  err bug id $
-    if isPredefCat c
-    then value0 env =<< lockRecType c defLinType -- hmm
-    else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
-  where e = fail $ "Not found: "++render m++"."++showIdent c
-
--- | Convert operators once, not every time they are looked up
-resourceValues :: Options -> SourceGrammar -> GlobalEnv
-resourceValues opts gr = env
-  where
-    env = GE gr rvs opts (L NoLoc identW)
-    rvs = Map.mapWithKey moduleResources (moduleMap gr)
-    moduleResources m = Map.mapWithKey (moduleResource m) . jments
-    moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
-                                  let loc = L l c
-                                      qloc = L l (Q (m,c))
-                                  eval (GE gr rvs opts loc) [] (traceRes qloc t)
-
-    traceRes = if flag optTrace opts
-               then traceResource
-               else const id
-
--- * Tracing
-
--- | Insert a call to the trace function under the top-level lambdas
-traceResource (L l q) t =
-  case termFormCnc t of
-    (abs,body) -> mkAbs abs (mkApp traceQ [args,body])
-      where
-        args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
-        lstr = render (l<>":"<>ppTerm Qualified 0 q)
-        traceQ = Q (cPredef,cTrace)
-
--- * Computing values
-
--- | Computing the value of a top-level term
-value0 :: CompleteEnv -> Term -> Err Value
-value0 env = eval (global env) []
-
--- | Computing the value of a term
-value :: CompleteEnv -> Term -> Err OpenValue
-value env t0 =
-  -- Each terms is traversed only once by this function, using only statically
-  -- available information. Notably, the values of lambda bound variables 
-  -- will be unknown during the term traversal phase.
-  -- The result is an OpenValue, which is a function that may be applied many
-  -- times to different dynamic values, but without the term traversal overhead
-  -- and without recomputing other statically known information.
-  -- For this to work, there should be no recursive calls under lambdas here.
-  -- Whenever we need to construct the OpenValue function with an explicit
-  -- lambda, we have to lift the recursive calls outside the lambda.
-  -- (See e.g. the rules for Let, Prod and Abs)
-{-
-  trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
-                                      brackets (fsep (map ppIdent (local env))),
-                                      ppTerm Unqualified 10 t0]) $
---}
-  errIn (render t0) $
-  case t0 of
-    Vr x   -> var env x
-    Q x@(m,f)
-      | m == cPredef -> if f==cErrorType                -- to be removed
-                        then let p = identS "P"
-                             in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
-                        else if f==cPBool
-                               then const # resource env x
-                               else const . flip VApp [] # predef f
-      | otherwise    -> const # resource env x --valueResDef (fst env) x
-    QC x   -> return $ const (VCApp x [])
-    App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
-    Let (x,(oty,t)) body -> do vb <- value (ext x env) body
-                               vt <- value env t
-                               return $ \ vs -> vb (vt vs:vs)
-    Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
-    Prod bt x t1 t2 ->
-       do vt1 <- value env t1
-          vt2 <- value (ext x env) t2
-          return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
-    Abs bt x t -> do vt <- value (ext x env) t
-                     return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
-    EInt n -> return $ const (VInt n)
-    EFloat f -> return $ const (VFloat f)
-    K s -> return $ const (VString s)
-    Empty -> return $ const (VString "")
-    Sort s | s == cTok -> return $ const (VSort cStr)        -- to be removed 
-           | otherwise -> return $ const (VSort s)
-    ImplArg t -> (VImplArg.) # value env t
-    Table p res -> liftM2 VTblType # value env p <# value env res
-    RecType rs -> do lovs <- mapPairsM (value env) rs
-                     return $ \vs->VRecType $ mapSnd ($vs) lovs
-    t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
-    FV ts   -> ((vfv .) # sequence) # mapM (value env) ts
-    R as    -> do lovs <- mapPairsM (value env.snd) as
-                  return $ \ vs->VRec $ mapSnd ($vs) lovs
-    T i cs  -> valueTable env i cs
-    V ty ts -> do pvs <- paramValues env ty
-                  ((VV ty pvs .) . sequence) # mapM (value env) ts
-    C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
-    S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
-    P t l   -> --maybe (bug $ "project "++show l++" from "++show v) id $
-               do ov <- value env t
-                  return $ \ vs -> let v = ov vs
-                                   in maybe (VP v l) id (proj l v)
-    Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
-    Strs ts    -> ((VStrs.) # sequence) # mapM (value env) ts
-    Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
-    ELin c r -> (unlockVRec (gloc env) c.) # value env r
-    EPatt p  -> return $ const (VPatt p) -- hmm
-    EPattType ty -> do vt <- value env ty
-                       return (VPattType . vt)
-    Typed t ty -> value env t
-    t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
-
-vconcat vv@(v1,v2) =
-    case vv of
-      (VString "",_) -> v2
-      (_,VString "") -> v1
-      (VApp NonExist _,_) -> v1
-      (_,VApp NonExist _) -> v2
-      _ -> VC v1 v2
-
-proj l v | isLockLabel l = return (VRec [])
-                ---- a workaround 18/2/2005: take this away and find the reason
-                ---- why earlier compilation destroys the lock field
-proj l v =
-    case v of
-      VFV vs -> liftM vfv (mapM (proj l) vs)
-      VRec rs -> lookup l rs
---    VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
-      VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
-      _ -> return (ok1 VP v l)
-
-ok1 f v1@(VError {}) _ = v1
-ok1 f v1 v2 = f v1 v2
- 
-ok2 f v1@(VError {}) _ = v1
-ok2 f _ v2@(VError {}) = v2
-ok2 f v1 v2 = f v1 v2
-
-ok2p f (v1@VError {},_) = v1
-ok2p f (_,v2@VError {}) = v2
-ok2p f vv = f vv
-
-unlockVRec loc c0 v0 = v0
-{-
-unlockVRec loc c0 v0 = unlockVRec' c0 v0
-  where
-    unlockVRec' ::Ident -> Value -> Value
-    unlockVRec' c v =
-        case v of
-    --    VClosure env t -> err bug (VClosure env) (unlockRecord c t)
-          VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
-          VRec rs        -> plusVRec rs lock
-    --    _              -> VExtR v (VRec lock) -- hmm
-          _              -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
-    --    _              -> bugloc loc $ "unlock non-record "++show v0
-      where
-        lock = [(lockLabel c,VRec [])]
--}
-
--- suspicious, but backwards compatible
-plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
-  where ls2 = map fst rs2
-
-extR t vv =
-    case vv of
-      (VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
-      (v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
-      (VRecType rs1, VRecType rs2) ->
-          case intersect (map fst rs1) (map fst rs2) of
-            [] -> VRecType (rs1 ++ rs2)
-            ls -> error $ "clash"<+>show ls
-      (VRec     rs1, VRec     rs2) -> plusVRec rs1 rs2
-      (v1          , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
-      (VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
---    (v1,v2) -> ok2 VExtR v1 v2 -- hmm
-      (v1,v2) -> error $ "not records" $$ show v1 $$ show v2
-  where
-    error explain = ppbug $ "The term" <+> t
-                            <+> "is not reducible" $$ explain
-
-glue env (v1,v2) = glu v1 v2
-  where
-    glu v1 v2 =
-        case (v1,v2) of
-          (VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
-          (v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
-          (VString s1,VString s2) -> VString (s1++s2)
-          (v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
-             where glx v2 = glu v1 v2
-          (v1@(VAlts {}),v2) ->
-           --err (const (ok2 VGlue v1 v2)) id $
-             err bug id $
-             do y' <- strsFromValue v2
-                x' <- strsFromValue v1
-                return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
-          (VC va vb,v2) -> VC va (glu vb v2)
-          (v1,VC va vb) -> VC (glu v1 va) vb
-          (VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
-          (v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
-          (v1@(VApp NonExist _),_) -> v1
-          (_,v2@(VApp NonExist _)) -> v2
---        (v1,v2) -> ok2 VGlue v1 v2
-          (v1,v2) -> if flag optPlusAsBind (opts env)
-                       then VC v1 (VC (VApp BIND []) v2)
-                       else let loc  = gloc env
-                                vt v = case value2term loc (local env) v of
-                                         Left i  -> Error ('#':show i)
-                                         Right t -> t
-                                originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
-                                                               (Glue (vt v1) (vt v2)))
-                                term = render $ pp  $ Glue (vt v1) (vt v2)
-                            in error $ unlines
-                                [originalMsg
-                                ,""
-                                ,"There was a problem in the expression `"++term++"`, either:"
-                                ,"1) You are trying to use + on runtime arguments, possibly via an oper."
-                                ,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
-                                ,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
-                                ]
-
-
--- | to get a string from a value that represents a sequence of terminals
-strsFromValue :: Value -> Err [Str]
-strsFromValue t = case t of
-  VString s   -> return [str s]
-  VC s t -> do
-    s' <- strsFromValue s
-    t' <- strsFromValue t
-    return [plusStr x y | x <- s', y <- t']
-{-
-  VGlue s t -> do
-    s' <- strsFromValue s
-    t' <- strsFromValue t
-    return [glueStr x y | x <- s', y <- t']
--}
-  VAlts d vs -> do
-    d0 <- strsFromValue d
-    v0 <- mapM (strsFromValue . fst) vs
-    c0 <- mapM (strsFromValue . snd) vs
-  --let vs' = zip v0 c0
-    return [strTok (str2strings def) vars | 
-              def  <- d0,
-              vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] | 
-                                                          vv <- sequence v0]
-           ]
-  VFV ts -> concat # mapM strsFromValue ts
-  VStrs ts -> concat # mapM strsFromValue ts
-
-  _ -> fail ("cannot get Str from value " ++ show t)
-
-vfv vs = case nub vs of
-           [v] -> v
-           vs -> VFV vs
-
-select env vv =
-    case vv of
-      (v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
-      (VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
-      (v1@(VV pty vs rs),v2) ->
-         err (const (VS v1 v2)) id $
-         do --ats <- allParamValues (srcgr env) pty
-            --let vs = map (value0 env) ats
-            i <- maybeErr "no match" $ findIndex (==v2) vs
-            return (ix (gloc env) "select" rs i)
-      (VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
-      (v1@(VT _ _ cs),v2) ->
-                 err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
-                 match (gloc env) cs v2
-      (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
-      (v1,v2) -> ok2 VS v1 v2
-
-match loc cs v = 
-  case value2term loc [] v of
-    Left i  -> bad ("variable #"++show i++" is out of scope")
-    Right t -> err bad return (matchPattern cs t)
-  where
-    bad = fail . ("In pattern matching: "++)
-
-valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
-valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
-
-valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
-valueTable env i cs =
-    case i of
-      TComp ty -> do pvs <- paramValues env ty
-                     ((VV ty pvs .) # sequence) # mapM (value env.snd) cs
-      _ -> do ty <- getTableType i
-              cs' <- mapM valueCase cs
-              err (dynamic cs' ty) return (convert cs' ty)
-  where
-    dynamic cs' ty _ = cases cs' # value env ty
-
-    cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
-      where
-        keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
-                   VT wild (vty vs) (mapSnd ($vs) cs')
-
-    wild = case i of TWild _ -> True; _ -> False
-
-    convertv cs' vty = 
-      case value2term (gloc env) [] vty of
-        Left i    -> fail ("variable #"++show i++" is out of scope")
-        Right pty -> convert' cs' =<< paramValues'' env pty
-
-    convert cs' ty = convert' cs' =<< paramValues' env ty
-
-    convert' cs' ((pty,vs),pvs) =
-      do sts  <- mapM (matchPattern cs') vs
-         return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
-                                           (mapFst ($vs) sts)
-
-    valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
-                         pvs <- linPattVars p'
-                         vt <- value (extend pvs env) t
-                         return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
-
-    inlinePattMacro p =
-        case p of
-          PM qc -> do r <- resource env qc
-                      case r of
-                        VPatt p' -> inlinePattMacro p'
-                        _ -> ppbug $ hang "Expected pattern macro:" 4
-                                          (show r)
-          _ -> composPattOp inlinePattMacro p
-
-
-paramValues env ty = snd # paramValues' env ty
-
-paramValues' env ty = paramValues'' env =<< nfx (global env) ty
-
-paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
-                           pvs <- mapM (eval (global env) []) ats
-                           return ((pty,ats),pvs)
-
-push' p bs xs = if length bs/=length xs
-                then bug $ "push "++show (p,bs,xs)
-                else push bs xs
-
-push :: Env -> LocalScope -> Stack -> Stack
-push bs [] vs = vs
-push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
-  where  err = bug $ "Unbound pattern variable "++showIdent x
-
-apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
-apply' env t [] = value env t
-apply' env t vs =
-  case t of
-    QC x                   -> return $ \ svs -> VCApp x (map ($svs) vs)
-{-
-    Q x@(m,f) | m==cPredef -> return $
-                              let constr = --trace ("predef "++show x) .
-                                           VApp x 
-                              in \ svs -> maybe constr id (Map.lookup f predefs)
-                                          $ map ($svs) vs
-              | otherwise  -> do r <- resource env x
-                                 return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
--}
-    App t1 t2              -> apply' env t1 . (:vs) =<< value env t2
-    _                      -> do fv <- value env t
-                                 return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
-
-vapply :: GLocation -> Value -> [Value] -> Value
-vapply loc v [] = v
-vapply loc v vs =
-  case v of
-    VError {} -> v
---  VClosure env (Abs b x t) -> beta gr env b x t vs
-    VAbs bt _ (Bind f) -> vbeta loc bt f vs
-    VApp pre vs1 -> delta' pre (vs1++vs)
-      where
-        delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
-                                  in vtrace loc v1 vr
-        delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
-        --msg = const (VApp pre (vs1++vs))
-        msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
-    VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
-    VFV fs -> vfv [vapply loc f vs|f<-fs]
-    VCApp f vs0 -> VCApp f (vs0++vs)
-    VMeta i env vs0 -> VMeta i env (vs0++vs)
-    VGen i vs0 -> VGen i (vs0++vs)
-    v -> bug $ "vapply "++show v++" "++show vs
-
-vbeta loc bt f (v:vs) =
-  case (bt,v) of
-    (Implicit,VImplArg v) -> ap v
-    (Explicit,         v) -> ap v
-  where
-    ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
-    ap v         = vapply loc (f v) vs
-
-vary (VFV vs) = vs
-vary v = [v]
-varyList = mapM vary
-
-{-
-beta env b x t (v:vs) =
-  case (b,v) of
-    (Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
-    (Explicit,         v) -> apply' (ext (x,v) env) t vs
--}
-
-vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
-  where
-    pv v = case v of
-             VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
-             _ -> ppV v
-    pf (_,VString n) = pp n
-    pf (_,v) = ppV v
-    pa (_,v) = ppV v
-    ppV v = case value2term' True loc [] v of
-              Left i  -> "variable #" <> pp i <+> "is out of scope"
-              Right t -> ppTerm Unqualified 10 t
-
--- | Convert a value back to a term
-value2term :: GLocation -> [Ident] -> Value -> Either Int Term
-value2term = value2term' False
-value2term' stop loc xs v0 =
-  case v0 of
-    VApp pre vs    -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
-    VCApp f vs     -> liftM  (foldl App (QC f))   (mapM v2t vs)
-    VGen j vs      -> liftM2 (foldl App) (var j)  (mapM v2t vs)
-    VMeta j env vs -> liftM  (foldl App (Meta j)) (mapM v2t vs)
-    VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
-    VAbs  bt   x f -> liftM  (Abs  bt x)         (v2t' x f)
-    VInt n         -> return (EInt n)
-    VFloat f       -> return (EFloat f)
-    VString s      -> return (if null s then Empty else K s)
-    VSort s        -> return (Sort s)
-    VImplArg v     -> liftM  ImplArg (v2t v)
-    VTblType p res -> liftM2 Table (v2t p) (v2t res)
-    VRecType rs    -> liftM  RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
-    VRec as        -> liftM  R       (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
-    VV t _ vs      -> liftM  (V t)   (mapM v2t vs)
-    VT wild v cs   -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
-    VFV vs         -> liftM  FV (mapM v2t vs)
-    VC v1 v2       -> liftM2 C (v2t v1) (v2t v2)
-    VS v1 v2       -> liftM2 S (v2t v1) (v2t v2)
-    VP v l         -> v2t v >>= \t -> return (P t l)
-    VPatt p        -> return (EPatt p)
-    VPattType v    -> v2t v >>= return . EPattType
-    VAlts v vvs    -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
-    VStrs vs       -> liftM  Strs (mapM v2t vs)
---  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
---  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
-    VError err     -> return (Error err)
-  
-  where
-    v2t = v2txs xs
-    v2txs = value2term' stop loc
-    v2t' x f = v2txs (x:xs) (bind f (gen xs))
-
-    var j
-      | j<length xs = Right (Vr (reverse xs !! j))
-      | otherwise   = Left  j
-
-
-    pushs xs e = foldr push e xs
-    push x (env,xs) = ((x,gen xs):env,x:xs)
-    gen xs = VGen (length xs) []
-
-    nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
-      where (env',xs') = pushs (pattVars p) ([],xs)
-
-    bind (Bind f) x = if stop
-                      then VSort (identS "...") -- hmm
-                      else f x
-
-
-linPattVars p =
-    if null dups
-    then return pvs
-    else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
-  where
-    allpvs = allPattVars p
-    pvs = nub allpvs
-    dups = allpvs \\ pvs
-
-pattVars = nub . allPattVars
-allPattVars p =
-    case p of
-      PV i    -> [i]
-      PAs i p -> i:allPattVars p
-      _       -> collectPattOp allPattVars p
-
----
-ix loc fn xs i =
-    if i<n
-    then xs !! i
-    else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
-  where n = length xs
-
-infixl 1 #,<# --,@@
-
-f # x = fmap f x
-mf <# mx  = ap mf mx
---m1 @@ m2 = (m1 =<<) . m2
-
-both f (x,y) = (,) # f x <# f y
-
-bugloc loc s = ppbug $ ppL loc s
-
-bug msg = ppbug msg
-ppbug doc = error $ render $ hang "Internal error in Compute.ConcreteNew:" 4 doc

src/compiler/GF/Compile/Compute/Value.hs

@@ -12,8 +12,8 @@ data Value
   | VGen Int [Value] -- for lambda bound variables, possibly applied
   | VMeta MetaId Env [Value]
 -- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
-  | VAbs BindType Ident Binding -- used in Compute.ConcreteNew
+  | VAbs BindType Ident Binding -- used in Compute.Concrete
-  | VProd BindType Value Ident Binding -- used in Compute.ConcreteNew
+  | VProd BindType Value Ident Binding -- used in Compute.Concrete
   | VInt Int
   | VFloat Double
   | VString String
@@ -47,10 +47,10 @@ type Env = [(Ident,Value)]
 
 -- | Predefined functions
 data Predefined = Drop | Take | Tk | Dp | EqStr | Occur | Occurs | ToUpper
-                | ToLower | IsUpper | Length | Plus | EqInt | LessInt 
+                | ToLower | IsUpper | Length | Plus | EqInt | LessInt
              {- | Show | Read | ToStr | MapStr | EqVal -}
                 | Error | Trace
                 -- Canonical values below:
-                | PBool | PFalse | PTrue | Int | Float | Ints | NonExist 
+                | PBool | PFalse | PTrue | Int | Float | Ints | NonExist
                 | BIND | SOFT_BIND | SOFT_SPACE | CAPIT | ALL_CAPIT
                 deriving (Show,Eq,Ord,Ix,Bounded,Enum)

src/compiler/GF/Compile/GeneratePMCFG.hs

@@ -25,7 +25,7 @@ import GF.Data.BacktrackM
 import GF.Data.Operations
 import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
 import GF.Data.Utilities (updateNthM) --updateNth
-import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(normalForm,resourceValues)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Data.List as List
@@ -82,7 +82,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
                           (goB b1 CNil [])
                           (pres,pargs)
       pmcfg      = getPMCFG pmcfgEnv1
-      
+
       stats      = let PMCFG prods funs = pmcfg
                        (s,e)            = bounds funs
                        !prods_cnt       = length prods
@@ -103,7 +103,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
           newArgs  = map getFIds newArgs'
       in addFunction env0 newCat fun newArgs
 
-addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat)) 
+addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat))
                                                              mdef@(Just (L loc1 def))
                                                              mref@(Just (L loc2 ref))
                                                              mprn
@@ -162,7 +162,7 @@ pgfCncCat :: SourceGrammar -> Type -> Int -> CncCat
 pgfCncCat gr lincat index =
   let ((_,size),schema) = computeCatRange gr lincat
   in PGF.CncCat index (index+size-1)
-                      (mkArray (map (renderStyle style{mode=OneLineMode} . ppPath) 
+                      (mkArray (map (renderStyle style{mode=OneLineMode} . ppPath)
                                     (getStrPaths schema)))
   where
     getStrPaths :: Schema Identity s c -> [Path]
@@ -243,7 +243,7 @@ choices nr path = do (args,_) <- get
                                                                                                                     | (value,index) <- values])
     descend schema       path              rpath = bug $ "descend "++show (schema,path,rpath)
 
-    updateEnv path value gr c (args,seq) = 
+    updateEnv path value gr c (args,seq) =
       case updateNthM (restrictProtoFCat path value) nr args of
         Just args -> c value (args,seq)
         Nothing   -> bug "conflict in updateEnv"
@@ -606,7 +606,7 @@ restrictProtoFCat path v (PFCat cat f schema) = do
                                                        Just index -> return (CPar (m,[(v,index)]))
                                                        Nothing    -> mzero
     addConstraint CNil             v (CStr _)      = bug "restrictProtoFCat: string path"
-    
+
     update k0 f [] = return []
     update k0 f (x@(k,Identity v):xs)
       | k0 == k    = do v <- f v

src/compiler/GF/Compile/GrammarToCanonical.hs

@@ -20,7 +20,7 @@ import GF.Compile.Compute.Value(Predefined(..))
 import GF.Infra.Ident(ModuleName(..),Ident,ident2raw,rawIdentS,showIdent,isWildIdent)
 import GF.Infra.Option(Options,optionsPGF)
 import PGF.Internal(Literal(..))
-import GF.Compile.Compute.ConcreteNew(GlobalEnv,normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
 import GF.Grammar.Canonical as C
 import System.FilePath ((</>), (<.>))
 import qualified Debug.Trace as T

src/compiler/GF/Compile/Optimize.hs

@@ -6,7 +6,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/09/16 13:56:13 $ 
+-- > CVS $Date: 2005/09/16 13:56:13 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.18 $
 --
@@ -21,7 +21,7 @@ import GF.Grammar.Printer
 import GF.Grammar.Macros
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
-import GF.Compile.Compute.ConcreteNew(GlobalEnv,normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
 import GF.Data.Operations
 import GF.Infra.Option
 
@@ -90,7 +90,7 @@ evalInfo opts resenv sgr m c info = do
     let ppr' = fmap (evalPrintname resenv c) ppr
     return $ CncFun mt pde' ppr' mpmcfg -- only cat in type actually needed
 {-
-  ResOper pty pde 
+  ResOper pty pde
     | not new && OptExpand `Set.member` optim -> do
          pde' <- case pde of
                    Just (L loc de) -> do de <- computeConcrete gr de
@@ -171,13 +171,13 @@ mkLinDefault gr typ = liftM (Abs Explicit varStr) $ mkDefField typ
      _ -> Bad (render ("linearization type field cannot be" <+> typ))
 
 mkLinReference :: SourceGrammar -> Type -> Err Term
-mkLinReference gr typ = 
+mkLinReference gr typ =
- liftM (Abs Explicit varStr) $ 
+ liftM (Abs Explicit varStr) $
    case mkDefField typ (Vr varStr) of
      Bad "no string" -> return Empty
      x               -> x
  where
-   mkDefField ty trm = 
+   mkDefField ty trm =
      case ty of
        Table pty ty -> do ps <- allParamValues gr pty
                           case ps of
@@ -203,7 +203,7 @@ factor param c i t =
     T (TComp ty) cs -> factors ty [(p, factor param c (i+1) v) | (p, v) <- cs]
     _               -> composSafeOp (factor param c i) t
   where
-    factors ty pvs0  
+    factors ty pvs0
                  | not param = V ty (map snd pvs0)
     factors ty []            = V ty []
     factors ty pvs0@[(p,v)]  = V ty [v]
@@ -224,7 +224,7 @@ factor param c i t =
 replace :: Term -> Term -> Term -> Term
 replace old new trm =
   case trm of
-    -- these are the important cases, since they can correspond to patterns  
+    -- these are the important cases, since they can correspond to patterns
     QC _     | trm == old -> new
     App _ _  | trm == old -> new
     R _      | trm == old -> new

src/compiler/GF/Compile/PGFtoHaskell.hs

@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/06/17 12:39:07 $ 
+-- > CVS $Date: 2005/06/17 12:39:07 $
 -- > CVS $Author: bringert $
 -- > CVS $Revision: 1.8 $
 --
@@ -22,7 +22,7 @@ import PGF.Internal
 import GF.Data.Operations
 import GF.Infra.Option
 
-import Data.List --(isPrefixOf, find, intersperse)
+import Data.List(isPrefixOf,find,intercalate,intersperse,groupBy,sortBy)
 import qualified Data.Map as Map
 
 type Prefix = String -> String
@@ -34,11 +34,12 @@ grammar2haskell :: Options
                 -> PGF
                 -> String
 grammar2haskell opts name gr = foldr (++++) [] $
-  pragmas ++ haskPreamble gadt name derivingClause extraImports ++
+  pragmas ++ haskPreamble gadt name derivingClause (extraImports ++ pgfImports) ++
   [types, gfinstances gId lexical gr'] ++ compos
     where gr' = hSkeleton gr
           gadt = haskellOption opts HaskellGADT
           dataExt = haskellOption opts HaskellData
+          pgf2 = haskellOption opts HaskellPGF2
           lexical cat = haskellOption opts HaskellLexical && isLexicalCat opts cat
           gId | haskellOption opts HaskellNoPrefix = rmForbiddenChars
               | otherwise = ("G"++) . rmForbiddenChars
@@ -50,21 +51,23 @@ grammar2haskell opts name gr = foldr (++++) [] $
           derivingClause
                  | dataExt = "deriving (Show,Data)"
                  | otherwise = "deriving Show"
-          extraImports | gadt = ["import Control.Monad.Identity",
+          extraImports | gadt = ["import Control.Monad.Identity", "import Data.Monoid"]
-                                 "import Data.Monoid"]
                        | dataExt = ["import Data.Data"]
                        | otherwise = []
+          pgfImports | pgf2 = ["import PGF2 hiding (Tree)", "", "showCId :: CId -> String", "showCId = id"]
+                     | otherwise = ["import PGF hiding (Tree)"]
           types | gadt = datatypesGADT gId lexical gr'
                 | otherwise = datatypes gId derivingClause lexical gr'
           compos | gadt = prCompos gId lexical gr' ++ composClass
                  | otherwise = []
 
-haskPreamble gadt name derivingClause extraImports =
+haskPreamble :: Bool -> String -> String -> [String] -> [String]
+haskPreamble gadt name derivingClause imports =
  [
   "module " ++ name ++ " where",
   ""
- ] ++ extraImports ++ [
+ ] ++ imports ++ [
-  "import PGF hiding (Tree)",
+  "",
   "----------------------------------------------------",
   "-- automatic translation from GF to Haskell",
   "----------------------------------------------------",
@@ -85,10 +88,11 @@ haskPreamble gadt name derivingClause extraImports =
   ""
  ]
 
+predefInst :: Bool -> String -> String -> String -> String -> String -> String
 predefInst gadt derivingClause gtyp typ destr consr =
   (if gadt
     then []
-    else ("newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ derivingClause ++ "\n\n")
+    else "newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ derivingClause ++ "\n\n"
     )
   ++
   "instance Gf" +++ gtyp +++ "where" ++++
@@ -103,10 +107,10 @@ type OIdent = String
 type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
 
 datatypes :: Prefix -> DerivingClause -> (OIdent -> Bool) -> (String,HSkeleton) -> String
-datatypes gId derivingClause lexical = (foldr (+++++) "") . (filter (/="")) . (map (hDatatype gId derivingClause lexical)) . snd
+datatypes gId derivingClause lexical = foldr (+++++) "" . filter (/="") . map (hDatatype gId derivingClause lexical) . snd
 
 gfinstances :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
-gfinstances gId lexical (m,g) = (foldr (+++++) "") $ (filter (/="")) $ (map (gfInstance gId lexical m)) g
+gfinstances gId lexical (m,g) = foldr (+++++) "" $ filter (/="") $ map (gfInstance gId lexical m) g
 
 
 hDatatype  :: Prefix -> DerivingClause -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> String
@@ -131,16 +135,17 @@ nonLexicalRules True rules = [r | r@(f,t) <- rules, not (null t)]
 lexicalConstructor :: OIdent -> String
 lexicalConstructor cat = "Lex" ++ cat
 
+predefTypeSkel :: HSkeleton
 predefTypeSkel = [(c,[]) | c <- ["String", "Int", "Float"]]
 
 -- GADT version of data types
 datatypesGADT :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
-datatypesGADT gId lexical (_,skel) = unlines $ 
+datatypesGADT gId lexical (_,skel) = unlines $
     concatMap (hCatTypeGADT gId) (skel ++ predefTypeSkel) ++
-    [ 
+    [
-      "", 
+      "",
       "data Tree :: * -> * where"
-    ] ++ 
+    ] ++
     concatMap (map ("  "++) . hDatatypeGADT gId lexical) skel ++
     [
       "  GString :: String -> Tree GString_",
@@ -164,23 +169,23 @@ hCatTypeGADT gId (cat,rules)
        "data"+++gId cat++"_"]
 
 hDatatypeGADT :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> [String]
-hDatatypeGADT gId lexical (cat, rules) 
+hDatatypeGADT gId lexical (cat, rules)
     | isListCat (cat,rules) = [gId cat+++"::"+++"["++gId (elemCat cat)++"]" +++ "->" +++ t]
     | otherwise =
-        [ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t 
+        [ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t
           | (f,args) <- nonLexicalRules (lexical cat) rules ]
         ++ if lexical cat then [lexicalConstructor cat +++ ":: String ->"+++ t] else []
   where t = "Tree" +++ gId cat ++ "_"
 
 hEqGADT :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> [String]
 hEqGADT gId lexical (cat, rules)
-  | isListCat (cat,rules) = let r = listr cat in ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ listeqs] 
+  | isListCat (cat,rules) = let r = listr cat in ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ listeqs]
   | otherwise = ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ eqs r | r <- nonLexicalRules (lexical cat) rules]
           ++ if lexical cat then ["(" ++ lexicalConstructor cat +++ "x" ++ "," ++ lexicalConstructor cat +++ "y" ++ ") -> x == y"] else []
 
  where
    patt s (f,xs) = unwords (gId f : mkSVars s (length xs))
-   eqs (_,xs) = unwords ("and" : "[" : intersperse "," [x ++ " == " ++ y | 
+   eqs (_,xs) = unwords ("and" : "[" : intersperse "," [x ++ " == " ++ y |
      (x,y) <- zip (mkSVars "x" (length xs)) (mkSVars "y" (length xs)) ] ++ ["]"])
    listr c = (c,["foo"]) -- foo just for length = 1
    listeqs = "and [x == y | (x,y) <- zip x1 y1]"
@@ -189,25 +194,26 @@ prCompos :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> [String]
 prCompos gId lexical (_,catrules) =
     ["instance Compos Tree where",
      "  compos r a f t = case t of"]
-    ++ 
+    ++
     ["    " ++ prComposCons (gId f) xs | (c,rs) <- catrules, not (isListCat (c,rs)),
-                                         (f,xs) <- rs, not (null xs)] 
+                                         (f,xs) <- rs, not (null xs)]
-    ++ 
+    ++
     ["    " ++ prComposCons (gId c) ["x1"] | (c,rs) <- catrules, isListCat (c,rs)]
-    ++ 
+    ++
     ["    _ -> r t"]
   where
-    prComposCons f xs = let vs = mkVars (length xs) in 
+    prComposCons f xs = let vs = mkVars (length xs) in
                         f +++ unwords vs +++ "->" +++ rhs f (zip vs xs)
     rhs f vcs = "r" +++ f +++ unwords (map (prRec f) vcs)
-    prRec f (v,c) 
+    prRec f (v,c)
       | isList f  = "`a` foldr (a . a (r (:)) . f) (r [])" +++ v
       | otherwise = "`a`" +++ "f" +++ v
-    isList f = (gId "List") `isPrefixOf` f
+    isList f = gId "List" `isPrefixOf` f
 
 gfInstance :: Prefix -> (OIdent -> Bool) -> String -> (OIdent, [(OIdent, [OIdent])]) -> String
 gfInstance gId lexical m crs = hInstance gId lexical m crs ++++ fInstance gId lexical m crs
 
+hInstance :: (String -> String) -> (String -> Bool) -> String -> (String, [(OIdent, [OIdent])]) -> String
 ----hInstance m ("Cn",_) = "" --- seems to belong to an old applic. AR 18/5/2004
 hInstance gId _ m (cat,[]) = unlines [
   "instance Show" +++ gId cat,
@@ -216,15 +222,15 @@ hInstance gId _ m (cat,[]) = unlines [
   "  gf _ = undefined",
   "  fg _ = undefined"
   ]
-hInstance gId lexical m (cat,rules) 
+hInstance gId lexical m (cat,rules)
  | isListCat (cat,rules) =
   "instance Gf" +++ gId cat +++ "where" ++++
-     "  gf (" ++ gId cat +++ "[" ++ concat (intersperse "," baseVars) ++ "])" 
+     "  gf (" ++ gId cat +++ "[" ++ intercalate "," baseVars ++ "])"
            +++ "=" +++ mkRHS ("Base"++ec) baseVars ++++
-     "  gf (" ++ gId cat +++ "(x:xs)) = " 
+     "  gf (" ++ gId cat +++ "(x:xs)) = "
-           ++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")] 
+           ++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")]
 -- no show for GADTs
---     ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)" 
+--     ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)"
  | otherwise =
   "instance Gf" +++ gId cat +++ "where\n" ++
   unlines ([mkInst f xx | (f,xx) <- nonLexicalRules (lexical cat) rules]
@@ -233,19 +239,22 @@ hInstance gId lexical m (cat,rules)
    ec = elemCat cat
    baseVars = mkVars (baseSize (cat,rules))
    mkInst f xx = let xx' = mkVars (length xx) in "  gf " ++
-     (if length xx == 0 then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
+     (if null xx then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
      "=" +++ mkRHS f xx'
-   mkRHS f vars = "mkApp (mkCId \"" ++ f ++ "\")" +++ 
+   mkRHS f vars = "mkApp (mkCId \"" ++ f ++ "\")" +++
-		   "[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
+       "[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
 
+mkVars :: Int -> [String]
 mkVars = mkSVars "x"
+
+mkSVars :: String -> Int -> [String]
 mkSVars s n = [s ++ show i | i <- [1..n]]
 
 ----fInstance m ("Cn",_) = "" ---
 fInstance _ _ m (cat,[]) = ""
 fInstance gId lexical m (cat,rules) =
   "  fg t =" ++++
-  (if isList 
+  (if isList
     then "    " ++ gId cat ++ " (fgs t) where\n     fgs t = case unApp t of"
     else "    case unApp t of") ++++
   unlines [mkInst f xx | (f,xx) <- nonLexicalRules (lexical cat) rules] ++++
@@ -257,27 +266,28 @@ fInstance gId lexical m (cat,rules) =
      "      Just (i," ++
      "[" ++ prTList "," xx' ++ "])" +++
      "| i == mkCId \"" ++ f ++ "\" ->" +++ mkRHS f xx'
-       where xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
+       where
-	     mkRHS f vars 
+         xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
-		 | isList =
+         mkRHS f vars
-		     if "Base" `isPrefixOf` f 
+           | isList =
-                       then "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
+               if "Base" `isPrefixOf` f
-		       else "fg" +++ (vars !! 0) +++ ":" +++ "fgs" +++ (vars !! 1)
+                             then "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
-		 | otherwise = 
+                 else "fg" +++ (vars !! 0) +++ ":" +++ "fgs" +++ (vars !! 1)
-		     gId f +++  
+           | otherwise =
-		     prTList " " [prParenth ("fg" +++ x) | x <- vars]
+               gId f +++
+               prTList " " [prParenth ("fg" +++ x) | x <- vars]
 
 --type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
 hSkeleton :: PGF -> (String,HSkeleton)
-hSkeleton gr = 
+hSkeleton gr =
-  (showCId (absname gr), 
+  (showCId (absname gr),
-   let fs = 
+   let fs =
-         [(showCId c, [(showCId f, map showCId cs) | (f, (cs,_)) <- fs]) | 
+         [(showCId c, [(showCId f, map showCId cs) | (f, (cs,_)) <- fs]) |
                                         fs@((_, (_,c)):_) <- fns]
-   in fs ++ [(sc, []) | c <- cts, let sc = showCId c, notElem sc (["Int", "Float", "String"] ++ map fst fs)]
+   in fs ++ [(sc, []) | c <- cts, let sc = showCId c, sc `notElem` (["Int", "Float", "String"] ++ map fst fs)]
   )
  where
-   cts = Map.keys (cats (abstract gr)) 
+   cts = Map.keys (cats (abstract gr))
    fns = groupBy valtypg (sortBy valtyps (map jty (Map.assocs (funs (abstract gr)))))
    valtyps (_, (_,x)) (_, (_,y)) = compare x y
    valtypg (_, (_,x)) (_, (_,y)) = x == y
@@ -291,9 +301,10 @@ updateSkeleton cat skel rule =
 -}
 isListCat :: (OIdent, [(OIdent, [OIdent])]) -> Bool
 isListCat (cat,rules) = "List" `isPrefixOf` cat && length rules == 2
-		    && ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
+        && ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
-    where c = elemCat cat
+    where
-	  fs = map fst rules
+      c = elemCat cat
+      fs = map fst rules
 
 -- | Gets the element category of a list category.
 elemCat :: OIdent -> OIdent
@@ -310,7 +321,7 @@ baseSize (_,rules) = length bs
     where Just (_,bs) = find (("Base" `isPrefixOf`) . fst) rules
 
 composClass :: [String]
-composClass = 
+composClass =
     [
      "",
      "class Compos t where",
@@ -337,4 +348,3 @@ composClass =
      "",
      "newtype C b a = C { unC :: b }"
     ]
-

src/compiler/GF/Compile/Rename.hs

@@ -39,6 +39,7 @@ import GF.Data.Operations
 
 import Control.Monad
 import Data.List (nub,(\\))
+import qualified Data.List as L
 import qualified Data.Map as Map
 import Data.Maybe(mapMaybe)
 import GF.Text.Pretty
@@ -105,7 +106,26 @@ renameIdentTerm' env@(act,imps) t0 =
                               ts@(t:_) -> do checkWarn ("atomic term" <+> ppTerm Qualified 0 t0 $$
                                                         "conflict" <+> hsep (punctuate ',' (map (ppTerm Qualified 0) ts)) $$
                                                         "given" <+> fsep (punctuate ',' (map fst qualifs)))
-                                             return t
+                                             return (bestTerm ts) -- Heuristic for resource grammar. Returns t for all others.
+       where
+        -- Hotfix for https://github.com/GrammaticalFramework/gf-core/issues/56
+        -- Real bug is probably somewhere deeper in recognising excluded functions. /IL 2020-06-06
+        notFromCommonModule :: Term -> Bool
+        notFromCommonModule term =
+          let t = render $ ppTerm Qualified 0 term :: String
+           in not $ any (\moduleName -> moduleName `L.isPrefixOf` t)
+                        ["CommonX", "ConstructX", "ExtendFunctor"
+                        ,"MarkHTMLX", "ParamX", "TenseX", "TextX"]
+
+        -- If one of the terms comes from the common modules,
+        -- we choose the other one, because that's defined in the grammar.
+        bestTerm :: [Term] -> Term
+        bestTerm [] = error "constant not found" -- not reached: bestTerm is only called for case ts@(t:_)
+        bestTerm ts@(t:_) =
+          let notCommon = [t | t <- ts, notFromCommonModule t]
+           in case notCommon of
+                []    -> t -- All terms are from common modules, return first of original list
+                (u:_) -> u -- ≥1 terms are not from common modules, return first of those
 
 info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
 info2status mq c i = case i of

src/compiler/GF/Compile/TypeCheck/Concrete.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE PatternGuards #-}
-module GF.Compile.TypeCheck.Concrete( {-checkLType, inferLType, computeLType, ppType-} ) where
+module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
-{-
+import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
+
 import GF.Infra.CheckM
 import GF.Data.Operations
 
@@ -22,10 +23,16 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
     _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
       | isPredefConstant ty     -> return ty ---- shouldn't be needed
 
-    Q (m,ident) -> checkIn (text "module" <+> ppIdent m) $ do
+    Q (m,ident) -> checkIn ("module" <+> m) $ do
       ty' <- lookupResDef gr (m,ident)
       if ty' == ty then return ty else comp g ty' --- is this necessary to test?
 
+    AdHocOverload ts -> do
+     over <- getOverload gr g (Just typeType) t
+     case over of
+       Just (tr,_) -> return tr
+       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t)
+
     Vr ident  -> checkLookup ident g -- never needed to compute!
 
     App f a -> do
@@ -73,26 +80,26 @@ inferLType gr g trm = case trm of
 
    Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
                                                 Just ty -> return ty
-                                                Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
+                                                Nothing -> checkError ("unknown in Predef:" <+> ident)
 
    Q ident -> checks [
      termWith trm $ lookupResType gr ident >>= computeLType gr g
      ,
      lookupResDef gr ident >>= inferLType gr g
      ,
-     checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
+     checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
      ]
 
    QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
                                                  Just ty -> return ty
-                                                 Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
+                                                 Nothing -> checkError ("unknown in Predef:" <+> ident)
 
    QC ident -> checks [
        termWith trm $ lookupResType gr ident >>= computeLType gr g
        ,
        lookupResDef gr ident >>= inferLType gr g
        ,
-       checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
+       checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
        ]
 
    Vr ident -> termWith trm $ checkLookup ident g
@@ -100,7 +107,12 @@ inferLType gr g trm = case trm of
    Typed e t -> do
      t' <- computeLType gr g t
      checkLType gr g e t'
-     return (e,t')
+
+   AdHocOverload ts -> do
+     over <- getOverload gr g Nothing trm
+     case over of
+       Just trty -> return trty
+       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
 
    App f a -> do
      over <- getOverload gr g Nothing trm
@@ -110,13 +122,17 @@ inferLType gr g trm = case trm of
          (f',fty) <- inferLType gr g f
          fty' <- computeLType gr g fty
          case fty' of
-           Prod bt z arg val -> do 
+           Prod bt z arg val -> do
              a' <- justCheck g a arg
-             ty <- if isWildIdent z 
+             ty <- if isWildIdent z
                       then return val
                       else substituteLType [(bt,z,a')] val
-             return (App f' a',ty) 
+             return (App f' a',ty)
-           _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
+           _ ->
+             let term = ppTerm Unqualified 0 f
+                 funName = pp . head . words .render $ term
+              in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$
+                             "\n   ** Maybe you gave too many arguments to" <+> funName <+> "\n")
 
    S f x -> do
      (f', fty) <- inferLType gr g f
@@ -124,7 +140,7 @@ inferLType gr g trm = case trm of
        Table arg val -> do
          x'<- justCheck g x arg
          return (S f' x', val)
-       _ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
+       _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
 
    P t i -> do
      (t',ty) <- inferLType gr g t   --- ??
@@ -132,16 +148,16 @@ inferLType gr g trm = case trm of
      let tr2 = P t' i
      termWith tr2 $ case ty' of
        RecType ts -> case lookup i ts of
-                       Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
+                       Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
                        Just x  -> return x
-       _          -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
+       _          -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
-                                 text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
+                                 " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
 
    R r -> do
      let (ls,fs) = unzip r
      fsts <- mapM inferM fs
      let ts = [ty | (Just ty,_) <- fsts]
-     checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
+     checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
      return $ (R (zip ls fsts), RecType (zip ls ts))
 
    T (TTyped arg) pts -> do
@@ -152,10 +168,10 @@ inferLType gr g trm = case trm of
      checkLType gr g trm (Table arg val)
    T ti pts -> do  -- tries to guess: good in oper type inference
      let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
-     case pts' of 
+     case pts' of
-       [] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
+       [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
-----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
+----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
-       _  -> do 
+       _  -> do
          (arg,val) <- checks $ map (inferCase Nothing) pts'
          checkLType gr g trm (Table arg val)
    V arg pts -> do
@@ -166,9 +182,9 @@ inferLType gr g trm = case trm of
    K s  -> do
      if elem ' ' s
         then do
-          let ss = foldr C Empty (map K (words s))  
+          let ss = foldr C Empty (map K (words s))
           ----- removed irritating warning AR 24/5/2008
-          ----- checkWarn ("token \"" ++ s ++ 
+          ----- checkWarn ("token \"" ++ s ++
           -----              "\" converted to token list" ++ prt ss)
           return (ss, typeStr)
         else return (trm, typeStr)
@@ -179,50 +195,56 @@ inferLType gr g trm = case trm of
 
    Empty -> return (trm, typeStr)
 
-   C s1 s2 -> 
+   C s1 s2 ->
      check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
 
-   Glue s1 s2 -> 
+   Glue s1 s2 ->
      check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
 
 ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
    Strs (Cn c : ts) | c == cConflict -> do
-     checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
+     checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
      inferLType gr g (head ts)
 
    Strs ts -> do
-     ts' <- mapM (\t -> justCheck g t typeStr) ts 
+     ts' <- mapM (\t -> justCheck g t typeStr) ts
      return (Strs ts', typeStrs)
 
    Alts t aa -> do
      t'  <- justCheck g t typeStr
      aa' <- flip mapM aa (\ (c,v) -> do
-        c' <- justCheck g c typeStr 
+        c' <- justCheck g c typeStr
         v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
         return (c',v'))
      return (Alts t' aa', typeStr)
 
    RecType r -> do
      let (ls,ts) = unzip r
-     ts' <- mapM (flip (justCheck g) typeType) ts 
+     ts' <- mapM (flip (justCheck g) typeType) ts
      return (RecType (zip ls ts'), typeType)
 
    ExtR r s -> do
-     (r',rT) <- inferLType gr g r 
+
+---     over <- getOverload gr g Nothing r
+---     let r1 = maybe r fst over
+     let r1 = r ---
+
+     (r',rT) <- inferLType gr g r1
      rT'     <- computeLType gr g rT
+
      (s',sT) <- inferLType gr g s
      sT'     <- computeLType gr g sT
 
      let trm' = ExtR r' s'
-     ---- trm'    <- plusRecord r' s'
      case (rT', sT') of
        (RecType rs, RecType ss) -> do
-         rt <- plusRecType rT' sT'
+         let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields
          checkLType gr g trm' rt ---- return (trm', rt)
-       _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
+       _ | rT' == typeType && sT' == typeType -> do
-       _ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
+         return (trm', typeType)
+       _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
 
-   Sort _     -> 
+   Sort _     ->
      termWith trm $ return typeType
 
    Prod bt x a b -> do
@@ -231,7 +253,7 @@ inferLType gr g trm = case trm of
      return (Prod bt x a' b', typeType)
 
    Table p t  -> do
-     p' <- justCheck g p typeType --- check p partype! 
+     p' <- justCheck g p typeType --- check p partype!
      t' <- justCheck g t typeType
      return $ (Table p' t', typeType)
 
@@ -250,9 +272,9 @@ inferLType gr g trm = case trm of
    ELin c trm -> do
      (trm',ty) <- inferLType gr g trm
      ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
-     return $ (ELin c trm', ty') 
+     return $ (ELin c trm', ty')
 
-   _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
+   _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
 
  where
    isPredef m = elem m [cPredef,cPredefAbs]
@@ -299,7 +321,6 @@ inferLType gr g trm = case trm of
      PChars _ -> return $ typeStr
      _ -> inferLType gr g (patt2term p) >>= return . snd
 
-
 -- type inference: Nothing, type checking: Just t
 -- the latter permits matching with value type
 getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
@@ -310,15 +331,28 @@ getOverload gr g mt ot = case appForm ot of
          v <- matchOverload f typs ttys
          return $ Just v
        _ -> return Nothing
+     (AdHocOverload cs@(f:_), ts) -> do     --- the function name f is only used in error messages
+       let typs = concatMap collectOverloads cs
+       ttys <- mapM (inferLType gr g) ts
+       v <- matchOverload f typs ttys
+       return $ Just v
      _ -> return Nothing
+
  where
+   collectOverloads tr@(Q c) = case lookupOverload gr c of
+     Ok typs -> typs
+     _ -> case lookupResType gr c of
+       Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
+       _ -> []
+   collectOverloads _ = [] --- constructors QC
+
    matchOverload f typs ttys = do
      let (tts,tys) = unzip ttys
      let vfs = lookupOverloadInstance tys typs
      let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
      let showTypes ty = hsep (map ppType ty)
 
-    
+
      let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])
 
      -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
@@ -329,50 +363,57 @@ getOverload gr g mt ot = case appForm ot of
      case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
        ([(_,val,fun)],_) -> return (mkApp fun tts, val)
        ([],[(pre,val,fun)]) -> do
-         checkWarn $  text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
+         checkWarn $  "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
-                      text "for" $$
+                      "for" $$
                       nest 2 (showTypes tys) $$
-                      text "using" $$
+                      "using" $$
                       nest 2 (showTypes pre)
          return (mkApp fun tts, val)
        ([],[]) -> do
-         checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
+         checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
-                      text "for" $$
+                      maybe empty (\x -> "with value type" <+> ppType x) mt $$
+                      "for argument list" $$
                       nest 2 stysError $$
-                      text "among" $$
+                      "among alternatives" $$
-                      nest 2 (vcat stypsError) $$
+                      nest 2 (vcat stypsError)
-                      maybe empty (\x -> text "with value type" <+> ppType x) mt
+
 
        (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
          ([(val,fun)],_) -> do
            return (mkApp fun tts, val)
          ([],[(val,fun)]) -> do
-           checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
+           checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
            return (mkApp fun tts, val)
 
 ----- unsafely exclude irritating warning AR 24/5/2008
------           checkWarn $ "overloading of" +++ prt f +++ 
+-----           checkWarn $ "overloading of" +++ prt f +++
 -----             "resolved by excluding partial applications:" ++++
 -----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
 
-
+--- now forgiving ambiguity with a warning AR 1/2/2014
-         _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
+--  This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
-                           text "for" <+> hsep (map ppType tys) $$ 
+--  But it also gives a chance to ambiguous overloadings that were banned before.
-                           text "with alternatives" $$
+         (nps1,nps2) -> do
-                           nest 2 (vcat [ppType ty | (_,ty,_) <- if null vfs1 then vfs2 else vfs2])
+              checkWarn $  "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
+                  ----     "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
+                           "resolved by selecting the first of the alternatives" $$
+                           nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
+              case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
+                 [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
+                 h:_ -> return h
 
    matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
 
    unlocked v = case v of
-     RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
+     RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
      _ -> v
    ---- TODO: accept subtypes
    ---- TODO: use a trie
-   lookupOverloadInstance tys typs = 
+   lookupOverloadInstance tys typs =
-     [((pre,mkFunType rest val, t),isExact) | 
+     [((pre,mkFunType rest val, t),isExact) |
        let lt = length tys,
        (ty,(val,t)) <- typs, length ty >= lt,
-       let (pre,rest) = splitAt lt ty, 
+       let (pre,rest) = splitAt lt ty,
        let isExact = pre == tys,
        isExact || map unlocked pre == map unlocked tys
      ]
@@ -385,20 +426,21 @@ getOverload gr g mt ot = case appForm ot of
 
 checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
 checkLType gr g trm typ0 = do
-
   typ <- computeLType gr g typ0
 
   case trm of
 
     Abs bt x c -> do
       case typ of
-        Prod bt' z a b -> do 
+        Prod bt' z a b -> do
           (c',b') <- if isWildIdent z
                        then checkLType gr ((bt,x,a):g) c b
-                       else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
+                       else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
                                checkLType gr ((bt,x,a):g) c b'
-          return $ (Abs bt x c', Prod bt' x a b')
+          return $ (Abs bt x c', Prod bt' z a b')
-        _ -> checkError $ text "function type expected instead of" <+> ppType typ
+        _ -> checkError $ "function type expected instead of" <+> ppType typ $$
+                          "\n   ** Double-check that the type signature of the operation" $$
+                          "matches the number of arguments given to it.\n"
 
     App f a -> do
        over <- getOverload gr g (Just typ) trm
@@ -408,6 +450,12 @@ checkLType gr g trm typ0 = do
           (trm',ty') <- inferLType gr g trm
           termWith trm' $ checkEqLType gr g typ ty' trm'
 
+    AdHocOverload ts -> do
+      over <- getOverload gr g Nothing trm
+      case over of
+        Just trty -> return trty
+        _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
+
     Q _ -> do
        over <- getOverload gr g (Just typ) trm
        case over of
@@ -417,21 +465,21 @@ checkLType gr g trm typ0 = do
           termWith trm' $ checkEqLType gr g typ ty' trm'
 
     T _ [] ->
-      checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
+      checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
-    T _ cs -> case typ of 
+    T _ cs -> case typ of
-      Table arg val -> do 
+      Table arg val -> do
         case allParamValues gr arg of
           Ok vs -> do
             let ps0 = map fst cs
             ps <- testOvershadow ps0 vs
-            if null ps 
+            if null ps
-              then return () 
+              then return ()
-              else checkWarn (text "patterns never reached:" $$
+              else checkWarn ("patterns never reached:" $$
                               nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
           _ -> return () -- happens with variable types
         cs' <- mapM (checkCase arg val) cs
         return (T (TTyped arg) cs', typ)
-      _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType typ)
+      _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
     V arg0 vs ->
       case typ of
         Table arg1 val ->
@@ -439,51 +487,54 @@ checkLType gr g trm typ0 = do
               vs1 <- allParamValues gr arg1
               if length vs1 == length vs
                  then return ()
-                 else checkError $ text "wrong number of values in table" <+> ppTerm Unqualified 0 trm
+                 else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
               vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
               return (V arg' vs',typ)
 
     R r -> case typ of --- why needed? because inference may be too difficult
        RecType rr -> do
-         let (ls,_) = unzip rr        -- labels of expected type
+       --let (ls,_) = unzip rr        -- labels of expected type
          fsts <- mapM (checkM r) rr   -- check that they are found in the record
          return $ (R fsts, typ)       -- normalize record
 
-       _ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
+       _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
 
     ExtR r s -> case typ of
        _ | typ == typeType -> do
          trm' <- computeLType gr g trm
          case trm' of
-           RecType _ -> termWith trm $ return typeType
+           RecType _ -> termWith trm' $ return typeType
-           ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
+           ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
                                       -- ext t = t ** ...
-           _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
+           _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
 
        RecType rr -> do
-         (r',ty,s') <- checks [
-            do (r',ty) <- inferLType gr g r
-               return (r',ty,s)
-           ,
-            do (s',ty) <- inferLType gr g s
-               return (s',ty,r)
-           ]
 
-         case ty of
+         ll2 <- case s of
-           RecType rr1 -> do
+           R ss -> return $ map fst ss
-                let (rr0,rr2) = recParts rr rr1
+           _ -> do
-                r2 <- justCheck g r' rr0
+             (s',typ2) <- inferLType gr g s
-                s2 <- justCheck g s' rr2
+             case typ2 of
-                return $ (ExtR r2 s2, typ) 
+               RecType ss -> return $ map fst ss
-           _ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
+               _ ->  checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
-                            text "but found" <+> ppTerm Unqualified 0 ty)
+         let ll1 = [l | (l,_) <- rr, notElem l ll2]
+
+---         over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
+---         let r1 = maybe r fst over
+         let r1 = r ---
+
+         (r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
+         (s',_) <- checkLType gr g s  (RecType [field | field@(l,_) <- rr, elem l ll2])
+
+         let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
+         return (rec, typ)
 
        ExtR ty ex -> do
          r' <- justCheck g r ty
          s' <- justCheck g s ex
          return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
 
-       _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
+       _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
 
     FV vs -> do
       ttys <- mapM (flip (checkLType gr g) typ) vs
@@ -498,7 +549,7 @@ checkLType gr g trm typ0 = do
           (arg',val) <- checkLType gr g arg p
           checkEqLType gr g typ t trm
           return (S tab' arg', t)
-        _ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
+        _ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
      , do
       (arg',ty) <- inferLType gr g arg
       ty'       <- computeLType gr g ty
@@ -507,7 +558,8 @@ checkLType gr g trm typ0 = do
       ]
     Let (x,(mty,def)) body -> case mty of
       Just ty -> do
-        (def',ty') <- checkLType gr g def ty
+        (ty0,_)    <- checkLType gr g ty typeType
+        (def',ty') <- checkLType gr g def ty0
         body' <- justCheck ((Explicit,x,ty'):g) body typ
         return (Let (x,(Just ty',def')) body', typ)
       _ -> do
@@ -523,10 +575,10 @@ checkLType gr g trm typ0 = do
       termWith trm' $ checkEqLType gr g typ ty' trm'
  where
    justCheck g ty te = checkLType gr g ty te >>= return . fst
-
+{-
-   recParts rr t = (RecType rr1,RecType rr2) where 
+   recParts rr t = (RecType rr1,RecType rr2) where
-     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr 
+     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr
-
+-}
    checkM rms (l,ty) = case lookup l rms of
      Just (Just ty0,t) -> do
        checkEqLType gr g ty ty0 t
@@ -535,12 +587,12 @@ checkLType gr g trm typ0 = do
      Just (_,t) -> do
        (t',ty') <- checkLType gr g t ty
        return (l,(Just ty',t'))
-     _ -> checkError $ 
+     _ -> checkError $
-            if isLockLabel l 
+            if isLockLabel l
               then let cat = drop 5 (showIdent (label2ident l))
-                   in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <> 
+                   in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
-                      text "; try wrapping it with lin" <+> text cat
+                      "; try wrapping it with lin" <+> cat
-              else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
+              else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
 
    checkCase arg val (p,t) = do
      cont <- pattContext gr g arg p
@@ -553,7 +605,7 @@ pattContext env g typ p = case p of
   PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
     t <- lookupResType env (q,c)
     let (cont,v) = typeFormCnc t
-    checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
+    checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
               (length cont == length ps)
     checkEqLType env g typ v (patt2term p)
     mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
@@ -564,7 +616,7 @@ pattContext env g typ p = case p of
         let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
         ----- checkWarn $ prt p ++++ show pts ----- debug
         mapM (uncurry (pattContext env g)) pts >>= return . concat
-      _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
+      _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
   PT t p' -> do
     checkEqLType env g typ t (patt2term p')
     pattContext env g typ p'
@@ -577,10 +629,10 @@ pattContext env g typ p = case p of
     g1 <- pattContext env g typ p'
     g2 <- pattContext env g typ q
     let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
-    checkCond 
+    checkCond
-      (text "incompatible bindings of" <+>
+      ("incompatible bindings of" <+>
-       fsep (map ppIdent pts) <+> 
+       fsep pts <+>
-       text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
+       "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
     return g1 -- must be g1 == g2
   PSeq p q -> do
     g1 <- pattContext env g typ p
@@ -590,11 +642,11 @@ pattContext env g typ p = case p of
   PNeg p' -> noBind typ p'
 
   _ -> return [] ---- check types!
- where 
+ where
    noBind typ p' = do
     co <- pattContext env g typ p'
     if not (null co)
-      then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
+      then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
            >> return []
       else return []
 
@@ -603,9 +655,31 @@ checkEqLType gr g t u trm = do
   (b,t',u',s) <- checkIfEqLType gr g t u trm
   case b of
     True  -> return t'
-    False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
+    False ->
-                          text "expected:" <+> ppType t $$
+      let inferredType = ppTerm Qualified 0 u
-                          text "inferred:" <+> ppType u
+          expectedType = ppTerm Qualified 0 t
+          term = ppTerm Unqualified 0 trm
+          funName = pp . head . words .render $ term
+          helpfulMsg =
+            case (arrows inferredType, arrows expectedType) of
+              (0,0) -> pp "" -- None of the types is a function
+              _ -> "\n   **" <+>
+                  if expectedType `isLessApplied` inferredType
+                    then "Maybe you gave too few arguments to" <+> funName
+                    else pp "Double-check that type signature and number of arguments match."
+      in checkError $ s <+> "type of" <+> term $$
+                            "expected:" <+> expectedType $$ -- ppqType t u $$
+                            "inferred:" <+> inferredType $$ -- ppqType u t
+                            helpfulMsg
+  where
+    -- count the number of arrows in the prettyprinted term
+    arrows :: Doc -> Int
+    arrows = length . filter (=="->") . words . render
+
+    -- If prettyprinted type t has fewer arrows then prettyprinted type u,
+    -- then t is "less applied", and we can print out more helpful error msg.
+    isLessApplied :: Doc -> Doc -> Bool
+    isLessApplied t u = arrows t < arrows u
 
 checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
 checkIfEqLType gr g t u trm = do
@@ -617,60 +691,62 @@ checkIfEqLType gr g t u trm = do
     --- better: use a flag to forgive? (AR 31/1/2006)
     _ -> case missingLock [] t' u' of
       Ok lo -> do
-        checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
+        checkWarn $ "missing lock field" <+> fsep lo
         return (True,t',u',[])
       Bad s -> return (False,t',u',s)
 
   where
 
-   -- t is a subtype of u 
+   -- check that u is a subtype of t
    --- quick hack version of TC.eqVal
-   alpha g t u = case (t,u) of  
+   alpha g t u = case (t,u) of
 
      -- error (the empty type!) is subtype of any other type
      (_,u) | u == typeError -> True
 
      -- contravariance
-     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d 
+     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
-                              
+
      -- record subtyping
-     (RecType rs, RecType ts) -> all (\ (l,a) -> 
+     (RecType rs, RecType ts) -> all (\ (l,a) ->
-                                   any (\ (k,b) -> alpha g a b && l == k) ts) rs
+                                   any (\ (k,b) -> l == k && alpha g a b) ts) rs
      (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
      (ExtR r s, t) -> alpha g r t || alpha g s t
 
      -- the following say that Ints n is a subset of Int and of Ints m >= n
-     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
+     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
+     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
            | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
            | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
 
      ---- this should be made in Rename
-     (Q  (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
+     (Q  (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                    || elem n (allExtendsPlus gr m)
                                    || m == n --- for Predef
-     (QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
+     (QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                    || elem n (allExtendsPlus gr m)
-     (QC (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
+     (QC (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                    || elem n (allExtendsPlus gr m)
-     (Q  (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
+     (Q  (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                    || elem n (allExtendsPlus gr m)
 
-     (Table a b,  Table c d)  -> alpha g a c && alpha g b d
+     -- contravariance
+     (Table a b,  Table c d)  -> alpha g c a && alpha g b d
      (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
-     _                        -> t == u 
+     _                        -> t == u
      --- the following should be one-way coercions only. AR 4/1/2001
                                   || elem t sTypes && elem u sTypes
-                                  || (t == typeType && u == typePType) 
+                                  || (t == typeType && u == typePType)
-                                  || (u == typeType && t == typePType) 
+                                  || (u == typeType && t == typePType)
 
-   missingLock g t u = case (t,u) of  
+   missingLock g t u = case (t,u) of
-     (RecType rs, RecType ts) -> 
+     (RecType rs, RecType ts) ->
-       let 
+       let
-         ls = [l | (l,a) <- rs, 
+         ls = [l | (l,a) <- rs,
                    not (any (\ (k,b) -> alpha g a b && l == k) ts)]
          (locks,others) = partition isLockLabel ls
        in case others of
-         _:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
+         _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
          _ -> return locks
      -- contravariance
      (Prod _ x a b, Prod _ y c d) -> do
@@ -696,7 +772,7 @@ termWith t ct = do
   return (t,ty)
 
 -- | compositional check\/infer of binary operations
-check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> 
+check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
           Term -> Term -> Type -> Check (Term,Type)
 check2 chk con a b t = do
   a' <- chk a
@@ -708,14 +784,18 @@ ppType :: Type -> Doc
 ppType ty =
   case ty of
     RecType fs   -> case filter isLockLabel $ map fst fs of
-                      [lock] -> text (drop 5 (showIdent (label2ident lock)))
+                      [lock] -> pp (drop 5 (showIdent (label2ident lock)))
                       _      -> ppTerm Unqualified 0 ty
-    Prod _ x a b -> ppType a <+> text "->" <+> ppType b
+    Prod _ x a b -> ppType a <+> "->" <+> ppType b
     _            -> ppTerm Unqualified 0 ty
-
+{-
+ppqType :: Type -> Type -> Doc
+ppqType t u = case (ppType t, ppType u) of
+  (pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
+  (pt,_) -> pt
+-}
 checkLookup :: Ident -> Context -> Check Type
 checkLookup x g =
   case [ty | (b,y,ty) <- g, x == y] of
-    []     -> checkError (text "unknown variable" <+> ppIdent x)
+    []     -> checkError ("unknown variable" <+> x)
     (ty:_) -> return ty
--}

src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs

@@ -10,7 +10,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType)
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
 import GF.Grammar.Lockfield
-import GF.Compile.Compute.ConcreteNew
+import GF.Compile.Compute.Concrete
 import GF.Compile.Compute.Predef(predef,predefName)
 import GF.Infra.CheckM
 import GF.Data.Operations
@@ -133,7 +133,7 @@ tcRho ge scope t@(RecType rs) (Just ty) = do
                          [] -> unifyVar ge scope i env vs vtypePType
                          _  -> return ()
     ty              -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
-                          tcError ("The record type" <+> ppTerm Unqualified 0 t $$ 
+                          tcError ("The record type" <+> ppTerm Unqualified 0 t $$
                                    "cannot be of type" <+> ppTerm Unqualified 0 ty)
   (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
   return (f (RecType rs),ty)
@@ -187,7 +187,7 @@ tcRho ge scope (R rs) (Just ty) = do
   case ty' of
     (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
                           rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
-                          return ((f . R)  rs, 
+                          return ((f . R)  rs,
                                   VRecType [(l, ty) | (l,t,ty) <- lttys]
                                  )
     ty              -> do lttys <- inferRecFields ge scope rs
@@ -277,11 +277,11 @@ tcApp ge scope (App fun arg) =                                  -- APP2
         varg <- liftErr (eval ge (scopeEnv scope) arg)
         return (App fun arg, res_ty varg)
 tcApp ge scope (Q id) =                                          -- VAR (global)
-  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> 
+  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
      do ty <- liftErr (eval ge [] ty)
         return (t,ty)
 tcApp ge scope (QC id) =                                         -- VAR (global)
-  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> 
+  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
      do ty <- liftErr (eval ge [] ty)
         return (t,ty)
 tcApp ge scope t =
@@ -350,7 +350,7 @@ tcPatt ge scope (PM q) ty0 = do
     Bad err -> tcError (pp err)
 tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
 
-inferRecFields ge scope rs = 
+inferRecFields ge scope rs =
   mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
 
 checkRecFields ge scope []          ltys
@@ -368,7 +368,7 @@ checkRecFields ge scope ((l,t):lts) ltys =
   where
     takeIt l1 []  = (Nothing, [])
     takeIt l1 (lty@(l2,ty):ltys)
-      | l1 == l2  = (Just ty,ltys) 
+      | l1 == l2  = (Just ty,ltys)
       | otherwise = let (mb_ty,ltys') = takeIt l1 ltys
                     in (mb_ty,lty:ltys')
 
@@ -390,7 +390,7 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
                | s == cPType -> return mb_ty
              VMeta _ _ _     -> return mb_ty
              _               -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
-                                   tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ 
+                                   tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
                                             "cannot be of type" <+> ppTerm Unqualified 0 sort)
   (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
   return ((l,ty):rs,mb_ty)
@@ -444,11 +444,11 @@ subsCheckRho ge scope t (VApp p1 _) (VApp p2 _)                         -- Rule
   | predefName p1 == cInts && predefName p2 == cInt = return t
 subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j])           -- Rule INT2
   | predefName p1 == cInts && predefName p2 == cInts =
-      if i <= j 
+      if i <= j
         then return t
         else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
 subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
-  let mkAccess scope t = 
+  let mkAccess scope t =
         case t of
           ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
                            (scope,mkProj2,mkWrap2) <- mkAccess scope t2
@@ -557,7 +557,7 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
 unify ge scope v1 v2 = do
   t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
   t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
-  tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ 
+  tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
                                       ppTerm Unqualified 0 t2))
 
 -- | Invariant: tv1 is a flexible type variable
@@ -609,7 +609,7 @@ quantify ge scope t tvs ty0 = do
   ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
   let used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
       new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
-  mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way 
+  mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way
   ty <- zonkTerm ty                  -- of doing the substitution
   vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
   return (foldr (Abs Implicit) t new_bndrs,vty)
@@ -619,7 +619,7 @@ quantify ge scope t tvs ty0 = do
     bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1  ++ bndrs t2
     bndrs _                = []
 
-allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,... 
+allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,...
 allBinders = [ identS [x]          | x <- ['a'..'z'] ] ++
              [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
 
@@ -688,12 +688,12 @@ runTcM f = case unTcM f IntMap.empty [] of
              TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
 
 newMeta :: Scope -> Sigma -> TcM MetaId
-newMeta scope ty = TcM (\ms msgs -> 
+newMeta scope ty = TcM (\ms msgs ->
   let i = IntMap.size ms
   in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
 
 getMeta :: MetaId -> TcM MetaValue
-getMeta i = TcM (\ms msgs -> 
+getMeta i = TcM (\ms msgs ->
   case IntMap.lookup i ms of
     Just mv -> TcOk mv ms msgs
     Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
@@ -702,7 +702,7 @@ setMeta :: MetaId -> MetaValue -> TcM ()
 setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
 
 newVar :: Scope -> Ident
-newVar scope = head [x | i <- [1..], 
+newVar scope = head [x | i <- [1..],
                          let x = identS ('v':show i),
                          isFree scope x]
   where
@@ -721,7 +721,7 @@ getMetaVars loc sc_tys = do
   return (foldr go [] tys)
   where
     -- Get the MetaIds from a term; no duplicates in result
-    go (Vr tv)    acc = acc 
+    go (Vr tv)    acc = acc
     go (App x y)  acc = go x (go y acc)
     go (Meta i)   acc
 	  | i `elem` acc  = acc
@@ -741,7 +741,7 @@ getFreeVars loc sc_tys = do
   tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
   return (foldr (go []) [] tys)
   where
-    go bound (Vr tv)            acc 
+    go bound (Vr tv)            acc
 	  | tv `elem` bound             = acc
 	  | tv `elem` acc               = acc
 	  | otherwise                   = tv : acc
@@ -771,7 +771,7 @@ tc_value2term loc xs v =
 
 
 
-data TcA x a 
+data TcA x a
   = TcSingle   (MetaStore -> [Message] -> TcResult a)
   | TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])
 

src/compiler/GF/Compile/TypeCheck/RConcrete.hs

@@ -1,801 +0,0 @@
-{-# LANGUAGE PatternGuards #-}
-module GF.Compile.TypeCheck.RConcrete( checkLType, inferLType, computeLType, ppType ) where
-import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
-
-import GF.Infra.CheckM
-import GF.Data.Operations
-
-import GF.Grammar
-import GF.Grammar.Lookup
-import GF.Grammar.Predef
-import GF.Grammar.PatternMatch
-import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
-import GF.Compile.TypeCheck.Primitives
-
-import Data.List
-import Control.Monad
-import GF.Text.Pretty
-
-computeLType :: SourceGrammar -> Context -> Type -> Check Type
-computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
- where
-  comp g ty = case ty of
-    _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
-      | isPredefConstant ty     -> return ty ---- shouldn't be needed
-
-    Q (m,ident) -> checkIn ("module" <+> m) $ do
-      ty' <- lookupResDef gr (m,ident)
-      if ty' == ty then return ty else comp g ty' --- is this necessary to test?
-
-    AdHocOverload ts -> do
-     over <- getOverload gr g (Just typeType) t
-     case over of
-       Just (tr,_) -> return tr
-       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t) 
-
-    Vr ident  -> checkLookup ident g -- never needed to compute!
-
-    App f a -> do
-      f' <- comp g f
-      a' <- comp g a
-      case f' of
-        Abs b x t -> comp ((b,x,a'):g) t
-        _ -> return $ App f' a'
-
-    Prod bt x a b -> do
-      a' <- comp g a
-      b' <- comp ((bt,x,Vr x) : g) b
-      return $ Prod bt x a' b'
-
-    Abs bt x b -> do
-      b' <- comp ((bt,x,Vr x):g) b
-      return $ Abs bt x b'
-
-    Let (x,(_,a)) b -> comp ((Explicit,x,a):g) b
-
-    ExtR r s -> do
-      r' <- comp g r
-      s' <- comp g s
-      case (r',s') of
-        (RecType rs, RecType ss) -> plusRecType r' s' >>= comp g
-        _ -> return $ ExtR r' s'
-
-    RecType fs -> do
-      let fs' = sortRec fs
-      liftM RecType $ mapPairsM (comp g) fs'
-
-    ELincat c t -> do
-      t' <- comp g t
-      lockRecType c t' ---- locking to be removed AR 20/6/2009
-
-    _ | ty == typeTok -> return typeStr
-    _ | isPredefConstant ty -> return ty
-
-    _ -> composOp (comp g) ty
-
--- the underlying algorithms
-
-inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
-inferLType gr g trm = case trm of
-
-   Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
-                                                Just ty -> return ty
-                                                Nothing -> checkError ("unknown in Predef:" <+> ident)
-
-   Q ident -> checks [
-     termWith trm $ lookupResType gr ident >>= computeLType gr g
-     ,
-     lookupResDef gr ident >>= inferLType gr g
-     ,
-     checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
-     ]
-
-   QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
-                                                 Just ty -> return ty
-                                                 Nothing -> checkError ("unknown in Predef:" <+> ident)
-
-   QC ident -> checks [
-       termWith trm $ lookupResType gr ident >>= computeLType gr g
-       ,
-       lookupResDef gr ident >>= inferLType gr g
-       ,
-       checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
-       ]
-
-   Vr ident -> termWith trm $ checkLookup ident g
-
-   Typed e t -> do
-     t' <- computeLType gr g t
-     checkLType gr g e t'
-
-   AdHocOverload ts -> do
-     over <- getOverload gr g Nothing trm
-     case over of
-       Just trty -> return trty
-       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) 
-
-   App f a -> do
-     over <- getOverload gr g Nothing trm
-     case over of
-       Just trty -> return trty
-       _ -> do
-         (f',fty) <- inferLType gr g f
-         fty' <- computeLType gr g fty
-         case fty' of
-           Prod bt z arg val -> do 
-             a' <- justCheck g a arg
-             ty <- if isWildIdent z 
-                      then return val
-                      else substituteLType [(bt,z,a')] val
-             return (App f' a',ty)
-           _ ->
-             let term = ppTerm Unqualified 0 f
-                 funName = pp . head . words .render $ term
-              in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$
-                             "\n   ** Maybe you gave too many arguments to" <+> funName <+> "\n")
-
-   S f x -> do
-     (f', fty) <- inferLType gr g f
-     case fty of
-       Table arg val -> do
-         x'<- justCheck g x arg
-         return (S f' x', val)
-       _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
-
-   P t i -> do
-     (t',ty) <- inferLType gr g t   --- ??
-     ty' <- computeLType gr g ty
-     let tr2 = P t' i
-     termWith tr2 $ case ty' of
-       RecType ts -> case lookup i ts of
-                       Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
-                       Just x  -> return x
-       _          -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
-                                 " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
-
-   R r -> do
-     let (ls,fs) = unzip r
-     fsts <- mapM inferM fs
-     let ts = [ty | (Just ty,_) <- fsts]
-     checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
-     return $ (R (zip ls fsts), RecType (zip ls ts))
-
-   T (TTyped arg) pts -> do
-     (_,val) <- checks $ map (inferCase (Just arg)) pts
-     checkLType gr g trm (Table arg val)
-   T (TComp arg) pts -> do
-     (_,val) <- checks $ map (inferCase (Just arg)) pts
-     checkLType gr g trm (Table arg val)
-   T ti pts -> do  -- tries to guess: good in oper type inference
-     let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
-     case pts' of 
-       [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
-----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
-       _  -> do 
-         (arg,val) <- checks $ map (inferCase Nothing) pts'
-         checkLType gr g trm (Table arg val)
-   V arg pts -> do
-     (_,val) <- checks $ map (inferLType gr g) pts
---   return (trm, Table arg val) -- old, caused issue 68
-     checkLType gr g trm (Table arg val)
-
-   K s  -> do
-     if elem ' ' s
-        then do
-          let ss = foldr C Empty (map K (words s))  
-          ----- removed irritating warning AR 24/5/2008
-          ----- checkWarn ("token \"" ++ s ++ 
-          -----              "\" converted to token list" ++ prt ss)
-          return (ss, typeStr)
-        else return (trm, typeStr)
-
-   EInt i -> return (trm, typeInt)
-
-   EFloat i -> return (trm, typeFloat)
-
-   Empty -> return (trm, typeStr)
-
-   C s1 s2 -> 
-     check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
-
-   Glue s1 s2 -> 
-     check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
-
----- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
-   Strs (Cn c : ts) | c == cConflict -> do
-     checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
-     inferLType gr g (head ts)
-
-   Strs ts -> do
-     ts' <- mapM (\t -> justCheck g t typeStr) ts 
-     return (Strs ts', typeStrs)
-
-   Alts t aa -> do
-     t'  <- justCheck g t typeStr
-     aa' <- flip mapM aa (\ (c,v) -> do
-        c' <- justCheck g c typeStr 
-        v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
-        return (c',v'))
-     return (Alts t' aa', typeStr)
-
-   RecType r -> do
-     let (ls,ts) = unzip r
-     ts' <- mapM (flip (justCheck g) typeType) ts 
-     return (RecType (zip ls ts'), typeType)
-
-   ExtR r s -> do
-   
----     over <- getOverload gr g Nothing r
----     let r1 = maybe r fst over
-     let r1 = r --- 
-
-     (r',rT) <- inferLType gr g r1
-     rT'     <- computeLType gr g rT
-     
-     (s',sT) <- inferLType gr g s
-     sT'     <- computeLType gr g sT
-
-     let trm' = ExtR r' s'
-     case (rT', sT') of
-       (RecType rs, RecType ss) -> do
-         let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields 
-         checkLType gr g trm' rt ---- return (trm', rt)
-       _ | rT' == typeType && sT' == typeType -> do
-         return (trm', typeType)
-       _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
-
-   Sort _     -> 
-     termWith trm $ return typeType
-
-   Prod bt x a b -> do
-     a' <- justCheck g a typeType
-     b' <- justCheck ((bt,x,a'):g) b typeType
-     return (Prod bt x a' b', typeType)
-
-   Table p t  -> do
-     p' <- justCheck g p typeType --- check p partype! 
-     t' <- justCheck g t typeType
-     return $ (Table p' t', typeType)
-
-   FV vs -> do
-     (_,ty) <- checks $ map (inferLType gr g) vs
----     checkIfComplexVariantType trm ty
-     checkLType gr g trm ty
-
-   EPattType ty -> do
-     ty' <- justCheck g ty typeType
-     return (EPattType ty',typeType)
-   EPatt p -> do
-     ty <- inferPatt p
-     return (trm, EPattType ty)
-
-   ELin c trm -> do
-     (trm',ty) <- inferLType gr g trm
-     ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
-     return $ (ELin c trm', ty') 
-
-   _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
-
- where
-   isPredef m = elem m [cPredef,cPredefAbs]
-
-   justCheck g ty te = checkLType gr g ty te >>= return . fst
-
-   -- for record fields, which may be typed
-   inferM (mty, t) = do
-     (t', ty') <- case mty of
-       Just ty -> checkLType gr g t ty
-       _ -> inferLType gr g t
-     return (Just ty',t')
-
-   inferCase mty (patt,term) = do
-     arg  <- maybe (inferPatt patt) return mty
-     cont <- pattContext gr g arg patt
-     (_,val) <- inferLType gr (reverse cont ++ g) term
-     return (arg,val)
-   isConstPatt p = case p of
-     PC _ ps -> True --- all isConstPatt ps
-     PP _ ps -> True --- all isConstPatt ps
-     PR ps -> all (isConstPatt . snd) ps
-     PT _ p -> isConstPatt p
-     PString _ -> True
-     PInt _ -> True
-     PFloat _ -> True
-     PChar -> True
-     PChars _ -> True
-     PSeq p q -> isConstPatt p && isConstPatt q
-     PAlt p q -> isConstPatt p && isConstPatt q
-     PRep p -> isConstPatt p
-     PNeg p -> isConstPatt p
-     PAs _ p -> isConstPatt p
-     _ -> False
-
-   inferPatt p = case p of
-     PP (q,c) ps | q /= cPredef -> liftM valTypeCnc (lookupResType gr (q,c))
-     PAs _ p  -> inferPatt p
-     PNeg p   -> inferPatt p
-     PAlt p q -> checks [inferPatt p, inferPatt q]
-     PSeq _ _ -> return $ typeStr
-     PRep _   -> return $ typeStr
-     PChar    -> return $ typeStr
-     PChars _ -> return $ typeStr
-     _ -> inferLType gr g (patt2term p) >>= return . snd
-
--- type inference: Nothing, type checking: Just t
--- the latter permits matching with value type
-getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
-getOverload gr g mt ot = case appForm ot of
-     (f@(Q c), ts) -> case lookupOverload gr c of
-       Ok typs -> do
-         ttys <- mapM (inferLType gr g) ts
-         v <- matchOverload f typs ttys
-         return $ Just v
-       _ -> return Nothing
-     (AdHocOverload cs@(f:_), ts) -> do     --- the function name f is only used in error messages
-       let typs = concatMap collectOverloads cs
-       ttys <- mapM (inferLType gr g) ts
-       v <- matchOverload f typs ttys
-       return $ Just v
-     _ -> return Nothing
-     
- where
-   collectOverloads tr@(Q c) = case lookupOverload gr c of 
-     Ok typs -> typs
-     _ -> case lookupResType gr c of
-       Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
-       _ -> []
-   collectOverloads _ = [] --- constructors QC
-
-   matchOverload f typs ttys = do
-     let (tts,tys) = unzip ttys
-     let vfs = lookupOverloadInstance tys typs
-     let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
-     let showTypes ty = hsep (map ppType ty)
-
-    
-     let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])
-
-     -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
-     let (stysError,stypsError) = if elem (render stys) (map render styps)
-            then (hsep (map (ppTerm Unqualified 0) tys), [hsep (map (ppTerm Unqualified 0) ty) | (ty,_) <- typs])
-            else (stys,styps)
-
-     case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
-       ([(_,val,fun)],_) -> return (mkApp fun tts, val)
-       ([],[(pre,val,fun)]) -> do
-         checkWarn $  "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
-                      "for" $$
-                      nest 2 (showTypes tys) $$
-                      "using" $$
-                      nest 2 (showTypes pre)
-         return (mkApp fun tts, val)
-       ([],[]) -> do
-         checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
-                      maybe empty (\x -> "with value type" <+> ppType x) mt $$
-                      "for argument list" $$
-                      nest 2 stysError $$
-                      "among alternatives" $$
-                      nest 2 (vcat stypsError) 
-
-
-       (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
-         ([(val,fun)],_) -> do
-           return (mkApp fun tts, val)
-         ([],[(val,fun)]) -> do
-           checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
-           return (mkApp fun tts, val)
-
------ unsafely exclude irritating warning AR 24/5/2008
------           checkWarn $ "overloading of" +++ prt f +++ 
------             "resolved by excluding partial applications:" ++++
------             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
-
---- now forgiving ambiguity with a warning AR 1/2/2014
---  This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before. 
---  But it also gives a chance to ambiguous overloadings that were banned before. 
-         (nps1,nps2) -> do 
-              checkWarn $  "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
-                  ----     "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$ 
-                           "resolved by selecting the first of the alternatives" $$
-                           nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
-              case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
-                 [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
-                 h:_ -> return h
-
-   matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
-
-   unlocked v = case v of
-     RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
-     _ -> v
-   ---- TODO: accept subtypes
-   ---- TODO: use a trie
-   lookupOverloadInstance tys typs = 
-     [((pre,mkFunType rest val, t),isExact) | 
-       let lt = length tys,
-       (ty,(val,t)) <- typs, length ty >= lt,
-       let (pre,rest) = splitAt lt ty, 
-       let isExact = pre == tys,
-       isExact || map unlocked pre == map unlocked tys
-     ]
-
-   noProds vfs = [(v,f) | (_,v,f) <- vfs, noProd v]
-
-   noProd ty = case ty of
-     Prod _ _ _ _ -> False
-     _ -> True
-
-checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
-checkLType gr g trm typ0 = do
-  typ <- computeLType gr g typ0
-
-  case trm of
-
-    Abs bt x c -> do
-      case typ of
-        Prod bt' z a b -> do 
-          (c',b') <- if isWildIdent z
-                       then checkLType gr ((bt,x,a):g) c b
-                       else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
-                               checkLType gr ((bt,x,a):g) c b'
-          return $ (Abs bt x c', Prod bt' z a b')
-        _ -> checkError $ "function type expected instead of" <+> ppType typ $$
-                          "\n   ** Double-check that the type signature of the operation" $$
-                          "matches the number of arguments given to it.\n"
-
-    App f a -> do
-       over <- getOverload gr g (Just typ) trm
-       case over of
-         Just trty -> return trty
-         _ -> do
-          (trm',ty') <- inferLType gr g trm
-          termWith trm' $ checkEqLType gr g typ ty' trm'
-
-    AdHocOverload ts -> do
-      over <- getOverload gr g Nothing trm
-      case over of
-        Just trty -> return trty
-        _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) 
-
-    Q _ -> do
-       over <- getOverload gr g (Just typ) trm
-       case over of
-         Just trty -> return trty
-         _ -> do
-          (trm',ty') <- inferLType gr g trm
-          termWith trm' $ checkEqLType gr g typ ty' trm'
-
-    T _ [] ->
-      checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
-    T _ cs -> case typ of 
-      Table arg val -> do 
-        case allParamValues gr arg of
-          Ok vs -> do
-            let ps0 = map fst cs
-            ps <- testOvershadow ps0 vs
-            if null ps 
-              then return () 
-              else checkWarn ("patterns never reached:" $$
-                              nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
-          _ -> return () -- happens with variable types
-        cs' <- mapM (checkCase arg val) cs
-        return (T (TTyped arg) cs', typ)
-      _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
-    V arg0 vs ->
-      case typ of
-        Table arg1 val ->
-           do arg' <- checkEqLType gr g arg0 arg1 trm
-              vs1 <- allParamValues gr arg1
-              if length vs1 == length vs
-                 then return ()
-                 else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
-              vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
-              return (V arg' vs',typ)
-
-    R r -> case typ of --- why needed? because inference may be too difficult
-       RecType rr -> do
-       --let (ls,_) = unzip rr        -- labels of expected type
-         fsts <- mapM (checkM r) rr   -- check that they are found in the record
-         return $ (R fsts, typ)       -- normalize record
-
-       _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
-
-    ExtR r s -> case typ of
-       _ | typ == typeType -> do
-         trm' <- computeLType gr g trm
-         case trm' of
-           RecType _ -> termWith trm' $ return typeType
-           ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType 
-                                      -- ext t = t ** ...
-           _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
-
-       RecType rr -> do
-
-         ll2 <- case s of
-           R ss -> return $ map fst ss
-           _ -> do
-             (s',typ2) <- inferLType gr g s
-             case typ2 of
-               RecType ss -> return $ map fst ss
-               _ ->  checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
-         let ll1 = [l | (l,_) <- rr, notElem l ll2]
-
----         over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
----         let r1 = maybe r fst over
-         let r1 = r ---
-         
-         (r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
-         (s',_) <- checkLType gr g s  (RecType [field | field@(l,_) <- rr, elem l ll2])
-
-         let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
-         return (rec, typ)
-
-       ExtR ty ex -> do
-         r' <- justCheck g r ty
-         s' <- justCheck g s ex
-         return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
-
-       _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
-
-    FV vs -> do
-      ttys <- mapM (flip (checkLType gr g) typ) vs
----      checkIfComplexVariantType trm typ
-      return (FV (map fst ttys), typ) --- typ' ?
-
-    S tab arg -> checks [ do
-      (tab',ty) <- inferLType gr g tab
-      ty'       <- computeLType gr g ty
-      case ty' of
-        Table p t -> do
-          (arg',val) <- checkLType gr g arg p
-          checkEqLType gr g typ t trm
-          return (S tab' arg', t)
-        _ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
-     , do
-      (arg',ty) <- inferLType gr g arg
-      ty'       <- computeLType gr g ty
-      (tab',_)  <- checkLType gr g tab (Table ty' typ)
-      return (S tab' arg', typ)
-      ]
-    Let (x,(mty,def)) body -> case mty of
-      Just ty -> do
-        (ty0,_)    <- checkLType gr g ty typeType
-        (def',ty') <- checkLType gr g def ty0
-        body' <- justCheck ((Explicit,x,ty'):g) body typ
-        return (Let (x,(Just ty',def')) body', typ)
-      _ -> do
-        (def',ty) <- inferLType gr g def  -- tries to infer type of local constant
-        checkLType gr g (Let (x,(Just ty,def')) body) typ
-
-    ELin c tr -> do
-      tr1 <- unlockRecord c tr
-      checkLType gr g tr1 typ
-
-    _ -> do
-      (trm',ty') <- inferLType gr g trm
-      termWith trm' $ checkEqLType gr g typ ty' trm'
- where
-   justCheck g ty te = checkLType gr g ty te >>= return . fst
-{-
-   recParts rr t = (RecType rr1,RecType rr2) where 
-     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr 
--}
-   checkM rms (l,ty) = case lookup l rms of
-     Just (Just ty0,t) -> do
-       checkEqLType gr g ty ty0 t
-       (t',ty') <- checkLType gr g t ty
-       return (l,(Just ty',t'))
-     Just (_,t) -> do
-       (t',ty') <- checkLType gr g t ty
-       return (l,(Just ty',t'))
-     _ -> checkError $ 
-            if isLockLabel l 
-              then let cat = drop 5 (showIdent (label2ident l))
-                   in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <> 
-                      "; try wrapping it with lin" <+> cat
-              else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
-
-   checkCase arg val (p,t) = do
-     cont <- pattContext gr g arg p
-     t' <- justCheck (reverse cont ++ g) t val
-     return (p,t')
-
-pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
-pattContext env g typ p = case p of
-  PV x -> return [(Explicit,x,typ)]
-  PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
-    t <- lookupResType env (q,c)
-    let (cont,v) = typeFormCnc t
-    checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
-              (length cont == length ps)
-    checkEqLType env g typ v (patt2term p)
-    mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
-  PR r -> do
-    typ' <- computeLType env g typ
-    case typ' of
-      RecType t -> do
-        let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
-        ----- checkWarn $ prt p ++++ show pts ----- debug
-        mapM (uncurry (pattContext env g)) pts >>= return . concat
-      _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
-  PT t p' -> do
-    checkEqLType env g typ t (patt2term p')
-    pattContext env g typ p'
-
-  PAs x p -> do
-    g' <- pattContext env g typ p
-    return ((Explicit,x,typ):g')
-
-  PAlt p' q -> do
-    g1 <- pattContext env g typ p'
-    g2 <- pattContext env g typ q
-    let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
-    checkCond 
-      ("incompatible bindings of" <+>
-       fsep pts <+> 
-       "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
-    return g1 -- must be g1 == g2
-  PSeq p q -> do
-    g1 <- pattContext env g typ p
-    g2 <- pattContext env g typ q
-    return $ g1 ++ g2
-  PRep p' -> noBind typeStr p'
-  PNeg p' -> noBind typ p'
-
-  _ -> return [] ---- check types!
- where 
-   noBind typ p' = do
-    co <- pattContext env g typ p'
-    if not (null co)
-      then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
-           >> return []
-      else return []
-
-checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
-checkEqLType gr g t u trm = do
-  (b,t',u',s) <- checkIfEqLType gr g t u trm
-  case b of
-    True  -> return t'
-    False ->
-      let inferredType = ppTerm Qualified 0 u
-          expectedType = ppTerm Qualified 0 t
-          term = ppTerm Unqualified 0 trm
-          funName = pp . head . words .render $ term
-          helpfulMsg =
-            case (arrows inferredType, arrows expectedType) of
-              (0,0) -> pp "" -- None of the types is a function
-              _ -> "\n   **" <+> 
-                  if expectedType `isLessApplied` inferredType
-                    then "Maybe you gave too few arguments to" <+> funName
-                    else pp "Double-check that type signature and number of arguments match."
-      in checkError $ s <+> "type of" <+> term $$
-                            "expected:" <+> expectedType $$ -- ppqType t u $$
-                            "inferred:" <+> inferredType $$ -- ppqType u t
-                            helpfulMsg
-  where
-    -- count the number of arrows in the prettyprinted term
-    arrows :: Doc -> Int
-    arrows = length . filter (=="->") . words . render
-
-    -- If prettyprinted type t has fewer arrows then prettyprinted type u,
-    -- then t is "less applied", and we can print out more helpful error msg.
-    isLessApplied :: Doc -> Doc -> Bool
-    isLessApplied t u = arrows t < arrows u
-
-checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
-checkIfEqLType gr g t u trm = do
-  t' <- computeLType gr g t
-  u' <- computeLType gr g u
-  case t' == u' || alpha [] t' u' of
-    True -> return (True,t',u',[])
-    -- forgive missing lock fields by only generating a warning.
-    --- better: use a flag to forgive? (AR 31/1/2006)
-    _ -> case missingLock [] t' u' of
-      Ok lo -> do
-        checkWarn $ "missing lock field" <+> fsep lo
-        return (True,t',u',[])
-      Bad s -> return (False,t',u',s)
-
-  where
-
-   -- check that u is a subtype of t
-   --- quick hack version of TC.eqVal
-   alpha g t u = case (t,u) of  
-
-     -- error (the empty type!) is subtype of any other type
-     (_,u) | u == typeError -> True
-
-     -- contravariance
-     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d 
-                              
-     -- record subtyping
-     (RecType rs, RecType ts) -> all (\ (l,a) -> 
-                                   any (\ (k,b) -> l == k && alpha g a b) ts) rs
-     (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
-     (ExtR r s, t) -> alpha g r t || alpha g s t
-
-     -- the following say that Ints n is a subset of Int and of Ints m >= n
-     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
-     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
-           | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
-           | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
-
-     ---- this should be made in Rename
-     (Q  (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
-                                   || elem n (allExtendsPlus gr m)
-                                   || m == n --- for Predef
-     (QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
-                                   || elem n (allExtendsPlus gr m)
-     (QC (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
-                                   || elem n (allExtendsPlus gr m)
-     (Q  (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) 
-                                   || elem n (allExtendsPlus gr m)
-
-     -- contravariance
-     (Table a b,  Table c d)  -> alpha g c a && alpha g b d
-     (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
-     _                        -> t == u 
-     --- the following should be one-way coercions only. AR 4/1/2001
-                                  || elem t sTypes && elem u sTypes
-                                  || (t == typeType && u == typePType) 
-                                  || (u == typeType && t == typePType) 
-
-   missingLock g t u = case (t,u) of  
-     (RecType rs, RecType ts) -> 
-       let 
-         ls = [l | (l,a) <- rs, 
-                   not (any (\ (k,b) -> alpha g a b && l == k) ts)]
-         (locks,others) = partition isLockLabel ls
-       in case others of
-         _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
-         _ -> return locks
-     -- contravariance
-     (Prod _ x a b, Prod _ y c d) -> do
-        ls1 <- missingLock g c a
-        ls2 <- missingLock g b d
-        return $ ls1 ++ ls2
-
-     _ -> Bad ""
-
-   sTypes = [typeStr, typeTok, typeString]
-
--- auxiliaries
-
--- | light-weight substitution for dep. types
-substituteLType :: Context -> Type -> Check Type
-substituteLType g t = case t of
-  Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
-  _ -> composOp (substituteLType g) t
-
-termWith :: Term -> Check Type -> Check (Term, Type)
-termWith t ct = do
-  ty <- ct
-  return (t,ty)
-
--- | compositional check\/infer of binary operations
-check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> 
-          Term -> Term -> Type -> Check (Term,Type)
-check2 chk con a b t = do
-  a' <- chk a
-  b' <- chk b
-  return (con a' b', t)
-
--- printing a type with a lock field lock_C as C
-ppType :: Type -> Doc
-ppType ty =
-  case ty of
-    RecType fs   -> case filter isLockLabel $ map fst fs of
-                      [lock] -> pp (drop 5 (showIdent (label2ident lock)))
-                      _      -> ppTerm Unqualified 0 ty
-    Prod _ x a b -> ppType a <+> "->" <+> ppType b
-    _            -> ppTerm Unqualified 0 ty
-{-
-ppqType :: Type -> Type -> Doc
-ppqType t u = case (ppType t, ppType u) of
-  (pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
-  (pt,_) -> pt
--}
-checkLookup :: Ident -> Context -> Check Type
-checkLookup x g =
-  case [ty | (b,y,ty) <- g, x == y] of
-    []     -> checkError ("unknown variable" <+> x)
-    (ty:_) -> return ty

src/compiler/GF/Infra/Option.hs

@@ -2,13 +2,13 @@ module GF.Infra.Option
     (
      -- ** Command line options
      -- *** Option types
-     Options, 
+     Options,
-     Flags(..), 
+     Flags(..),
-     Mode(..), Phase(..), Verbosity(..), 
+     Mode(..), Phase(..), Verbosity(..),
-     OutputFormat(..), 
+     OutputFormat(..),
      SISRFormat(..), Optimization(..), CFGTransform(..), HaskellOption(..),
      Dump(..), Pass(..), Recomp(..),
-     outputFormatsExpl, 
+     outputFormatsExpl,
      -- *** Option parsing
      parseOptions, parseModuleOptions, fixRelativeLibPaths,
      -- *** Option pretty-printing
@@ -47,7 +47,7 @@ import PGF.Internal(Literal(..))
 import qualified Control.Monad.Fail as Fail
 
 usageHeader :: String
-usageHeader = unlines 
+usageHeader = unlines
  ["Usage: gf [OPTIONS] [FILE [...]]",
   "",
   "How each FILE is handled depends on the file name suffix:",
@@ -90,10 +90,10 @@ data Phase = Preproc | Convert | Compile | Link
 data OutputFormat = FmtPGFPretty
                   | FmtCanonicalGF
                   | FmtCanonicalJson
-                  | FmtJavaScript 
+                  | FmtJavaScript
                   | FmtJSON
-                  | FmtPython 
+                  | FmtPython
-                  | FmtHaskell 
+                  | FmtHaskell
                   | FmtJava
                   | FmtProlog
                   | FmtBNF
@@ -102,37 +102,42 @@ data OutputFormat = FmtPGFPretty
                   | FmtNoLR
                   | FmtSRGS_XML
                   | FmtSRGS_XML_NonRec
-                  | FmtSRGS_ABNF 
+                  | FmtSRGS_ABNF
                   | FmtSRGS_ABNF_NonRec
-                  | FmtJSGF 
+                  | FmtJSGF
-                  | FmtGSL 
+                  | FmtGSL
                   | FmtVoiceXML
                   | FmtSLF
                   | FmtRegExp
                   | FmtFA
   deriving (Eq,Ord)
 
-data SISRFormat = 
+data SISRFormat =
     -- | SISR Working draft 1 April 2003
     --   <http://www.w3.org/TR/2003/WD-semantic-interpretation-20030401/>
-    SISR_WD20030401    
+    SISR_WD20030401
   | SISR_1_0
  deriving (Show,Eq,Ord)
 
 data Optimization = OptStem | OptCSE | OptExpand | OptParametrize
   deriving (Show,Eq,Ord)
 
-data CFGTransform = CFGNoLR 
+data CFGTransform = CFGNoLR
                   | CFGRegular
-                  | CFGTopDownFilter 
+                  | CFGTopDownFilter
-                  | CFGBottomUpFilter 
+                  | CFGBottomUpFilter
                   | CFGStartCatOnly
                   | CFGMergeIdentical
                   | CFGRemoveCycles
   deriving (Show,Eq,Ord)
 
-data HaskellOption = HaskellNoPrefix | HaskellGADT | HaskellLexical
+data HaskellOption = HaskellNoPrefix
-                   | HaskellConcrete | HaskellVariants | HaskellData
+                   | HaskellGADT
+                   | HaskellLexical
+                   | HaskellConcrete
+                   | HaskellVariants
+                   | HaskellData
+                   | HaskellPGF2
   deriving (Show,Eq,Ord)
 
 data Warning = WarnMissingLincat
@@ -196,7 +201,7 @@ instance Show Options where
 parseOptions :: ErrorMonad err =>
                 [String]                   -- ^ list of string arguments
              -> err (Options, [FilePath])
-parseOptions args 
+parseOptions args
   | not (null errs) = errors errs
   | otherwise       = do opts <- concatOptions `fmap` liftErr (sequence optss)
                          return (opts, files)
@@ -208,7 +213,7 @@ parseModuleOptions :: ErrorMonad err =>
                    -> err Options
 parseModuleOptions args = do
   (opts,nonopts) <- parseOptions args
-  if null nonopts 
+  if null nonopts
     then return opts
     else errors $ map ("Non-option among module options: " ++) nonopts
 
@@ -281,7 +286,7 @@ defaultFlags = Flags {
       optOptimizations   = Set.fromList [OptStem,OptCSE,OptExpand,OptParametrize],
       optOptimizePGF     = False,
       optSplitPGF        = False,
-      optCFGTransforms   = Set.fromList [CFGRemoveCycles, CFGBottomUpFilter, 
+      optCFGTransforms   = Set.fromList [CFGRemoveCycles, CFGBottomUpFilter,
                                          CFGTopDownFilter, CFGMergeIdentical],
       optLibraryPath     = [],
       optStartCat        = Nothing,
@@ -301,7 +306,7 @@ defaultFlags = Flags {
 -- | Option descriptions
 {-# NOINLINE optDescr #-}
 optDescr :: [OptDescr (Err Options)]
-optDescr = 
+optDescr =
     [
      Option ['?','h'] ["help"] (NoArg (mode ModeHelp)) "Show help message.",
      Option ['V'] ["version"] (NoArg (mode ModeVersion)) "Display GF version number.",
@@ -327,44 +332,44 @@ optDescr =
 --   Option ['t'] ["trace"] (NoArg (trace True)) "Trace computations",
 --   Option [] ["no-trace"] (NoArg (trace False)) "Don't trace computations",
      Option [] ["gfo-dir"] (ReqArg gfoDir "DIR") "Directory to put .gfo files in (default = '.').",
-     Option ['f'] ["output-format"] (ReqArg outFmt "FMT") 
+     Option ['f'] ["output-format"] (ReqArg outFmt "FMT")
         (unlines ["Output format. FMT can be one of:",
                   "Canonical GF grammar: canonical_gf, canonical_json, (and haskell with option --haskell=concrete)",
                   "Multiple concrete: pgf (default), json, js, pgf_pretty, prolog, python, ...", -- gar,
                   "Single concrete only: bnf, ebnf, fa, gsl, jsgf, regexp, slf, srgs_xml, srgs_abnf, vxml, ....", -- cf, lbnf,
                   "Abstract only: haskell, ..."]), -- prolog_abs,
-     Option [] ["sisr"] (ReqArg sisrFmt "FMT") 
+     Option [] ["sisr"] (ReqArg sisrFmt "FMT")
         (unlines ["Include SISR tags in generated speech recognition grammars.",
                   "FMT can be one of: old, 1.0"]),
-     Option [] ["haskell"] (ReqArg hsOption "OPTION") 
+     Option [] ["haskell"] (ReqArg hsOption "OPTION")
-            ("Turn on an optional feature when generating Haskell data types. OPTION = " 
+            ("Turn on an optional feature when generating Haskell data types. OPTION = "
              ++ concat (intersperse " | " (map fst haskellOptionNames))),
-     Option [] ["lexical"] (ReqArg lexicalCat "CAT[,CAT[...]]") 
+     Option [] ["lexical"] (ReqArg lexicalCat "CAT[,CAT[...]]")
             "Treat CAT as a lexical category.",
-     Option [] ["literal"] (ReqArg literalCat "CAT[,CAT[...]]") 
+     Option [] ["literal"] (ReqArg literalCat "CAT[,CAT[...]]")
             "Treat CAT as a literal category.",
-     Option ['D'] ["output-dir"] (ReqArg outDir "DIR") 
+     Option ['D'] ["output-dir"] (ReqArg outDir "DIR")
            "Save output files (other than .gfo files) in DIR.",
-     Option [] ["gf-lib-path"] (ReqArg gfLibPath "DIR") 
+     Option [] ["gf-lib-path"] (ReqArg gfLibPath "DIR")
            "Overrides the value of GF_LIB_PATH.",
-     Option [] ["src","force-recomp"] (NoArg (recomp AlwaysRecomp)) 
+     Option [] ["src","force-recomp"] (NoArg (recomp AlwaysRecomp))
                  "Always recompile from source.",
-     Option [] ["recomp-if-newer"] (NoArg (recomp RecompIfNewer)) 
+     Option [] ["recomp-if-newer"] (NoArg (recomp RecompIfNewer))
                  "(default) Recompile from source if the source is newer than the .gfo file.",
-     Option [] ["gfo","no-recomp"] (NoArg (recomp NeverRecomp)) 
+     Option [] ["gfo","no-recomp"] (NoArg (recomp NeverRecomp))
                  "Never recompile from source, if there is already .gfo file.",
      Option [] ["retain"] (NoArg (set $ \o -> o { optRetainResource = True })) "Retain opers.",
      Option [] ["probs"] (ReqArg probsFile "file.probs") "Read probabilities from file.",
-     Option ['n'] ["name"] (ReqArg name "NAME") 
+     Option ['n'] ["name"] (ReqArg name "NAME")
            (unlines ["Use NAME as the name of the output. This is used in the output file names, ",
                      "with suffixes depending on the formats, and, when relevant, ",
                      "internally in the output."]),
      Option ['i'] [] (ReqArg addLibDir "DIR") "Add DIR to the library search path.",
      Option [] ["path"] (ReqArg setLibPath "DIR:DIR:...") "Set the library search path.",
-     Option [] ["preproc"] (ReqArg preproc "CMD") 
+     Option [] ["preproc"] (ReqArg preproc "CMD")
                  (unlines ["Use CMD to preprocess input files.",
                            "Multiple preprocessors can be used by giving this option multiple times."]),
-     Option [] ["coding"] (ReqArg coding "ENCODING") 
+     Option [] ["coding"] (ReqArg coding "ENCODING")
                 ("Character encoding of the source grammar, ENCODING = utf8, latin1, cp1251, ..."),
      Option [] ["startcat"] (ReqArg startcat "CAT") "Grammar start category.",
      Option [] ["language"] (ReqArg language "LANG") "Set the speech language flag to LANG in the generated grammar.",
@@ -372,7 +377,7 @@ optDescr =
      Option [] ["unlexer"] (ReqArg unlexer "UNLEXER") "Use unlexer UNLEXER.",
      Option [] ["pmcfg"] (NoArg (pmcfg True)) "Generate PMCFG (default).",
      Option [] ["no-pmcfg"] (NoArg (pmcfg False)) "Don't generate PMCFG (useful for libraries).",
-     Option [] ["optimize"] (ReqArg optimize "OPT") 
+     Option [] ["optimize"] (ReqArg optimize "OPT")
                 "Select an optimization package. OPT = all | values | parametrize | none",
      Option [] ["optimize-pgf"] (NoArg (optimize_pgf True))
                 "Enable or disable global grammar optimization. This could significantly reduce the size of the final PGF file",
@@ -447,7 +452,7 @@ optDescr =
        optimize    x = case lookup x optimizationPackages of
                          Just p  -> set $ \o -> o { optOptimizations = p }
                          Nothing -> fail $ "Unknown optimization package: " ++ x
-                         
+
        optimize_pgf x = set $ \o -> o { optOptimizePGF = x }
        splitPGF x = set $ \o -> o { optSplitPGF = x }
 
@@ -471,7 +476,7 @@ outputFormats :: [(String,OutputFormat)]
 outputFormats = map fst outputFormatsExpl
 
 outputFormatsExpl :: [((String,OutputFormat),String)]
-outputFormatsExpl = 
+outputFormatsExpl =
     [(("pgf_pretty",   FmtPGFPretty),"human-readable pgf"),
      (("canonical_gf", FmtCanonicalGF),"Canonical GF source files"),
      (("canonical_json", FmtCanonicalJson),"Canonical JSON source files"),
@@ -504,11 +509,11 @@ instance Read OutputFormat where
     readsPrec = lookupReadsPrec outputFormats
 
 optimizationPackages :: [(String, Set Optimization)]
-optimizationPackages = 
+optimizationPackages =
     [("all",         Set.fromList [OptStem,OptCSE,OptExpand,OptParametrize]),
      ("values",      Set.fromList [OptStem,OptCSE,OptExpand]),
      ("noexpand",    Set.fromList [OptStem,OptCSE]),
-     
+
      -- deprecated
      ("all_subs",    Set.fromList [OptStem,OptCSE,OptExpand,OptParametrize]),
      ("parametrize", Set.fromList [OptStem,OptCSE,OptExpand,OptParametrize]),
@@ -516,7 +521,7 @@ optimizationPackages =
     ]
 
 cfgTransformNames :: [(String, CFGTransform)]
-cfgTransformNames = 
+cfgTransformNames =
     [("nolr",         CFGNoLR),
      ("regular",      CFGRegular),
      ("topdown",      CFGTopDownFilter),
@@ -532,7 +537,8 @@ haskellOptionNames =
      ("lexical",  HaskellLexical),
      ("concrete", HaskellConcrete),
      ("variants", HaskellVariants),
-     ("data",     HaskellData)]
+     ("data",     HaskellData),
+     ("pgf2",     HaskellPGF2)]
 
 -- | This is for bacward compatibility. Since GHC 6.12 we
 -- started using the native Unicode support in GHC but it
@@ -558,7 +564,7 @@ onOff f def = OptArg g "[on,off]"
                         _     -> fail $ "Expected [on,off], got: " ++ show x
 
 readOutputFormat :: Fail.MonadFail m => String -> m OutputFormat
-readOutputFormat s = 
+readOutputFormat s =
     maybe (fail $ "Unknown output format: " ++ show s) return $ lookup s outputFormats
 
 -- FIXME: this is a copy of the function in GF.Devel.UseIO.
@@ -570,7 +576,7 @@ splitInModuleSearchPath s = case break isPathSep s of
     isPathSep :: Char -> Bool
     isPathSep c = c == ':' || c == ';'
 
--- 
+--
 -- * Convenience functions for checking options
 --
 
@@ -592,7 +598,7 @@ isLiteralCat opts c = Set.member c (flag optLiteralCats opts)
 isLexicalCat :: Options -> String -> Bool
 isLexicalCat opts c = Set.member c (flag optLexicalCats opts)
 
--- 
+--
 -- * Convenience functions for setting options
 --
 
@@ -623,8 +629,8 @@ readMaybe s = case reads s of
 
 toEnumBounded :: (Bounded a, Enum a, Ord a) => Int -> Maybe a
 toEnumBounded i = let mi = minBound
-                      ma = maxBound `asTypeOf` mi                      
+                      ma = maxBound `asTypeOf` mi
-                   in if i >= fromEnum mi && i <= fromEnum ma 
+                   in if i >= fromEnum mi && i <= fromEnum ma
                         then Just (toEnum i `asTypeOf` mi)
                         else Nothing
 

testsuite/run.hs

@@ -1,13 +1,17 @@
 import Data.List(partition)
 import System.IO
 import Distribution.Simple.BuildPaths(exeExtension)
-import Distribution.System ( buildPlatform, OS (Windows), Platform (Platform) )
+import Distribution.System(buildPlatform, OS (Windows), Platform (Platform) )
 import System.Process(readProcess)
 import System.Directory(doesFileExist,getDirectoryContents)
 import System.FilePath((</>),(<.>),takeExtension)
 import System.Exit(exitSuccess,exitFailure)
 
-main = 
+type TestResult = (FilePath, RunResult)
+type RunResult = (String, (String, String, String)) -- (message, (input commands, gold output, actual output))
+
+main :: IO ()
+main =
    do res <- walk "testsuite"
       let cnt = length res
           (good,bad) = partition ((=="OK").fst.snd) res
@@ -16,29 +20,16 @@ main =
       putStrLn $ show ok++"/"++show cnt++ " passed/tests"
       let overview = "gf-tests.html"
       writeFile overview (toHTML bad)
-      if ok<cnt 
+      if ok<cnt
         then do putStrLn $ overview++" contains an overview of the failed tests"
                 exitFailure
         else exitSuccess
+
+-- | Recurse through files in path, running a test for all .gfs files
+walk :: FilePath -> IO [TestResult]
+walk path = fmap concat . mapM (walkFile . (path </>)) =<< ls path
   where
-    toHTML res =
+    walkFile :: FilePath -> IO [TestResult]
-        "<!DOCTYPE html>\n"
-        ++ "<meta charset=\"UTF-8\">\n"
-        ++ "<style>\n"
-        ++ "pre { max-width: 600px; overflow: scroll; }\n"
-        ++ "th,td { vertical-align: top; text-align: left; }\n"
-        ++ "</style>\n"
-        ++ "<table border=1>\n<tr><th>Result<th>Input<th>Gold<th>Output\n"
-        ++ unlines (map testToHTML res)
-        ++ "</table>\n"
-
-    testToHTML (in_file,(res,(input,gold,output))) =
-      "<tr>"++concatMap td [pre res,in_file++":\n"++pre input,pre gold,pre output]
-    pre s = "<pre>"++s++"</pre>"
-    td s = "<td>"++s
-
-    walk path = fmap concat . mapM (walkFile . (path </>)) =<< ls path
-
     walkFile fpath = do
       exists <- doesFileExist fpath
       if exists
@@ -53,25 +44,23 @@ main =
                else return []
         else walk fpath
 
-    runTest in_file out_file gold_file = do
+-- | Run an individual test
-      input <- readFile in_file
+runTest :: FilePath -> FilePath -> FilePath -> IO RunResult
-      writeFile out_file =<< run_gf ["-run"] input
+runTest in_file out_file gold_file = do
-      exists <- doesFileExist gold_file
+  input <- readFile in_file
-      if exists
+  writeFile out_file =<< runGF ["-run"] input
-        then do out <- compatReadFile out_file
+  exists <- doesFileExist gold_file
-                gold <- compatReadFile gold_file
+  if exists
-                let info = (input,gold,out)
+    then do out <- compatReadFile out_file
-                if in_file `elem` expectedFailures
+            gold <- compatReadFile gold_file
-                  then return $! if out == gold then ("Unexpected success",info) else ("FAIL (expected)",info)
+            let info = (input,gold,out)
-                  else return $! if out == gold then ("OK",info) else ("FAIL",info)
+            if in_file `elem` expectedFailures
-        else do out <- compatReadFile out_file
+              then return $! if out == gold then ("Unexpected success",info) else ("FAIL (expected)",info)
-                return ("MISSING GOLD",(input,"",out))
+              else return $! if out == gold then ("OK",info) else ("FAIL",info)
-    -- Avoid failures caused by Win32/Unix text file incompatibility
+    else do out <- compatReadFile out_file
-    compatReadFile path =
+            return ("MISSING GOLD",(input,"",out))
-      do h <- openFile path ReadMode
-         hSetNewlineMode h universalNewlineMode
-         hGetContents h
 
+-- | Test scripts which should fail
 expectedFailures :: [String]
 expectedFailures =
   [ "testsuite/runtime/parser/parser.gfs" -- Only parses `z` as `zero` and not also as e.g. `succ zero` as expected
@@ -79,9 +68,34 @@ expectedFailures =
   , "testsuite/compiler/typecheck/abstract/non-abstract-terms.gfs" -- Gives a different error than expected
   ]
 
+-- | Produce HTML document with test results
+toHTML :: [TestResult] -> String
+toHTML res =
+    "<!DOCTYPE html>\n"
+    ++ "<meta charset=\"UTF-8\">\n"
+    ++ "<style>\n"
+    ++ "pre { max-width: 600px; overflow: scroll; }\n"
+    ++ "th,td { vertical-align: top; text-align: left; }\n"
+    ++ "</style>\n"
+    ++ "<table border=1>\n<tr><th>Result<th>Input<th>Gold<th>Output\n"
+    ++ unlines (map testToHTML res)
+    ++ "</table>\n"
+    where
+      testToHTML (in_file,(res,(input,gold,output))) =
+        "<tr>"++concatMap td [pre res,in_file++":\n"++pre input,pre gold,pre output]
+      pre s = "<pre>"++s++"</pre>"
+      td s = "<td>"++s
+
+-- | Run commands in GF shell, returning output
+runGF
+  :: [String] -- ^ command line flags
+  -> String -- ^ standard input (shell commands)
+  -> IO String -- ^ standard output
+runGF = readProcess defaultGF
+
 -- Should consult the Cabal configuration!
-run_gf = readProcess default_gf 
+defaultGF :: FilePath
-default_gf = "gf"<.>exeExtension
+defaultGF = "gf"<.>exeExtension
   where
     -- shadows Distribution.Simple.BuildPaths.exeExtension, which changed type signature in Cabal 2.4
     exeExtension = case buildPlatform of
@@ -89,4 +103,12 @@ default_gf = "gf"<.>exeExtension
       _ -> ""
 
 -- | List files, excluding "." and ".."
+ls :: FilePath -> IO [String]
 ls path = filter (`notElem` [".",".."]) `fmap` getDirectoryContents path
+
+-- | Avoid failures caused by Win32/Unix text file incompatibility
+compatReadFile :: FilePath -> IO String
+compatReadFile path =
+  do h <- openFile path ReadMode
+     hSetNewlineMode h universalNewlineMode
+     hGetContents h