diff options
author | Son Ho | 2021-11-22 10:25:09 +0100 |
---|---|---|
committer | Son Ho | 2021-11-22 10:25:09 +0100 |
commit | 61e54d5c7fa5e8662d8cc438f4f2bd4856bf3ca6 (patch) | |
tree | e279ea490bd1522822bdd7b4d65a4d08b86c50f8 /src | |
parent | c1f628b7fde13df56bc7e71f1619f4427ed157dc (diff) |
Implement typed_avalue_to_string_
Diffstat (limited to 'src')
-rw-r--r-- | src/Print.ml | 113 | ||||
-rw-r--r-- | src/Values.ml | 8 |
2 files changed, 110 insertions, 11 deletions
diff --git a/src/Print.ml b/src/Print.ml index 47350324..1555afc4 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -262,22 +262,121 @@ module Values = struct match lc with | SharedLoan (loans, v) -> let loans = BorrowId.set_to_string loans in - "@shared_loan({" ^ loans ^ "}, " ^ typed_value_to_string fmt v ^ ")" + "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")" | MutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋" + let symbolic_value_proj_to_string (fmt : value_formatter) + (sv : symbolic_value) (rty : rty) : string = + symbolic_value_id_to_string sv.sv_id + ^ " : " + ^ ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty + ^ " <: " + ^ ty_to_string (value_to_rtype_formatter fmt) rty + let rec abstract_shared_borrows_to_string (fmt : value_formatter) (abs : abstract_shared_borrows) : string = match abs with | AsbSet bs -> BorrowId.set_to_string bs | AsbProjReborrows (sv, rty) -> - "{" - ^ symbolic_value_id_to_string sv.sv_id - ^ " : " - ^ ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty - ^ " <: " - ^ ty_to_string (value_to_rtype_formatter fmt) rty + "{" ^ symbolic_value_proj_to_string fmt sv rty ^ "}" | AsbUnion (asb1, asb2) -> abstract_shared_borrows_to_string fmt asb1 ^ " U " ^ abstract_shared_borrows_to_string fmt asb2 + + let rec typed_avalue_to_string (fmt : value_formatter) (v : typed_avalue) : + string = + match v.avalue with + | AConcrete cv -> constant_value_to_string cv + | AAdt av -> + let adt_ident = + match av.avariant_id with + | Some vid -> fmt.type_def_id_variant_id_to_string av.adef_id vid + | None -> fmt.type_def_id_to_string av.adef_id + in + let field_values = FieldId.vector_to_list av.afield_values in + if List.length field_values > 0 then + let field_values = + String.concat " " + (List.map (typed_avalue_to_string fmt) field_values) + in + adt_ident ^ " " ^ field_values + else adt_ident + | ATuple values -> + let values = FieldId.vector_to_list values in + let values = + String.concat ", " (List.map (typed_avalue_to_string fmt) values) + in + "(" ^ values ^ ")" + | ABottom -> "⊥" + | ALoan lc -> aloan_content_to_string fmt lc + | ABorrow bc -> aborrow_content_to_string fmt bc + | AAssumed av -> ( + match av with ABox bv -> "@Box(" ^ typed_avalue_to_string fmt bv ^ ")") + | AProj pv -> aproj_to_string fmt pv + + and aloan_content_to_string (fmt : value_formatter) (lc : aloan_content) : + string = + match lc with + | AMutLoan (bid, av) -> + "⌊mut@" ^ BorrowId.to_string bid ^ ", " + ^ typed_avalue_to_string fmt av + ^ "⌋" + | ASharedLoan (loans, v, av) -> + let loans = BorrowId.set_to_string loans in + "@shared_loan(" ^ loans ^ ", " + ^ typed_value_to_string fmt v + ^ ", " + ^ typed_avalue_to_string fmt av + ^ ")" + | AEndedMutLoan ml -> + "@ended_mut_loan{ given_back=" + ^ typed_value_to_string fmt ml.given_back + ^ "; child=" + ^ typed_avalue_to_string fmt ml.child + ^ " }" + | AEndedSharedLoan (v, av) -> + "@ended_shared_loan(" + ^ typed_value_to_string fmt v + ^ ", " + ^ typed_avalue_to_string fmt av + ^ ")" + | AIgnoredMutLoan (bid, av) -> + "@ignored_mut_loan(" ^ BorrowId.to_string bid ^ ", " + ^ typed_avalue_to_string fmt av + ^ ")" + | AIgnoredSharedLoan asb -> + "@ignored_shared_loan(" + ^ abstract_shared_borrows_to_string fmt asb + ^ ")" + + and aborrow_content_to_string (fmt : value_formatter) (bc : aborrow_content) : + string = + match bc with + | AMutBorrow (bid, av) -> + "&mut@" ^ BorrowId.to_string bid ^ " (" + ^ typed_avalue_to_string fmt av + ^ ")" + | ASharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋" + | AIgnoredMutBorrow av -> + "@ignored_mut_borrow(" ^ typed_avalue_to_string fmt av ^ ")" + | AEndedIgnoredMutLoan ml -> + "@ended_ignored_mut_borrow{ given_back=" + ^ typed_avalue_to_string fmt ml.given_back + ^ "; child: " + ^ typed_avalue_to_string fmt ml.child + ^ "}" + | AIgnoredSharedBorrow sb -> + "@ignored_shared_borrow(" + ^ abstract_shared_borrows_to_string fmt sb + ^ ")" + + and aproj_to_string (fmt : value_formatter) (pv : aproj) : string = + match pv with + | AProjLoans sv -> + "proj_loans (" + ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv + ^ ")" + | AProjBorrows (sv, rty) -> + "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" end diff --git a/src/Values.ml b/src/Values.ml index 5ebc97b0..d63ace85 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -146,9 +146,9 @@ and aadt_value = { and aloan_content = | AMutLoan of BorrowId.id * typed_avalue - | ASharedLoan of BorrowId.Set.t * value * typed_avalue - | AEndedMutLoan of value * typed_avalue (* TODO: given_back, child *) - | AEndedSharedLoan of value * typed_avalue + | ASharedLoan of BorrowId.Set.t * typed_value * typed_avalue + | AEndedMutLoan of { given_back : typed_value; child : typed_avalue } + | AEndedSharedLoan of typed_value * typed_avalue | AIgnoredMutLoan of BorrowId.id * typed_avalue | AIgnoredSharedLoan of abstract_shared_borrows @@ -159,7 +159,7 @@ and aborrow_content = | AMutBorrow of BorrowId.id * typed_avalue | ASharedBorrow of BorrowId.id | AIgnoredMutBorrow of typed_avalue - | AEndedIgnoredMutLoan of typed_avalue * typed_avalue (* TODO: given back, child *) + | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue } | AIgnoredSharedBorrow of abstract_shared_borrows and aassumed_value = ABox of typed_avalue |