Add debruijn term

diff --git a/Temple.lean b/Temple.lean
index 8b015eb6b2f54eb3efefe68c97a1309d30449548..81fe8681b45b1ba39d29c9c3c16f5879afc48587 100644 (file)
--- a/Temple.lean
+++ b/Temple.lean
@@ -1 +1,2 @@
-import «Temple».Syntax
\ No newline at end of file
+import Temple.Syntax
+import Temple.DeBruijn
\ No newline at end of file

diff --git a/Temple/DeBruijn.lean b/Temple/DeBruijn.lean
new file mode 100644 (file)
index 0000000..f761fad
--- /dev/null
+++ b/Temple/DeBruijn.lean
@@ -0,0 +1,86 @@
+import Temple.Syntax
+
+namespace TempleDeBruijn
+
+inductive Var
+| bound : Int -> Var
+| free : String -> Var
+deriving BEq, Repr, Inhabited
+
+instance : ToString Var where
+  toString
+  | .bound i => toString i
+  | .free s => s
+
+inductive Term
+| text : String -> Term
+| op : String -> List String -> Term
+| var : Var -> Term
+| forloop : Var -> List Term -> Term
+deriving BEq, Repr, Inhabited
+
+partial instance : ToString Term where
+  toString :=
+    let rec toStr x :=
+      have : ToString Term := ⟨toStr⟩
+      match x with
+      | .text t => t
+      | .var v => "{{ " ++ toString v ++ " }}"
+      | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}"
+      | .forloop name body =>
+        "{% for " ++ toString name ++ " %}\n"
+          ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
+          ++ "\n{% endfor %}"
+    toStr
+
+def index (v : String) (binds : List String) : Option Nat :=
+  List.lookup v (List.zip binds (List.range (List.length binds)))
+
+partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term :=
+  match t with
+  | .text t => Term.text t
+  | .var v => match (index v binds) with
+    | .some i => .var (Var.bound i)
+    | .none => .var (Var.free v)
+  | .op n args => Term.op n args
+  | .forloop v range ts =>
+    let range_bind := match (index range binds) with
+      | .some i => Var.bound i
+      | .none => Var.free range
+    Term.forloop range_bind (List.map (fromSyntaxTermInner ([v] ++ binds)) ts)
+
+def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t
+
+section Test
+
+#eval show Bool from
+  let t := fromSyntaxTerm (.text "hello")
+  t == .text "hello"
+
+#eval show Bool from
+  let t := fromSyntaxTerm (.var "hello")
+  t == .var (.free "hello")
+
+#eval show Bool from
+  let t := fromSyntaxTerm (.op "hello" [ "world" ])
+  t == .op "hello" [ "world" ]
+
+#eval show IO Bool from do
+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .text "world", .var "x" ])
+  return t == .forloop (Var.free "fruits") [ .text "world", .var (.bound 0) ]
+
+#eval show IO Bool from do
+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "vegetables" [ .var "x", .var "y" ] ])
+  return t == .forloop (.free "fruits") [ .forloop (.free "vegetables") [ .var (.bound 1), .var (.bound 0) ] ]
+
+#eval show IO Bool from do
+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "x", .var "y" ] ])
+  return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.bound 1), .var (.bound 0) ] ]
+
+#eval show IO Bool from do
+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "hello", .var "y" ] ])
+  return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.free "hello"), .var (.bound 0) ] ]
+
+end Test
+
+end TempleDeBruijn
\ No newline at end of file