smyth/src/denotation.ml at main · UChicago-PL/smyth · GitHub

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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
open Smyth
open Lang

type 'a t =
  ('a -> exp) * typ

let bool : bool t =
  ( begin fun b ->
      ECtor
        ( (if b then "T" else "F")
        , []
        , ETuple []
        )
    end
  , TData ("Boolean", [])
  )

let int : int t =
  ( Desugar.nat
  , TData ("Nat", [])
  )

let var : string t =
  ( begin fun x ->
      EVar x
    end
  , TData ("Polymorphic var unimplemented", [])
  )

let opt : 'a t -> 'a option t =
  fun (da, typ) ->
    ( begin fun x_opt ->
        match x_opt with
          | None ->
              ECtor ("None", [typ], ETuple [])

          | Some x ->
              ECtor ("Some", [typ], da x)
        end
    , TData ("Polymorphic opt unimplemented", [])
    )

let list : 'a t -> 'a list t =
  fun (da, typ) ->
    ( begin fun xs ->
        List.fold_right
          ( fun x acc ->
              ECtor ("Cons", [typ], ETuple [da x; acc])
          )
          xs
          (ECtor ("Nil", [typ], ETuple []))
      end
    , TData ("List", [typ])
    )

let nested_list : 'a t -> 'a list list t =
  fun d ->
    list (list d)

let tree : 'a t -> 'a Tree2.t t =
  fun (da, typ) ->
    ( let rec helper t =
        match t with
          | Tree2.Leaf ->
              ECtor ("Leaf", [typ], ETuple [])

          | Tree2.Node (left, x, right) ->
              ECtor
                ( "Node"
                , [typ]
                , ETuple
                    [ helper left
                    ; da x
                    ; helper right
                    ]
                )
      in
      helper
    , TData ("Tree", [typ])
    )

let args2 : 'a1 t -> 'a2 t -> ('a1 * 'a2) t =
  fun (da1, _) (da2, _) ->
    ( begin fun (x1, x2) ->
        ECtor ("args", [], ETuple [da1 x1; da2 x2])
      end
    , TData ("Polymorphic args2 unimplemented", [])
    )

let args3 : 'a1 t -> 'a2 t -> 'a3 t -> ('a1 * 'a2 * 'a3) t =
  fun (da1, _) (da2, _) (da3, _) ->
    ( begin fun (x1, x2, x3) ->
        ECtor ("args", [], ETuple [da1 x1; da2 x2; da3 x3])
      end
    , TData ("Polymorphic args3 unimplemented", [])
    )

let rec poly_to_mono : exp -> exp =
  function
    (* Main cases *)

    | EApp (_, e1, EAType _) ->
        poly_to_mono e1

    | ECtor (ctor_name, [TData ("List", _)], arg) ->
        ECtor ("L" ^ ctor_name, [], poly_to_mono arg)

    | ECtor (ctor_name, _, arg) ->
        ECtor (ctor_name, [], poly_to_mono arg)

    (* Other cases *)

    | EFix (f, x, body) ->
        EFix (f, x, poly_to_mono body)

    | EApp (special, e1, EAExp e2) ->
        EApp (special, poly_to_mono e1, EAExp (poly_to_mono e2))

    | EVar x ->
        EVar x

    | ETuple components ->
        ETuple (List.map poly_to_mono components)

    | EProj (n, i, arg) ->
        EProj (n, i, poly_to_mono arg)

    | ECase (scrutinee, branches) ->
        ECase
          ( poly_to_mono scrutinee
          , List.map (Pair2.map_snd (Pair2.map_snd poly_to_mono)) branches
          )

    | EHole hole_name ->
        EHole hole_name

    | EAssert (e1, e2) ->
        EAssert (poly_to_mono e1, poly_to_mono e2)

    | ETypeAnnotation (e, tau) ->
        ETypeAnnotation (poly_to_mono e, tau)

let poly : 'a t -> 'a -> exp =
  fun (da, _) x ->
    da x

let mono : 'a t -> 'a -> exp =
  fun d x ->
    poly_to_mono (poly d x)