X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaScript.ml;h=c35fb9307232975b1b8409005aea93bcc1810562;hb=3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c;hp=34e0408c598f281aa0d6bee4417bc3ad5493e407;hpb=82247d9af61693c803bbc87bc6df2de62f359976;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 34e0408c5..c35fb9307 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,7 +24,7 @@ *) open Printf -open MatitaTypes +open GrafiteTypes module TA = GrafiteAst @@ -108,7 +108,9 @@ 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 + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command ~include_paths:include_ ~do_heavy_checks:true new_status st in let new_aliases = @@ -126,13 +128,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 +163,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 -> + | GrafiteEngine.UnableToInclude what + | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = let target = what in let refresh_cb () = @@ -213,9 +216,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 = MatitaTypes.get_proof_metasenv status in - let context = MatitaTypes.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 +229,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 +249,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 +265,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 +278,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let proof = MatitaTypes.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 +292,26 @@ 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 + ~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 = MatitaTypes.get_proof_metasenv status in - let context = MatitaTypes.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 +352,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 GrafiteMisc.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,7 +368,9 @@ 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 @@ -372,49 +379,18 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script | 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 +400,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 +425,7 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView.source_view) - ~(init: MatitaTypes.status) + ~(init: GrafiteTypes.status) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -494,6 +478,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 +486,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 +517,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,7 +528,7 @@ object (self) *) in let s = match statement with Some s -> s | None -> self#getFuture in - MatitaLog.debug ("evaluating: " ^ first_line 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 = @@ -613,7 +596,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,7 +628,7 @@ 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 = @@ -760,10 +743,10 @@ object (self) | Intermediate _ -> assert false (* method proofStatus = MatitaTypes.get_proof_status self#status *) - method proofMetasenv = MatitaTypes.get_proof_metasenv self#status - method proofContext = MatitaTypes.get_proof_context self#status userGoal - method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal - method stack = MatitaTypes.get_stack 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 +757,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 @@ -788,11 +771,11 @@ object (self) (* 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));