st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2025-12-24 09:48:42 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

draft rules in prolog-like syntax

Browse source
This commit is contained in:
ProgramSnail 2025-12-09 16:39:47 +03:00
parent f770620742
commit 658415536b
1 changed files with 46 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

46
description.typ Normal file
View file

@ -0,0 +1,46 @@
```prolog
/* TODO: arg_tags_eq: check by ndex in array */
/* TODO: arg_tags_neq: check by index in array */
not_in_list(I, []).
not_in_list(I, [X | XT]) : X != I, not_in_list(I, XT).
correct_body_on_arg_borrow(ARGT, B, [], I).
correct_body_on_arg_borrow(ARGT, B, [Write(I)|XT], I). /* overwrite */
correct_body_on_arg_borrow(ARGT, B, [Write(J)|XT], I) :-
I != J, correct_body_on_arg_borrow(ARGT, B, XT, I).
correct_body_on_arg_borrow(ARGT, B, [Read(J)|XT], I) :-
I != J, correct_body_on_arg_borrow(ARGT, B, XT, I).
/* read of I is incorrect */
correct_body_on_arg_borrow(ARGT, B, [Call(F, FARGT, ARGS)|XT], I) :-
not_in_list(I, ARGS), correct_body_on_arg_borrow(ARGT, B, XT, I).
/* func call only correct in all args are not I */
/* TODO: correct_args_map(ARGT, B, FARGT, ARGS) */
correct_args_map(ARGT, B, [], []).
correct_args_map(ARGT, B, BT, [Ref|TS], [I|IS]) :-
arg_tags_neq(ARGT, I, ConstRef),
correct_body_on_arg_borrow(ARGT, B, BT, I),
correct_args_map(ARGT, B, BT, TS, IS).
correct_args_map(ARGT, B, BT, [ConstRef|TS], [I|IS]) :-
correct_args_map(ARGT, B, BT, TS, IS).
correct_args_map(ARGT, B, BT, [Copy|TS], [I|IS]) :-
correct_args_map(ARGT, B, BT, TS, IS).
correct_body(ARGT, B, [Write(I)|XT]) :- arg_tags_neq(ARGT, I, ConstRef),
correct_body(ARGT, B, XT).
correct_body(ARGT, B, [Read(I)|XT]) :- correct_body(ARGT, B, XT).
correct_body(ARGT, B, [Call(F, FARGT, ARGS)|XT]) :- correct_args_map(ARGT, B, BT, FARGT, ARGS),
correct_body(ARGT, B, XT).
/* FARGT - deduced in the program beforehand */
correct_func(P, func(ARGT, B)) :- correct_body(ARGT, B, B).
correct_all(P, []).
correct_all(P, [X | XT]) :- correct_func(P, X), correct_all(P, XT).
correct(prog(X)) :- correct_all(X, X).
```