repos / temple.lean4.git

commit

001063c

parent

0fe449a

author

Evgenii Akentev

date

2024-03-24 13:09:47 +0400 +04

Add debruijn term

1@@ -1 +1,2 @@
2-import «Temple».Syntax
3+import Temple.Syntax
4+import Temple.DeBruijn

 1@@ -0,0 +1,86 @@
 2+import Temple.Syntax
 3+
 4+namespace TempleDeBruijn
 5+
 6+inductive Var
 7+| bound : Int -> Var
 8+| free : String -> Var
 9+deriving BEq, Repr, Inhabited
10+
11+instance : ToString Var where
12+  toString
13+  | .bound i => toString i
14+  | .free s => s
15+
16+inductive Term
17+| text : String -> Term
18+| op : String -> List String -> Term
19+| var : Var -> Term
20+| forloop : Var -> List Term -> Term
21+deriving BEq, Repr, Inhabited
22+
23+partial instance : ToString Term where
24+  toString :=
25+    let rec toStr x :=
26+      have : ToString Term := ⟨toStr⟩
27+      match x with
28+      | .text t => t
29+      | .var v => "{{ " ++ toString v ++ " }}"
30+      | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}"
31+      | .forloop name body =>
32+        "{% for " ++ toString name ++ " %}\n"
33+          ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
34+          ++ "\n{% endfor %}"
35+    toStr
36+
37+def index (v : String) (binds : List String) : Option Nat :=
38+  List.lookup v (List.zip binds (List.range (List.length binds)))
39+
40+partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term :=
41+  match t with
42+  | .text t => Term.text t
43+  | .var v => match (index v binds) with
44+    | .some i => .var (Var.bound i)
45+    | .none => .var (Var.free v)
46+  | .op n args => Term.op n args
47+  | .forloop v range ts =>
48+    let range_bind := match (index range binds) with
49+      | .some i => Var.bound i
50+      | .none => Var.free range
51+    Term.forloop range_bind (List.map (fromSyntaxTermInner ([v] ++ binds)) ts)
52+
53+def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t
54+
55+section Test
56+
57+#eval show Bool from
58+  let t := fromSyntaxTerm (.text "hello")
59+  t == .text "hello"
60+
61+#eval show Bool from
62+  let t := fromSyntaxTerm (.var "hello")
63+  t == .var (.free "hello")
64+
65+#eval show Bool from
66+  let t := fromSyntaxTerm (.op "hello" [ "world" ])
67+  t == .op "hello" [ "world" ]
68+
69+#eval show IO Bool from do
70+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .text "world", .var "x" ])
71+  return t == .forloop (Var.free "fruits") [ .text "world", .var (.bound 0) ]
72+
73+#eval show IO Bool from do
74+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "vegetables" [ .var "x", .var "y" ] ])
75+  return t == .forloop (.free "fruits") [ .forloop (.free "vegetables") [ .var (.bound 1), .var (.bound 0) ] ]
76+
77+#eval show IO Bool from do
78+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "x", .var "y" ] ])
79+  return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.bound 1), .var (.bound 0) ] ]
80+
81+#eval show IO Bool from do
82+  let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "hello", .var "y" ] ])
83+  return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.free "hello"), .var (.bound 0) ] ]
84+
85+end Test
86+
87+end TempleDeBruijn