search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Tweaks to default pretty instances. #3471

Closed gebner closed 2 months ago

gebner commented 2 months ago

Before:

  (ELet
    { 
      name = "s";
      typ = (TQualified (["DPE"], "session_state"));
      mut = false;
      meta = []
      }
    (EApp (EQualified (["DPE"],"replace_session"))
      [(EBound 4);EUnit;(ECons (TQualified (["DPE"], "session_state")) "InUse"
        []);EUnit])
    (EMatch (EBound 0) [iou:branch;iou:branch;iou:branch;iou:branch;iou:branch])))
  (DFunction None [Private] 0 (TQualified (["DPETypes"], "profile_descriptor_t"))
  (["DPE"],"get_profile")
  [{ name = "uu___"; typ = TUnit; mut = false; meta = [] }]
  (EApp (EQualified (["DPETypes"],"mk_profile_descriptor"))
    [(EString "");(EConstant (UInt32,"1"));(EConstant (UInt32,"0"));(EBool false);(EBool
      false);(EBool false);(EBool false);(EConstant (SizeT,"0"));(EString "");(EBool
      false);(EString "");(EString "");(EBool false);(EBool true);(EConstant
      (SizeT,"1"));(EConstant (SizeT,"16"));(EBool false);(EBool false);(EBool
      false);(EBool false);(EBool true);(EBool false);(EBool false);(EBool false);(EBool
      false);(EBool false);(EBool true);(EBool false);(EBool false);(EBool false);(EBool
      false);(EBool false);(EBool true);(EString "");(EString "");(EString "");(EBool
      false);(EString "");(EString "");(EString "");(EBool false);(EBool false);(EBool
      false);(EString "");(EString "");(EString "");(EBool false);(EConstant
      (SizeT,"0"));(EConstant (SizeT,"0"));(EBool false);(EBool false);(EBool
      false);(EBool false);(EBool false);(EBool false);(EBool false);(EBool
      false);(EString "");(EBool false);(EString "");(EString "");(EString "");(EBool
      false);(EString "");(EString "");(EBool false);(EBool false);(EBool false);(EString
      "")]))

After:

  (ELet
    {
      name = "s";
      typ = (TQualified (["DPE"], "session_state"));
      mut = false;
      meta = []
      }
    (EApp (EQualified (["DPE"], "replace_session"))
      [(EBound 4); EUnit;
        (ECons (TQualified (["DPE"], "session_state")) "InUse" []); EUnit])
    (EMatch (EBound 0)
      [iou:branch; iou:branch; iou:branch; iou:branch; iou:branch])))
  (DFunction None [Private] 0 (TQualified (["DPETypes"], "profile_descriptor_t"))
  (["DPE"], "get_profile")
  [{ name = "uu___"; typ = TUnit; mut = false; meta = [] }]
  (EApp (EQualified (["DPETypes"], "mk_profile_descriptor"))
    [(EString ""); (EConstant (UInt32, "1")); (EConstant (UInt32, "0"));
      (EBool false); (EBool false); (EBool false); (EBool false);
      (EConstant (SizeT, "0")); (EString ""); (EBool false); (EString "");
      (EString ""); (EBool false); (EBool true); (EConstant (SizeT, "1"));
      (EConstant (SizeT, "16")); (EBool false); (EBool false); (EBool false);
      (EBool false); (EBool true); (EBool false); (EBool false); (EBool false);
      (EBool false); (EBool false); (EBool true); (EBool false); (EBool false);
      (EBool false); (EBool false); (EBool false); (EBool true); (EString "");
      (EString ""); (EString ""); (EBool false); (EString ""); (EString "");
      (EString ""); (EBool false); (EBool false); (EBool false); (EString "");
      (EString ""); (EString ""); (EBool false); (EConstant (SizeT, "0"));
      (EConstant (SizeT, "0")); (EBool false); (EBool false); (EBool false);
      (EBool false); (EBool false); (EBool false); (EBool false); (EBool false);
      (EString ""); (EBool false); (EString ""); (EString ""); (EString "");
      (EBool false); (EString ""); (EString ""); (EBool false); (EBool false);
      (EBool false); (EString "")]))