open Common

(** Surface terms are the direct output from the parser. These use user-friendly
    explicit naming and distinguish top-level definitions from local let bindings. *)

type expr =
  | Var of name                                 (* x                            *)
  | Ann of expr * expr                          (* e : τ                        *)
  | Pi of name * expr * expr                    (* (a : A) → B                  *)
  | Lam of name * expr option * expr            (* λ x . e                      *)
  | Sig of (name * expr) list                   (* (x : A ; y : B ; z : C)      *)
  | Rcd of (name * expr) list                   (* (x = a , y = b , z = c)      *)
  | Prod of expr list                           (* (A ; B ; C)                  *)
  | Tup of expr list                            (* (a , b , c)                  *)
  | App of expr * expr                          (* a b                          *)
  | Proj of expr * name                         (* e.x                          *)
  | ProjAt of expr * int                        (* e.i                          *)
  | Let of name * expr option * expr * expr     (* let x : τ = e in e'          *)
  | Uni                                         (* Type                         *)
  | Bool                                        (* Bool                         *)
  | False                                       (* False                        *)
  | True                                        (* True                         *)
  | BoolInd of expr option * expr * expr * expr (* towards τ if e then a else b *)
  | Nat                                         (* ℕ                            *)
  Zero                         
  | NatS of expr                                (* Succ n                       *)
  0 , 1 , 2 , 3 , ...              
  | NatInd of expr * expr option                (* rec n at τ                   *)
  | Zero . e₁ | Succ m , p . e₂

and stmt =
  | Def of name * expr option * expr
  | Inf of expr
  | Eval of expr
  | Exec of expr
  | Check of expr * expr
  | Conv of expr * expr * expr
  | Parse of expr
  | Import of string

type prog = stmt list
* Surface terms are the direct output from the parser. These use user-friendly
    explicit naming and distinguish top-level definitions from local let bindings. 
 x                            
 e : τ                        
 (a : A) → B                  
 λ x . e                      
 (x : A ; y : B ; z : C)      
 (x = a , y = b , z = c)      
 (A ; B ; C)                  
 (a , b , c)                  
 a b                          
 e.x                          
 e.i                          
 let x : τ = e in e'          
 Type                         
 Bool                         
 False                        
 True                         
 towards τ if e then a else b 
 ℕ                            
 Succ n                       
 rec n at τ                   
open Common


type expr =
  Zero                         
  0 , 1 , 2 , 3 , ...              
  | Zero . e₁ | Succ m , p . e₂

and stmt =
  | Def of name * expr option * expr
  | Inf of expr
  | Eval of expr
  | Exec of expr
  | Check of expr * expr
  | Conv of expr * expr * expr
  | Parse of expr
  | Import of string

type prog = stmt list