* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
+open Printf
+
exception Drop
exception IncludedFileNotCompiled of string (* file name *)
+exception Macro of
+ GrafiteAst.loc *
+ (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+exception ReadOnlyUri of string
type options = {
do_heavy_checks: bool ;
| GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
let reduction =
match reduction_kind with
+ | `Demodulate ->
+ GrafiteTypes.command_error "demodulation can't be folded"
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| 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)
+ | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
+ | `Normalize -> Tactics.normalize ~pattern
+ | `Reduce -> Tactics.reduce ~pattern
+ | `Simpl -> Tactics.simpl ~pattern
+ | `Unfold what -> Tactics.unfold ~pattern what
+ | `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
| GrafiteAst.Replace (_, pattern, with_what) ->
Tactics.replace ~pattern ~with_what
'obj GrafiteAst.command ->
GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ disambiguate_macro:
+ (GrafiteTypes.status ->
+ 'term GrafiteAst.macro ->
+ Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
?do_heavy_checks:bool ->
?clean_baseuri:bool ->
GrafiteTypes.status ->
'obj GrafiteAst.command ->
GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ disambiguate_macro:
+ (GrafiteTypes.status ->
+ 'term GrafiteAst.macro ->
+ Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
options ->
GrafiteTypes.status ->
('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code ->
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
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
None)
lemmas)
in
+ prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
coercions;
- let status = GrafiteTypes.add_moo_content moo_content status in
- let basedir = Helm_registry.get "matita.basedir" in
- List.fold_left
- (fun (status,lemmas) uri ->
- let status,new_lemmas =
- GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
- in
- status,new_lemmas@lemmas
- ) (status,[]) 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
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Include (loc, baseuri) ->
let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
- let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
if not (Sys.file_exists moopath) then
raise (IncludedFileNotCompiled moopath);
let status = eval_from_moo.efm_go status moopath in
let v = Http_getter_misc.strip_trailing_slash value in
try
ignore (String.index v ' ');
- raise (GrafiteTypes.Command_error "baseuri can't contain spaces")
+ 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 (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
- HLog.warn ("baseuri " ^ value ^ " is not empty");
+ HLog.message ("baseuri " ^ value ^ " is not empty");
HLog.message ("cleaning baseuri " ^ value);
LibraryClean.clean_baseuris ~basedir [value];
end;
"\nPlease use a variant."));
end;
assert (metasenv = metasenv');
- let goalno =
- match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false
- in
let initial_proof = (Some uri, metasenv, bo, ty) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv in
{ status with GrafiteTypes.proof_status =
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
| _ -> status,uris
-} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex ->
+} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status ex ->
match ex with
| GrafiteAst.Tactical (_, tac, None) ->
eval_tactical ~disambiguate_tactic status tac,[]
eval_tactical ~disambiguate_tactic status punct,[]
| GrafiteAst.Command (_, cmd) ->
eval_command.ec_go ~disambiguate_command opts status cmd
- | GrafiteAst.Macro (_, mac) ->
-(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
- raise (Command_error
- (Printf.sprintf "The macro %s can't be in a script"
- (GrafiteAstPp.pp_macro_ast mac)))
-*) assert false
+ | GrafiteAst.Macro (loc, macro) ->
+ raise (Macro (loc,disambiguate_macro status macro))
} and eval_from_moo = {efm_go = fun status fname ->
let ast_of_cmd cmd =
eval_ast.ea_go
~disambiguate_tactic:(fun status _ tactic -> status,tactic)
~disambiguate_command:(fun status cmd -> status,cmd)
+ ~disambiguate_macro:(fun _ _ -> assert false)
status ast
in
assert (lemmas=[]);
status)
status moo
-} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
- st
+} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status st
->
let opts = {
do_heavy_checks = do_heavy_checks ;
in
match st with
| GrafiteAst.Executable (_,ex) ->
- eval_executable.ee_go ~disambiguate_tactic
- ~disambiguate_command opts status ex
+ eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
+ ~disambiguate_macro opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c,[]
}
projects / helm.git / blobdiff