rego-proofs.git - Lean proofs for my Master's thesis

Age	Commit message (Expand)	Author
2023-11-07	Basic expression simplification	Jakob L. Kreuze
2023-11-07	Fix parsing issue for set rules	Jakob L. Kreuze
2023-11-07	Compile imports (not really)	Jakob L. Kreuze
2023-11-07	Re-instate assignment order assertion	Jakob L. Kreuze
2023-11-07	Handle existential quantification over objects	Jakob L. Kreuze
2023-11-03	Checkpoint	Jakob L. Kreuze
2023-11-03	More reliable handling of rules with formal parameters	Jakob L. Kreuze
2023-11-03	Ensure identifiers produced by gensym are legal Lean variable names	Jakob L. Kreuze
2023-11-02	Add support for Negate rules	Jakob L. Kreuze
2023-11-02	Parse Negate properly	Jakob L. Kreuze
2023-11-02	Compile functions	Jakob L. Kreuze
2023-11-02	Minor refactoring	Jakob L. Kreuze
2023-11-01	Initial attempt at compiling rules with sets/objects as headsa	Jakob L. Kreuze
2023-11-01	Fix assignment rule parsing	Jakob L. Kreuze
2023-11-01	Compile default rules	Jakob L. Kreuze
2023-11-01	Compile references to inductively-defined variables	Jakob L. Kreuze
2023-11-01	Replace complete with more detailed description of variable usage	Jakob L. Kreuze
2023-10-31	Add support for nested definitions	Jakob L. Kreuze
2023-10-31	Use gensym for generated identifiers	Jakob L. Kreuze
2023-10-31	Error on variables used before assignment	Jakob L. Kreuze
2023-10-31	Assigned field for variable records	Jakob L. Kreuze
2023-10-31	More detailed variable usage analysis	Jakob L. Kreuze
2023-10-31	No longer need to pass up local definitions	Jakob L. Kreuze
2023-10-30	Basic scope construction	Jakob L. Kreuze
2023-10-30	Re-do first pass variable identification	Jakob L. Kreuze
2023-10-26	Compiles examples/01-computable-assign-scalar.rego	Jakob L. Kreuze
2023-10-26	Export more operations on AST elements	Jakob L. Kreuze
2023-10-25	Return side information when compiling terms	Jakob L. Kreuze
2023-10-24	Compile literals	Jakob L. Kreuze
2023-10-21	Import Lean representation from XACML compiler	Jakob L. Kreuze
2023-10-21	Last refactoring before sending out update	Jakob L. Kreuze
2023-10-21	Move OPA interaction to AST module	Jakob L. Kreuze
2023-10-21	ocamlformat	Jakob L. Kreuze
2023-10-21	Integrate test suite	Jakob L. Kreuze
2023-10-21	Extract functionality to library	Jakob L. Kreuze
2023-10-19	Initial ast walking example	Jakob L. Kreuze
2023-10-19	Fix parse errors on existing examples	Jakob L. Kreuze
2023-10-17	Complete parsing of rule_head_rhs	Jakob L. Kreuze
2023-10-17	Complete parsing of expressions	Jakob L. Kreuze
2023-10-17	Allow call as a term	Jakob L. Kreuze
2023-10-17	Last commit before allowing calls as expressions	Jakob L. Kreuze
2023-10-17	Re-implement in terms of parse_term	Jakob L. Kreuze
2023-10-17	Re-order inductive definitions	Jakob L. Kreuze
2023-10-17	Remove infix/unary operators	Jakob L. Kreuze
2023-10-17	Complete parse_term	Jakob L. Kreuze
2023-10-17	Better support for parsing bodies	Jakob L. Kreuze
2023-10-15	Rego compiler: initial commit	Jakob L. Kreuze
2023-09-12	Prepare to replay XACML repository on top of this one	Jakob L. Kreuze