From 71739f089d790cd238b44b8ab533da7d2b026ffb Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Tue, 24 Oct 2023 18:59:42 -0400
Subject: Compile literals

---
 rego-proofs/compiler-rewrite/lib/compiler.ml | 54 +++++++++++++++++++++++++++-
 rego-proofs/compiler-rewrite/lib/lean.ml     |  4 +--
 rego-proofs/compiler-rewrite/lib/lean.mli    |  2 +-
 3 files changed, 56 insertions(+), 4 deletions(-)

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 57b93e7..fbf5ceb 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -1,5 +1,6 @@
 open Ast
 open Core
+open Lean
 
 module Environ = Map.Make (String)
 type environ = string Environ.t
@@ -33,7 +34,7 @@ let extract_local_variables (env : environ) (q : query) : string list =
     | Every (Some _key, _value, _, _q) -> failwith "unimplemented"
     | Every (None, _value, _, _q) -> failwith "unimplemented"
   in
-  let handle_literal env = function
+  let handle_literal env : literal -> (environ * string list) = function
     | Exists (exprs, _) ->
         let env', ys = map_with_environment_updates env exprs handle_expr in
         (env', ys |> List.concat)
@@ -46,3 +47,54 @@ let extract_local_variables (env : environ) (q : query) : string list =
 
 let extract_local_variables_wrapper (q : query) : string list =
   extract_local_variables Environ.empty q
+
+(* --- *)
+
+let term_of_object_key : object_key -> term = function
+  | Scalar s -> Scalar s
+  | Ref r    -> Ref r
+  | Var v    -> Var v
+
+let term_of_ref_target : ref_target -> term = function
+  | Var s                        -> Var s
+  | Array xs                     -> Array xs
+  | Object kvs                   -> Object kvs
+  | Set xs                       -> Set xs
+  | ArrayComprehension (key, q)  -> ArrayComprehension (key, q)
+  | ObjectComprehension (key, q) -> ObjectComprehension (key, q)
+  | SetComprehension (key, q)    -> SetComprehension (key, q)
+  | Call (fn, args)              -> Call (fn, args)
+
+let rec compile_term env : term -> lean_expression = function
+  | Scalar s ->
+     (match s with
+      | String s -> Application (Identifier "Rego.Any.str",  [String s])
+      | Number x -> Application (Identifier "Rego.Any.num",  [Number x])
+      | Bool b   -> Application (Identifier "Rego.Any.bool", [Bool b])
+      | Null     -> Application (Identifier "Rego.Any.null", []))
+  | Var id -> Identifier (Map.find_exn env id)
+  | Ref (target, terms) ->
+    List.fold
+      terms
+      ~init:(compile_term env (term_of_ref_target target))
+      ~f:(fun x y -> (Application ((Identifier "Rego.Any.deref"), [x; compile_term env y])))
+  | Array xs ->
+     Application (Identifier "Rego.Any.array", List.map ~f:(compile_term env) xs)
+  | Set xs ->
+     Application (Identifier "Rego.Any.set", List.map ~f:(compile_term env) xs)
+  | Object kvs ->
+     let compile_kv = function
+       | (key, value) ->
+          Tuple [compile_term env (term_of_object_key key);
+                 compile_term env value]
+     in
+     Application (Identifier "Rego.Any.object", List.map ~f:compile_kv kvs)
+  | ArrayComprehension (_term, _query) ->
+     failwith "unimplemented"
+  | SetComprehension (_term, _query) ->
+     failwith "unimplemented"
+  | ObjectComprehension ((_key, _value), _query) ->
+     failwith "unimplemented"
+  | Call (fn, args) ->
+     let head = compile_term env (Ref fn) in
+     Application (head, List.map ~f:(compile_term env) args)
diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler-rewrite/lib/lean.ml
index d670d5e..975b563 100644
--- a/rego-proofs/compiler-rewrite/lib/lean.ml
+++ b/rego-proofs/compiler-rewrite/lib/lean.ml
@@ -4,7 +4,7 @@ type lean_expression =
   | Identifier of string
   | Bool of bool
   | String of string
-  | Number of int
+  | Number of float
   | List of lean_expression list
   | Tuple of lean_expression list
   | Application of lean_expression * lean_expression list
@@ -22,7 +22,7 @@ let rec fmt_lean_expression : lean_expression -> string = function
   | Identifier s -> s
   | Bool b -> if b then "True" else "False"
   | String s -> Printf.sprintf "\"%s\"" s
-  | Number n -> Int.to_string n
+  | Number n -> Float.to_string n
   | List xs ->
       Printf.sprintf "[%s]"
         (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler-rewrite/lib/lean.mli
index c77cf81..3b2b10c 100644
--- a/rego-proofs/compiler-rewrite/lib/lean.mli
+++ b/rego-proofs/compiler-rewrite/lib/lean.mli
@@ -2,7 +2,7 @@ type lean_expression =
   | Identifier of string
   | Bool of bool
   | String of string
-  | Number of int
+  | Number of float
   | List of lean_expression list
   | Tuple of lean_expression list
   | Application of lean_expression * lean_expression list
-- 
cgit v1.3