X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=da2c5b2fa168a85080812a7e329004d38f2a2c4d;hb=41be5e85a1103a5b14495bb487995a6a88e79c48;hp=080450416feacdcb27e5b62bdf6c8caf7ca80111;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 080450416..da2c5b2fa 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,7 +24,7 @@ *) open Printf -open MatitaTypes +open GrafiteTypes module TA = GrafiteAst @@ -98,7 +98,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = (* | Incomplete_proof { stack = stack } when not (List.mem user_goal (Continuationals.head_goals stack)) -> let status = - MatitaEngine.eval_ast ~include_paths:include_ + MatitaEngine.eval_ast ~do_heavy_checks:true status (goal_ast user_goal) in let initial_space = if initial_space = "" then "\n" else initial_space @@ -108,8 +108,11 @@ let eval_with_engine guistuff status user_goal parsed_text st = initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *) | _ -> initial_space,status,[] in let new_status = - MatitaEngine.eval_ast - ~include_paths:include_ ~do_heavy_checks:true new_status st + GrafiteEngine.eval_ast + ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_) + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command + ~do_heavy_checks:true new_status st in let new_aliases = match ex with @@ -126,13 +129,14 @@ let eval_with_engine guistuff status user_goal parsed_text st = let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in + let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in List.fold_left ( fun (initial_space,status,acc) (k,((v,_) as value)) -> - let b = - try - let v = UM.strip_xpointer (UM.uri_of_string v) in - List.exists (fun (s,_) -> s = v) new_status.objects - with UM.IllFormedUri _ -> false + let b = + try + UM.buri_of_uri (UM.uri_of_string v) = baseuri + with + UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) in if b then initial_space,status,acc @@ -160,8 +164,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = try eval_with_engine guistuff status user_goal parsed_text st with - | MatitaEngine.UnableToInclude what - | MatitaEngine.IncludedFileNotCompiled what as exc -> + | GrafiteParserMisc.UnableToInclude what + | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = let target = what in let refresh_cb () = @@ -213,9 +217,9 @@ let eval_with_engine guistuff status user_goal parsed_text st = let disambiguate_macro_term term status user_goal = let module MD = MatitaDisambiguator in - let dbd = MatitaDb.instance () in - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status user_goal in + let dbd = LibraryDb.instance () in + let metasenv = GrafiteTypes.get_proof_metasenv status in + let context = GrafiteTypes.get_proof_context status user_goal in let interps = MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term in @@ -226,18 +230,17 @@ let disambiguate_macro_term term status user_goal = let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in - let module MDB = MatitaDb in + let module MDB = LibraryDb in let module CTC = CicTypeChecker in let module CU = CicUniv in (* no idea why ocaml wants this *) - let advance ?statement () = script#advance ?statement () in let parsed_text_length = String.length parsed_text in - let dbd = MatitaDb.instance () in + let dbd = LibraryDb.instance () in match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> let term = disambiguate_macro_term term status user_goal in - let l = MQ.match_term ~dbd term in + let l = Whelp.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." (HExtlib.trim_blanks unparsed_text) @@ -247,12 +250,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate_macro_term term status user_goal in - let l = MQ.instance ~dbd term in + let l = Whelp.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WLocate (loc, s) -> - let l = MQ.locate ~dbd s in + let l = Whelp.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length @@ -263,7 +266,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None | _ -> failwith "Not a MutInd" in - let l = MQ.elim ~dbd uri in + let l = Whelp.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length @@ -276,7 +279,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let proof = MatitaMisc.get_current_proof status in + let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, user_goal in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in @@ -290,22 +293,27 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = TA.Apply (loc, CicNotationPt.Uri (suri, None))), Some (TA.Dot loc)))) in - let new_status = MatitaEngine.eval_ast status ast in + let new_status = + GrafiteEngine.eval_ast + ~baseuri_of_script:(fun _ -> assert false) + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command + status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast in [ new_status , (extra_text, ast) ], parsed_text_length | _ -> - MatitaLog.error + HLog.error "The result of the urichooser should be only 1 uri, not:\n"; List.iter ( - fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n") + fun u -> HLog.error (UriManager.string_of_uri u ^ "\n") ) selected; assert false) | TA.Check (_,term) -> - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status user_goal in + let metasenv = GrafiteTypes.get_proof_metasenv status in + let context = GrafiteTypes.get_proof_context status user_goal in let interps = MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term @@ -346,15 +354,14 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script = let module TAPp = GrafiteAstPp in let module MD = MatitaDisambiguator in - let module ML = MatitacleanLib in - let parsed_text_length = String.length parsed_text in + let module ML = MatitaMisc in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try - (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () | Some u -> - if not (MatitaMisc.is_empty u) then + if not (GrafiteMisc.is_empty u) then match guistuff.ask_confirmation ~title:"Baseuri redefinition" @@ -363,58 +370,29 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script "Do you want to redefine the corresponding "^ "part of the library?") with - | `YES -> MatitacleanLib.clean_baseuris [u] + | `YES -> + let basedir = Helm_registry.get "matita.basedir" in + LibraryClean.clean_baseuris ~basedir [u] | `NO -> () | `CANCEL -> raise MatitaTypes.Cancel); - eval_with_engine - guistuff status user_goal parsed_text (TA.Executable (loc, ex)) + eval_with_engine + guistuff status user_goal parsed_text (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> eval_macro guistuff status user_goal unparsed_text parsed_text script mac -let parse_statement baseoffset parsedlen ?error_tag (buffer: GText.buffer) text -= - try - GrafiteParser.parse_statement (Ulexing.from_utf8_string text) - with CicNotationParser.Parse_error (floc, err) as exn -> - match error_tag with - | None -> raise exn - | Some error_tag -> - let (x, y) = CicNotationPt.loc_of_floc floc in - let x = parsedlen + x in - let y = parsedlen + y in - let x' = baseoffset + x in - let y' = baseoffset + y in - let x_iter = buffer#get_iter (`OFFSET x') in - let y_iter = buffer#get_iter (`OFFSET y') in - buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; - let id = ref None in - id := Some (buffer#connect#changed ~callback:(fun () -> - buffer#remove_tag error_tag ~start:buffer#start_iter - ~stop:buffer#end_iter; - match !id with - | None -> assert false (* a race condition occurred *) - | Some id -> - (new GObj.gobject_ops buffer#as_buffer)#disconnect id)); - let flocb,floce = floc in - let floc = - { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } - in - buffer#place_cursor (buffer#get_iter (`OFFSET x')); - raise (CicNotationParser.Parse_error (floc, err)) - -let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) - guistuff status user_goal script statement +let rec eval_statement (buffer : GText.buffer) guistuff status user_goal + script statement = let st, unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - parse_statement baseoffset parsedlen ~error_tag buffer text, text + GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text | `Ast (st, text) -> st, text in let text_of_loc loc = - let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in + let parsed_text_length = snd (HExtlib.loc_of_floc loc) in let parsed_text = safe_substring unparsed_text 0 parsed_text_length in parsed_text, parsed_text_length in @@ -424,8 +402,16 @@ let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in let s,len = - eval_statement baseoffset (parsedlen + parsed_text_length) error_tag - buffer guistuff status user_goal script (`Raw s) + try + eval_statement buffer guistuff status user_goal script + (`Raw s) + with + HExtlib.Localized (floc, exn) -> + HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn + | MatitaDisambiguator.DisambiguationError (offset,errorll) -> + raise + (MatitaDisambiguator.DisambiguationError + (offset+parsed_text_length, errorll)) in (match s with | (status, (text, ast)) :: tl -> @@ -441,7 +427,6 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView.source_view) - ~(init: MatitaTypes.status) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -477,7 +462,7 @@ object (self) (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified)) val mutable statements = []; (** executed statements *) - val mutable history = [ init ]; + val mutable history = [ MatitaSync.init () ]; (** 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. @@ -494,6 +479,7 @@ object (self) method locked_mark = locked_mark method locked_tag = locked_tag + method error_tag = error_tag (* history can't be empty, the invariant above grant that it contains at * least the init status *) @@ -501,10 +487,8 @@ object (self) method private _advance ?statement () = let rec aux st = - let baseoffset = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in let (entries, parsed_len) = - eval_statement baseoffset 0 error_tag buffer guistuff self#status - userGoal self st + eval_statement buffer guistuff self#status userGoal self st in let (new_statuses, new_statements, new_asts) = let statuses, statements = List.split entries in @@ -534,7 +518,7 @@ object (self) in let text = self#getFuture in (try - (match parse_statement baseoffset 0 ?error_tag:None buffer text with + (match parse_statement baseoffset 0 buffer text with | TA.Executable (loc, TA.Tactical (_, tac, None)) as st when GrafiteAst.is_punctuation tac -> let len = snd (CicNotationPt.loc_of_floc loc) in @@ -545,8 +529,8 @@ object (self) *) in let s = match statement with Some s -> s | None -> self#getFuture in - MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); - aux (`Raw s) + HLog.debug ("evaluating: " ^ first_line s ^ " ..."); + (try aux (`Raw s) with End_of_file -> raise Margin) method private _retract offset status new_statements new_history = let cur_status = match history with s::_ -> s | [] -> assert false in @@ -613,7 +597,7 @@ object (self) val mutable observers = [] - method addObserver (o: MatitaTypes.status -> unit) = + method addObserver (o: GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = @@ -645,15 +629,24 @@ object (self) output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; - MatitaLog.debug ("backup " ^ f ^ " saved") + HLog.debug ("backup " ^ f ^ " saved") end method private goto_top = + let init = + let rec last x = function + | [] -> x + | hd::tl -> last hd tl + in + last self#status history + in + (* FIXME: this is not correct since there is no undo for + * library_objects.set_default... *) MatitaSync.time_travel ~present:self#status ~past:init method private reset_buffer = statements <- []; - history <- [ init ]; + history <- [ MatitaSync.init () ]; userGoal <- ~-1; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -664,7 +657,7 @@ object (self) source_buffer#begin_not_undoable_action (); buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; source_buffer#end_not_undoable_action (); - buffer#set_modified false + buffer#set_modified false; method template () = let template = HExtlib.input_file BuildTimeConf.script_template in @@ -759,11 +752,11 @@ object (self) | Incomplete_proof _ -> true | Intermediate _ -> assert false -(* method proofStatus = MatitaMisc.get_proof_status self#status *) - method proofMetasenv = MatitaMisc.get_proof_metasenv self#status - method proofContext = MatitaMisc.get_proof_context self#status userGoal - method proofConclusion = MatitaMisc.get_proof_conclusion self#status userGoal - method stack = MatitaMisc.get_stack self#status +(* method proofStatus = MatitaTypes.get_proof_status self#status *) + method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status + method proofContext = GrafiteTypes.get_proof_context self#status userGoal + method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal + method stack = GrafiteTypes.get_stack self#status method setGoal n = userGoal <- n method goal = userGoal @@ -774,7 +767,7 @@ object (self) let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in match st with | GrafiteAst.Comment (loc,_)-> - let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in + let parsed_text_length = snd (HExtlib.loc_of_floc loc) in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_and_executable next @@ -784,17 +777,15 @@ object (self) is_there_and_executable s with | CicNotationParser.Parse_error _ -> false - | Margin -> true - - - + | Margin | End_of_file -> true + (* debug *) method dump () = - MatitaLog.debug "script status:"; - MatitaLog.debug ("history size: " ^ string_of_int (List.length history)); - MatitaLog.debug (sprintf "%d statements:" (List.length statements)); - List.iter MatitaLog.debug statements; - MatitaLog.debug ("Current file name: " ^ + HLog.debug "script status:"; + HLog.debug ("history size: " ^ string_of_int (List.length history)); + HLog.debug (sprintf "%d statements:" (List.length statements)); + List.iter HLog.debug statements; + HLog.debug ("Current file name: " ^ (match guistuff.filenamedata with |None,_ -> "[ no name ]" | Some f,_ -> f)); @@ -803,10 +794,10 @@ end let _script = ref None -let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star () +let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star () = let s = new script - ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () + ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () in _script := Some s; s