repos / temple.lean4.git

DeBruijnEval.lean

  1import Std.Data.HashMap
  2
  3import Temple.DeBruijn
  4
  5open TempleDeBruijn
  6
  7namespace TempleDeBruijnEval
  8
  9inductive Value where
 10| text : String -> Value
 11| list : List Value -> Value
 12deriving BEq, Repr, Inhabited
 13
 14partial instance : ToString Value where
 15  toString :=
 16    let rec toStr x :=
 17      have : ToString Value := ⟨toStr⟩
 18      match x with
 19      | .text s => s
 20      | .list s => "[" ++ ",".intercalate (s.map toStr) ++ "]"
 21    toStr
 22
 23structure UserContext where
 24  data : Std.HashMap String Value := Std.HashMap.ofList []
 25  operators : Std.HashMap String (Value -> Except String Value) := Std.HashMap.ofList []
 26
 27def defaultOperators : List (Prod String (Value -> Except String Value)) :=
 28  let toUpper
 29    | .text t => return .text (String.toUpper t)
 30    | _ => throw "toUpper: list is not supported"
 31  let toLower
 32    | .text t => return .text (String.toLower t)
 33    | _ => throw "toLower: list is not supported"
 34  [ ("toUpper", toUpper), ("toLower", toLower) ]
 35
 36structure Context where
 37  data : Std.HashMap String Value
 38  operators : Std.HashMap String (Value -> Except String Value)
 39  binds : List Value := []
 40
 41private partial def eval' (ctx : Context) (t : Term) : IO String :=
 42  match t with
 43  | .text s => return s
 44  | .op name args =>
 45    match (Std.HashMap.get? ctx.operators name) with
 46    | .some operator => do
 47      let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
 48      let operatorResult := operator $ match resolvedArgs with
 49        | [x] => .text x
 50        | _ => .list $ resolvedArgs.map .text
 51      match operatorResult with
 52        | .ok r => return toString r
 53        | .error e => throw $ IO.userError s!"operator {name} execution result: {e}"
 54    | _ => throw $ IO.userError s!"\"{name}\" operator is not provided"
 55  | .forloop v ts => do
 56    let processVariable name o := match o with
 57      | .some (.text t) => return t.toList.map $ fun c => .text ([c].asString)
 58      | .some (.list vs) => return vs
 59      | .none => throw $ IO.userError s!"\"{name}\" is not provided"
 60    let vals <- match v with
 61      | .free n => processVariable n $ Std.HashMap.get? ctx.data n
 62      | .bound (i, n) => processVariable n ctx.binds[i]?
 63    let processVal val := ts.mapM $ eval' {ctx with binds := List.cons val ctx.binds }
 64    let results <- vals.mapM processVal
 65    return String.join (results.map String.join)
 66  | .var (.free n) => match (Std.HashMap.get? ctx.data n) with
 67    | .some v => return toString v
 68    | .none => throw $ IO.userError s!"\"{n}\" is not provided"
 69  | .var (.bound (i, n)) => match ctx.binds[i]? with
 70    | .some v => return toString v
 71    | .none => throw $ IO.userError s!"\"{n}\" is not defined in this scope"
 72
 73partial def eval (userContext : UserContext) : Term -> IO String :=
 74  TempleDeBruijnEval.eval'
 75    { data := userContext.data
 76    , operators := Std.HashMap.ofList $ defaultOperators ++ userContext.operators.toList
 77    }
 78
 79section Test
 80
 81#eval show IO Bool from do
 82  let t <- eval {} (.text "hello")
 83  return (t == "hello")
 84
 85#eval show IO Bool from do
 86  let t <- eval ({operators := Std.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])
 87  return (t == "world")
 88
 89#eval show IO Bool from do
 90  let t <- eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
 91                (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
 92  return (t == "hello worldhello land")
 93
 94#eval show IO Bool from do
 95  let t <- eval ({data := Std.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
 96                                                            , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
 97                (.forloop (Var.free "fruits")
 98                  [ .text "got an ", .var (.bound (0, "0")), .text "\n"
 99                  , .forloop (Var.free "vegetables") [ .var (.bound (0, "0")) ] ])
100  return (t == "got an apple\nsaladoniongot an orange\nsaladonion")
101
102#eval show IO String from
103  eval ({data := Std.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
104                                                            , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
105                (.forloop (Var.free "fruits")
106                  [ .text "got an ", .var (.bound (0, "0")), .text "\n"
107                  , .forloop (Var.free "vegetables") [ .var (.bound (1, "1")) ] ])
108
109#eval show IO String from
110  try
111    eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
112                  (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
113  catch e => pure s!"Caught exception: {e}"
114
115#eval show IO String from
116  try
117    eval ({data := Std.HashMap.ofList [ ]})
118                  (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
119  catch e => pure s!"Caught exception: {e}"
120
121#eval show IO String from
122  try
123    eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
124                  (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
125  catch e => pure s!"Caught exception: {e}"
126
127end Test
128
129end TempleDeBruijnEval