type check cc command

3 files changed, 12 insertions, 1 deletions

diff --git a/grammars/logic/Arithm.gf b/grammars/logic/Arithm.gf
index 0cf07e0c1..2d2e12fd9 100644
--- a/grammars/logic/Arithm.gf
+++ b/grammars/logic/Arithm.gf
@@ -44,6 +44,7 @@ def
               (LtNat one n) 
               (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
 
+  Abs = Abs ;
 ---  data Elem = zero | succ ;
 
 fun ex1 : Text ;
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index c4de7beb1..811437f57 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -65,6 +65,13 @@ checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod
  where
    gr  = MGrammar $ (name,mod):ms
 
+-- check if a term is typable
+
+justCheckLTerm :: SourceGrammar -> Term -> Err Term
+justCheckLTerm src t = do
+  ((t',_),_) <- checkStart (inferLType src t)
+  return t'
+
 checkAbsInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info)
 checkAbsInfo st m (c,info) = do
 ---- checkReservedId c
diff --git a/src/GF/Shell.hs b/src/GF/Shell.hs
index 27ceb19e0..294160a82 100644
--- a/src/GF/Shell.hs
+++ b/src/GF/Shell.hs
@@ -5,6 +5,7 @@ import Str
 import qualified Grammar as G
 import qualified Ident as I
 import qualified Compute as Co
+import qualified CheckGrammar as Ch
 import qualified Lookup as L
 import qualified GFC
 import qualified Look
@@ -169,7 +170,9 @@ execC co@(comm, opts0) sa@((st,(h,_)),a) = checkOptions st co >> case comm of
            maybe (resourceOfShellState st) (return . I.identC) $ -- topmost res
              getOptVal opts useResource             -- flag -res=m
     justOutput (putStrLn (err id (prt . stripTerm) (
-                string2srcTerm src m t >>= Co.computeConcrete src))) sa
+                string2srcTerm src m t >>= 
+                Ch.justCheckLTerm src  >>=
+                Co.computeConcrete src))) sa
   CShowOpers t -> do
     m <- return $
          maybe (I.identC "?") id $  -- meaningful if no opers in t