X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=4738a38f673dd55bd6b6496358b655194007a32f;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=108b23237d74e9db01195ffb456a73bbba80b1df;hpb=290350836dd1727b3e3cdd4ee71e666a39cc4a09;p=helm.git diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 108b23237..4738a38f6 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -74,8 +74,6 @@ type guistuff = { 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 parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in @@ -212,7 +210,7 @@ let cic2grafite context menv t = | Cic.Const _ as t -> PT.Ident (pp_t c t, None) | Cic.Appl l -> PT.Appl (List.map (aux c) l) - | Cic.Implicit _ -> PT.Implicit + | Cic.Implicit _ -> PT.Implicit `JustOne | Cic.Lambda (Cic.Name n, s, t) -> PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), aux (Some (Cic.Name n, Cic.Decl s)::c) t) @@ -222,7 +220,7 @@ let cic2grafite context menv t = | Cic.LetIn (Cic.Name n, s, ty, t) -> PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t) - | Cic.Meta _ -> PT.Implicit + | Cic.Meta _ -> PT.Implicit `JustOne | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u) | Cic.Sort Cic.Set -> PT.Sort `Set | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u) @@ -367,17 +365,75 @@ let cic2grafite context menv t = prerr_endline script; stupid_indenter script ;; +let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = + let parsed_text_length = String.length parsed_text in + match mac with + | TA.Screenshot (_,name) -> + let status = script#grafite_status in + let _,_,menv,subst,_ = status#obj in + let name = Filename.dirname (script#filename) ^ "/" ^ name in + let sequents = + let selected = Continuationals.Stack.head_goals status#stack in + List.filter (fun x,_ -> List.mem x selected) menv + in + guistuff.mathviewer#screenshot status sequents menv subst name; + [status, parsed_text], "", parsed_text_length + | TA.NCheck (_,t) -> + let status = script#grafite_status in + let _,_,menv,subst,_ = status#obj in + let ctx = + try let _,(_,ctx,_) = List.hd menv in ctx + with Failure "hd" -> [] + in + let m, s, status, t = + GrafiteDisambiguate.disambiguate_nterm + None status ctx menv subst (parsed_text,parsed_text_length, + CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne)) + (* XXX use the metasenv, if possible *) + in + guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); + [status, parsed_text], "", parsed_text_length + | TA.NIntroGuess _loc -> + let names_ref = ref [] in + let s = + NTactics.intros_tac ~names_ref [] script#grafite_status + in + let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in + let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in + [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length + | TA.NAutoInteractive (_loc, (None,a)) -> + let trace_ref = ref [] in + let s = + NnAuto.auto_tac + ~params:(None,a) ~trace_ref script#grafite_status + in + let depth = + try List.assoc "depth" a + with Not_found -> "" + in + let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in + let thms = + match !trace_ref with + | [] -> "{}" + | thms -> + String.concat ", " + (HExtlib.filter_map (function + | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) + | _ -> None) + thms) + in + let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in + let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in + [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length + | TA.NAutoInteractive (_, (Some _,_)) -> assert false 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 let module CTC = CicTypeChecker in - let module CU = CicUniv in (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in let dbd = LibraryDb.instance () in - let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in + let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> @@ -536,13 +592,13 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status in let ty,_ = CicTypeChecker.type_of_aux' - menv [] proof_term CicUniv.empty_ugraph + [] [] proof_term CicUniv.empty_ugraph in - prerr_endline (CicPp.ppterm proof_term); + prerr_endline (CicPp.ppterm proof_term ^ " n lambda= " ^ string_of_int how_many_lambdas); (* use declarative output *) let obj = (* il proof_term vive in cc, devo metterci i lambda no? *) - (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[])) + (Cic.CurrentProof ("xxx",[],proof_term,ty,[],[])) in ApplyTransformation.txt_of_cic_object ~map_unicode_to_tex:(Helm_registry.get_bool @@ -581,9 +637,6 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = - let module TAPp = GrafiteAstPp in - let module MD = MultiPassDisambiguator in - let module ML = MatitaMisc in try ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars @@ -601,23 +654,26 @@ script ex loc let grafite_status,macro = lazy_macro context in eval_macro include_paths buffer guistuff grafite_status user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro + | GrafiteEngine.NMacro (_loc,macro) -> + eval_nmacro 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 grafite_status user_goal script statement = - let (lexicon_status,st), unparsed_text = + let (grafite_status,st), unparsed_text = match statement with | `Raw text -> 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)) - (GrafiteTypes.get_estatus grafite_status) + grafite_status in ast, text - | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text + | `Ast (st, text) -> (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 @@ -632,6 +688,15 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff let parsed_text, _, _, parsed_text_length = text_of_loc loc in [grafite_status,parsed_text],"", parsed_text_length + | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> + let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer guistuff + grafite_status user_goal unparsed_text skipped nonskipped script ex loc + | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) + when Helm_registry.get_bool "matita.execcomments" -> + let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer guistuff + grafite_status user_goal unparsed_text skipped nonskipped script ex loc | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in @@ -654,18 +719,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff | (statuses,text)::tl -> (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len | [] -> [], "", 0) - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> - let _, nonskipped, skipped, parsed_text_length = - text_of_loc loc - in - eval_executable include_paths buffer guistuff - grafite_status user_goal unparsed_text skipped nonskipped script ex loc let fresh_script_id = let i = ref 0 in fun () -> incr i; !i -class script ~(source_view: GSourceView.source_view) +class script ~(source_view: GSourceView2.source_view) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -673,9 +732,17 @@ class script ~(source_view: GSourceView.source_view) () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in -let initial_statuses baseuri = +let initial_statuses current baseuri = + let empty_lstatus = new LexiconEngine.status in + (match current with + Some current -> + LexiconSync.time_travel ~present:current ~past:empty_lstatus; + GrafiteSync.time_travel ~present:current (); + (* CSC: there is a known bug in invalidation; temporary fix here *) + NCicEnvironment.invalidate () + | None -> ()); let lexicon_status = - CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status) + CicNotation2.load_notation ~include_paths:[] empty_lstatus BuildTimeConf.core_notation_script in let grafite_status = GrafiteSync.init lexicon_status baseuri in @@ -744,7 +811,7 @@ object (self) val mutable statements = [] (** executed statements *) - val mutable history = [ initial_statuses default_buri ] + val mutable history = [ initial_statuses None default_buri ] (** list of states before having executed statements. Head element of this * list is the current state, last element is the state at the beginning of * the script. @@ -774,12 +841,15 @@ object (self) let s = match statement with Some s -> s | None -> self#getFuture in if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file]; HLog.debug ("evaluating: " ^ first_line s ^ " ..."); + let time1 = Unix.gettimeofday () in let entries, newtext, parsed_len = try eval_statement self#include_paths buffer guistuff self#grafite_status userGoal self (`Raw s) with End_of_file -> raise Margin in + let time2 = Unix.gettimeofday () in + HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s"); let new_statuses, new_statements = let statuses, texts = List.split entries in statuses, texts @@ -815,10 +885,8 @@ object (self) let cur_grafite_status = match history with s::_ -> s | [] -> assert false in - 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; + LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status; + GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status (); statements <- new_statements; history <- new_history; self#moveMark (- offset) @@ -943,7 +1011,6 @@ object (self) | Some f -> Some (Librarian.absolutize f) | None -> None in - self#goto_top; filename_ <- file; include_paths_ <- (match file with Some file -> read_include_paths file | None -> []); @@ -973,24 +1040,9 @@ object (self) HLog.debug ("backup " ^ f ^ " saved") end - method private goto_top = - let grafite_status = - let rec last x = function - | [] -> x - | hd::tl -> last hd tl - in - 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:(GrafiteTypes.get_estatus self#grafite_status) - ~past:(GrafiteTypes.get_estatus grafite_status) - method private reset_buffer = statements <- []; - history <- [ initial_statuses self#buri_of_current_file ]; + history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ]; userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -1021,7 +1073,6 @@ object (self) match pos with | `Top -> dispose_old_locked_mark (); - self#goto_top; self#reset_buffer; self#notify | `Bottom -> @@ -1140,9 +1191,7 @@ object (self) | GrafiteParser.LNone _ | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in - try - is_there_only_comments - (GrafiteTypes.get_estatus self#grafite_status) self#getFuture + try is_there_only_comments self#grafite_status self#getFuture with | LexiconEngine.IncludedFileNotCompiled _ | HExtlib.Localized _