MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "DottedConstructors.ma" ---
--- scope checking ---
--- type checking ---
type  Unit : Set
term  Unit.unit : < Unit.unit : Unit >
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.suc : ^(n : Nat) -> < Nat.suc n : Nat >
term  plus : Nat -> Nat -> Nat
{ plus Nat.zero m = m
; plus (Nat.suc n) m = Nat.suc (plus n m)
}
type  List : ++(A : Set) -> Set
term  List.nil : .[A : Set] -> < List.nil : List A >
term  List.cons : .[A : Set] -> ^(x : A) -> ^(xs : List A) -> < List.cons x xs : List A >
type  Vec : ++(A : Set) -> ^(n : Nat) -> Set
term  Vec.vnil : .[A : Set] -> < Vec.vnil : Vec A Nat.zero >
term  Vec.vcons : .[A : Set] -> .[n : Nat] -> ^(vhead : A) -> ^(vtail : Vec A n) -> < Vec.vcons vhead vtail : Vec A (Nat.suc n) >
term  vhead : .[A : Set] -> .[n : Nat] -> (vcons : Vec A (Nat.suc n)) -> A
{ vhead [A] [n] (Vec.vcons #vhead #vtail) = #vhead
}
term  vtail : .[A : Set] -> .[n : Nat] -> (vcons : Vec A (Nat.suc n)) -> Vec A n
{ vtail [A] [n] (Vec.vcons #vhead #vtail) = #vtail
}
term  append : .[A : Set] -> .[n : Nat] -> .[m : Nat] -> Vec A n -> Vec A m -> Vec A (plus n m)
{ append [A] [.Nat.zero] [m] Vec.vnil ys = ys
; append [A] [.Nat.suc [n]] [m] (Vec.vcons x xs) ys = Vec.vcons x (append [A] [n] [m] xs ys)
}
type  Fin : ^(n : Nat) -> Set
term  Fin.fzero : .[n : Nat] -> < Fin.fzero : Fin (Nat.suc n) >
term  Fin.fsuc : .[n : Nat] -> ^(i : Fin n) -> < Fin.fsuc i : Fin (Nat.suc n) >
term  lookup : .[A : Set] -> .[n : Nat] -> (i : Fin n) -> (xs : Vec A n) -> A
{ lookup [A] [.Nat.zero] () Vec.vnil
; lookup [A] [.Nat.suc [n]] Fin.fzero (.Vec.vcons x xs) = x
; lookup [A] [.Nat.suc [n]] (Fin.fsuc i) (.Vec.vcons x xs) = lookup [A] [n] i xs
}
type  Ty : Set
term  Ty.nat : < Ty.nat : Ty >
term  Ty.arr : ^(a : Ty) -> ^(b : Ty) -> < Ty.arr a b : Ty >
type  Cxt : Set
type  Cxt = List Ty
type  Var : ^(cxt : Cxt) -> ^(a : Ty) -> Set
term  Var.vzero : .[a : Ty] -> .[cxt : List Ty] -> .[a : Ty] -> < Var.vzero : Var (List.cons a cxt) a >
term  Var.vsuc : .[a : Ty] -> .[cxt : List Ty] -> .[b : Ty] -> ^(x : Var cxt b) -> < Var.vsuc x : Var (List.cons a cxt) b >
type  Tm : ^(cxt : Cxt) -> ^(a : Ty) -> Set
term  Tm.var : .[cxt : Cxt] -> .[a : Ty] -> ^(x : Var cxt a) -> < Tm.var x : Tm cxt a >
term  Tm.app : .[cxt : List Ty] -> .[b : Ty] -> .[a : Ty] -> ^(r : Tm cxt (Ty.arr a b)) -> ^(s : Tm cxt a) -> < Tm.app a r s : Tm cxt b >
term  Tm.abs : .[cxt : List Ty] -> .[a : Ty] -> .[b : Ty] -> ^(t : Tm (List.cons a cxt) b) -> < Tm.abs t : Tm cxt (Ty.arr a b) >
type  Sem : Ty -> Set
{ Sem Ty.nat = Nat
; Sem (Ty.arr a b) = Sem a -> Sem b
}
type  Env : Cxt -> Set
{ Env List.nil = Unit
; Env (List.cons a as) = Sem a & Env as
}
term  val : .[cxt : Cxt] -> .[a : Ty] -> Var cxt a -> Env cxt -> Sem a
{ val [.List.cons [a] [cxt]] [.a] Var.vzero (v, vs) = v
; val [.List.cons [a] [cxt]] [b] (Var.vsuc x) (v, vs) = val [cxt] [b] x vs
}
term  sem : .[cxt : Cxt] -> .[a : Ty] -> Tm cxt a -> Env cxt -> Sem a
{ sem [cxt] [a] (Tm.var x) rho = val [cxt] [a] x rho
; sem [cxt] [b] (Tm.app [a] r s) rho = sem [cxt] [Ty.arr a b] r rho (sem [cxt] [a] s rho)
; sem [cxt] [.Ty.arr [a] [b]] (Tm.abs t) rho v = sem [List.cons a cxt] [b] t (v , rho)
}
--- evaluating ---
--- closing "DottedConstructors.ma" ---