Normalization-By-Evaluation example

examples/normalization-by-evaluation.hvm

@@ -0,0 +1,313 @@
+// Pair
+// ====
+
+// (PairGet (Pair a b) (∀a ∀b c)) : c
+(PairGet (Pair x y) fn) = (fn x y)
+
+// Maybe
+// =====
+
+// (Default (Maybe a) a) : a
+(Default None     y) = y
+(Default (Some x) y) = x
+
+(ToMaybe 0 x) = None
+(ToMaybe 1 x) = (Some x)
+
+// List
+// ====
+
+// (Find (∀a (Maybe b)) (List a)) : (Maybe b)
+(Find cond Nil)             = None
+(Find cond (Cons x xs))     = (FindGo (cond x) cond xs)
+  (FindGo None     cond xs) = (Find cond xs)
+  (FindGo (Some x) cond xs) = (Some x)
+
+// String
+// ======
+
+// (StrIsEmpty String) : Bool
+(StrIsEmpty StrNil)         = 1
+(StrIsEmpty (StrCons x xs)) = 0
+
+// (StrConcat a:String b:String) : String
+(StrConcat StrNil         ys) = ys
+(StrConcat (StrCons x xs) ys) = (StrCons x (StrConcat xs ys))
+
+// (StrFlatten a:(List String)) : String
+(StrFlatten Nil)         = StrNil
+(StrFlatten (Cons x xs)) = (StrConcat x (StrFlatten xs))
+
+// (StrEqual (List String) (List String)) : U32
+(StrEqual StrNil         StrNil)         = 1
+(StrEqual (StrCons x xs) (StrCons y ys)) = (& (== x y) (StrEqual xs ys))
+(StrEqual xs             ys)             = 0
+
+// Todo: improve this
+// (StrHash String) : String
+(StrHash str) = (StrHashGo str 0)
+  (StrHashGo StrNil         hash) = hash
+  (StrHashGo (StrCons x xs) hash) = (StrHashGo xs (+ (- (<< hash 5) hash) x))
+
+// Parser
+// ======
+
+// Code : Type
+// Code = String
+
+// Answer : Type -> Type
+// Answer A = Parsed Code A | Failed String
+
+// Parser : Type -> Type
+// Parser A = Code -> Answer A
+
+// (IsNameChar Char) : Bool
+(IsNameChar chr) =
+  let is_letter = (| (& (<= 'a' chr) (<= chr 'z')) (& (<= 'A' chr) (<= chr 'Z')))
+  let is_number = (& (<= '0' chr) (<= chr '9'))
+  let is_symbol = (& (== '_' chr) (== '.' chr))
+  (| is_letter (| is_number is_symbol))
+
+// (Bind a_parser:(Parser a) b_parser:(∀a (Parser B))) : (Parser B)
+(Bind a_parser b_parser) = λcode (BindGo b_parser (a_parser code))
+  (BindGo b_parser (Parsed code a_val)) = (b_parser a_val code)
+  (BindGo b_parser (Failed err))        = (Failed err)
+
+// (Done val:a) : (Parser a)
+(Done value) = λcode (Parsed code value)
+
+// (IsSpace Char) : Bool
+(IsSpace chr) = (| (== 10 chr) (== ' ' chr))
+
+// (GetName String) : (Pair code:String name:String)
+(GetName)                             = λcode (GetNameGo code)
+  (GetNameGo StrNil)                  = (Pair StrNil StrNil)
+  (GetNameGo (StrCons head tail))     = (GetName_1 (IsNameChar head) head tail)
+    (GetName_1 0 head tail)           = (Pair (StrCons head tail) StrNil)
+    (GetName_1 1 head tail)           = (GetName_2 head (GetNameGo tail))
+    (GetName_2 head (Pair code name)) = (Pair code (StrCons head name))
+
+// (PeekHere text:String) : (Parser Bool)
+(PeekHere text)                               = λcode (Peek_0 text code λx(x))
+  (Peek_0 StrNil         ys             init) = (Parsed (init ys)  True)
+  (Peek_0 (StrCons x xs) StrNil         init) = (Parsed (init Nil) False)
+  (Peek_0 (StrCons x xs) (StrCons y ys) init) = (Peek_1 (== x y) xs y ys init)
+  (Peek_1 0 xs y ys init)                     = (Parsed (init (StrCons y ys)) False)
+  (Peek_1 1 xs y ys init)                     = (Peek_0 xs ys λk (init (StrCons y k)))
+
+// TODO: simplify by calling Peek here
+// (MatchHere text:String) : (Parser Bool)
+(MatchHere text)                               = λcode (Match_0 text code λx(x))
+  (Match_0 StrNil         ys             init) = (Parsed ys True)
+  (Match_0 (StrCons x xs) StrNil         init) = (Parsed (init Nil) False)
+  (Match_0 (StrCons x xs) (StrCons y ys) init) = (Match_1 (== x y) xs y ys init)
+  (Match_1 0 xs y ys init)                     = (Parsed (init (StrCons y ys)) False)
+  (Match_1 1 xs y ys init)                     = (Match_0 xs ys λk (init (StrCons y k)))
+
+// (Match text:String) : (Parser Bool)
+(Match text) = λcode ((MatchHere text) (SkipSpaces code))
+
+// (ParseTextHere text:String) : (Parser Unit)
+(ParseTextHere text)      = (Bind (MatchHere text) λgot(ParseTextHere_0 got))
+  (ParseTextHere_0 False) = (Failed "Expected...")
+  (ParseTextHere_0 True)  = (Done Unit)
+
+// (ParseText text:String) : (Parser Unit)
+(ParseText text) = λcode ((ParseTextHere text) (SkipSpaces code))
+
+// (SkipSpaces String) : String
+(SkipSpaces (StrCons x xs)) = (SkipSpaces_0 (IsSpace x) x xs)
+  (SkipSpaces_0 0 x xs)     = (StrCons x xs)
+  (SkipSpaces_0 1 x xs)     = (SkipSpaces xs)
+
+// (ParseNameHere) : (Parser String)
+ParseNameHere                        = λcode (ParseNameHere_0 ((GetName) code))
+  (ParseNameHere_0 (Pair code name)) = (Parsed code name)
+
+// (ParseName) : (Parser String)
+ParseName = λcode ((ParseNameHere) (SkipSpaces code))
+
+// (Grammar choices:(List (Parser (Maybe a)))) : (Parser a)
+(Grammar Nil)                                     = λcode (Failed "Expected...")
+(Grammar (Cons choice choices))                   = λcode (Grammar_0 (choice code) choices)
+  (Grammar_0 (Failed err)                choices) = (Failed err)
+  (Grammar_0 (Parsed code None)          choices) = ((Grammar choices) code)
+  (Grammar_0 (Parsed code (Some result)) choices) = (Parsed code result)
+
+// Note: unlike Rust's version, this won't rollback
+// (Guard head:(Parser Bool) body:(Parser a)) : (Parser (Maybe a))
+(Guard head body) = λcode (Guard_0 (head code) body)
+  (Guard_0 (Failed err)          body) = (Failed err)
+  (Guard_0 (Parsed code False)   body) = (Parsed code None)
+  (Guard_0 (Parsed code True)    body) = ((Bind body λgot(Done (Some got))) code)
+
+// Term
+// ====
+
+// Term Parsing
+// ------------
+
+// (ParseLet) : (Parser (Maybe Term))
+(ParseLet) = (Guard (Match "let ")
+  (Bind ParseName λname
+  (Bind (ParseText "=") λx
+  (Bind ParseTerm     λexpr
+  (Bind ParseTerm     λbody
+  (Done (Let name expr body)))))))
+
+// (ParseLam) : (Parser (Maybe Term))
+(ParseLam) = (Guard (Match "λ")
+  (Bind ParseNameHere λname
+  (Bind ParseTerm     λbody
+  (Done (Lam name body)))))
+
+// (ParseApp) : (Parser (Maybe Term)) 
+(ParseApp) = (Guard (Match "(")
+  (Bind ParseTerm       λfunc
+  (Bind ParseTerm       λargm
+  (Bind (ParseText ")") λx
+  (Done (App func argm))))))
+
+// (ParseCtr) : (Parser (Maybe Term))
+(ParseCtr) =
+  (Guard (Match "[")
+    (Bind ParseName    λctor
+    (Bind ParseCtrArgs λargs
+    (Done (Ctr ctor args)))))
+  (ParseCtrArgs) =
+    (Bind (Match "]") λdone
+    (ParseCtrArgs_0 done))
+  (ParseCtrArgs_0 True) =
+    (Done Nil)
+  (ParseCtrArgs_0 False) =
+    (Bind ParseTerm    λhead
+    (Bind ParseCtrArgs λtail
+    (Done (Cons head tail))))
+
+// (ParseVar) : (Parser (Maybe Term))
+(ParseVar) = (Bind ParseName λname (ParseVar_0 name))
+  (ParseVar_0 StrNil        ) = (Done None)
+  (ParseVar_0 (StrCons x xs)) = (Done (Some (Var (StrCons x xs))))
+
+// (ParseTerm) : (Parser Term)
+(ParseTerm) = (Grammar [
+  ParseLet,
+  ParseLam,
+  ParseApp,
+  ParseCtr,
+  ParseVar,
+])
+
+// (Read code) : Term
+(Read code) = (Read_0 ((ParseTerm) code))
+  (Read_0 (Parsed code term)) = term
+
+// Term Stringification
+// --------------------
+
+// (Show term:Term) : String
+(Show term) = ((ShowGo term) "")
+  (ShowGo (Let name expr body)) =
+    λx((ShowGoStr "let ")
+      ((ShowGoStr name)
+      ((ShowGoStr " = ")
+      ((ShowGo expr)
+      ((ShowGoStr "; ")
+      ((ShowGo body)
+      x))))))
+  (ShowGo (Lam name body)) =
+    λx((ShowGoStr "λ")
+      ((ShowGoStr name)
+      ((ShowGoStr " ")
+      ((ShowGo body)
+      x))))
+  (ShowGo (App func argm)) =
+    λx((ShowGoStr "(")
+      ((ShowGo func)
+      ((ShowGoStr " ")
+      ((ShowGo argm)
+      ((ShowGoStr ")")
+      x)))))
+  (ShowGo (Ctr ctor args)) =
+    λx((ShowGoStr "[")
+      ((ShowGoStr ctor)
+      ((ShowGoCtrArgs args)
+      ((ShowGoStr "]")
+      x))))
+    (ShowGoCtrArgs Nil) = λx x
+    (ShowGoCtrArgs (Cons head tail)) =
+      λx((ShowGoStr " ")
+        ((ShowGo head)
+        ((ShowGoCtrArgs tail)
+        x)))
+  (ShowGo (Var name)) =
+    λx((ShowGoStr name)
+      x)
+  (ShowGoStr xs) =
+    λx(StrConcat xs x)
+
+// Term Evaluation
+// ---------------
+
+// Counts free occurrences of a name
+(Count nm (Var name))      = (StrEqual name nm)
+(Count nm (App func argm)) = (+ (Count nm func) (Count nm argm))
+(Count nm (Lam name body)) = (CountShadow (StrEqual nm name) nm body)
+  (CountShadow 0 nm body) = (Count nm body) 
+  (CountShadow 1 nm body) = 0
+
+// Appends N copies of a term to a vars context
+(Clone 0 name term ctx) = ctx
+(Clone 1 name term ctx) = (Cons (Pair name term) ctx)
+(Clone n name term ctx) = (Cons (Pair name term) (Clone (- n 1) name term ctx))
+
+// Converts a term to high-order
+// (High term:Term) : HTerm
+(High term) = (PairGet (HighGo term Nil) λx λy y)
+  (HighGo (Var name) vars) = (HighFind name vars)
+    (HighFind name (Cons (Pair var val) vars)) = (HighFound (StrEqual name var) name var val vars)
+      (HighFound 1 name var val vars) = (Pair vars val)
+      (HighFound 0 name var val vars) = (PairGet (HighFind name vars) λvars λgot (Pair (Cons (Pair var val) vars) got))
+  (HighGo (Let name expr body) vars) =
+    (PairGet (HighGo expr vars)                       λvars λexpr
+    (PairGet (HighGo body (Cons (Pair name $x) vars)) λvars λbody
+    (Pair vars (HLet expr λ$x body))))
+  (HighGo (App func argm) vars) =
+    (PairGet (HighGo func vars) λvars λfunc
+    (PairGet (HighGo argm vars) λvars λargm
+    (Pair vars (HApply func argm))))
+  (HighGo (Lam name body) vars) =
+    let vars = (Clone (Count name body) name $x vars)
+    (PairGet (HighGo body vars) λvars λbody
+    (Pair vars (HLam λ$x body)))
+  (HighGo (Ctr ctor args) vars) =
+    (PairGet (HighGoArgs args vars) λvars λargs
+      (Pair vars (HCtr ctor args)))
+    (HighGoArgs Nil vars) =
+      (Pair vars Nil)
+    (HighGoArgs (Cons head tail) vars) =
+      (PairGet (HighGo head vars) λvars λhead
+      (PairGet (HighGoArgs tail vars) λvars λtail
+      (Pair vars (Cons head tail))))
+
+// Application
+(HApply (HLam fbody) argm) = (fbody argm)
+(HApply func         argm) = (HApp func argm)
+
+// Converts a term to low-order
+(Low term) = (LowGo term 0)
+  (LowGo (HVar name) depth) = (Var name)
+  (LowGo (HLam body) depth) =
+    let name = (StrCons (+ 97 depth) StrNil)
+    let body = (LowGo (body (HVar name)) (+ depth 1))
+    (Lam name body)
+  (LowGo (HApp func argm) depth) =
+    let func = (LowGo func depth)
+    let argm = (LowGo argm depth)
+    (App func argm)
+
+(Main n) =
+  let term = (Read "(λf λx (f (f (f (f x)))) λf λx (f (f (f (f x)))))")
+  let term = (High term)
+  let term = (Low term)
+  (Show term)