From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 10:45:52 +0000 (+0000) Subject: "include" command implemented. X-Git-Tag: PRE_GETTER_STORAGE~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=29a3bd5d160f31873236c93a008a9e4fd31c305e;p=helm.git "include" command implemented. --- diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile index 5721ad954..74bc862bc 100644 --- a/helm/matita/library/Makefile +++ b/helm/matita/library/Makefile @@ -30,9 +30,16 @@ verboseopt: 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) $< diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma index 842b952b9..d0049187a 100644 --- a/helm/matita/library/Z.ma +++ b/helm/matita/library/Z.ma @@ -14,30 +14,7 @@ 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 diff --git a/helm/matita/library/nat.ma b/helm/matita/library/nat.ma index 114f8d1c1..066018d9e 100644 --- a/helm/matita/library/nat.ma +++ b/helm/matita/library/nat.ma @@ -14,25 +14,10 @@ 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 diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 2de254ab3..17532cc90 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -218,9 +218,25 @@ let generate_projections uri fields status = ("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 @@ -250,28 +266,24 @@ let eval_command output status cmd = | 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 @@ -314,19 +326,19 @@ let eval_command output status cmd = | 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 = @@ -347,11 +359,8 @@ 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 = @@ -377,11 +386,8 @@ 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) = @@ -532,6 +538,7 @@ and disambiguate_tacticals status tacticals = 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) @@ -570,27 +577,31 @@ let disambiguate_statement status statement = 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 () = (* @@ -611,6 +622,7 @@ let default_options () = let initial_status = lazy { aliases = DisambiguateTypes.empty_environment; + moo_content_rev = []; proof_status = No_proof; options = default_options (); objects = []; diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index c94f9748e..249bad8f4 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -25,30 +25,26 @@ 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 diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index acaf2123c..1ea4e7e92 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -191,7 +191,7 @@ let get_proof_context 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 diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 92fc2e42c..83aa60362 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -65,7 +65,7 @@ let goal_ast n = 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 @@ -77,10 +77,10 @@ let eval_with_engine output status user_goal parsed_text st = 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 _) -> @@ -133,7 +133,7 @@ let disambiguate term status = | [_,_,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 @@ -197,7 +197,7 @@ let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser 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 @@ -250,7 +250,7 @@ let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser | 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 @@ -258,12 +258,12 @@ user_goal parsed_text script ex = 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; @@ -279,7 +279,7 @@ let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer) 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 -> @@ -287,7 +287,7 @@ let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer) | [] -> [], 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 = @@ -341,7 +341,7 @@ object (self) 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"; diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 660be6c10..76ec992be 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -27,6 +27,24 @@ open Printf 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 = @@ -48,13 +66,13 @@ let env_of_list l env = 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 @@ -212,15 +230,6 @@ let time_travel ~present ~past = 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 = diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 376ba3794..06807a1e4 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -36,6 +36,11 @@ val time_travel: 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 *) diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 9ed52f568..e349a6e4d 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -59,6 +59,7 @@ let no_options = StringMap.empty 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; diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index b7afff475..c16915e63 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -38,7 +38,7 @@ let usage = 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 @@ -58,7 +58,7 @@ let run_script output is eval_function = 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 @@ -84,7 +84,7 @@ let pp_ocaml_mode () = 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 () @@ -124,10 +124,7 @@ let main ~mode = | "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 = @@ -139,9 +136,9 @@ let main ~mode = 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 @@ -152,9 +149,13 @@ let main ~mode = 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 diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index fbbfc137b..966b02b09 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -45,6 +45,8 @@ let main () = | 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 diff --git a/helm/matita/tests/Makefile b/helm/matita/tests/Makefile index 73cf367a9..47ed823a5 100644 --- a/helm/matita/tests/Makefile +++ b/helm/matita/tests/Makefile @@ -30,9 +30,14 @@ verboseopt: 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) $< @@ -43,13 +48,13 @@ $(DEPEND_NAME): $(SRC) $(LINKS) # 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)