forked from anakrish/Rego-FStar
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRego.Main.fst
92 lines (80 loc) · 2.19 KB
/
Rego.Main.fst
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
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
module Rego.Main
open Rego.Ast
open Rego.Interpreter
open Rego.Value
let v1 = insert_at_path (Object []) (String "hello"::String "world"::[]) (Number 42)
let v2 = insert_at_path v1 (String "monde"::[]) v1
let v3 = insert_at_path v2 (v2::[]) v2
let v4 = Array (v1::v2::v3::[])
let expr = Ast.Array (
Ast.Value (String "hello")::
Ast.Value (String "world")::
Ast.Array (
Ast.Value (Number 42)::
Ast.Set (
Ast.Value (Number 3)::
Ast.Value (Number 2)::
Ast.Value (Number 1)::
Ast.Object (
(Ast.Value (String "Hello"), Ast.Value (String "World"))
::[]
)::
[]
)::[]
)::[]
)
let intr = Interpreter.make_new()
let (v5, intr1) = Interpreter.eval intr expr
// [ [a, b] |
// true
// a = {"English": "Hello", "French": "Salut"}
// b = a["English"]
// ]
let query = {
stmts= [
{ literal = Expr(Value(Bool true)); with_mods=[] }; // true
{ literal =
Expr(AssignExpr
(ColEq,
(Var "a"),
(Ast.Object [
(Value (String "English"), Value (String "Hello"));
(Value (String "French"), Value (String "Salut"));
]))
);
with_mods=[]
};
{
literal =
Expr(AssignExpr
(ColEq,
(Var "b"),
(RefBrack ((Var "a"), (Value (String "English")))))
);
with_mods=[]
};
{ literal = ArrayComprOutput (Ast.Array [Var "a"; Var"b"]);
with_mods = []; }
];
}
let intr2 = Interpreter.make_new()
let (v6, intr3) = Interpreter.eval_user_query intr2 query
let main () =
FStar.IO.print_string (to_json_pretty v1);
FStar.IO.print_string "\n";
FStar.IO.print_string (to_json_pretty v2);
FStar.IO.print_string "\n";
FStar.IO.print_string (to_json_pretty v3);
FStar.IO.print_string "\n";
FStar.IO.print_string (to_json_pretty v4);
FStar.IO.print_string "\n";
FStar.IO.print_string (to_json_pretty v5);
FStar.IO.print_string "\n";
FStar.IO.print_string (to_json_pretty v6);
FStar.IO.print_string "\n"
//Run ``main ()`` when the module loads
#push-options "--warn_error -272"
let _ = main ()
#pop-options