From 504bbea31eb62cc0ce63bbdfe4dc1e03e479aba1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 3 Feb 2004 15:02:52 +0000 Subject: [PATCH] - comment inside .test file that explain what follows - use a list to clear buffers - better comment for .test file format --- helm/gTopLevel/regtest.ml | 48 +++++++++++++++++++++++---------------- 1 file changed, 28 insertions(+), 20 deletions(-) diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 8f42a29fc..b79ca5bf1 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -33,7 +33,7 @@ let usage () = exit 2 let rawsep = "###" -let sep = Pcre.regexp rawsep +let sep = Pcre.regexp (sprintf "^%s" rawsep) let msg_prefix = "*** REGTEST *** " let print_msg s = prerr_endline (msg_prefix ^ s) @@ -42,11 +42,13 @@ type state = Term | EMetasenv | ETerm | EType | EReduced (* regtest file format * < cic term in concrete syntax > * separator (* see sep above *) - * < expected cic term after disambiguation as PPed by CicPp.ppterm > + * < expected metasenv after disambiguation (CicMetaSubst.ppmetasenv) > * separator (* see sep above *) - * < expected cic type as per type_of as PPed by CicPp.ppterm > + * < expected cic term after disambiguation (CicPp.ppterm) > * separator (* see sep above *) - * < expected reduced cic term as PPed by CicPp.ppterm > + * < expected cic type as per type_of (CicPp.ppterm) > + * separator (* see sep above *) + * < expected reduced cic term as (CicPp.ppterm) > *) type regtest = { @@ -57,15 +59,18 @@ type regtest = { ereduced: string; (* expected reduced term *) } - (* this should be the only function here printing on stdout *) let print_test test fname = let oc = open_out fname in output_string oc (String.concat "" - [ test.term; rawsep ^ "\n"; - test.emetasenv; rawsep ^ "\n"; - test.eterm; rawsep ^ "\n"; - test.etype; rawsep ^ "\n"; + [ test.term; + sprintf "%s (* METASENV after disambiguation *)\n" rawsep; + test.emetasenv; + sprintf "%s (* TERM after disambiguation *)\n" rawsep; + test.eterm; + sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep; + test.etype; + sprintf "%s (* REDUCED disambiguated term *)\n" rawsep; test.ereduced ]); close_out oc @@ -85,12 +90,15 @@ let parse_regtest = | EReduced -> assert false in let buffer_of_state = function - | Term -> term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype | EReduced -> ereduced + | Term -> term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype + | EReduced -> ereduced + in + let clear_buffers () = + List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ] in fun fname -> state := Term; - Buffer.clear term; Buffer.clear emetasenv; Buffer.clear eterm; - Buffer.clear etype; Buffer.clear ereduced; + clear_buffers (); let ic = open_in fname in (try while true do @@ -108,14 +116,6 @@ let parse_regtest = let as_expected expected found = (* ignores "term" field *) let outcome = ref true in - if expected.emetasenv <> found.emetasenv then begin - print_msg "Metasenv mismatch"; - print_msg " expected:"; - print_msg (" " ^ expected.emetasenv); - print_msg " found:"; - print_msg (" " ^ found.emetasenv); - outcome := false; - end; if expected.eterm <> found.eterm then begin print_msg "Term mismatch"; print_msg " expected:"; @@ -124,6 +124,14 @@ let as_expected expected found = (* ignores "term" field *) print_msg (" " ^ found.eterm); outcome := false; end; + if expected.emetasenv <> found.emetasenv then begin + print_msg "Metasenv mismatch"; + print_msg " expected:"; + print_msg (" " ^ expected.emetasenv); + print_msg " found:"; + print_msg (" " ^ found.emetasenv); + outcome := false; + end; if expected.etype <> found.etype then begin print_msg "Type mismatch"; print_msg " expected:"; -- 2.39.2