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

interface Parametric = {

oper

-- primitive

  PS : Type ;
  S  : Type ;
  Cl : Type ;
  NP : Type ;
  CN : Type ;
  AP : Type ;

  VPComp : 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 ;

-- derived

  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} ;

}