msyds/gf-rgl
1
0
Fork 0
forked from GitHub/gf-rgl
Code Pull Requests Activity

1. Created Linearization types for V2V as Res.Verb ** {comp,c3 : Str ; typ : Res.VVType} ; but however I have eerors with mkV2 overload methods and lock_C fields. I cannot seem to find out the reason for the error.

Browse Source
This commit is contained in:
David Bamutura
2020-10-12 17:31:40 +03:00
parent 7a07513f8e
commit 7c997ea280
5 changed files with 408 additions and 400 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/prelude/Coordination.gf
View File

@@ -6,14 +6,14 @@ param
oper
ListX = {s1,s2 : Str} ;
twoStr : (x,y : Str) -> ListX = \x,y ->
twoStr : (x,y : Str) -> ListX = \x,y -> --stores two strings in a record
{s1 = x ; s2 = y} ;
consStr : Str -> ListX -> Str -> ListX = \comma,xs,x ->
consStr : Str -> ListX -> Str -> ListX = \comma,xs,x ->
{s1 = xs.s1 ++ comma ++ xs.s2 ; s2 = x } ;
twoSS : (_,_ : SS) -> ListX = \x,y ->
twoSS : (_,_ : SS) -> ListX = \x,y -> --stores two string records into one record
twoStr x.s y.s ;
consSS : Str -> ListX -> SS -> ListX = \comma,xs,x ->
consSS : Str -> ListX -> SS -> ListX = \comma,xs,x -> -- Combines and a record into a record separated by a comma.
consStr comma xs x.s ;
Conjunction : Type = SS ;
@@ -33,7 +33,7 @@ oper
-- all this lifted to tables
ListTable : PType -> Type = \P -> {s1,s2 : P => Str} ;
ListTable : PType -> Type = \P -> {s1,s2 : P => Str} ; --Type family for tables
twoTable : (P : PType) -> (_,_ : {s : P => Str}) -> ListTable P = \_,x,y ->
{s1 = x.s ; s2 = y.s} ;