Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Program slicing for ambiguous dates computation #477

Draft
wants to merge 31 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
123b9c7
Add a new type of VC for date computation program slicing
denismerigoux Jun 15, 2023
40a40fb
Placeholder for scooping in variable values
denismerigoux Jun 19, 2023
1128c94
Lift asserts to scope
denismerigoux Jun 19, 2023
d23c0e2
Inside ctx rather than a returned list
denismerigoux Jun 19, 2023
a58e488
Generate possible values for variables in scope
denismerigoux Jun 19, 2023
715422e
Expression slicing for date comparison (to have more interesting resu…
rmonat Jun 21, 2023
1b57934
WIP (ugly code) on creating universal programs for date ambiguity det…
rmonat Jun 21, 2023
e57fb04
Formatting
denismerigoux Jun 22, 2023
fcc19f1
Refactor code and solve bindling problems
denismerigoux Jun 22, 2023
1740473
Simplify code
denismerigoux Jun 22, 2023
7d4d3e8
Identify unknown variables
denismerigoux Jun 22, 2023
eb10ccc
Fix variable categorization and make it recursive
denismerigoux Jun 23, 2023
bcc2a21
WIP on Catala/Mopsa-dates connection: program generation is almost co…
rmonat Jun 23, 2023
b08841e
Verification conditions, track variables typs more accurately
rmonat Jun 23, 2023
d61123c
Alpha version of Mopsa-compatible program generation
rmonat Jun 23, 2023
e2bf3cc
Format code
rmonat Jun 23, 2023
3e2a1ab
Mopsa export: top init all necessary variables
rmonat Jun 23, 2023
b062e1e
Format
rmonat Jun 23, 2023
7fea73e
WIP On Mopsa Backend
rmonat Jun 25, 2023
66678e6
Mopsa backend should work (when Mopsa is installed...)
rmonat Jun 25, 2023
1712de2
Two temporary changes we'll have to discuss
rmonat Jun 25, 2023
4982679
Formatting
denismerigoux Jun 26, 2023
c4b554b
Temporary fix in verification's dune
rmonat Jun 26, 2023
0ccc1d0
Unlinking unexisting files may crash indeed
rmonat Jun 26, 2023
2c45eec
Call mopsa-universal to avoid share path issues
rmonat Jun 26, 2023
ebe3efb
Formatting
denismerigoux Jun 27, 2023
5a88ad8
Cleaner code and more robust MOPSA obligation infrastructure
denismerigoux Jun 27, 2023
22faf14
Big refactoring
denismerigoux Jun 27, 2023
97b8709
More informative warning and debug messages when Mopsa cannot analyze…
rmonat Dec 7, 2023
4413af3
Tweak ppx_yojson version
rmonat Dec 8, 2023
ad81409
Fix dummy z3 backend with compatible IO interface
rmonat Dec 8, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion catala.opam
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ depends: [
"ocaml" {>= "4.13.0"}
"ocamlfind" {!= "1.9.5"}
"ocamlgraph" {>= "1.8.8"}
"ppx_yojson_conv" {>= "0.14.0"}
"ppx_yojson_conv" {= "v0.15.1"}
"re" {>= "1.9.0"}
"sedlex" {>= "2.4"}
"uutf" {>= "1.0.3"}
Expand Down
3 changes: 1 addition & 2 deletions compiler/driver.ml
Original file line number Diff line number Diff line change
Expand Up @@ -370,8 +370,7 @@ let driver source_file (options : Cli.options) : int =
| None -> None
| Some _ -> Some scope_uid)
in

Verification.Solver.solve_vc prgm.decl_ctx vcs
Verification.Solver.solve_vcs prgm.decl_ctx vcs
| `Interpret ->
Message.emit_debug "Starting interpretation (dcalc)...";
let results =
Expand Down
5 changes: 4 additions & 1 deletion compiler/shared_ast/print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -542,7 +542,10 @@ let rec expr_aux :
pr colors fmt e;
Format.pp_close_box fmt ()
| EApp { f = EOp { op; _ }, _; args = [arg1] } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" (operator ~debug) op (rhs exprc) arg1
(* FIXME: I'd like to have an imperative style printing of function calls
(ie f(a,b,c) rather than (f a b c)) for Mopsa export. How to concialiate
both? *)
Format.fprintf fmt "@[<hv 2>%a(%a)@]" (operator ~debug) op (rhs exprc) arg1
| EApp { f; args } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
(Format.pp_print_list
Expand Down
10 changes: 10 additions & 0 deletions compiler/shared_ast/var.ml
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,11 @@ module Set = struct
let of_list l = of_list (List.map t l)
let elements s = elements s |> List.map get
let diff s1 s2 = diff s1 s2
let choose_opt s = Option.map get (choose_opt s)
let filter f s = filter (fun v -> f (get v)) s
let exists f s = exists (fun v -> f (get v)) s
let inter s1 s2 = inter s1 s2
let fold f s init = fold (fun v acc -> f (get v) acc) s init

(* Add more as needed *)
end
Expand All @@ -95,9 +100,14 @@ module Map = struct
let find v m = find (t v) m
let find_opt v m = find_opt (t v) m
let bindings m = bindings m |> List.map (fun (v, x) -> get v, x)
let map f m = map f m
let mapi f m = mapi (fun v x -> f (get v) x) m
let mem x m = mem (t x) m
let union f m1 m2 = union (fun v x1 x2 -> f (get v) x1 x2) m1 m2
let fold f m acc = fold (fun v x acc -> f (get v) x acc) m acc
let filter f m = filter (fun k v -> f (get k) v) m
let exists f m = exists (fun k v -> f (get k) v) m
let remove x s = remove (t x) s

(* Add more as needed *)
end
10 changes: 10 additions & 0 deletions compiler/shared_ast/var.mli
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,11 @@ module Set : sig
val of_list : 'e var list -> 'e t
val elements : 'e t -> 'e var list
val diff : 'e t -> 'e t -> 'e t
val choose_opt : 'e t -> 'e var option
val filter : ('e var -> bool) -> 'e t -> 'e t
val exists : ('e var -> bool) -> 'e t -> bool
val inter : 'e t -> 'e t -> 'e t
val fold : ('e var -> 'x -> 'x) -> 'e t -> 'x -> 'x
end

(** Wrapper over [Map.S] but with a type variable for the AST type parameters.
Expand All @@ -59,14 +64,19 @@ module Map : sig
val empty : ('e, 'x) t
val singleton : 'e var -> 'x -> ('e, 'x) t
val add : 'e var -> 'x -> ('e, 'x) t -> ('e, 'x) t
val remove : 'e var -> ('e, 'x) t -> ('e, 'x) t
val update : 'e var -> ('x option -> 'x option) -> ('e, 'x) t -> ('e, 'x) t
val find : 'e var -> ('e, 'x) t -> 'x
val find_opt : 'e var -> ('e, 'x) t -> 'x option
val bindings : ('e, 'x) t -> ('e var * 'x) list
val mem : 'e var -> ('e, 'x) t -> bool
val map : ('x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
val mapi : ('e var -> 'x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
val filter : ('e var -> 'x -> bool) -> ('e, 'x) t -> ('e, 'x) t

val union :
('e var -> 'x -> 'x -> 'x option) -> ('e, 'x) t -> ('e, 'x) t -> ('e, 'x) t

val fold : ('e var -> 'x -> 'acc -> 'acc) -> ('e, 'x) t -> 'acc -> 'acc
val exists : ('e var -> 'x -> bool) -> ('e, 'x) t -> bool
end
Loading