Juvix.Core.Main.Language

Juvix.lean

@@ -1,3 +1,3 @@
 -- This module serves as the root of the `Juvix` library.
 -- Import modules here that should be built as part of the library.
-import Juvix.Basic
+import Juvix.Core.Main

Juvix/Core/Main.lean

@@ -0,0 +1,3 @@
+
+import Juvix.Core.Main.Language
+import Juvix.Core.Main.Semantics

Juvix/Core/Main/Language.lean

@@ -0,0 +1,3 @@
+
+import Juvix.Core.Main.Language.Base
+import Juvix.Core.Main.Language.Value

Juvix/Core/Main/Language/Base.lean

@@ -0,0 +1,40 @@
+
+namespace Juvix.Core.Main
+
+abbrev Name : Type := String
+
+inductive Constant : Type where
+  | int : Int → Constant
+  | string : String → Constant
+  deriving Inhabited, DecidableEq
+
+inductive BuiltinOp : Type where
+  | add_int : BuiltinOp
+  | sub_int : BuiltinOp
+  | mul_int : BuiltinOp
+  | div_int : BuiltinOp
+  deriving Inhabited, DecidableEq
+
+mutual
+  inductive Expr : Type where
+    | var : Nat → Expr
+    | ident : Name → Expr
+    | const : Constant → Expr
+    | app : Expr → Expr → Expr
+    | builtin_app : (oper : BuiltinOp) → (args : List Expr) → Expr
+    | constr_app : (constr : Name) → (args : List Expr) → Expr
+    | lambda : (body : Expr) → Expr
+    | let : (value : Expr) → (body : Expr) → Expr
+    | case : (value : Expr) → (branches : List CaseBranch) → Expr
+    | unit : Expr
+    deriving Inhabited
+
+  structure CaseBranch where
+    constr : Name
+    body : Expr
+end
+
+structure Program where
+  defs : List Expr
+
+end Juvix.Core.Main

Juvix/Core/Main/Language/Value.lean

@@ -0,0 +1,15 @@
+
+import Juvix.Core.Main.Language.Base
+
+namespace Juvix.Core.Main
+
+inductive Value : Type where
+  | const : Constant → Value
+  | constr_app : (constr : Name) → (args : List Value) → Value
+  | closure : (ctx : List Value) → (value : Expr) → Value
+  | unit : Value
+  deriving Inhabited
+
+abbrev Context : Type := List Value
+
+end Juvix.Core.Main

Juvix/Core/Main/Semantics.lean

@@ -0,0 +1,11 @@
+
+import Juvix.Core.Main.Language
+
+namespace Juvix.Core.Main
+
+def f : Expr -> Expr := λ e =>
+  match e with
+  | Expr.lambda (body := e) => e
+  | _ => Expr.lambda (body := e)
+
+end Juvix.Core.Main