let coercion_moo_statement_of uri =
GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+let refinement_toolkit = {
+ RefinementTool.type_of_aux' =
+ (fun ?localization_tbl e c t u ->
+ let saved = !CicRefine.insert_coercions in
+ CicRefine.insert_coercions:= false;
+ let rc =
+ try
+ let t, ty, metasenv, ugraph =
+ CicRefine.type_of_aux' ?localization_tbl e c t u in
+ RefinementTool.Success (t, ty, metasenv, ugraph)
+ with
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s -> RefinementTool.Exception s
+ in
+ CicRefine.insert_coercions := saved;
+ rc);
+ RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+ RefinementTool.apply_subst = CicMetaSubst.apply_subst;
+ RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv;
+ RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+
let eval_coercion status ~add_composites uri =
let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
prerr_endline "evaluating a coercion command";
- GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+ GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
| _ -> None)
fields
in
+ (*
prerr_endline "wanted coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- wanted_coercions;
+ wanted_coercions; *)
let coercions, moo_content =
List.split
(HExtlib.filter_map
None)
lemmas)
in
- prerr_endline "actual coercions:";
+ (* prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- coercions;
+ coercions; *)
let status = GrafiteTypes.add_moo_content moo_content status in
{status with
GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
let add_obj uri obj status =
let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in
status, lemmas
let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->