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