X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=8de5ccebc3dd74f54d218b85ccdf065b7e5ddf77;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=fe82e939cc01926ff000950bfb375a8e401309b2;hpb=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index fe82e939c..8de5ccebc 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -71,12 +71,11 @@ type guistuff = { ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } -let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal +let eval_with_engine include_paths guistuff grafite_status user_goal skipped_txt nonskipped_txt st = let module TAPp = GrafiteAstPp in let module DTE = DisambiguateTypes.Environment in - let module DP = DisambiguatePp in let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in @@ -85,7 +84,7 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g let enriched_history_fragment = MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") - lexicon_status grafite_status (text,prefix_len,st) + grafite_status (text,prefix_len,st) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) @@ -106,7 +105,7 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g * so that we can ensure the inclusion is performed after the included file * is compiled (if needed). matitac does not need that, since it compiles files * in the good order, here files may be compiled on demand. *) -let wrap_with_make include_paths (f : GrafiteParser.statement) x = +let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = try f ~never_include:true ~include_paths x with @@ -347,8 +346,8 @@ let cic2grafite context menv t = let width = max_int in let term_pp content_term = let pres_term = TermContentPres.pp_ast content_term in - let dummy_tbl = Hashtbl.create 1 in - let markup = CicNotationPres.render dummy_tbl pres_term in + let lookup_uri = fun _ -> None in + let markup = CicNotationPres.render ~lookup_uri pres_term in let s = "(" ^ BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") @@ -369,7 +368,7 @@ let cic2grafite context menv t = stupid_indenter script ;; -let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac = +let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in let module MDB = LibraryDb in @@ -450,7 +449,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let loc = HExtlib.floc_of_loc (0,text_len) in let statement = `Ast (GrafiteParser.LSome (ast loc),text) in let res,_,_parsed_text_len = - eval_statement include_paths buffer guistuff lexicon_status + eval_statement include_paths buffer guistuff grafite_status user_goal script statement in (* we need to replace all the parsed_text *) @@ -486,7 +485,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status in let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [({grafite_status with proof_status = No_proof},lexicon_status), parsed_text ],"", + [({grafite_status with proof_status = No_proof}), parsed_text ],"", parsed_text_length | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in @@ -513,7 +512,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let (_,menv,subst,_,_,_), _ = ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params - ~universe:grafite_status.GrafiteTypes.universe) proof_status + ~automation_cache:grafite_status.GrafiteTypes.automation_cache) + proof_status in let proof_term = let irl = @@ -549,7 +549,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status "matita.paste_unicode_as_tex") ~skip_thm_and_qed:true ~skip_initial_lambdas:how_many_lambdas - 80 GrafiteAst.Declarative "" obj + 80 [] obj else if true then (* use cic2grafite *) @@ -560,7 +560,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status Helm_registry.get_bool "matita.paste_unicode_as_tex" in ApplyTransformation.procedural_txt_of_cic_term - ~map_unicode_to_tex 78 cc proof_term + ~map_unicode_to_tex 78 [] cc proof_term in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length @@ -568,17 +568,17 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status ProofEngineTypes.Fail _ as exn -> raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) - | TA.Inline (_,style,suri,prefix,flavour) -> - let str = + | TA.Inline (_, suri, params) -> + let str = "\n\n" ^ ApplyTransformation.txt_of_inline_macro ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - style ?flavour prefix suri + params suri in [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff -lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt +grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = let module TAPp = GrafiteAstPp in @@ -589,7 +589,7 @@ script ex loc ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; eval_with_engine include_paths - guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt + guistuff grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 @@ -599,10 +599,10 @@ script ex loc None -> [] | Some n -> GrafiteTypes.get_proof_context grafite_status n in let grafite_status,macro = lazy_macro context in - eval_macro include_paths buffer guistuff lexicon_status grafite_status + eval_macro include_paths buffer guistuff grafite_status user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro -and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status +and eval_statement include_paths (buffer : GText.buffer) guistuff grafite_status user_goal script statement = let (lexicon_status,st), unparsed_text = @@ -611,11 +611,13 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let ast = wrap_with_make include_paths - (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status + (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) + (GrafiteTypes.get_estatus grafite_status) in ast, text - | `Ast (st, text) -> (lexicon_status, st), text + | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text in + let grafite_status = GrafiteTypes.set_estatus lexicon_status grafite_status in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in let start, stop = HExtlib.loc_of_floc floc in @@ -628,7 +630,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status match st with | GrafiteParser.LNone loc -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in - [(grafite_status,lexicon_status),parsed_text],"", + [grafite_status,parsed_text],"", parsed_text_length | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in @@ -636,7 +638,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status let s = String.sub unparsed_text parsed_text_length remain_len in let s,text,len = try - eval_statement include_paths buffer guistuff lexicon_status + eval_statement include_paths buffer guistuff grafite_status user_goal script (`Raw s) with HExtlib.Localized (floc, exn) -> @@ -656,7 +658,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in - eval_executable include_paths buffer guistuff lexicon_status + eval_executable include_paths buffer guistuff grafite_status user_goal unparsed_text skipped nonskipped script ex loc let fresh_script_id = @@ -673,11 +675,11 @@ let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses baseuri = let lexicon_status = - CicNotation2.load_notation ~include_paths:[] + CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status) BuildTimeConf.core_notation_script in - let grafite_status = GrafiteSync.init baseuri in - grafite_status,lexicon_status + let grafite_status = GrafiteSync.init lexicon_status baseuri in + grafite_status in let read_include_paths file = try @@ -766,8 +768,7 @@ object (self) (* history can't be empty, the invariant above grant that it contains at * least the init grafite_status *) - method grafite_status = match history with (s,_)::_ -> s | _ -> assert false - method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false + method grafite_status = match history with s::_ -> s | _ -> assert false method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in @@ -775,7 +776,7 @@ object (self) HLog.debug ("evaluating: " ^ first_line s ^ " ..."); let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff self#lexicon_status + eval_statement self#include_paths buffer guistuff self#grafite_status userGoal self (`Raw s) with End_of_file -> raise Margin in @@ -808,13 +809,15 @@ object (self) with Failure _ -> None) | _ -> userGoal <- None - method private _retract offset lexicon_status grafite_status new_statements + method private _retract offset grafite_status new_statements new_history = - let cur_grafite_status,cur_lexicon_status = + let cur_grafite_status = match history with s::_ -> s | [] -> assert false in - LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status; + LexiconSync.time_travel + ~present:(GrafiteTypes.get_estatus cur_grafite_status) + ~past:(GrafiteTypes.get_estatus grafite_status); GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; statements <- new_statements; history <- new_history; @@ -832,7 +835,7 @@ object (self) method retract () = try - let cmp,new_statements,new_history,(grafite_status,lexicon_status) = + let cmp,new_statements,new_history,grafite_status = match statements,history with stat::statements, _::(status::_ as history) -> assert (Glib.Utf8.validate stat); @@ -840,7 +843,7 @@ object (self) | [],[_] -> raise Margin | _,_ -> assert false in - self#_retract cmp lexicon_status grafite_status new_statements + self#_retract cmp grafite_status new_statements new_history; self#notify with @@ -849,9 +852,43 @@ object (self) | exc -> self#notify; raise exc method private getFuture = - buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) - ~stop:buffer#end_iter () + let lock = buffer#get_iter_at_mark (`MARK locked_mark) in + let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in + text + method expandAllVirtuals = + let lock = buffer#get_iter_at_mark (`MARK locked_mark) in + let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in + buffer#delete ~start:lock ~stop:buffer#end_iter; + let text = Pcre.replace ~pat:":=" ~templ:"\\def" text in + let text = Pcre.replace ~pat:"->" ~templ:"\\to" text in + let text = Pcre.replace ~pat:"=>" ~templ:"\\Rightarrow" text in + let text = + Pcre.substitute_substrings + ~subst:(fun str -> + let pristine = Pcre.get_substring str 0 in + let input = + if pristine.[0] = ' ' then + String.sub pristine 1 (String.length pristine -1) + else pristine + in + let input = + if input.[String.length input-1] = ' ' then + String.sub input 0 (String.length input -1) + else input + in + let before, after = + if input = "\\forall" || + input = "\\lambda" || + input = "\\exists" then "","" else " ", " " + in + try + before ^ Glib.Utf8.from_unichar + (snd (Virtuals.symbol_of_virtual input)) ^ after + with Virtuals.Not_a_virtual -> pristine) + ~pat:" ?\\\\[a-zA-Z]+ ?" text + in + buffer#insert ~iter:lock text (** @param rel_offset relative offset from current position of locked_mark *) method private moveMark rel_offset = @@ -883,13 +920,12 @@ object (self) val mutable observers = [] - method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) = + method addObserver (o: GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = - let lexicon_status = self#lexicon_status in let grafite_status = self#grafite_status in - List.iter (fun o -> o lexicon_status grafite_status) observers + List.iter (fun o -> o grafite_status) observers method loadFromString s = buffer#set_text s; @@ -938,17 +974,19 @@ object (self) end method private goto_top = - let grafite_status,lexicon_status = + let grafite_status = let rec last x = function | [] -> x | hd::tl -> last hd tl in - last (self#grafite_status,self#lexicon_status) history + last (self#grafite_status) history in (* FIXME: this is not correct since there is no undo for * library_objects.set_default... *) GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status; - LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status + LexiconSync.time_travel + ~present:(GrafiteTypes.get_estatus self#grafite_status) + ~past:(GrafiteTypes.get_estatus grafite_status) method private reset_buffer = statements <- []; @@ -1029,9 +1067,9 @@ object (self) in let rec back_until_cursor len = (* go backward until locked < cursor *) function - statements, ((grafite_status,lexicon_status)::_ as history) + statements, ((grafite_status)::_ as history) when len <= 0 -> - self#_retract (icmp - len) lexicon_status grafite_status statements + self#_retract (icmp - len) grafite_status statements history | statement::tl1, _::tl2 -> back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2) @@ -1103,7 +1141,8 @@ object (self) | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in try - is_there_only_comments self#lexicon_status self#getFuture + is_there_only_comments + (GrafiteTypes.get_estatus self#grafite_status) self#getFuture with | LexiconEngine.IncludedFileNotCompiled _ | HExtlib.Localized _