Skip to content

Commit

Permalink
finished the reasoning of toss deep and right
Browse files Browse the repository at this point in the history
  • Loading branch information
@songyahui
songyahui committed Feb 26, 2024
1 parent 0db687c commit a2b5dd1
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 34 deletions.
84 changes: 53 additions & 31 deletions parsing/forward_rules.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,10 +168,16 @@ let renamingexistientalVar (specs:disj_spec): disj_spec =
r
) specs

let renameSpecAndInstantiate specList bindings =
let renameSpecListAndInstantiate specList bindings =
let specList' = renamingexistientalVar specList in
instantiateSpecList bindings specList'

let renameSpecAndInstantiate spec bindings =
let specList' = renamingexistientalVar [spec] in
match specList' with
| hd::_ -> instantiateSpec bindings hd
| _ -> failwith ("error renameSpecAndInstantiate")

(** substitutes existentials with fresh variables, and the resulting formula has no quantifiers *)
let freshen (specs:disj_spec): disj_spec =
renamingexistientalVar specs
Expand Down Expand Up @@ -355,24 +361,26 @@ let cartesian_product li1 li2 =


let instantiateSpecListUponResume (handlingSpec: spec list) (contiInput:string) (continuation: spec list) : spec list =
print_endline ("contiInput = " ^ contiInput );
(*print_endline ("contiInput = " ^ contiInput ); *)
let rec helper (handlingSpecIn:spec) (continuationIn:spec list) : spec list =
match handlingSpecIn with
| [] -> [[]]
| HigherOrder ((p', h', (f', hd'::actual::rest), r')) :: xs ->
let x = (p', h', (f', hd'::actual::rest), r') in (* hd' is k, and we assume there is only one argument for effects *)
if String.compare f' "continue" == 0
then
let instantiations = (normalise_spec_list (instantiateSpecList [(contiInput, actual)] continuationIn)) in
print_endline ("instantiation_continuationIn: " ^ string_of_spec_list instantiations);
let instantiations = normalise_spec_list ( (renameSpecListAndInstantiate continuationIn [(contiInput, actual)])) in
(*(normalise_spec_list (instantiateSpecList [(contiInput, actual)] )) in *)
(*print_endline ("instantiation_continuationIn: " ^ string_of_spec_list instantiations);
*)

List.map (fun instantiation ->
let contiRet = retrieve_return_value instantiation in

let instantiation = instantiateSpec ["res", contiRet] instantiation in

let newPi= And (p', Atomic(EQ, contiRet, r' ) ) in
print_endline (string_of_pi newPi);
(*print_endline (string_of_pi newPi); *)

let (prefix:spec) = NormalReturn (newPi, h') :: instantiation in

Expand All @@ -391,7 +399,15 @@ let instantiateSpecListUponResume (handlingSpec: spec list) (contiInput:string)

in

List.flatten (List.map (fun (h_spec) -> helper h_spec continuation) handlingSpec)
List.flatten (List.map (fun (h_spec) ->
let temp =
helper h_spec continuation in
(*print_endline ("!!!!!!!!" ^ string_of_spec h_spec ^ " \nand conti = " ^ string_of_spec_list continuation);
print_endline ("= " ^ string_of_spec_list temp);
*)
temp

) handlingSpec)


let findTheActualArg4AccTerm arg (term:term): term option =
Expand Down Expand Up @@ -487,14 +503,15 @@ let rec handling_spec env (match_summary:tryCatchLemma option) (scr_spec:normali

if startingFromALowerCase label then
(
print_endline ("lower case " ^ label) ;
(*print_endline ("lower case " ^ label) ; *)


match match_summary with
| Some (tcl_head, Some tcl_handledCont, tcl_summary) ->
print_endline (string_of_try_catch_lemma (tcl_head, Some tcl_handledCont, tcl_summary) ^ "\n");
| Some (tcl_head, Some _, tcl_summary) ->
(*print_endline (string_of_try_catch_lemma (tcl_head, Some tcl_handledCont, tcl_summary) ^ "\n");
print_endline (string_of_effHOTryCatchStages (EffHOStage x) ^ " # " ^ string_of_spec_list handledContinuation);
print_endline ("");
*)
let effFormalArg =
match normalize_spec tcl_head with
| ([(EffHOStage y) ], _) ->
Expand All @@ -506,27 +523,28 @@ let rec handling_spec env (match_summary:tryCatchLemma option) (scr_spec:normali

in

Format.printf "effActualArg: %s@." (string_of_list string_of_term (effActualArg@[x.e_ret]));
(*Format.printf "effActualArg: %s@." (string_of_list string_of_term (effActualArg@[x.e_ret]));
Format.printf "effFormalArg: %s@." (string_of_list Fun.id effFormalArg);

*)
let bindings = bindFormalNActual (effFormalArg) (effActualArg@[x.e_ret]) in

let instantiate_tcl_handledCont = instantiateSpecList bindings tcl_handledCont in
print_endline ("instantiate_tcl_handledCont: " ^ string_of_spec_list instantiate_tcl_handledCont);


let contiRet = findTheActualArg4Acc_x_e_ret x.e_ret handledContinuation in

(*
print_endline ("continuation_spec: " ^ string_of_spec_list handledContinuation);

let newPi = Atomic(EQ, contiRet, Var "acc") in
*)
(*let newPi = Atomic(EQ, contiRet, Var "acc") in
print_endline (string_of_pi newPi);
*)

let instantiate_tcl_summary = renameSpecAndInstantiate tcl_summary bindings in
let instantiate_tcl_summary = List.map (fun s -> NormalReturn (newPi, EmptyHeap) :: s) instantiate_tcl_summary in
let instantiate_tcl_summary = renameSpecListAndInstantiate tcl_summary (("acc", contiRet)::bindings) in
let instantiate_tcl_summary = normalise_spec_list instantiate_tcl_summary in


(*
print_endline ("instantiate_instantiate_tcl_summary: " ^ string_of_spec_list instantiate_tcl_summary ^"\n");

*)

instantiate_tcl_summary, env

Expand All @@ -546,9 +564,9 @@ let rec handling_spec env (match_summary:tryCatchLemma option) (scr_spec:normali
| None -> concatenateEventWithSpecs (effectStage2Spec [EffHOStage x]) handledContinuation, env
| Some (effFormalArg, handler_body_spec) ->
let effFormalArg = match effFormalArg with | None -> [] | Some v -> [v] in
Format.printf "effActualArg: %s@." (string_of_list string_of_term effActualArg);
(*Format.printf "effActualArg: %s@." (string_of_list string_of_term effActualArg);
Format.printf "effFormalArg: %s@." (string_of_list Fun.id effFormalArg);

*)
let bindings = bindFormalNActual (effFormalArg) (effActualArg) in
(*print_endline ("binding length " ^ string_of_int (List.length bindings));*)
(* effect x is handled by a branch of the form (| (Eff effFormalArg) k -> spec) *)
Expand All @@ -558,13 +576,15 @@ let rec handling_spec env (match_summary:tryCatchLemma option) (scr_spec:normali
let handler_body_spec = renamingexistientalVar handler_body_spec in
let handler_body_spec = instantiateSpecList bindings handler_body_spec in
(* debug ~at:5 ~title:(Format.asprintf "handler_body_spec for effect stage %s" (fst x.e_constr)) "%s" (string_of_disj_spec handler_body_spec); *)
print_endline ("Effect: " ^label ^ " and handler_body_spec: " ^ string_of_disj_spec handler_body_spec);
(*print_endline ("Effect: " ^label ^ " and handler_body_spec: " ^ string_of_disj_spec handler_body_spec);
(* the rest of the trace is now the spec of the continuation *)
print_endline ("continuation_spec: " ^ string_of_spec_list handledContinuation);

*)

let handler_body_specAfterSubstituteK = instantiateSpecListUponResume handler_body_spec perform_ret handledContinuation in
(*
print_endline ("handler_body_specAfterSubstituteK: " ^ string_of_spec_list handler_body_specAfterSubstituteK);
*)
let res = concatenateEventWithSpecs (normalStage2Spec norm) handler_body_specAfterSubstituteK in
res, env
)
Expand Down Expand Up @@ -804,9 +824,10 @@ let rec infer_of_expression (env:fvenv) (history:disj_spec) (expr:core_lang): di
(*let sp = normalize_spec sp in *)
let sp = (normalise_spec_list sp) in

print_endline ("Inferred_effect_cases_specs: --------- \n" ^ effname ^ (match param with | None -> " " | Some p -> "("^ p ^ ") ")^ ": " ^
(*print_endline ("Inferred_effect_cases_specs: --------- \n" ^ effname ^ (match param with | None -> " " | Some p -> "("^ p ^ ") ")^ ": " ^
string_of_disj_spec sp
);
);
*)


(effname, param, sp) :: t, env
Expand All @@ -817,8 +838,9 @@ let rec infer_of_expression (env:fvenv) (history:disj_spec) (expr:core_lang): di
let (param, body) = val_case in
let inf_val_spec, env = infer_of_expression env [[]] body in

print_endline ("Inferred_nromal_clause_spec: --------- \n" ^ (match param with | p -> p ^ "")^ ": " ^
(*print_endline ("Inferred_nromal_clause_spec: --------- \n" ^ (match param with | p -> p ^ "")^ ": " ^
string_of_disj_spec (normalise_spec_list inf_val_spec));
*)

(param, inf_val_spec), env
in
Expand All @@ -830,21 +852,21 @@ let rec infer_of_expression (env:fvenv) (history:disj_spec) (expr:core_lang): di
in
*)

print_endline ("\nSpec of the try block: " ^ string_of_disj_spec phi1 ^ "\n\n");

(*print_endline ("\nSpec of the try block: " ^ string_of_disj_spec phi1 ^ "\n\n");
*)

let afterHandling, env =
concat_map_state env (fun spec env ->
let spec_n = (normalize_spec spec) in
let temp = handling_spec env match_summary spec_n inferred_val_case inferred_branch_specs in
print_endline ("-------------------");
(*print_endline ("-------------------"); *)
temp
) phi1
in


print_endline ("\nAfter afterHandling at handler: \n" ^ string_of_disj_spec afterHandling ^ "\n\n");

(*print_endline ("\nAfter afterHandling at handler: \n" ^ string_of_disj_spec afterHandling ^ "\n\n");
*)

let res, env = concatenateSpecsWithSpec history afterHandling, env in

Expand Down
6 changes: 3 additions & 3 deletions src/demo/3_Deep_Right_Toss.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ let rec tossNtimeTail n
in r1 && r2

(* try ex r; req n>=0; tossNtimeTail(n,r) # Norm((acc&&r)=false,0) \/ Norm((acc&&r)=true,1) catch
= ex w final; req i->w; Norm (i->w+(2^(n+1) -2) /\ (final=1/\acc=true \/ final=0/\acc=false), final) *)
= ex w final; req counter->w; Norm (counter->w+(2^(n+1) -2) /\ (final=1/\acc=true \/ final=0/\acc=false), final) *)

let tossHandlerTail counter n
(*@ ex w; req counter->w /\ n>=1; Norm (counter->w+((2^(n+1)) -2) ,1) @*)
Expand All @@ -20,8 +20,8 @@ let tossHandlerTail counter n
(* try-catch lemma defined here *)
(*@ try ex r; req n>=0; tossNtimeTail(n,r)
# Norm((acc&&r)=false,0) \/ Norm((acc&&r)=true,1) catch
= ex w1 r1; req i->w1; Norm (i->w1+((2^(n+1)) -2) /\ res=r1/\r1=1/\acc=true , res)
\/ ex w2 r2; req i->w2; Norm (i->w2+((2^(n+1)) -2) /\ res=r2/\r2=0/\acc=false, res) @*)
= ex w1 r1; req counter->w1; Norm (counter->w1+((2^(n+1)) -2) /\ res=r1/\r1=1/\acc=true , res)
\/ ex w2 r2; req counter->w2; Norm (counter->w2+((2^(n+1)) -2) /\ res=r2/\r2=0/\acc=false, res) @*)

| x -> if x
then 1
Expand Down

0 comments on commit a2b5dd1

Please sign in to comment.