From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 08:57:07 +0000 (+0000) Subject: alias declarations are now put in the .moo file. X-Git-Tag: PRE_GETTER_STORAGE~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6ec0a251ac681afb3a305323097d72ab80d7da6b;p=helm.git alias declarations are now put in the .moo file. --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 852608d51..2de254ab3 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -219,7 +219,7 @@ let generate_projections uri fields status = status ) status projections -let eval_command status cmd = +let eval_command output status cmd = match cmd with | TacticAst.Set (loc, name, value) -> let value = @@ -250,7 +250,8 @@ let eval_command status cmd = | TacticAst.Coercion (loc, coercion) -> eval_coercion status coercion | TacticAst.Alias (loc, spec) -> - (match spec with + let status = + match spec with | TacticAst.Ident_alias (id,uri) -> {status with aliases = DisambiguateTypes.Environment.add @@ -267,7 +268,10 @@ let eval_command status cmd = {status with aliases = DisambiguateTypes.Environment.add (DisambiguateTypes.Num instance) - (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }) + (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } + in + output (TacticAstPp.pp_alias spec ^ ".\n"); + status | TacticAst.Obj (loc,obj) -> let ext,name = match obj with @@ -310,19 +314,19 @@ let eval_command status cmd = | Cic.CurrentProof _ | Cic.Variable _ -> assert false -let eval_executable status ex = +let eval_executable output status ex = match ex with | TacticAst.Tactical (_, tac) -> eval_tactical status tac - | TacticAst.Command (_, cmd) -> eval_command status cmd + | TacticAst.Command (_, cmd) -> eval_command output 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 status st = +let eval output status st = match st with - | TacticAst.Executable (_,ex) -> eval_executable status ex + | TacticAst.Executable (_,ex) -> eval_executable output status ex | TacticAst.Comment (_,c) -> eval_comment status c let disambiguate_term status term = @@ -566,26 +570,27 @@ let disambiguate_statement status statement = let status, ex = disambiguate_executable status ex in status, TacticAst.Executable (loc,ex) -let eval_ast status ast = +let eval_ast output status ast = let status,st = disambiguate_statement status ast in (* this disambiguation step should be deferred to support tacticals *) - eval status st + eval output status st -let eval_from_stream status str cb = +let eval_from_stream output status str cb = let stl = CicTextualParser2.parse_statements str in - List.iter (fun ast -> cb !status ast;status := eval_ast !status ast) stl + List.iter + (fun ast -> cb !status ast;status := eval_ast output !status ast) stl -let eval_from_stream_greedy status str cb = +let eval_from_stream_greedy output status str cb = while true do print_string "matita> "; flush stdout; let ast = CicTextualParser2.parse_statement str in cb !status ast; - status := eval_ast !status ast + status := eval_ast output !status ast done -let eval_string status str = - eval_from_stream status (Stream.of_string str) (fun _ _ -> ()) +let eval_string output status str = + eval_from_stream output status (Stream.of_string str) (fun _ _ -> ()) let default_options () = (* diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 249bad8f4..c94f9748e 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -25,26 +25,30 @@ exception Drop -val eval_string: MatitaTypes.status ref -> string -> unit +val eval_string: (string -> unit) -> 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/matitaScript.ml b/helm/matita/matitaScript.ml index bd526212e..92fc2e42c 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 status user_goal parsed_text st = +let eval_with_engine output 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 status user_goal parsed_text st = match status.proof_status with | Incomplete_proof (_, goal) when goal <> user_goal -> goal_changed := true; - MatitaEngine.eval_ast status (goal_ast user_goal) + MatitaEngine.eval_ast output status (goal_ast user_goal) | _ -> status in - let new_status = MatitaEngine.eval_ast status st in + let new_status = MatitaEngine.eval_ast output status st in let new_aliases = match ex with | TA.Command (_, TA.Alias _) -> @@ -133,8 +133,8 @@ let disambiguate term status = | [_,_,x,_] -> x | _ -> assert false -let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text - script mac +let eval_macro output status (mathviewer:MatitaTypes.mathViewer) urichooser + parsed_text script mac = let module TA = TacticAst in let module TAPp = TacticAstPp in @@ -192,12 +192,12 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text | [] -> [], parsed_text_length | [uri] -> let ast = - (TA.Executable (loc, - (TA.Tactical (loc, - TA.Tactic (loc, - TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None))))))) + TA.Executable (loc, + (TA.Tactical (loc, + TA.Tactic (loc, + TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))) in - let new_status = MatitaEngine.eval_ast status ast in + let new_status = MatitaEngine.eval_ast output status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast @@ -250,7 +250,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser +let eval_executable output status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in @@ -258,12 +258,14 @@ 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 status user_goal parsed_text (TA.Executable (loc, ex)) + eval_with_engine output status user_goal parsed_text + (TA.Executable (loc, ex)) | TA.Macro (_,mac) -> - eval_macro status mathviewer urichooser parsed_text script mac + eval_macro output status mathviewer urichooser parsed_text script mac -let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser -user_goal script s = +let rec eval_statement output status (mathviewer:MatitaTypes.mathViewer) + urichooser user_goal script s += if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let st = CicTextualParser2.parse_statement (Stream.of_string s) in let text_of_loc loc = @@ -277,7 +279,7 @@ user_goal script s = 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 status mathviewer urichooser user_goal script s + eval_statement output status mathviewer urichooser user_goal script s in (match s with | (status, text) :: tl -> @@ -285,8 +287,8 @@ user_goal script s = | [] -> [], 0) | TacticAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in - eval_executable - status mathviewer urichooser user_goal parsed_text script ex + eval_executable output status mathviewer urichooser user_goal + parsed_text script ex let fresh_script_id = let i = ref 0 in @@ -339,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 self#status mathviewer urichooser userGoal self s in + eval_statement (assert false) 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/matitacLib.ml b/helm/matita/matitacLib.ml index d82d3f755..b7afff475 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -38,7 +38,7 @@ let usage = let status = ref None -let run_script is eval_function = +let run_script output is eval_function = let status = match !status with | None -> assert false @@ -58,7 +58,7 @@ let run_script is eval_function = MatitaLog.debug ("Executing: ``" ^ stm ^ "''") in try - eval_function status is cb + eval_function output 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 str MatitaEngine.eval_from_stream_greedy + run_script ignore str MatitaEngine.eval_from_stream_greedy with | MatitaEngine.Drop -> pp_ocaml_mode () | Sys.Break -> MatitaLog.error "user break!"; go () @@ -124,7 +124,10 @@ let main ~mode = | "stdin" -> stdin | fname -> open_in fname) in - run_script is MatitaEngine.eval_from_stream; + 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; let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in let sec = @@ -151,7 +154,7 @@ let main ~mode = begin MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); - close_out (open_out (MatitaMisc.obj_file_of_script fname)); + close_out os; exit 0 end with