repos / temple.lean4.git

DeBruijn.lean

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