From: Claudio Sacerdoti Coen Date: Tue, 2 Mar 2004 15:19:06 +0000 (+0000) Subject: The regression tests now check also the generated disambiguation environments. X-Git-Tag: v0_0_4~58 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57f2f0152b79ad7096b72b7e3e83939d63454a88;p=helm.git The regression tests now check also the generated disambiguation environments. --- diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index 515c417cb..f7370422f 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -66,11 +66,10 @@ let parse mqi_handle ?(uri_pred = constants_only) = let empty_context = [] in let empty_metasenv = [] in fun input -> - List.map (fun (_,metasenv,term) -> metasenv,term) - (Disambiguate'.disambiguate_term - mqi_handle empty_context empty_metasenv input empty_environment) + (Disambiguate'.disambiguate_term + mqi_handle empty_context empty_metasenv input empty_environment) let parse_pp mqi_handle ?uri_pred input = - List.map (fun (_,t) -> CicPp.ppterm t) + List.map (fun (_,_,t) -> CicPp.ppterm t) (parse mqi_handle ?uri_pred input) diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index ff82e6fa0..9ba49ef52 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -37,7 +37,9 @@ val uri_pred_of_conf: bool -> string -> (string -> bool) * batch mode if possible, otherwise raises Failure above. * uri_pred is the predicate used to select which uris are tried. Per default * only constant URIs are accepted *) -val parse: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> (Cic.metasenv * Cic.term) list +val parse: + MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> + (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list (** as above, but instead of returning the parsed cic term, pretty prints it * (ignoring returned metasenv) diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index fb91bf200..e31b1da05 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -34,10 +34,13 @@ let print s = print_string s; flush stdout let print_endline s = print_endline s let print_endline_to_channel ch s = output_string ch (s ^ "\n") -type state = Term | EMetasenv | ETerm | EType | EReduced +type state = Term | EEnv | EMetasenv | ETerm | EType | EReduced (* regtest file format * < cic term in concrete syntax > + * separatorseparator INTERPRETATION NUMBER separatorseparator + * separator (* see sep above *) + * < expected disambiguating environment (EnvironmentP3.to_string) > * separator (* see sep above *) * < expected metasenv after disambiguation (CicMetaSubst.ppmetasenv) > * separator (* see sep above *) @@ -46,10 +49,12 @@ type state = Term | EMetasenv | ETerm | EType | EReduced * < expected cic type as per type_of (CicPp.ppterm) > * separator (* see sep above *) * < expected reduced cic term as (CicPp.ppterm) > + * ... (* repeat from ... INTERPRETATION NUMBER ... *) *) type regtest = { term: string; (* raw cic term *) + eenv : string; (* disambiguating parsing environment *) emetasenv : string; (* expected metasenv *) eterm: string; (* expected term *) etype: string; (* expected type *) @@ -66,6 +71,8 @@ let print_test tests fname = output_string oc (String.concat "" [ sprintf "%s%s INTERPRETATION NUMBER %d %s%s\n" rawsep rawsep !i rawsep rawsep ; + sprintf "%s (* disambiguation environment *)\n" rawsep; + test.eenv; sprintf "%s (* METASENV after disambiguation *)\n" rawsep; test.emetasenv; sprintf "%s (* TERM after disambiguation *)\n" rawsep; @@ -79,6 +86,7 @@ let print_test tests fname = let parse_regtest = let term = Buffer.create 1024 in (* raw term *) + let eenv = Buffer.create 1024 in (* disambiguating parser environment *) let emetasenv = Buffer.create 1024 in (* expected metasenv *) let eterm = Buffer.create 1024 in (* raw expected term *) let etype = Buffer.create 1024 in (* raw expected type *) @@ -86,18 +94,19 @@ let parse_regtest = let state = ref Term in let bump_state () = match !state with - | Term -> state := EMetasenv + | Term -> state := EEnv + | EEnv -> state := EMetasenv | EMetasenv -> state := ETerm | ETerm -> state := EType | EType -> state := EReduced | EReduced -> assert false in let buffer_of_state = function - | Term -> term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype + | Term -> term | EEnv -> eenv | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype | EReduced -> ereduced in let clear_buffers () = - List.iter Buffer.clear [ emetasenv; eterm; etype; ereduced ] + List.iter Buffer.clear [ eenv; emetasenv; eterm; etype; ereduced ] in fun fname -> state := Term; @@ -105,7 +114,8 @@ let parse_regtest = let res = ref [] in let push_res () = res := - { term = Buffer.contents term; + {term = Buffer.contents term; + eenv = Buffer.contents eenv; emetasenv = Buffer.contents emetasenv; eterm = Buffer.contents eterm; etype = Buffer.contents etype; @@ -130,10 +140,13 @@ let parse_regtest = let as_expected_one och expected found = (* ignores "term" field *) let eterm_ok = expected.eterm = found.eterm in + let eenv_ok = expected.eenv = found.eenv in let emetasenv_ok = expected.emetasenv = found.emetasenv in let etype_ok = expected.etype = found.etype in let ereduced_ok = expected.ereduced = found.ereduced in - let outcome = eterm_ok && emetasenv_ok && etype_ok && ereduced_ok in + let outcome = + eterm_ok && eenv_ok && emetasenv_ok && etype_ok && ereduced_ok + in begin let print_endline s = print_endline_to_channel (Lazy.force och) s in if not eterm_ok then begin @@ -143,6 +156,13 @@ let as_expected_one och expected found = (* ignores "term" field *) print_endline "# found:"; print_endline (" " ^ found.eterm); end; + if not eenv_ok then begin + print_endline "### Disambiguation environment mismatch ###"; + print_endline "# expected:"; + print_endline (" " ^ expected.eenv); + print_endline "# found:"; + print_endline (" " ^ found.eenv); + end; if not emetasenv_ok then begin print_endline "### Metasenv mismatch ###"; print_endline "# expected:"; @@ -191,7 +211,7 @@ let as_expected report_fname expected found = let test_this mqi_handle uri_pred raw_term = let empty_context = [] in List.map - (function (metasenv, cic_term) -> + (function (env, metasenv, cic_term) -> let etype = try CicPp.ppterm @@ -203,8 +223,8 @@ let test_this mqi_handle uri_pred raw_term = CicPp.ppterm (CicReduction.whd empty_context cic_term) with _ -> "MALFORMED" in - { - term = raw_term; (* useless *) + { term = raw_term; (* useless *) + eenv = DisambiguatingParser.EnvironmentP3.to_string env ^ "\n"; emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n"; eterm = CicPp.ppterm cic_term ^ "\n"; etype = etype ^ "\n";