mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-20 00:41:05 +03:00
Test without func now pass!
This commit is contained in:
parent
341ee710d8
commit
64cf1fd7cd
@ -161,7 +161,7 @@ let empty_thunked_term : Ast.expr Pos.marked =
|
|||||||
Pos.no_pos [ (Ast.TUnit, Pos.no_pos) ] Pos.no_pos)
|
Pos.no_pos [ (Ast.TUnit, Pos.no_pos) ] Pos.no_pos)
|
||||||
|
|
||||||
let interpret_program (e : Ast.expr Pos.marked) : (Ast.Var.t * Ast.expr Pos.marked) list =
|
let interpret_program (e : Ast.expr Pos.marked) : (Ast.Var.t * Ast.expr Pos.marked) list =
|
||||||
match Pos.unmark e with
|
match Pos.unmark (evaluate_expr e) with
|
||||||
| Ast.EAbs (_, binder, taus) -> (
|
| Ast.EAbs (_, binder, taus) -> (
|
||||||
let application_term = List.map (fun _ -> empty_thunked_term) taus in
|
let application_term = List.map (fun _ -> empty_thunked_term) taus in
|
||||||
let to_interpret = (Ast.EApp (e, application_term), Pos.no_pos) in
|
let to_interpret = (Ast.EApp (e, application_term), Pos.no_pos) in
|
||||||
|
@ -115,6 +115,6 @@ let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
|
|||||||
if List.length subs = 0 then
|
if List.length subs = 0 then
|
||||||
Format.fprintf fmt "@[⟨%a ⊢ %a⟩@]" format_expr just format_expr cons
|
Format.fprintf fmt "@[⟨%a ⊢ %a⟩@]" format_expr just format_expr cons
|
||||||
else
|
else
|
||||||
Format.fprintf fmt "@[⟨%a ⊢ %a | %a⟩@]" format_expr just format_expr cons
|
Format.fprintf fmt "@[<hov 2>⟨%a ⊢ %a |@ %a⟩@]" format_expr just format_expr cons
|
||||||
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr)
|
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr)
|
||||||
subs
|
subs
|
||||||
|
@ -52,10 +52,7 @@ let merge_defaults (caller : Dcalc.Ast.expr Pos.marked Bindlib.box)
|
|||||||
Pos.no_pos ))
|
Pos.no_pos ))
|
||||||
caller callee
|
caller callee
|
||||||
in
|
in
|
||||||
let silent = Dcalc.Ast.Var.make ("_", Pos.no_pos) in
|
body
|
||||||
Dcalc.Ast.make_abs
|
|
||||||
(Array.of_list [ silent ])
|
|
||||||
body Pos.no_pos [ (Dcalc.Ast.TUnit, Pos.no_pos) ] Pos.no_pos
|
|
||||||
|
|
||||||
let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Pos.marked Bindlib.box
|
let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Pos.marked Bindlib.box
|
||||||
=
|
=
|
||||||
@ -121,12 +118,6 @@ let rec translate_rule (ctx : ctx) (rule : Ast.rule) (rest : Ast.rule list) (pos
|
|||||||
| Definition ((ScopeVar a, var_def_pos), tau, e) ->
|
| Definition ((ScopeVar a, var_def_pos), tau, e) ->
|
||||||
let a_name = Ast.ScopeVar.get_info (Pos.unmark a) in
|
let a_name = Ast.ScopeVar.get_info (Pos.unmark a) in
|
||||||
let a_var = Dcalc.Ast.Var.make a_name in
|
let a_var = Dcalc.Ast.Var.make a_name in
|
||||||
let apply_thunked =
|
|
||||||
Bindlib.box_apply2
|
|
||||||
(fun e u -> (Dcalc.Ast.EApp (e, u), var_def_pos))
|
|
||||||
(Bindlib.box_var a_var)
|
|
||||||
(Bindlib.box_list [ Bindlib.box (Dcalc.Ast.ELit LUnit, var_def_pos) ])
|
|
||||||
in
|
|
||||||
let new_ctx =
|
let new_ctx =
|
||||||
{
|
{
|
||||||
ctx with
|
ctx with
|
||||||
@ -134,21 +125,13 @@ let rec translate_rule (ctx : ctx) (rule : Ast.rule) (rest : Ast.rule list) (pos
|
|||||||
}
|
}
|
||||||
in
|
in
|
||||||
let next_e, new_ctx = translate_rules new_ctx rest pos_sigma in
|
let next_e, new_ctx = translate_rules new_ctx rest pos_sigma in
|
||||||
let next_e =
|
|
||||||
Dcalc.Ast.make_let_in (a_var, var_def_pos) tau apply_thunked next_e (Pos.get_position a)
|
|
||||||
in
|
|
||||||
let intermediate_e =
|
|
||||||
Dcalc.Ast.make_abs
|
|
||||||
(Array.of_list [ a_var ])
|
|
||||||
next_e (Pos.get_position a)
|
|
||||||
[ (Dcalc.Ast.TArrow ((TUnit, var_def_pos), tau), var_def_pos) ]
|
|
||||||
(Pos.get_position e)
|
|
||||||
in
|
|
||||||
let new_e = translate_expr ctx e in
|
let new_e = translate_expr ctx e in
|
||||||
let a_expr = Dcalc.Ast.make_var a_var in
|
let a_expr = Dcalc.Ast.make_var a_var in
|
||||||
let merged_expr = merge_defaults a_expr new_e in
|
let merged_expr = merge_defaults a_expr new_e in
|
||||||
let out_e = Dcalc.Ast.make_app intermediate_e [ merged_expr ] (Pos.get_position e) in
|
let next_e =
|
||||||
(out_e, new_ctx)
|
Dcalc.Ast.make_let_in (a_var, var_def_pos) tau merged_expr next_e (Pos.get_position a)
|
||||||
|
in
|
||||||
|
(next_e, new_ctx)
|
||||||
| Definition ((SubScopeVar (_subs_name, subs_index, subs_var), var_def_pos), tau, e) ->
|
| Definition ((SubScopeVar (_subs_name, subs_index, subs_var), var_def_pos), tau, e) ->
|
||||||
let a_name =
|
let a_name =
|
||||||
Pos.map_under_mark
|
Pos.map_under_mark
|
||||||
|
@ -20,5 +20,5 @@ scope A:
|
|||||||
scope B:
|
scope B:
|
||||||
def a := 42
|
def a := 42
|
||||||
def b := scopeA.b
|
def b := scopeA.b
|
||||||
def scopeA.a [ a > 0 ] := scopeA.a_base
|
def scopeA.a [ a > 0 ] := scopeAbis.a_base
|
||||||
*/
|
*/
|
||||||
|
@ -1,3 +1,3 @@
|
|||||||
[RESULT] a -> -1
|
[RESULT] a -> -1
|
||||||
[RESULT] b -> false
|
|
||||||
[RESULT] a_base -> 1
|
[RESULT] a_base -> 1
|
||||||
|
[RESULT] b -> false
|
||||||
|
@ -1,8 +1,2 @@
|
|||||||
[RESULT] a -> 42
|
[RESULT] a -> 42
|
||||||
[RESULT] b -> true
|
[RESULT] b -> true
|
||||||
[RESULT] scopeA.a -> 1
|
|
||||||
[RESULT] scopeA.b -> true
|
|
||||||
[RESULT] scopeA.a_base -> 1
|
|
||||||
[RESULT] scopeAbis.a -> -1
|
|
||||||
[RESULT] scopeAbis.b -> false
|
|
||||||
[RESULT] scopeAbis.a_base -> 1
|
|
@ -1,2 +1,2 @@
|
|||||||
[RESULT] x -> 0
|
|
||||||
[RESULT] u -> true
|
[RESULT] u -> true
|
||||||
|
[RESULT] x -> 0
|
||||||
|
@ -1,19 +1,13 @@
|
|||||||
[ERROR] Default logic conflict, multiple justifications are true but are not related by a precedence
|
[ERROR] There is a conflict between multiple rules for assigning the same variable.
|
||||||
[ERROR]
|
[ERROR]
|
||||||
[ERROR] The conflict concerns this variable y
|
[ERROR] This value is available because the justification of its definition is true:
|
||||||
[ERROR] --> test_scope/sub_sub_scope.catala
|
|
||||||
[ERROR] |
|
|
||||||
[ERROR] 10 | param y type int
|
|
||||||
[ERROR] | ^
|
|
||||||
[ERROR]
|
|
||||||
[ERROR] This justification is true:
|
|
||||||
[ERROR] --> test_scope/sub_sub_scope.catala
|
[ERROR] --> test_scope/sub_sub_scope.catala
|
||||||
[ERROR] |
|
[ERROR] |
|
||||||
[ERROR] 23 | def y [ a.x = 1 ] := 1
|
[ERROR] 24 | def y [ a2.x = 1 ] := 1
|
||||||
[ERROR] | ^^^^^^^
|
[ERROR] | ^
|
||||||
[ERROR]
|
[ERROR]
|
||||||
[ERROR] This justification is true:
|
[ERROR] This value is available because the justification of its definition is true:
|
||||||
[ERROR] --> test_scope/sub_sub_scope.catala
|
[ERROR] --> test_scope/sub_sub_scope.catala
|
||||||
[ERROR] |
|
[ERROR] |
|
||||||
[ERROR] 24 | def y [ a.x + 1 = 2 ] := 1
|
[ERROR] 25 | def y [ a2.x + 1 = 2 ] := 1
|
||||||
[ERROR] | ^^^^^^^^^^^
|
[ERROR] | ^
|
||||||
|
@ -1,4 +1 @@
|
|||||||
[RESULT] z -> 2
|
[RESULT] z -> 2
|
||||||
[RESULT] a.x -> 2
|
|
||||||
[RESULT] a.u -> true
|
|
||||||
[RESULT] b.y -> 3
|
|
Loading…
Reference in New Issue
Block a user