~thon/thon

ref: fd82ecc4851b6e941a5aabb6c1747c1580f94fa1 thon/parse/ast.sml -rw-r--r-- 3.5 KiB
fd82ecc4Evan Bergeron Add no-op elaboration 9 months ago
                                                                                
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
signature AST =
sig

    (* TODO is there a way to dedupe this with the structure defn below? *)
    datatype Typ =
        Nat
      | TypVar of string * int
      | Arr of Typ * Typ
      | All of string * Typ (* binds *)
      | Some of string * Typ (* binds *)
      | Prod of Typ * Typ
      | Plus of Typ * Typ (* sum type *)
      | TyRec of string * Typ (* binds *)
      | Unit (* nullary sum *)

    datatype Idx = int

    datatype Exp =
        Zero
      | Var of string * int (* idx into ctx *)
      | Succ of Exp
      | Lam of string * Typ (*argType*) * Exp (*funcBody*)
      | Let of string * Typ (*vartype*) * Exp (*varval*) * Exp (*varscope*)
      | App of Exp * Exp
      | Rec of Exp (*i : Nat*) * Exp (*baseCase: t*) * string * Exp (*recCase - binds*)
      | Fix of string (*x*) * Typ (*: t*) * Exp (*x's scope*)
      | TypAbs of string * Exp (* binds type variable *)
      | Ifz of Exp * Exp * string * Exp
      | TypApp of Typ * Exp
      | Impl of Typ (*reprType*)* Exp (*pkgImpl*)* Typ (*pkgType - first example of explicit type binding - there's not one cannonical type*)
      | Use of Exp (*package*) * string (*exp name*) * string (*type name*) * Exp (* client that binds BOTH a TypVar and a Exp Var *)
      | Tuple of Exp * Exp
      (* Elimination forms for terms of Prod type *)
      | ProdLeft of Exp
      | ProdRight of Exp
      (* Elimination forms for terms of Plus type *)
      | PlusLeft of Typ * Exp
      | PlusRight of Typ * Exp
      | Case of Exp (* thing being cased on*) *
                string * Exp (* Left binds term var *) *
                string * Exp (* Right binds term var *)
      | Fold of Typ (*binds*) * Exp
      | Unfold of Exp
      | TmUnit

  structure Print :
  sig
    val pp : Exp -> string
  end

end


structure Ast :> AST =
struct
    datatype Typ =
        Nat
      | TypVar of string * int
      | Arr of Typ * Typ
      | All of string * Typ (* binds *)
      | Some of string * Typ (* binds *)
      | Prod of Typ * Typ
      | Plus of Typ * Typ (* sum type *)
      | TyRec of string * Typ (* binds *)
      | Unit (* nullary sum *)

    datatype Idx = int

    datatype Exp =
        Zero
      | Var of string * int (* idx into ctx *)
      | Succ of Exp
      | Lam of string * Typ (*argType*) * Exp (*funcBody*)
      | Let of string * Typ (*vartype*) * Exp (*varval*) * Exp (*varscope*)
      | App of Exp * Exp
      | Rec of Exp (*i : Nat*) * Exp (*baseCase: t*) * string * Exp (*recCase - binds*)
      | Fix of string (*x*) * Typ (*: t*) * Exp (*x's scope*)
      | TypAbs of string * Exp (* binds type variable *)
      | Ifz of Exp * Exp * string * Exp
      | TypApp of Typ * Exp
      | Impl of Typ (*reprType*)* Exp (*pkgImpl*)* Typ (*pkgType - first example of explicit type binding - there's not one cannonical type*)
      | Use of Exp (*package*) * string (*exp name*) * string (*type name*) * Exp (* client that binds BOTH a TypVar and a Exp Var *)
      | Tuple of Exp * Exp
      (* Elimination forms for terms of Prod type *)
      | ProdLeft of Exp
      | ProdRight of Exp
      (* Elimination forms for terms of Plus type *)
      | PlusLeft of Typ * Exp
      | PlusRight of Typ * Exp
      | Case of Exp (* thing being cased on*) *
                string * Exp (* Left binds term var *) *
                string * Exp (* Right binds term var *)
      | Fold of Typ (*binds*) * Exp
      | Unfold of Exp
      | TmUnit

  structure Print =
  struct
    fun pp e =
        case e of
            Zero => "Z"
          | Succ e => "S (" ^ (pp e) ^ ")"
  end

end