1
0
forked from GitHub/gf-core

started create/drop with lin & lincat

This commit is contained in:
krangelov
2021-12-23 23:04:31 +01:00
parent b000b80159
commit 5c16693da3
3 changed files with 67 additions and 1 deletions

View File

@@ -16,8 +16,12 @@ data Command
data TransactionCommand
= CreateFun [Option] Fun Type
| CreateCat [Option] Cat [Hypo]
| CreateLin [Option] Fun Term
| CreateLincat [Option] Cat Term
| DropFun [Option] Fun
| DropCat [Option] Cat
| DropLin [Option] Fun
| DropLincat [Option] Cat
deriving Show
data Option

View File

@@ -1,7 +1,9 @@
module GF.Command.Parse(readCommandLine, readTransactionCommand, pCommand) where
import PGF(pExpr,pIdent)
import PGF2(readType,readContext)
import PGF2(BindType(..),readType,readContext)
import GF.Infra.Ident(identS)
import GF.Grammar.Grammar(Term(Abs))
import GF.Grammar.Parser(runPartial,pTerm)
import GF.Command.Abstract
@@ -73,6 +75,33 @@ pTransactionCommand = do
| take 1 cmd == "d" -> do
c <- pIdent
return (DropCat opts c)
"lin" | take 1 cmd == "c" -> do
f <- pIdent
skipSpaces
args <- sepBy pIdent skipSpaces
skipSpaces
char '='
skipSpaces
t <- readS_to_P (\s -> case runPartial pTerm s of
Right (s,t) -> [(t,s)]
_ -> [])
return (CreateLin opts f (foldr (Abs Explicit . identS) t args))
| take 1 cmd == "d" -> do
f <- pIdent
return (DropLin opts f)
"lincat"
| take 1 cmd == "c" -> do
f <- pIdent
skipSpaces
char '='
skipSpaces
t <- readS_to_P (\s -> case runPartial pTerm s of
Right (s,t) -> [(t,s)]
_ -> [])
return (CreateLincat opts f t)
| take 1 cmd == "d" -> do
f <- pIdent
return (DropLincat opts f)
_ -> pfail
pOption = do