1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
open Ast
open Core
open Lean
module Environ = Map.Make (String)
type environ = string Environ.t
let rec term_ground (env : environ) (term : term) : bool =
match term with
| Var name -> Map.find env name |> Option.is_some
| Ref (Var name, _) -> Map.find env name |> Option.is_some
| Call (_, subterms) ->
List.reduce_exn ~f:( && ) (List.map ~f:(term_ground env) subterms)
| _ -> true
let map_with_environment_updates env xs fn =
List.fold xs ~init:(env, []) ~f:(fun (env, ys) x ->
let env', y = fn env x in
(env', List.append ys [ y ]))
let extract_local_variables (env : environ) (q : query) : string list =
let handle_term env : term -> (environ * string list) = function
| Call ((Var func, []), [ Var name; rhs ])
when String.equal func "assign" || String.equal func "eq" ->
if Map.find env name |> Option.is_none && term_ground env rhs then
match Map.add env ~key:name ~data:name with
| `Duplicate -> failwith "should shadow?"
| `Ok env' -> (env', [ name ])
else (env, [])
| _ -> (env, [])
in
let handle_expr env = function
| Term t -> handle_term env t
| Every (Some _key, _value, _, _q) -> failwith "unimplemented"
| Every (None, _value, _, _q) -> failwith "unimplemented"
in
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)
| Expr (expr, _) -> handle_expr env expr
| Negate (expr, _) -> handle_expr env expr
in
let _env', identifiers = map_with_environment_updates env q handle_literal in
List.concat identifiers
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)
|
