Skip to content

Commit 422d9da

Browse files
garesgares
committed
fixup
1 parent 0ad37db commit 422d9da

File tree

8 files changed

+309
-307
lines changed

8 files changed

+309
-307
lines changed

‎src/compiler/determinacy_checker.ml‎

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -335,6 +335,13 @@ let check_clause, check_chr_guard_and_newgoal =
335335

336336
let is_cut ~types ScopedTerm.{ it } = match it with App(b,[]) -> is_global ~types b S.cut | _ -> false in
337337

338+
let rec replace_signature_tgt ~loc ~with_ d' = function
339+
| [] -> with_
340+
| _::xs -> match d' with
341+
| Arrow (_, Variadic, _, _) -> replace_signature_tgt ~loc ~with_ d' xs
342+
| Arrow (m, NotVariadic, l, r) -> Arrow (m, NotVariadic, l, replace_signature_tgt ~loc ~with_ r xs)
343+
| _ -> error ~loc @@ Format.asprintf "replace_signature_tgt: Type error: found %a " pp_dtype d' in
344+
338345
let rec infer ~type_abbrevs ~types ~ctx ~var ~exp t : dtype * Good_call.t =
339346
let rec infer_fold ~was_input ~was_data ~loc ~user_dtype ctx d hd tl =
340347
Format.eprintf "Starting infer fold at %a with dtype:@[%a@] and user_dtype:@[%a@]@." Loc.pp loc pp_dtype d (Format.pp_print_option pp_dtype) user_dtype;
@@ -505,19 +512,22 @@ let check_clause, check_chr_guard_and_newgoal =
505512
Format.eprintf "Calling assume_app on: %a with dtype %a with args [%a] and@." F.pp name pp_dtype d
506513
(pplist ~boxed:true ScopedTerm.pretty " ; ")
507514
tl;
508-
let det_head = get_const_dtype ~type_abbrevs ~ctx ~var:!var ~loc s in
509-
assume_fold ~was_input ~was_data:(is_exp d) ~loc ctx det_head tl;
510-
Format.eprintf "The map after call to assume_app is %a@." Uvar.pp !var
515+
match t with
516+
| Scope.Bound b -> assume_bound_var b ~ctx ~loc d s tl
517+
| _ ->
518+
let det_head = get_const_dtype ~type_abbrevs ~ctx ~var:!var ~loc s in
519+
assume_fold ~was_input ~was_data:(is_exp d) ~loc ctx det_head tl;
520+
Format.eprintf "The map after call to assume_app is %a@." Uvar.pp !var
521+
and assume_bound_var ~ctx ~loc b d ({ ScopedTerm.name } as s) tl =
522+
let dtype = get_uvar_dtype ~type_abbrevs ~ctx ~var:!var ~loc s in
523+
Format.eprintf "Dtype of %a is %a@." F.pp name pp_dtype dtype;
524+
let d' = replace_signature_tgt dtype tl ~loc ~with_:d in
525+
Format.eprintf "d' is %a@." pp_dtype d';
526+
BVar.add ~new_:false ctx ~v:d' ~loc (name, b) |> ignore
511527
and assume_var ~ctx ~loc d ({ ScopedTerm.name } as s) tl =
512-
let rec replace_signature_tgt ~with_ d' = function
513-
| [] -> with_
514-
| _::xs -> match d' with
515-
| Arrow (_, Variadic, _, _) -> replace_signature_tgt ~with_ d' xs
516-
| Arrow (m, NotVariadic, l, r) -> Arrow (m, NotVariadic, l, replace_signature_tgt ~with_ r xs)
517-
| _ -> error ~loc @@ Format.asprintf "replace_signature_tgt: Type error: found %a " pp_dtype d' in
518528
let dtype = get_uvar_dtype ~type_abbrevs ~ctx ~var:!var ~loc s in
519529
Format.eprintf "Dtype of %a is %a@." F.pp name pp_dtype dtype;
520-
let d' = replace_signature_tgt dtype tl ~with_:d in
530+
let d' = replace_signature_tgt dtype tl ~loc ~with_:d in
521531
Format.eprintf "d' is %a@." pp_dtype d';
522532
add ~loc ~v:d' name
523533
and assume ~was_input ctx d ScopedTerm.({ loc; it }) : unit =
@@ -738,7 +748,7 @@ let check_clause, check_chr_guard_and_newgoal =
738748
let rec aux ScopedTerm.{ it; loc } =
739749
match it with
740750
| Impl (R2L, _, ({ it = App (b, xs) } as hd), bo) -> (b, assume_hd ~type_abbrevs ~types ~loc ~ctx:!ctx ~var:var b hd xs, hd, Some bo)
741-
(* | Impl (R2L, _, ({ it = UVar(b,xs) } as hd), bo) -> (b, assume_hd ~type_abbrevs ~types ~loc ~ctx:!ctx ~var:var (`UVar b) hd xs, hd, Some bo) *)
751+
| Impl (R2L, _, ({ it = UVar _ }), _) -> raise (LoadFlexClause t)
742752
(* For clauses with quantified unification variables *)
743753
| App (n, [{ it = Lam (oname, _, body) }]) when is_quantifier ~types n ->
744754
ctx := BVar.add_oname ~new_:true ~loc oname (Compilation.type_ass_2func_mut ~loc ~type_abbrevs) !ctx;

‎tests/sources/heap_discard2.elpi‎

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎tests/sources/trace2.elab.json‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@
2121
"rule": [
2222
"UserRule",
2323
{
24-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
24+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
2525
"rule_loc": [
2626
"File",
2727
{
@@ -38,7 +38,7 @@
3838
"siblings": [
3939
{ "goal_text": "print 1", "goal_id": 5 },
4040
{
41-
"goal_text": "pi c0 \\ sigma c1 \\ fail => (true , fail)",
41+
"goal_text": "pi c0 \\ sigma c0 \\ fail => (true , fail)",
4242
"goal_id": 6
4343
}
4444
],
@@ -51,7 +51,7 @@
5151
"rule": [
5252
"UserRule",
5353
{
54-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
54+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
5555
"rule_loc": [
5656
"File",
5757
{
@@ -102,7 +102,7 @@
102102
"rule": [
103103
"UserRule",
104104
{
105-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
105+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
106106
"rule_loc": [
107107
"File",
108108
{
@@ -129,7 +129,7 @@
129129
"Inference",
130130
{
131131
"current_goal_id": 6,
132-
"current_goal_text": "pi c0 \\ sigma c1 \\ fail => (true , fail)",
132+
"current_goal_text": "pi c0 \\ sigma c0 \\ fail => (true , fail)",
133133
"current_goal_predicate": "pi",
134134
"failed_attempts": [],
135135
"successful_attempts": [
@@ -158,7 +158,7 @@
158158
"rule": [
159159
"UserRule",
160160
{
161-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
161+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
162162
"rule_loc": [
163163
"File",
164164
{
@@ -216,7 +216,7 @@
216216
"rule": [
217217
"UserRule",
218218
{
219-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
219+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
220220
"rule_loc": [
221221
"File",
222222
{
@@ -277,7 +277,7 @@
277277
"rule": [
278278
"UserRule",
279279
{
280-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
280+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
281281
"rule_loc": [
282282
"File",
283283
{
@@ -346,7 +346,7 @@
346346
"rule": [
347347
"UserRule",
348348
{
349-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
349+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
350350
"rule_loc": [
351351
"File",
352352
{
@@ -445,7 +445,7 @@
445445
"rule": [
446446
"UserRule",
447447
{
448-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
448+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
449449
"rule_loc": [
450450
"File",
451451
{
@@ -522,7 +522,7 @@
522522
"rule": [
523523
"UserRule",
524524
{
525-
"rule_text": "main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail)))))).",
525+
"rule_text": "main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail))))).",
526526
"rule_loc": [
527527
"File",
528528
{

‎tests/sources/trace2.json‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,17 +2,17 @@
22
{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["main","main"]}
33
{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
44
{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace2.elpi\", line 1, column 0, characters 0-56:"]}
5-
{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace2.elpi\", line 1, column 0, characters 0-56:","main :- (print 1), (pi (c0 \\ (sigma (c1 \\ (fail => (true , fail))))))."]}
5+
{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace2.elpi\", line 1, column 0, characters 0-56:","main :- (print 1), (pi c0 \\ (sigma (c0 \\ (fail => (true , fail)))))."]}
66
{"step" : 1,"kind" : ["Info"],"goal_id" : 4,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["5"]}
77
{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["print 1"]}
88
{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["6"]}
9-
{"step" : 1,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["pi c0 \\ sigma c1 \\ fail => (true , fail)"]}
9+
{"step" : 1,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["pi c0 \\ sigma c0 \\ fail => (true , fail)"]}
1010
{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]}
1111
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["print","print 1"]}
1212
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["builtin"]}
1313
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:builtin:name","payload" : ["print"]}
1414
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]}
15-
{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["pi","pi c0 \\ sigma c1 \\ fail => (true , fail)"]}
15+
{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["pi","pi c0 \\ sigma c0 \\ fail => (true , fail)"]}
1616
{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:rule","payload" : ["pi"]}
1717
{"step" : 3,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]}
1818
{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["sigma c1 \\ fail => (true , fail)"]}

‎tests/sources/trace_chr.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,15 +96,15 @@
9696
{"step" : 13,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X1"]}
9797
{"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]}
9898
{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 1, column 21, characters 21-66:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]}
99-
{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--371 []"]}
99+
{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--420 []"]}
100100
{"step" : 0,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]}
101101
{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]}
102102
{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
103103
{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : []}
104104
{"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["fail"]}
105105
{"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:rule-failed","payload" : []}
106106
{"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 2, column 45, characters 67-116:"," \\ (even A0) (odd A0) | (odd (s z)) <=> (fail)"]}
107-
{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--372 []"]}
107+
{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--421 []"]}
108108
{"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]}
109109
{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]}
110110
{"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}

0 commit comments

Comments
 (0)