- {
- term = raw_term; (* useless *)
- emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
- eterm = CicPp.ppterm cic_term ^ "\n";
- etype = etype ^ "\n";
- ereduced = ereduced ^ "\n";
- }
+ let outcome = aux (expected,found) in
+ (if Lazy.lazy_is_val och then close_out (Lazy.force och)) ;
+ outcome
+
+let test_this mqi_handle uri_pred raw_term =
+ let empty_context = [] in
+ List.map
+ (function (metasenv, cic_term) ->
+ let etype =
+ try
+ CicPp.ppterm
+ (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
+ with _ -> "MALFORMED"
+ in
+ let ereduced =
+ try
+ CicPp.ppterm (CicReduction.whd empty_context cic_term)
+ with _ -> "MALFORMED"
+ in
+ {
+ term = raw_term; (* useless *)
+ emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
+ eterm = CicPp.ppterm cic_term ^ "\n";
+ etype = etype ^ "\n";
+ ereduced = ereduced ^ "\n";
+ }
+ ) (BatchParser.parse mqi_handle ~uri_pred raw_term)