operations in the abstract syntax

examples/nqueens/Nat.gf

@@ -11,8 +11,8 @@ data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
      lNE : (j : Nat) -> NE zero (succ j) ;
      rNE : (j : Nat) -> NE (succ j) zero ;
 
-fun plus : Nat -> Nat -> Nat ;
+oper plus : Nat -> Nat -> Nat ;
-def plus zero     n = n ;
+def  plus zero     n = n ;
-    plus (succ m) n = succ (plus m n) ;
+     plus (succ m) n = succ (plus m n) ;
 
 }

src/compiler/GF/Compile/CheckGrammar.hs

@@ -94,7 +94,7 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
   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
@@ -138,7 +138,7 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
    checkCnc js i@(c,info) =
      case info of
        CncFun _ d pn -> 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 $ updateTree (c,CncFun (Just linty) d pn) js
@@ -161,7 +161,7 @@ checkInfo ms (m,mo) c info = do
       mkCheck loc "category" $ 
         checkContext gr cont
 
-    AbsFun (Just (L loc typ0)) ma md -> do
+    AbsFun (Just (L loc typ0)) ma md moper -> do
       typ <- compAbsTyp [] typ0   -- to calculate let definitions
       mkCheck loc "type of function" $
         checkTyp gr typ
@@ -169,7 +169,7 @@ checkInfo ms (m,mo) c info = do
         Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "definition of function" $
 	                                        checkDef gr (m,c) typ eq) eqs
         Nothing  -> return ()
-      return (AbsFun (Just (L loc typ)) ma md)
+      return (AbsFun (Just (L loc typ)) ma md moper)
 
     CncFun linty@(Just (cat,cont,val)) (Just (L loc trm)) mpr -> chIn loc "linearization of" $ do
       (trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars

src/compiler/GF/Compile/GrammarToPGF.hs

@@ -58,14 +58,14 @@ canon2pgf opts gr cgr@(M.MGrammar (am:cms)) = do
         flags = Map.fromList [(mkCId f,C.LStr x) | (f,x) <- optionsPGF (M.flags abm)]
         
         funs = Map.fromAscList [(i2i f, (mkType [] ty, mkArrity ma, mkDef pty, 0)) | 
-                                   (f,AbsFun (Just (L _ ty)) ma pty) <- Map.toAscList (M.jments abm)]
+                                   (f,AbsFun (Just (L _ ty)) ma pty _) <- Map.toAscList (M.jments abm)]
                                    
         cats = Map.fromAscList [(i2i c, (snd (mkContext [] cont),catfuns c)) |
                                    (c,AbsCat (Just (L _ cont))) <- Map.toAscList (M.jments abm)]
 
         catfuns cat =
               (map (\x -> (0,snd x)) . sortBy (compare `on` fst))
-                 [(loc,i2i f) | (f,AbsFun (Just (L loc ty)) _ _) <- tree2list (M.jments abm), snd (GM.valCat ty) == cat]
+                 [(loc,i2i f) | (f,AbsFun (Just (L loc ty)) _ _ (Just True)) <- tree2list (M.jments abm), snd (GM.valCat ty) == cat]
 
     mkConcr am cm@(lang,mo) = do
       cnc <- convertConcrete opts gr am cm

src/compiler/GF/Compile/Rename.hs

@@ -105,7 +105,7 @@ renameIdentTerm env@(act,imps) t =
 
 info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
 info2status mq (c,i) = case i of
-  AbsFun _ _ Nothing -> maybe Con (curry QC) mq
+  AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq
   ResValue _  -> maybe Con (curry QC) mq
   ResParam _ _  -> maybe Con (curry QC) mq
   AnyInd True m -> maybe Con (const (curry QC m)) mq
@@ -141,7 +141,7 @@ renameInfo :: Status -> Ident -> Ident -> Info -> Check Info
 renameInfo status m i info =
   case info of
     AbsCat pco -> liftM AbsCat (renPerh (renameContext status) pco)
-    AbsFun  pty pa ptr -> liftM3 AbsFun (renTerm pty) (return pa) (renMaybe (mapM (renLoc (renEquation status))) ptr)
+    AbsFun  pty pa ptr poper -> liftM4 AbsFun (renTerm pty) (return pa) (renMaybe (mapM (renLoc (renEquation status))) ptr) (return poper)
     ResOper pty ptr -> liftM2 ResOper (renTerm pty) (renTerm ptr)
     ResOverload os tysts -> liftM (ResOverload os) (mapM (renPair (renameTerm status [])) tysts)
     ResParam (Just pp) m -> do

src/compiler/GF/Compile/Update.hs

@@ -161,7 +161,7 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old
       (b,n') = case info of
         ResValue _ -> (True,n)
         ResParam _ _ -> (True,n)
-        AbsFun _ _ Nothing -> (True,n) 
+        AbsFun _ _ Nothing _ -> (True,n) 
         AnyInd b k -> (b,k)
         _ -> (False,n) ---- canonical in Abs
 
@@ -169,8 +169,8 @@ unifyAnyInfo :: Ident -> Info -> Info -> Err Info
 unifyAnyInfo m i j = case (i,j) of
   (AbsCat mc1, AbsCat mc2) -> 
     liftM AbsCat (unifMaybeL mc1 mc2)
-  (AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) -> 
+  (AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) -> 
-    liftM3 AbsFun (unifMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
+    liftM4 AbsFun (unifMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) (unifMaybe moper1 moper2) -- adding defs
 
   (ResParam mt1 mv1, ResParam mt2 mv2) ->
     liftM2 ResParam (unifMaybe mt1 mt2) (unifMaybe mv1 mv2)

src/compiler/GF/Grammar/Binary.hs

@@ -88,7 +88,7 @@ instance Binary Options where
 
 instance Binary Info where
   put (AbsCat x)       = putWord8 0 >> put x
-  put (AbsFun x y z)   = putWord8 1 >> put (x,y,z)
+  put (AbsFun w x y z) = putWord8 1 >> put (w,x,y,z)
   put (ResParam x y)   = putWord8 2 >> put (x,y)
   put (ResValue x)     = putWord8 3 >> put x
   put (ResOper x y)    = putWord8 4 >> put (x,y)
@@ -98,15 +98,15 @@ instance Binary Info where
   put (AnyInd x y)     = putWord8 8 >> put (x,y)
   get = do tag <- getWord8
            case tag of
-             0 -> get >>= \x       -> return (AbsCat x)
+             0 -> get >>= \x         -> return (AbsCat x)
-             1 -> get >>= \(x,y,z) -> return (AbsFun x y z)
+             1 -> get >>= \(w,x,y,z) -> return (AbsFun w x y z)
-             2 -> get >>= \(x,y)   -> return (ResParam x y)
+             2 -> get >>= \(x,y)     -> return (ResParam x y)
-             3 -> get >>= \x       -> return (ResValue x)
+             3 -> get >>= \x         -> return (ResValue x)
-             4 -> get >>= \(x,y)   -> return (ResOper x y)
+             4 -> get >>= \(x,y)     -> return (ResOper x y)
-             5 -> get >>= \(x,y)   -> return (ResOverload x y)
+             5 -> get >>= \(x,y)     -> return (ResOverload x y)
-             6 -> get >>= \(x,y,z) -> return (CncCat x y z)
+             6 -> get >>= \(x,y,z)   -> return (CncCat x y z)
-             7 -> get >>= \(x,y,z) -> return (CncFun x y z)
+             7 -> get >>= \(x,y,z)   -> return (CncFun x y z)
-             8 -> get >>= \(x,y)   -> return (AnyInd x y)
+             8 -> get >>= \(x,y)     -> return (AnyInd x y)
              _ -> decodingError
 
 instance Binary a => Binary (L a) where

src/compiler/GF/Grammar/CF.hs

@@ -110,7 +110,7 @@ cf2cat (L loc (_,(cat, items))) = map identS $ cat : [c | Left c <- items]
 cf2rule :: CFRule -> ((Ident,Info),(Ident,Info))
 cf2rule (L loc (fun, (cat, items))) = (def,ldef) where
   f     = identS fun
-  def   = (f, AbsFun (Just (L loc (mkProd args' (Cn (identS cat)) []))) Nothing Nothing)
+  def   = (f, AbsFun (Just (L loc (mkProd args' (Cn (identS cat)) []))) Nothing Nothing (Just True))
   args0 = zip (map (identS . ("x" ++) . show) [0..]) items
   args  = [((Explicit,v), Cn (identS c)) | (v, Left c) <- args0]
   args' = [(Explicit,identS "_", Cn (identS c)) | (_, Left c) <- args0]

src/compiler/GF/Grammar/Grammar.hs

@@ -76,8 +76,8 @@ mapSourceModule f (i,mi) = (i, f mi)
 -- and indirection to module (/INDIR/)
 data Info =
 -- judgements in abstract syntax
-   AbsCat   (Maybe (L Context))                                -- ^ (/ABS/) context of a category
+   AbsCat   (Maybe (L Context))                                            -- ^ (/ABS/) context of a category
- | AbsFun   (Maybe (L Type)) (Maybe Int) (Maybe [L Equation])  -- ^ (/ABS/) type, arrity and definition of a function
+ | AbsFun   (Maybe (L Type)) (Maybe Int) (Maybe [L Equation]) (Maybe Bool) -- ^ (/ABS/) type, arrity and definition of a function
 
 -- judgements in resource
  | ResParam (Maybe [L Param]) (Maybe [Term])     -- ^ (/RES/) the second parameter is list of all possible values

src/compiler/GF/Grammar/Lookup.hs

@@ -156,9 +156,9 @@ lookupAbsDef gr m c = errIn (render (text "looking up absdef of" <+> ppIdent c))
   mo <- lookupModule gr m
   info <- lookupIdentInfo mo c
   case info of
-    AbsFun _ a d -> return (a,fmap (map unLoc) d)
+    AbsFun _ a d _ -> return (a,fmap (map unLoc) d)
-    AnyInd _ n   -> lookupAbsDef gr n c
+    AnyInd _ n     -> lookupAbsDef gr n c
-    _            -> return (Nothing,Nothing)
+    _              -> return (Nothing,Nothing)
 
 lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
 lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed?
@@ -176,9 +176,9 @@ lookupFunType gr m c = do
   mo <- lookupModule gr m
   info <- lookupIdentInfo mo c
   case info of
-    AbsFun (Just (L _ t)) _ _ -> return t
+    AbsFun (Just (L _ t)) _ _ _ -> return t
-    AnyInd _ n                -> lookupFunType gr n c
+    AnyInd _ n                  -> lookupFunType gr n c
-    _                         -> Bad (render (text "cannot find type of" <+> ppIdent c))
+    _                           -> Bad (render (text "cannot find type of" <+> ppIdent c))
 
 -- | this is needed at compile time
 lookupCatContext :: SourceGrammar -> Ident -> Ident -> Err Context

src/compiler/GF/Grammar/Macros.hs

@@ -624,7 +624,7 @@ allDependencies ism b =
       ResParam (Just ps) _ -> [Just (L loc t) | L loc (_,cont) <- ps, (_,_,t) <- cont]
       CncCat pty _ _ -> [pty]
       CncFun _   pt _ -> [pt]  ---- (Maybe (Ident,(Context,Type))
-      AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
+      AbsFun pty _ ptr _ -> [pty] --- ptr is def, which can be mutual
       AbsCat (Just (L loc co)) -> [Just (L loc ty) | (_,_,ty) <- co]
       _              -> []
 

src/compiler/GF/Grammar/Parser.y

@@ -112,7 +112,7 @@ ModDef
                                           (mtype,id) = $2
                                           (extends,with,content) = $4
                                           (opens,jments,opts) = case content of { Just c -> c; Nothing -> ([],[],noOptions) }
-                                      mapM_ (checkInfoType mtype) jments
+                                      jments <- mapM (checkInfoType mtype) jments
                                       defs <- case buildAnyTree id jments of
                                                 Ok x    -> return x
                                                 Bad msg -> fail msg
@@ -233,19 +233,19 @@ CatDef
 
 FunDef :: { [(Ident,Info)] }
 FunDef
-  : Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing (Just [])) | fun <- $2] } 
+  : Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing (Just []) (Just True)) | fun <- $2] } 
 
 DefDef :: { [(Ident,Info)] }
 DefDef
-  : Posn ListName '=' Exp         Posn { [(f, AbsFun Nothing (Just 0)           (Just [mkL $1 $5 ([],$4)])) | f <- $2] }
+  : Posn ListName '=' Exp         Posn { [(f, AbsFun Nothing (Just 0)           (Just [mkL $1 $5 ([],$4)]) Nothing) | f <- $2] }
-  | Posn Name ListPatt '=' Exp    Posn { [($2,AbsFun Nothing (Just (length $3)) (Just [mkL $1 $6 ($3,$5)]))] }
+  | Posn Name ListPatt '=' Exp    Posn { [($2,AbsFun Nothing (Just (length $3)) (Just [mkL $1 $6 ($3,$5)]) Nothing)] }
 
 DataDef :: { [(Ident,Info)] }
 DataDef
   : Posn Ident '=' ListDataConstr Posn { ($2,   AbsCat Nothing) :
-                                         [(fun, AbsFun Nothing   Nothing Nothing) | fun <- $4] }
+                                         [(fun, AbsFun Nothing Nothing Nothing  (Just True)) | fun <- $4] }
   | Posn ListIdent ':' Exp Posn        { -- (snd (valCat $4), AbsCat Nothing) :
-                                         [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing Nothing) | fun <- $2] }                                         
+                                         [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing Nothing (Just True)) | fun <- $2] }                                         
 
 ParamDef :: { [(Ident,Info)] }
 ParamDef
@@ -620,8 +620,8 @@ listCatDef (L loc (id,cont,size)) = [catd,nilfund,consfund]
     consId = mkConsId id
 
     catd     = (listId, AbsCat (Just (L loc cont')))
-    nilfund  = (baseId, AbsFun (Just (L loc niltyp))  Nothing Nothing)
+    nilfund  = (baseId, AbsFun (Just (L loc niltyp))  Nothing Nothing (Just True))
-    consfund = (consId, AbsFun (Just (L loc constyp)) Nothing Nothing)
+    consfund = (consId, AbsFun (Just (L loc constyp)) Nothing Nothing (Just True))
 
     cont' = [(b,mkId x i,ty) | (i,(b,x,ty)) <- zip [0..] cont]
     xs = map (\(b,x,t) -> Vr x) cont'
@@ -671,34 +671,34 @@ isOverloading t =
     Vr keyw | showIdent keyw == "overload" -> True      -- overload is a "soft keyword"
     _                                      -> False
 
-checkInfoType mt (id,info) =
+checkInfoType mt jment@(id,info) =
   case info of
-    AbsCat pcont      -> ifAbstract mt (locPerh pcont)
+    AbsCat pcont       -> ifAbstract mt (locPerh pcont)
-    AbsFun pty _ pde  -> ifAbstract mt (locPerh pty ++ maybe [] locAll pde)
+    AbsFun pty _ pde _ -> ifAbstract mt (locPerh pty ++ maybe [] locAll pde)
-    CncCat pty pd ppn -> ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh ppn)
+    CncCat pty pd ppn  -> ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh ppn)
-    CncFun _   pd ppn -> ifConcrete mt (locPerh pd ++ locPerh ppn)
+    CncFun _   pd ppn  -> ifConcrete mt (locPerh pd ++ locPerh ppn)
-    ResParam pparam _ -> ifResource mt (maybe [] locAll pparam)
+    ResParam pparam _  -> ifResource mt (maybe [] locAll pparam)
-    ResValue ty       -> ifResource mt (locL ty)
+    ResValue ty        -> ifResource mt (locL ty)
-    ResOper  pty pt   -> ifResource mt (locPerh pty ++ locPerh pt)
+    ResOper  pty pt    -> return (id,AbsFun pty (fmap (const 0) pt) (Just (maybe [] (\(L l t) -> [L l ([],t)]) pt)) (Just False))
-    ResOverload _ xs  -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
+    ResOverload _ xs   -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
   where
     locPerh = maybe [] locL
     locAll xs = [loc | L loc x <- xs]
     locL (L loc x) = [loc]
     
     illegal ((s,e):_) = failLoc (Pn s 0) "illegal definition"
-    illegal _         = return ()
+    illegal _         = return jment
 
-    ifAbstract MTAbstract     locs = return ()
+    ifAbstract MTAbstract     locs = return jment
     ifAbstract _              locs = illegal locs
 
-    ifConcrete (MTConcrete _) locs = return ()
+    ifConcrete (MTConcrete _) locs = return jment
     ifConcrete _              locs = illegal locs
 
-    ifResource (MTConcrete _) locs = return ()
+    ifResource (MTConcrete _) locs = return jment
-    ifResource (MTInstance _) locs = return ()
+    ifResource (MTInstance _) locs = return jment
-    ifResource MTInterface    locs = return ()
+    ifResource MTInterface    locs = return jment
-    ifResource MTResource     locs = return ()
+    ifResource MTResource     locs = return jment
     ifResource _              locs = illegal locs
 
 mkAlts cs = case cs of

src/compiler/GF/Grammar/Printer.hs

@@ -78,9 +78,13 @@ ppJudgement q (id, AbsCat pcont ) =
   (case pcont of
      Just (L _ cont) -> hsep (map (ppDecl q) cont)
      Nothing         -> empty) <+> semi
-ppJudgement q (id, AbsFun ptype _ pexp) =
+ppJudgement q (id, AbsFun ptype _ pexp poper) =
+  let kind | isNothing pexp      = "data"
+           | poper == Just False = "oper"
+           | otherwise           = "fun"
+  in
   (case ptype of
-     Just (L _ typ) -> text (if isNothing pexp then "data" else "fun") <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi
+     Just (L _ typ) -> text kind <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi
      Nothing        -> empty) $$
   (case pexp of
      Just []  -> empty

src/runtime/haskell/PGF/Generate.hs

@@ -86,7 +86,6 @@ prove dp scope (TTyp env1 (DTyp hypos1 cat es1)) = do
   vs1 <- mapM (PGF.TypeCheck.eval env1) es1
   let scope' = exScope scope env1 hypos1
   (fe,TTyp env2 (DTyp hypos2 _ es2)) <- select cat scope' dp
-  if fe == EFun (mkCId "plus") then mzero else return ()
   case dp of
     Just 0 | not (null hypos2) -> mzero
     _                          -> return ()

testsuite/compiler/check/abstract-operations/Nat.gf

@@ -0,0 +1,13 @@
+abstract Nat = {
+
+cat Nat ;
+data zero : Nat ;
+     succ : Nat -> Nat ;
+     
+oper plus : Nat -> Nat -> Nat ;
+def  plus zero     y = y ;
+     plus (succ x) y = succ (plus x y) ;
+
+oper twice : Nat -> Nat = \x -> plus x x ;
+
+}

testsuite/compiler/check/abstract-operations/abstract-operations.gfs

@@ -0,0 +1,5 @@
+-- here we test that the abstract operations are not used for proof search
+
+i testsuite\compiler\check\abstract-operations\Nat.gf
+gt -cat=Nat -number=10 -depth=10
+pt -compute (twice (succ zero))

testsuite/compiler/check/abstract-operations/abstract-operations.gfs.gold

@@ -0,0 +1,13 @@
+zero
+succ zero
+succ (succ zero)
+succ (succ (succ zero))
+succ (succ (succ (succ zero)))
+succ (succ (succ (succ (succ zero))))
+succ (succ (succ (succ (succ (succ zero)))))
+succ (succ (succ (succ (succ (succ (succ zero))))))
+succ (succ (succ (succ (succ (succ (succ (succ zero)))))))
+succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))
+
+succ (succ zero)
+