FStarLang / FStar

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

Pretty-print ML extraction terms. #3468

Closed gebner closed 2 months ago

gebner commented 2 months ago

I've been staring too much at ML extraction debugging output recently. This PR replaces the printf-based printer for ML terms with a pretty-printer using documents.

+++About to extract {FStar.List.Tot.Base.append}
Execution time of ---Extracted {FStar.List.Tot.Base.append}: 0.114 ms
Extraction result: [
MLM_Loc;
MLM_Let (Rec, [{
    mllb_name = append;
    mllb_tysc =
      Some
      (<MLTY_Fun> (<MLTY_Named> 'a Prims.list) ->
        (<MLTY_Fun> (<MLTY_Named> 'a Prims.list) -> (<MLTY_Named> 'a Prims.list)));
    mllb_add_unit = false;
    mllb_def =
      (MLE_Fun
        ([(x, (<MLTY_Named> 'a Prims.list)); (y, (<MLTY_Named> 'a Prims.list))],
        (MLE_Match
          ((MLE_Var x),
          [((MLP_CTor (Prims.Nil, [])), None, (MLE_Var y));
            ((MLP_CTor (Prims.Cons, [(MLP_Var a1); (MLP_Var tl1)])),
            None,
            (MLE_CTor
              (Prims.Cons,
              [(MLE_Var a1);
                (MLE_App
                  ((MLE_TApp ((MLE_Name (FStar.List.Tot.Base, append)), ['a])),
                  [(MLE_Var tl1); (MLE_Var y)]))])))]))))
    }])
]
mtzguido commented 2 months ago

Nice!