next-lib/src/parametric/Parametric.gf


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

interface Parametric = {

oper

-- primitive

  S  : Type ;
  NP : Type ;
  CN : Type ;
  AP : Type ;

  VPComp : Type ;

  ITense : Type ;
  CCase : Type ;
  Agr : Type ;

  V  : Type ;
  N  : Type ;
  A  : Type ;

  agrNP : NP -> Agr ;

  PredVP : NP -> VP -> Cl ;

  mkVPComp : (Agr => Str) -> Str -> Str -> VPComp ;

  insertVPComp : VPComp -> VP -> VP ;

  insertNP : CCase -> NP -> VP -> VP ;

  iTense : Tense -> ITense ;

-- derived

  Cl : Type = {s : ITense => Polarity => S} ;

  VP : Type = {
    verb : V ; 
    comp : VPComp
    } ;

  VPSlash : Type = VP ** {c : CComp} ;

  UseV : V -> VP = \v -> {
    verb = v ;
    comp = mkVPComp (\\_ => []) [] [] 
    } ;

  SlashV : V -> (Agr => Str) -> Str -> Str -> CCase -> VPSlash = 
    \v,comp,adv,ext,c -> 
      insertVPComp (mkVPComp comp adv ext) (UseV v) ** {c = c} ;

  ComplSlash : VPSlash -> NP -> VP = \vp,np -> insertNP vp.c np vp ;

  UseCl : Tense -> Polarity -> Cl -> S = \t,p,cl -> cl.s ! iTense t ! p ;

}