(* $Id$ *)
+module PEH = ProofEngineHelpers
+
exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
(Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
-exception ReadOnlyUri of string
type 'a disambiguator_input = string * int * 'a
type options = {
do_heavy_checks: bool ;
- clean_baseuri: bool
}
(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
- | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
+ | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
~pattern what
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
- | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
| `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
| `Unfold None ->
PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
| `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
| `Unfold what -> Tactics.unfold ~pattern what
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
| GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Subst _ -> Tactics.subst
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
(* Implementazioni Aggiunte *)
| _ -> false
let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
- let module PEH = ProofEngineHelpers in
(* let print_m name metasenv =
prerr_endline (">>>>> " ^ name);
prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)
Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
?do_heavy_checks:bool ->
- ?clean_baseuri:bool ->
GrafiteTypes.status ->
(('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
disambiguator_input ->
RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
}
-let eval_coercion status ~add_composites uri arity saturations baseuri =
+let eval_coercion status ~add_composites uri arity saturations =
let status,compounds =
GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
- saturations baseuri
+ saturations (GrafiteTypes.get_baseuri status)
in
let moo_content =
List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
with Not_found -> false,0
with Not_found -> assert false
in
+ let buri = GrafiteTypes.get_baseuri status in
(* looking at the fields we can know the 'wanted' coercions, but not the
* actually generated ones. So, only the intersection between the wanted
* and the actual should be in the moo as coercion, while everithing in
(function
| (name,true,arity) ->
Some
- (arity, UriManager.uri_of_string
- (GrafiteTypes.qualify status name ^ ".con"))
+ (arity, UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con" ))
| _ -> None)
fields
in
let status = GrafiteTypes.add_moo_content [cmd] status in
status,[]
| GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
- eval_coercion status ~add_composites uri arity saturations
- (GrafiteTypes.get_string_option status "baseuri")
+ eval_coercion status ~add_composites uri arity saturations
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
status,[]
| GrafiteAst.Print (_,"proofterm") ->
let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
- print_endline (Auto.pp_proofterm p);
+ prerr_endline (Auto.pp_proofterm p);
status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Qed loc ->
| GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) ->
Setoids.add_relation id a aeq refl sym trans;
status, [] (*CSC: TO BE FIXED *)
- | GrafiteAst.Set (loc, name, value) ->
- if name = "baseuri" then begin
- let value =
- let v = Http_getter_misc.strip_trailing_slash value in
- try
- ignore (String.index v ' ');
- GrafiteTypes.command_error "baseuri can't contain spaces"
- with Not_found -> v
- in
- if Http_getter_storage.is_read_only value then begin
- HLog.error (Printf.sprintf "uri %s belongs to a read-only repository" value);
- raise (ReadOnlyUri value)
- end;
- if (not (Http_getter_storage.is_empty ~local:true value) ||
- LibraryClean.db_uris_of_baseuri value <> [])
- && opts.clean_baseuri
- then begin
- HLog.message ("baseuri " ^ value ^ " is not empty");
- HLog.message ("cleaning baseuri " ^ value);
- LibraryClean.clean_baseuris [value];
- assert (Http_getter_storage.is_empty ~local:true value);
- end;
- if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
- ~default:false)
- then
- HExtlib.mkdir
- (Filename.dirname
- (Http_getter.filename ~local:true ~writable:true (value ^
- "/foo.con")));
- end;
- GrafiteTypes.set_option status name value,[]
+ | GrafiteAst.Set (loc, name, value) -> status, []
+(* GrafiteTypes.set_option status name value,[] *)
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with
".ind",
(match types with (name,_,_,_)::_ -> name | _ -> assert false)
| _ -> assert false in
- let uri =
- UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in
+ let buri = GrafiteTypes.get_baseuri status in
+ let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in
let obj = CicRefine.pack_coercion_obj obj in
let metasenv = GrafiteTypes.get_proof_metasenv status in
match obj with
status)
status moo
} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
-~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status
+~disambiguate_macro ?(do_heavy_checks=false) status
(text,prefix_len,st)
->
- let opts = {
- do_heavy_checks = do_heavy_checks ;
- clean_baseuri = clean_baseuri }
- in
+ let opts = { do_heavy_checks = do_heavy_checks ; } in
match st with
| GrafiteAst.Executable (_,ex) ->
eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
projects / helm.git / blobdiff