struct: remove unrequired comments - old code

model_with_structures/synthesizer.ml

@@ -819,7 +819,6 @@ struct
           v == FunV fstmts &
           tp == FunT tps &
           st' == StEnv (mem, types', vals') &
-          (* TODO: type error, fix required *)
           list_foldl2o (stmt_addarg_foldero vals)
                        (Std.pair st' 0) tps es
                        (Std.pair state_with_args _arg_id) &
@@ -875,423 +874,10 @@ struct
       stmt_evalo init_st s st'
   }
 
-  (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
-
   (* --- tests --- *)
   (* TODO *)
 
   (* - shortcuts *)
   (* TODO *)
 
-  (* --- *)
-
-  (* let rec list_zip_witho f xs ys zs = ocanren { *)
-    (* { fresh x, xs', y, ys', z, zs' in *)
-      (* xs == x :: xs' & *)
-      (* ys == y :: ys' & *)
-      (* zs == z :: zs' & *)
-      (* f x y z & *)
-      (* list_zip_witho f xs' ys' zs' } | *)
-    (* { fresh x, xs' in *)
-      (* xs == x :: xs' & *)
-      (* ys == [] & *)
-      (* zs == [] } | *)
-    (* { fresh y, ys' in *)
-      (* xs == [] & *)
-      (* ys == y :: ys' & *)
-      (* zs == [] } | *)
-    (* { xs == [] & ys == [] & zs == [] } *)
-  (* } *)
-
-  (* --- *)
-
-  (* let value_combineo left right res = let open Value in ocanren { *)
-    (* { left == Unit & right == Unit & res == Unit } | *)
-    (* { left == Bot & right == Bot & res == Bot } | *)
-    (* { left == Unit & right == Bot & res == Undef } | *)
-    (* { left == Bot & right == Unit & res == Undef } *)
-  (* } *)
-
-  (* let memory_combineo left right res = ocanren { *)
-    (* list_zip_witho value_combineo left right res *)
-  (* } *)
-
-  (* let state_combineo left right res = let open St in ocanren { *)
-    (* fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in *)
-    (* left == St (lenv, lmem, lmem_len, lvisited) & *)
-    (* right == St (renv, rmem, rmem_len, rvisited) & *)
-    (* lenv == renv & lmem_len == rmem_len & *)
-    (* memory_combineo lmem rmem res_mem  & *)
-    (* res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited) *)
-    (* TODO: union visited lists instead ? *)
-  (* } *)
-
-  (* --- *)
-
-  (* let rec list_replaceo xs id value ys = ocanren { *)
-    (* xs == [] & ys == [] | (* NOTE: error *) *)
-    (* { fresh x, xs' in *)
-        (* xs == x :: xs' & *)
-        (* id == Nat.o & *)
-        (* ys == value :: xs' } | *)
-    (* { fresh x, xs', id', ys' in *)
-        (* xs == x :: xs' & *)
-        (* id == Nat.s id' & *)
-        (* ys == x :: ys' & *)
-        (* list_replaceo xs' id' value ys' } *)
-  (* } *)
-
-  (* let env_geto state id tag' mem_id' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh env, _mem, _mem_len, _visited, elem in *)
-      (* state == St (env, _mem, _mem_len, _visited) & *)
-      (* List.assoco id env elem & *)
-      (* Std.pair tag' mem_id' == elem *)
-  (* } *)
-
-  (* let env_addo state id tg mem_id state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh env, env', mem, mem_len, visited, elem in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* Std.pair tg mem_id == elem & *) 
-      (* (Std.pair id elem) :: env == env' & *)
-      (* state' == St (env', mem, mem_len, visited) *)
-  (* } *)
-
-  (* let inv_ido mem_len id id' = ocanren { *)
-    (* fresh inv_id_inc in *)
-      (* Nat.addo inv_id_inc id mem_len & *)
-      (* Nat.addo id' 1 inv_id_inc *)
-  (* } *)
-
-  (* --- *)
-
-  (* let rec list_ntho xs id x' = ocanren { *)
-    (* xs == [] | (* NOTE: error *) *)
-    (* { fresh y', xs' in *)
-      (* id == Nat.o & *)
-      (* y' :: xs' == xs & *)
-      (* x' == y' } | *)
-    (* { fresh id', y', xs' in *)
-      (* Nat.s id' == id & *)
-      (* y' :: xs' == xs & *)
-      (* list_ntho xs' id' x' } *)
-  (* } *)
-
-  (* let mem_geto state id value' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh mem, mem_len, mem_id, mem_id_inv, _env, _visited, _tag in *)
-    (* state == St (_env, mem, mem_len, _visited) & *)
-    (* env_geto state id _tag mem_id & *)
-    (* inv_ido mem_len mem_id mem_id_inv & *)
-    (* list_ntho mem mem_id_inv value' *)
-  (* } *)
-
-  (* let mem_seto state id value state'= *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh env, mem, mem_len, visited, mem_id, inv_mem_id, mem', _tag in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* env_geto state id _tag mem_id & *)
-      (* inv_ido mem_len mem_id inv_mem_id & *)
-      (* list_replaceo mem inv_mem_id value mem' & *)
-      (* state' == St (env, mem', mem_len, visited) *)
-  (* } *)
-
-  (* let mem_addo state value state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh env, mem, mem_len, mem_len', visited, mem' in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* mem' == value :: mem & *)
-      (* mem_len' == Nat.s mem_len & *)
-      (* state' == St (env, mem', mem_len', visited) *)
-  (* } *)
-
-  (* let mem_checko state id = *)
-    (* let open Value in *)
-    (* ocanren { *)
-      (* mem_geto state id Unit *)
-    (* } *)
-
-  (* --- *)
-
-  (* let rec list_foldlo f acc xs acc' = ocanren { *)
-    (* xs == [] & acc' == acc | *)
-    (* { fresh x', xs', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* list_foldlo f acc xs' acc_upd & *)
-      (* f acc_upd x' acc' } *)
-  (* } *)
-
-  (* let rec list_foldro f acc xs acc' = ocanren { *)
-    (* xs == [] & acc' == acc | *)
-    (* { fresh x', xs', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* f acc x' acc_upd & *)
-      (* list_foldro f acc_upd xs' acc' } *)
-    (* TODO: inf search on swap, investigate *)
-  (* } *)
-
-
-  (* let rec list_foldr2o f acc xs ys acc' = ocanren { *)
-    (* xs == [] & ys == [] & acc' == acc | *)
-    (* { fresh x', xs', y', ys', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* ys == y' :: ys' & *)
-      (* f acc x' y' acc_upd & *)
-      (* list_foldr2o f acc_upd xs' ys' acc' } *)
-  (* } *)
-
-  (* let rec list_foldl2o f acc xs ys acc' = ocanren { *)
-    (* xs == [] & ys == [] & acc' == acc | *)
-    (* { fresh x', xs', y', ys', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* ys == y' :: ys' & *)
-      (* list_foldl2o f acc xs' ys' acc_upd & *)
-      (* f acc_upd x' y' acc' } *)
-  (* } *)
-
-  (* let arg_to_valueo state arg value' = *)
-    (* let open Arg in *)
-    (* let open Value in *)
-    (* ocanren { *)
-    (* arg == RValue & value' == Unit | *)
-    (* { fresh id in *)
-      (* arg == LValue id & *)
-      (* mem_geto state id value' } *)
-  (* } *)
-
-  (* let arg_to_rvalueo arg value' = *)
-    (* let open Arg in *)
-    (* let open Tag in *)
-    (* ocanren { is_valueo arg & value' == RValue } *)
-
-  (* let st_mem_leno state mem_len' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh _env, _mem, _visited in *)
-      (* state == St (_env, _mem, mem_len', _visited) *)
-  (* } *)
-
-  (* let tag_correcto tg = *)
-    (* let open Tag in *)
-    (* ocanren { *)
-      (* {is_not_outo tg | { is_outo tg & is_always_writeo tg } } & *)
-      (* {is_not_reado tg | { is_reado tg & is_ino tg } } *)
-    (* } *)
-
-  (* let st_add_argo state state_before id arg_tag arg state'' = *)
-    (* let open Nat in *)
-    (* let open Value in *)
-    (* let open Arg in *)
-    (* let open Tag in *)
-    (* ocanren { *)
-        (* tag_correcto arg_tag & { *)
-        (* { fresh value', state', mem_len_prev' in *)
-          (* is_valueo arg_tag & *)
-          (* arg_to_valueo state_before arg value' & *)
-          (* mem_addo state value' state' & *)
-          (* st_mem_leno state mem_len_prev' & *)
-          (* env_addo state' id arg_tag mem_len_prev' state'' } | *)
-        (* { fresh arg', parent_tag, mem_id, state' in *)
-          (* is_refo arg_tag & *)
-            (* { arg == RValue } *) (* NOTE: not allowed for now *)
-          (* arg == LValue arg' & *)
-          (* env_geto state_before id parent_tag mem_id & *)
-          (* env_addo state id arg_tag mem_id state' & *)
-          (* { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } & *)
-          (* { *)
-            (* { is_reado arg_tag & state' == state'' } | *)
-            (* { is_not_reado arg_tag & mem_seto state' id Bot state'' } *)
-          (* } *)
-        (* } *)
-      (* } *)
-    (* } *)
-
-  (* let st_spoil_foldero state_before state tg id state' = *)
-    (* let open Value in *)
-    (* let open Tag in *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh env, mem, mem_len, _visited, parent_tg, _mem_id in *)
-      (* state == St (env, mem, mem_len, _visited) & *)
-      (* env_geto state id parent_tg _mem_id & *)
-      (* { is_not_reado tg | { is_reado tg & mem_checko state_before id } } & *)
-      (* { { is_never_writeo tg & state == state'} | *)
-        (* { is_always_writeo tg & *) 
-          (* is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } | *)
-        (* { is_may_writeo tg & { *)
-          (* { is_not_outo tg & is_valueo tg & state == state' } | *)
-          (* { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' } *)
-        (* } } *)
-      (* } *)
-    (* } *)
-
-  (* let st_spoil_by_argso state arg_tags args state' = *)
-    (* ocanren { *)
-      (* fresh state_before in *)
-      (* state == state_before & (* TODO: required ? *) *)
-      (* list_foldl2o (st_spoil_foldero state_before) state arg_tags args state' *)
-    (* } *)
-
-  (* let st_spoil_assignmentso state state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh _env, _mem, _mem_len, visited in *)
-      (* state == St (_env, _mem, _mem_len, visited) & *)
-      (* list_foldlo st_spoil_foldero state visited state' *)
-  (* } *)
-
-  (* --- *)
-
-  (* let arg_to_lvalueo arg arg' = *)
-    (* let open Arg in *)
-    (* ocanren { arg' == LValue arg } *)
-
-  (* let rec list_dropo n xs xs' = ocanren { *)
-    (* xs == [] & xs' == [] | *)
-    (* n == Nat.o & xs == xs' & xs =/= [] | *)
-    (* { fresh n', _y, ys in *)
-        (* Nat.s n' == n & *)
-        (* xs == _y :: ys & *)
-        (* list_dropo n' ys xs' } *)
-  (* } *)
-
-  (* let rec list_not_membero xs x = ocanren { *)
-    (* xs == [] | *)
-    (* { fresh x', xs' in *)
-        (* xs == x' :: xs' & *)
-        (* x' =/= x & *)
-        (* list_not_membero xs' x } *)
-  (* } *)
-
-  (* let visited_checko state f_id = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh _env, _mem, _mem_len, visited in *)
-      (* state == St (_env, _mem, _mem_len, visited) & *)
-      (* List.membero visited f_id *)
-    (* } *)
-
-  (* let not_visited_checko state f_id = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh _env, _mem, _mem_len, visited in *)
-      (* state == St (_env, _mem, _mem_len, visited) & *)
-      (* list_not_membero visited f_id *)
-    (* } *)
-
-  (* let visited_addo state f_id state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh env, mem, mem_len, visited, visited' in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* visited' == f_id :: visited & *)
-      (* state' == St (env,mem, mem_len, visited') *)
-    (* } *)
-
-  (* let rec eval_stmto state prog stmt state' = *)
-    (* let open Stmt in *)
-    (* let open Value in *)
-    (* let open FunDecl in *)
-    (* let open Tag in *)
-    (* ocanren { *)
-    (* { fresh f_id, args, f, args', state_after_call, arg_tags, _body in *)
-      (* stmt == Call (f_id, args) & *)
-      (* list_ntho prog f_id f & *)
-      (* FunDecl (arg_tags, _body) == f & *)
-      (* List.mapo arg_to_lvalueo args args' & *)
-      (* TODO: FIXME: memoisation, do not do calls on check successfull *)
-      
-      (* NOTE: tmp simplification for less branching (TODO?) *)
-      (* { { fresh state_with_visited in *)
-          (* not_visited_checko state f_id & *)
-          (* visited_addo state f_id state_with_visited & *)
-          (* eval_funo state_with_visited prog f args' state_after_call } | *)
-        (* { visited_checko state f_id & *)
-          (* state_after_call == state } } & *)
-      (* st_spoil_by_argso state_after_call arg_tags args state' } | *)
-    (* { fresh id in stmt == Read id & mem_checko state id & state == state' } | *)
-    (* { fresh id, tag, _mem_id in *)
-      (* stmt == Write id & *)
-      (* env_geto state id tag _mem_id & *)
-      (* is_may_writeo tag & *)
-      (* mem_seto state id Unit state' } | *)
-    (* { fresh xs, ys in *)
-      (* stmt == Choice (xs, ys) } *)
-    (* TODO: FIXME: choice actions *)
-  (* } *)
-
-  (* and eval_body_foldero prog state stmt state' = *)
-    (* eval_stmto state prog stmt state' *)
-
-  (* and eval_bodyo state prog body state' = *)
-    (* list_foldro (eval_body_foldero prog) state body state' *) 
-
-  (* and add_arg_foldero state_before state_c arg_tag arg state_c' = *)
-    (* ocanren { *)
-    (* fresh state, id, state', id' in *)
-      (* state_c == Std.pair state id & *)
-      (* st_add_argo state state_before id arg_tag arg state' & *)
-      (* id' == Nat.s id & *)
-      (* state_c' == Std.pair state' id' *)
-  (* } *)
-
-  (* and eval_funo state prog decl args state' = *)
-    (* let open FunDecl in *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh arg_tags, body, *)
-          (* env_before, mem_before, len_before, visited_before, *)
-          (* state_clean, *)
-          (* state_with_vars, _counter, *)
-          (* state_evaled, *)
-          (* _env, _mem, _len, visited, *)
-          (* nil_env, nil_visited in *)
-      (* nil_env == [] & *)
-      (* nil_visited == [] & *)
-      (* decl == FunDecl (arg_tags, body) & *)
-      (* state == St (env_before, mem_before, len_before, visited_before) & *)
-      (* state_clean == St (nil_env, mem_before, len_before, nil_visited) & *)
-      (* list_foldr2o (add_arg_foldero state) *)
-                   (* (Std.pair state Nat.o) arg_tags args *)
-                   (* (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *) *)
-      (* eval_bodyo state_with_vars prog body state_evaled & *)
-      (* state_evaled == St (_env,_mem, _len, visited) & *)
-      (* state' == St (env_before, mem_before, len_before, visited) *)
-  (* } *)
-
-  (* and eval_fun_empty_argso state prog decl state' = *)
-    (* let open FunDecl in *)
-    (* ocanren { *)
-    (* fresh arg_tags, args, _body in *)
-      (* decl == FunDecl (arg_tags, _body) & *)
-      (* List.mapo arg_to_rvalueo arg_tags args & *)
-      (* eval_funo state prog decl args state' *)
-  (* } *)
-
-  (* --- *)
-
-  (* let empty_stateo state = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh nil_env, nil_mem, nil_visited in *)
-      (* nil_env == [] & *)
-      (* nil_visited == [] & *)
-      (* nil_mem == [] & *)
-      (* state == St (nil_env, nil_mem, Nat.o, nil_visited) *)
-  (* } *)
-
-  (* let eval_progo all_prog state' = *)
-    (* let open Prog in *)
-    (* ocanren { *)
-    (* fresh prog, main_decl, state in *)
-      (* all_prog == Prog (prog, main_decl) & *)
-      (* empty_stateo state & *)
-      (* eval_fun_empty_argso state prog main_decl state' *)
-  (* } *)
 end