| GrafiteAst.Clear (_,id) -> Tactics.clear id
| GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
| GrafiteAst.Contradiction _ -> Tactics.contradiction
- | GrafiteAst.Compare (_, term) -> Tactics.compare term
| GrafiteAst.Constructor (_, n) -> Tactics.constructor n
| GrafiteAst.Cut (_, ident, term) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
| GrafiteAst.Decompose (_, types, what, names) ->
let to_type = function
| GrafiteAst.Type (uri, typeno) -> uri, typeno
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 ~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},
lemmas
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 refinement_toolkit uri obj status in
status, lemmas
let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
let status,cmd = disambiguate_command status cmd in
- let basedir = Helm_registry.get "matita.basedir" in
let status,uris =
match cmd with
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Include (loc, baseuri) ->
- let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
- if not (Sys.file_exists moopath) then
- raise (IncludedFileNotCompiled moopath);
+ let moopath_rw, moopath_r =
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ let moopath =
+ if Sys.file_exists moopath_r then moopath_r else
+ if Sys.file_exists moopath_rw then moopath_rw else
+ raise (IncludedFileNotCompiled moopath_rw)
+ in
let status = eval_from_moo.efm_go status moopath in
status,[]
| GrafiteAst.Set (loc, name, value) ->
HLog.error (sprintf "uri %s belongs to a read-only repository" value);
raise (ReadOnlyUri value)
end;
- if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
+ if not (Http_getter_storage.is_empty value) &&
+ opts.clean_baseuri
+ then begin
HLog.message ("baseuri " ^ value ^ " is not empty");
HLog.message ("cleaning baseuri " ^ value);
- LibraryClean.clean_baseuris ~basedir [value];
+ LibraryClean.clean_baseuris [value];
+ assert (Http_getter_storage.is_empty value);
end;
+ HExtlib.mkdir
+ (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ "/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| GrafiteAst.Drop loc -> raise Drop
(match types with (name,_,_,_)::_ -> name | _ -> assert false)
| _ -> assert false in
let uri =
- UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext)
- in
+ UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in
+ let obj = CicRefine.pack_coercion_obj obj in
let metasenv = GrafiteTypes.get_proof_metasenv status in
match obj with
| Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
("Theorem already proved: " ^ UriManager.string_of_uri x ^
"\nPlease use a variant."));
end;
- assert (metasenv = metasenv');
- let initial_proof = (Some uri, metasenv, bo, ty) in
- let initial_stack = Continuationals.Stack.of_metasenv metasenv in
+ let initial_proof = (Some uri, metasenv', bo, ty) in
+ let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof
{ GrafiteTypes.proof = initial_proof; stack = initial_stack } },