clean: $(LINKS)
@rm -f $(SRC:%.ma=%.moo)
- @$(MATITACLEAN) all
+ @$(MATITACLEAN) $(SRC)
-depend: $(DEPEND_NAME)
+cleanall: $(LINKS)
+ @rm -f $(SRC:%.ma=%.moo)
+ $(MATITACLEAN) all
+
+depend:
+ rm $(DEPEND_NAME)
+ make $(DEPEND_NAME)
+.PHONY: depend
%.moo:%.ma $(DEPEND_NAME) $(LINKS)
@[ ! -e $@ ] || $(MATITACLEAN) $<
set "baseuri" "cic:/matita/Z/".
-alias id "nat" = "cic:/matita/nat/nat.ind#xpointer(1/1)".
-alias id "O" = "cic:/matita/nat/nat.ind#xpointer(1/1/1)".
-alias id "false" = "cic:/matita/bool/bool.ind#xpointer(1/1/2)".
-alias id "true" = "cic:/matita/bool/bool.ind#xpointer(1/1/1)".
-alias id "Not" = "cic:/matita/logic/Not.con".
-alias id "eq" = "cic:/matita/equality/eq.ind#xpointer(1/1)".
-alias id "if_then_else" = "cic:/matita/bool/if_then_else.con".
-alias id "refl_equal" = "cic:/matita/equality/eq.ind#xpointer(1/1/1)".
-alias id "False" = "cic:/matita/logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/matita/logic/True.ind#xpointer(1/1)".
-alias id "sym_eq" = "cic:/matita/equality/sym_eq.con".
-alias id "I" = "cic:/matita/logic/True.ind#xpointer(1/1/1)".
-alias id "S" = "cic:/matita/nat/nat.ind#xpointer(1/1/2)".
-alias id "LT" = "cic:/matita/compare/compare.ind#xpointer(1/1/1)".
-alias id "minus" = "cic:/matita/nat/minus.con".
-alias id "nat_compare" = "cic:/matita/nat/nat_compare.con".
-alias id "plus" = "cic:/matita/nat/plus.con".
-alias id "pred" = "cic:/matita/nat/pred.con".
-alias id "sym_plus" = "cic:/matita/nat/sym_plus.con".
-alias id "nat_compare_invert" = "cic:/matita/nat/nat_compare_invert.con".
-alias id "plus_n_O" = "cic:/matita/nat/plus_n_O.con".
-alias id "plus_n_Sm" = "cic:/matita/nat/plus_n_Sm.con".
-alias id "nat_double_ind" = "cic:/matita/nat/nat_double_ind.con".
-alias id "f_equal" = "cic:/matita/equality/f_equal.con".
+include "nat.ma".
inductive Z : Set \def
OZ : Z
set "baseuri" "cic:/matita/nat/".
-alias id "eq" = "cic:/matita/equality/eq.ind#xpointer(1/1)".
-alias id "refl_equal" = "cic:/matita/equality/eq.ind#xpointer(1/1/1)".
-alias id "sym_eq" = "cic:/matita/equality/sym_eq.con".
-alias id "f_equal" = "cic:/matita/equality/f_equal.con".
-alias id "Not" = "cic:/matita/logic/Not.con".
-alias id "False" = "cic:/matita/logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/matita/logic/True.ind#xpointer(1/1)".
-alias id "trans_eq" = "cic:/matita/equality/trans_eq.con".
-alias id "I" = "cic:/matita/logic/True.ind#xpointer(1/1/1)".
-alias id "f_equal2" = "cic:/matita/equality/f_equal2.con".
-alias id "False_ind" = "cic:/matita/logic/False_ind.con".
-alias id "false" = "cic:/matita/bool/bool.ind#xpointer(1/1/2)".
-alias id "true" = "cic:/matita/bool/bool.ind#xpointer(1/1/1)".
-alias id "if_then_else" = "cic:/matita/bool/if_then_else.con".
-alias id "EQ" = "cic:/matita/compare/compare.ind#xpointer(1/1/2)".
-alias id "GT" = "cic:/matita/compare/compare.ind#xpointer(1/1/3)".
-alias id "LT" = "cic:/matita/compare/compare.ind#xpointer(1/1/1)".
-alias id "compare" = "cic:/matita/compare/compare.ind#xpointer(1/1)".
-alias id "compare_invert" = "cic:/matita/compare/compare_invert.con".
+include "equality.ma".
+include "logic.ma".
+include "bool.ma".
+include "compare.ma".
inductive nat : Set \def
| O : nat
("Unable to create projection " ^ name ^ " because it requires " ^ depend);
status
) status projections
+
+(* to avoid a long list of recursive functions *)
+let eval_from_stream_greedy_ref = ref (fun _ _ _ -> assert false);;
-let eval_command output status cmd =
+let eval_command status cmd =
match cmd with
+ | TacticAst.Include (loc, path) ->
+ let path = MatitaMisc.obj_file_of_script path in
+ let stream = Stream.of_channel (open_in path) in
+ let status = ref status in
+ (try
+ !eval_from_stream_greedy_ref status stream (fun _ _ -> ())
+ with
+ CicTextualParser2.Parse_error (floc,err) as exc ->
+ (* check for EOI *)
+ if Stream.peek stream = None then ()
+ else raise exc
+ );
+ !status
| TacticAst.Set (loc, name, value) ->
let value =
if name = "baseuri" then
| TacticAst.Coercion (loc, coercion) ->
eval_coercion status coercion
| TacticAst.Alias (loc, spec) ->
- let status =
+ let aliases =
match spec with
| TacticAst.Ident_alias (id,uri) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Id id)
- ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
- status.aliases }
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Id id)
+ (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
+ status.aliases
| TacticAst.Symbol_alias (symb, instance, desc) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Symbol (symb,instance))
- (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
- status.aliases }
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Symbol (symb,instance))
+ (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
+ status.aliases
| TacticAst.Number_alias (instance,desc) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Num instance)
- (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Num instance)
+ (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
in
- output (TacticAstPp.pp_alias spec ^ ".\n");
- status
+ MatitaSync.set_proof_aliases status aliases
| TacticAst.Obj (loc,obj) ->
let ext,name =
match obj with
| Cic.CurrentProof _
| Cic.Variable _ -> assert false
-let eval_executable output status ex =
+let eval_executable status ex =
match ex with
| TacticAst.Tactical (_, tac) -> eval_tactical status tac
- | TacticAst.Command (_, cmd) -> eval_command output status cmd
+ | TacticAst.Command (_, cmd) -> eval_command status cmd
| TacticAst.Macro (_, mac) ->
command_error (sprintf "The macro %s can't be in a script"
(TacticAstPp.pp_macro_cic mac))
let eval_comment status c = status
-let eval output status st =
+let eval status st =
match st with
- | TacticAst.Executable (_,ex) -> eval_executable output status ex
+ | TacticAst.Executable (_,ex) -> eval_executable status ex
| TacticAst.Comment (_,c) -> eval_comment status c
let disambiguate_term status term =
| Intermediate _ -> Intermediate metasenv
| Proof _ -> assert false
in
- let status =
- { status with
- aliases = aliases;
- proof_status = proof_status }
- in
+ let status = { status with proof_status = proof_status } in
+ let status = MatitaSync.set_proof_aliases status aliases in
status, cic
let disambiguate_obj status obj =
| Intermediate _
| Proof _ -> assert false
in
- let status =
- { status with
- aliases = aliases;
- proof_status = proof_status }
- in
+ let status = { status with proof_status = proof_status } in
+ let status = MatitaSync.set_proof_aliases status aliases in
status, cic
let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
status, tacticals
let disambiguate_command status = function
+ | TacticAst.Include (loc,path) as cmd -> status,cmd
| TacticAst.Coercion (loc, term) ->
let status, term = disambiguate_term status term in
status, TacticAst.Coercion (loc,term)
let status, ex = disambiguate_executable status ex in
status, TacticAst.Executable (loc,ex)
-let eval_ast output status ast =
+let eval_ast status ast =
let status,st = disambiguate_statement status ast in
(* this disambiguation step should be deferred to support tacticals *)
- eval output status st
+ eval status st
-let eval_from_stream output status str cb =
+let eval_from_stream status str cb =
let stl = CicTextualParser2.parse_statements str in
List.iter
- (fun ast -> cb !status ast;status := eval_ast output !status ast) stl
+ (fun ast -> cb !status ast;status := eval_ast !status ast) stl
-let eval_from_stream_greedy output status str cb =
+let eval_from_stream_greedy status str cb =
while true do
print_string "matita> ";
flush stdout;
let ast = CicTextualParser2.parse_statement str in
cb !status ast;
- status := eval_ast output !status ast
+ status := eval_ast !status ast
done
+;;
+
+(* to avoid a long list of recursive functions *)
+eval_from_stream_greedy_ref := eval_from_stream_greedy;;
-let eval_string output status str =
- eval_from_stream output status (Stream.of_string str) (fun _ _ -> ())
+let eval_string status str =
+ eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
let default_options () =
(*
let initial_status =
lazy {
aliases = DisambiguateTypes.empty_environment;
+ moo_content_rev = [];
proof_status = No_proof;
options = default_options ();
objects = [];
exception Drop
-val eval_string: (string -> unit) -> MatitaTypes.status ref -> string -> unit
+val eval_string: MatitaTypes.status ref -> string -> unit
val eval_from_stream:
- (string -> unit) ->
MatitaTypes.status ref -> char Stream.t ->
(MatitaTypes.status ->
(CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) ->
unit
val eval_from_stream_greedy:
- (string -> unit) ->
MatitaTypes.status ref-> char Stream.t ->
(MatitaTypes.status ->
(CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) ->
unit
val eval_ast:
- (string -> unit) ->
MatitaTypes.status ->
(CicAst.term,TacticAst.obj,string) TacticAst.statement ->
MatitaTypes.status
val eval:
- (string -> unit) ->
MatitaTypes.status -> (Cic.term,Cic.obj,string) TacticAst.statement ->
MatitaTypes.status
| _ -> []
let get_proof_aliases status = status.aliases
-
+
let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
let unopt = function None -> failwith "unopt: None" | Some v -> v
let loc = CicAst.dummy_floc in
A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
-let eval_with_engine output status user_goal parsed_text st =
+let eval_with_engine status user_goal parsed_text st =
let module TA = TacticAst in
let module TAPp = TacticAstPp in
let parsed_text_length = String.length parsed_text in
match status.proof_status with
| Incomplete_proof (_, goal) when goal <> user_goal ->
goal_changed := true;
- MatitaEngine.eval_ast output status (goal_ast user_goal)
+ MatitaEngine.eval_ast status (goal_ast user_goal)
| _ -> status
in
- let new_status = MatitaEngine.eval_ast output status st in
+ let new_status = MatitaEngine.eval_ast status st in
let new_aliases =
match ex with
| TA.Command (_, TA.Alias _) ->
| [_,_,x,_] -> x
| _ -> assert false
-let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser
+let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser
parsed_text script mac
=
let module TA = TacticAst in
TA.Tactic (loc,
TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None))))))
in
- let new_status = MatitaEngine.eval_ast output status ast in
+ let new_status = MatitaEngine.eval_ast status ast in
let extra_text =
comment parsed_text ^
"\n" ^ TAPp.pp_statement ast
| TA.Search_term (_, search_kind, term) -> failwith "not implemented"
-let eval_executable output status (mathviewer:MatitaTypes.mathViewer) urichooser
+let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser
user_goal parsed_text script ex =
let module TA = TacticAst in
let module TAPp = TacticAstPp in
let parsed_text_length = String.length parsed_text in
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _) ->
- eval_with_engine output status user_goal parsed_text
+ eval_with_engine status user_goal parsed_text
(TA.Executable (loc, ex))
| TA.Macro (_,mac) ->
- eval_macro output status mathviewer urichooser parsed_text script mac
+ eval_macro status mathviewer urichooser parsed_text script mac
-let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer)
+let rec eval_statement status (mathviewer:MatitaTypes.mathViewer)
urichooser user_goal script s
=
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
let remain_len = String.length s - parsed_text_length in
let s = String.sub s parsed_text_length remain_len in
let s,len =
- eval_statement output status mathviewer urichooser user_goal script s
+ eval_statement status mathviewer urichooser user_goal script s
in
(match s with
| (status, text) :: tl ->
| [] -> [], 0)
| TacticAst.Executable (loc, ex) ->
let parsed_text, parsed_text_length = text_of_loc loc in
- eval_executable output status mathviewer urichooser user_goal
+ eval_executable status mathviewer urichooser user_goal
parsed_text script ex
let fresh_script_id =
let s = match statement with Some s -> s | None -> self#getFuture in
MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
let (entries, parsed_len) =
- eval_statement (assert false) self#status mathviewer urichooser userGoal self s in
+ eval_statement self#status mathviewer urichooser userGoal self s in
let (new_statuses, new_statements) = List.split entries in
(*
prerr_endline "evalStatement returned";
open MatitaTypes
+let alias_diff ~from status =
+ let module Map = DisambiguateTypes.Environment in
+ Map.fold
+ (fun domain_item codomain_item acc ->
+ if not (Map.mem domain_item from.aliases) then
+ Map.add domain_item codomain_item acc
+ else
+ acc)
+ status.aliases Map.empty
+
+let set_proof_aliases status aliases =
+ let new_status = {status with aliases = aliases } in
+ let diff = alias_diff ~from:status new_status in
+ let moo_content_rev =
+ CicTextualParser2.EnvironmentP3.to_string diff ::
+ status.moo_content_rev in
+ {new_status with moo_content_rev = moo_content_rev}
+
(** given a uri and a type list (the contructors types) builds a list of pairs
* (name,uri) that is used to generate authomatic aliases **)
let extract_alias types uri =
let add_aliases_for_inductive_def status types suri =
let uri = UriManager.uri_of_string suri in
let aliases = env_of_list (extract_alias types uri) status.aliases in
- {status with aliases = aliases }
+ set_proof_aliases status aliases
let add_alias_for_constant status suri =
let uri = UriManager.uri_of_string suri in
let name = UriManager.name_of_uri uri in
let new_env = env_of_list [(name,suri)] status.aliases in
- {status with aliases = new_env }
+ set_proof_aliases status new_env
let add_aliases_for_object status suri =
function
MatitaLog.debug "l2:";
List.iter MatitaLog.debug l2
-let alias_diff ~from status =
- let module Map = DisambiguateTypes.Environment in
- Map.fold
- (fun domain_item codomain_item acc ->
- if not (Map.mem domain_item from.aliases) then
- Map.add domain_item codomain_item acc
- else
- acc)
- status.aliases Map.empty
let remove uri =
let derived_uris_of_uri uri =
val alias_diff: from:MatitaTypes.status -> MatitaTypes.status ->
DisambiguateTypes.environment
+ (** set the proof aliases enriching the moo_content *)
+val set_proof_aliases :
+ MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status
+
+
(* removes the object from DB, Disk, CoercionsDB, getter
* asserts the uri is resolved to file:// so it is only for
* user's objects *)
type status = {
aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ moo_content_rev: string list; (*CSC: a TacticAst.command list would be better *)
proof_status: proof_status;
options: options;
objects: (UriManager.uri * string) list;
let status = ref None
-let run_script output is eval_function =
+let run_script is eval_function =
let status =
match !status with
| None -> assert false
MatitaLog.debug ("Executing: ``" ^ stm ^ "''")
in
try
- eval_function output status is cb
+ eval_function status is cb
with
| MatitaEngine.Drop
| CicTextualParser2.Parse_error _ as exn -> raise exn
let rec go () =
let str = Stream.of_channel stdin in
try
- run_script ignore str MatitaEngine.eval_from_stream_greedy
+ run_script str MatitaEngine.eval_from_stream_greedy
with
| MatitaEngine.Drop -> pp_ocaml_mode ()
| Sys.Break -> MatitaLog.error "user break!"; go ()
| "stdin" -> stdin
| fname -> open_in fname)
in
- let os = open_out (MatitaMisc.obj_file_of_script fname) in
- let output s = output_string os s in
- output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
- run_script output is MatitaEngine.eval_from_stream;
+ run_script is MatitaEngine.eval_from_stream;
let elapsed = Unix.time () -. time in
let tm = Unix.gmtime elapsed in
let sec =
let hou =
if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
in
- let proof_status =
+ let proof_status,moo_content_rev =
match !status with
- | Some s -> !s.proof_status
+ | Some s -> !s.proof_status, !s.moo_content_rev
| None -> assert false
in
if proof_status <> MatitaTypes.No_proof then
end
else
begin
+ let os = open_out (MatitaMisc.obj_file_of_script fname) in
+ let output s = output_string os s in
+ output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
+ List.iter output (List.rev moo_content_rev);
+ close_out os;
MatitaLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
- close_out os;
exit 0
end
with
| TA.Executable (_, TA.Command
(_, TA.Alias (_, TA.Ident_alias(_, uri)))) ->
Hashtbl.add aliases file uri
+ | TA.Executable (_, TA.Command (_, TA.Include (_, path))) ->
+ Hashtbl.add deps file path
| _ -> ())
stms;
Hashtbl.iter
clean: $(LINKS)
@rm -f $(SRC:%.ma=%.moo)
- @$(MATITACLEAN) all
+ @$(MATITACLEAN) $(SRC)
+
+cleanall: $(LINKS)
+ @rm -f $(SRC:%.ma=%.moo)
+ $(MATITACLEAN) all
depend: $(DEPEND_NAME)
+.PHONY: depend
%.moo:%.ma $(DEPEND_NAME) $(LINKS)
@[ ! -e $@ ] || $(MATITACLEAN) $<
# Let's prepare the environment
.matita:
- @ln -s ../.matita .
+ @ln -fs ../.matita .
matita.lang:
- @ln -s ../matita.lang .
+ @ln -fs ../matita.lang .
matita.conf.xml:
- @ln -s ../matita.conf.xml .
+ @ln -fs ../matita.conf.xml .
#done
include $(DEPEND_NAME)
projects / helm.git / commitdiff