1
0
forked from GitHub/gf-core

create lin/lincat can now fetch the definitions from the source grammar

This commit is contained in:
Krasimir Angelov
2024-02-08 15:14:05 +01:00
parent ab30f1f9e5
commit 3b4f12e621
3 changed files with 46 additions and 28 deletions

View File

@@ -17,8 +17,8 @@ data TransactionCommand
= CreateFun [Option] Fun Type
| CreateCat [Option] Cat [Hypo]
| CreateConcrete [Option] ConcName
| CreateLin [Option] Fun Term Bool
| CreateLincat [Option] Cat Term
| CreateLin [Option] Fun (Maybe Term) Bool
| CreateLincat [Option] Cat (Maybe Term)
| DropFun [Option] Fun
| DropCat [Option] Cat
| DropConcrete [Option] ConcName

View File

@@ -84,28 +84,32 @@ pTransactionCommand = do
return (DropConcrete opts name)
"lin" | elem (take 1 cmd) ["c","a"] -> 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 == "a"))
body <- option Nothing $ do
skipSpaces
args <- sepBy pIdent skipSpaces
skipSpaces
char '='
skipSpaces
t <- readS_to_P (\s -> case runPartial pTerm s of
Right (s,t) -> [(t,s)]
_ -> [])
return (Just (foldr (Abs Explicit . identS) t args))
return (CreateLin opts f body (take 1 cmd == "a"))
| 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)
body <- option Nothing $ do
skipSpaces
char '='
skipSpaces
t <- readS_to_P (\s -> case runPartial pTerm s of
Right (s,t) -> [(t,s)]
_ -> [])
return (Just t)
return (CreateLincat opts f body)
| take 1 cmd == "d" -> do
f <- pIdent
return (DropLincat opts f)