X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=864583d888149d1dd922e24c90e5f7f38f51ea6f;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=9fa039b311add2643ac4c3acde8d9d7bd1886a15;hpb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 9fa039b31..864583d88 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -67,7 +67,7 @@ let first_line s = type guistuff = { mathviewer:MatitaTypes.mathViewer; - urichooser: UriManager.uri list -> UriManager.uri list; + urichooser: NReference.reference list -> NReference.reference list; ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } @@ -80,7 +80,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal let text = skipped_txt ^ nonskipped_txt in let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in let enriched_history_fragment = - MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") grafite_status (text,prefix_len,st) in @@ -92,7 +92,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" | Some (k,value) -> - let newtxt = LexiconAstPp.pp_alias value in + let newtxt = GrafiteAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in @@ -103,11 +103,10 @@ let eval_with_engine include_paths guistuff grafite_status user_goal * 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 : #LexiconEngine.status GrafiteParser.statement) x = - try - f ~never_include:true ~include_paths x - with - | GrafiteParser.NoInclusionPerformed mafilename -> +let wrap_with_make include_paths f x = + match f x with + GrafiteParser.LSome (GrafiteAst.Executable (_,GrafiteAst.NCommand + (_,GrafiteAst.Include (_,_,mafilename)))) as cmd -> let root, buri, _, tgt = try Librarian.baseuri_of_script ~include_paths mafilename with Librarian.NoRootFor _ -> @@ -115,18 +114,13 @@ let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statem HLog.error "please create it."; raise (Failure ("No root file for "^mafilename)) in - let b = MatitacLib.Make.make root [tgt] in - if b then - try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ -> - raise - (Failure ("Including: "^tgt^ - "\nNothing to do... did you run matitadep?")) + if MatitacLib.Make.make root [tgt] then + cmd else raise (Failure ("Compiling: " ^ tgt)) + | cmd -> cmd ;; -let pp_eager_statement_ast = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) +let pp_eager_statement_ast = GrafiteAstPp.pp_statement 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 @@ -151,7 +145,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm None status ctx menv subst (parsed_text,parsed_text_length, - CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne)) + NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); @@ -181,7 +175,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us | thms -> String.concat ", " (HExtlib.filter_map (function - | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) + | NotationPt.NRef r -> Some (NCicPp.r2s true r) | _ -> None) thms) in @@ -190,50 +184,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us [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 CTC = CicTypeChecker in - (* no idea why ocaml wants this *) - let parsed_text_length = String.length parsed_text in - let dbd = LibraryDb.instance () in - match mac with - (* REAL macro *) - | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false - | TA.Eval (_, kind, term) -> assert false (* MATITA 1.0 - let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - let context = - match user_goal with - None -> [] - | Some n -> GrafiteTypes.get_proof_context grafite_status n in - let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let term = - match kind with - | `Normalize -> - CicReduction.normalize ~delta:true ~subst:[] context term - | `Simpl -> - ProofEngineReduction.simpl context term - | `Unfold None -> - ProofEngineReduction.unfold ?what:None context term - | `Unfold (Some lazy_term) -> - let what, _, _ = - lazy_term context metasenv CicUniv.empty_ugraph in - ProofEngineReduction.unfold ~what context term - | `Whd -> - CicReduction.whd ~delta:true ~subst:[] context term - in - let t_and_ty = Cic.Cast (term,ty) in - guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [(grafite_status#set_proof_status No_proof), parsed_text ],"", - parsed_text_length *) - | 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") - params suri - in - [], str, String.length parsed_text - -and eval_executable include_paths (buffer : GText.buffer) guistuff +let rec eval_executable include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = @@ -246,11 +197,6 @@ script ex loc (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 - | GrafiteEngine.Macro (_loc,lazy_macro) -> - let context = [] in - 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 @@ -259,17 +205,17 @@ script ex loc and eval_statement include_paths (buffer : GText.buffer) guistuff grafite_status user_goal script statement = - let (grafite_status,st), unparsed_text = + let 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)) - grafite_status + (GrafiteParser.parse_statement grafite_status) + (Ulexing.from_utf8_string text) in ast, text - | `Ast (st, text) -> (grafite_status, st), text + | `Ast (st, text) -> st, text in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in @@ -330,11 +276,11 @@ class script ~(source_view: GSourceView2.source_view) let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses current baseuri = - let empty_lstatus = new LexiconEngine.status in + let empty_lstatus = new LexiconTypes.status in (match current with Some current -> - LexiconSync.time_travel ~present:current ~past:empty_lstatus; - GrafiteSync.time_travel ~present:current (); + NCicLibrary.time_travel + ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus); (* CSC: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () | None -> ()); @@ -342,7 +288,7 @@ let initial_statuses current baseuri = CicNotation2.load_notation ~include_paths:[] empty_lstatus BuildTimeConf.core_notation_script in - let grafite_status = GrafiteSync.init lexicon_status baseuri in + let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in grafite_status in let read_include_paths file = @@ -471,14 +417,8 @@ object (self) bottom) and we will face a macro *) userGoal <- None - method private _retract offset grafite_status new_statements - new_history - = - let cur_grafite_status = - match history with s::_ -> s | [] -> assert false - in - LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status; - GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status (); + method private _retract offset grafite_status new_statements new_history = + NCicLibrary.time_travel grafite_status; statements <- new_statements; history <- new_history; self#moveMark (- offset) @@ -749,11 +689,9 @@ object (self) method eos = let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let lexicon_status,st = - GrafiteParser.parse_statement (Ulexing.from_utf8_string s) - ~include_paths:self#include_paths lexicon_status - in - match st with + match + GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s) + with | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) @@ -766,7 +704,7 @@ object (self) in try is_there_only_comments self#grafite_status self#getFuture with - | LexiconEngine.IncludedFileNotCompiled _ + | NCicLibrary.IncludedFileNotCompiled _ | HExtlib.Localized _ | CicNotationParser.Parse_error _ -> false | Margin | End_of_file -> true