From: Claudio Sacerdoti Coen Date: Tue, 3 Oct 2006 15:59:34 +0000 (+0000) Subject: Inline command implemented. X-Git-Tag: 0.4.95@7852~934 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afea2be14c1c197e0804e8607fc6dcc49ce46955;p=helm.git Inline command implemented. --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index c7d644e60..6ab2b2fc6 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -114,6 +114,7 @@ type 'term macro = (* real macros *) | Check of loc * 'term | Hint of loc + | Inline of loc * string (* the string is a URI or a base-uri *) (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 569b68399..547e28b3d 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -198,8 +198,9 @@ let pp_macro ~term_pp = | WElim (_, t) -> "whelp elim " ^ term_pp t | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) - | Check (_, term) -> sprintf "Check %s" (term_pp term) + | Check (_, term) -> sprintf "check %s" (term_pp term) | Hint _ -> "hint" + | Inline (_,suri) -> sprintf "inline %s" suri let pp_associativity = function | Gramext.LeftA -> "left associative" diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 4baac499f..134a16895 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -415,5 +415,6 @@ let disambiguate_macro let metasenv,term = disambiguate_term context metasenv term in metasenv,GrafiteAst.Check (loc,term) | GrafiteAst.Hint _ - | GrafiteAst.WLocate _ as macro -> + | GrafiteAst.WLocate _ + | GrafiteAst.Inline _ as macro -> metasenv,macro diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 19f9e359e..5c7d31223 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -263,7 +263,7 @@ EXTEND (floc,CicNotationParser.Parse_error "tactic_term expected here")) | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2))) - | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> GrafiteAst.We_need_to_prove (loc, t, id, t1) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> GrafiteAst.We_proceed_by_induction_on (loc, t, t1) @@ -281,14 +281,14 @@ EXTEND ] ]; by_continuation: [ - [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1) + [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1) + | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; + IDENT "done" -> BYC_weproved (ty,None,t1) | IDENT "done" -> BYC_done | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; - IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; - RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) - | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ; - "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> - BYC_wehaveand (id1,t1,id2,t2) + IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) + | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> + BYC_wehaveand (id1,t1,id2,t2) ] ]; rewriting_step_continuation : [ @@ -405,6 +405,8 @@ EXTEND macro: [ [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) + | [ IDENT "inline"]; suri = QSTRING -> + GrafiteAst.Inline (loc,suri) | [ IDENT "hint" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) diff --git a/matita/matita.lang b/matita/matita.lang index 2258e1229..c41cc5fdc 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -171,6 +171,7 @@ + inline check hint set diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 718ea7a23..23de391c6 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -103,7 +103,7 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in - res,parsed_text_length + res,"",parsed_text_length let wrap_with_developments guistuff f arg = let compile_needed_and_go_on lexiconfile d exc = @@ -212,17 +212,17 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let l = Whelp.match_term ~dbd term in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + [], "", parsed_text_length | TA.WInstance (loc, term) -> let l = Whelp.instance ~dbd term in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + [], "", parsed_text_length | TA.WLocate (loc, s) -> let l = Whelp.locate ~dbd s in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + [], "", parsed_text_length | TA.WElim (loc, term) -> let uri = match term with @@ -232,13 +232,13 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let l = Whelp.elim ~dbd uri in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + [], "", parsed_text_length | TA.WHint (loc, term) -> let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + [], "", parsed_text_length (* REAL macro *) | TA.Hint loc -> let user_goal' = @@ -251,7 +251,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in (match selected with - | [] -> [], parsed_text_length + | [] -> [], "", parsed_text_length | [uri] -> let suri = UriManager.string_of_uri uri in let ast loc = @@ -265,12 +265,12 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let text_len = MatitaGtkMisc.utf8_string_length text in let loc = HExtlib.floc_of_loc (0,text_len) in let statement = `Ast (GrafiteParser.LSome (ast loc),text) in - let res,_parsed_text_len = + let res,_,_parsed_text_len = eval_statement include_paths buffer guistuff lexicon_status grafite_status user_goal script statement in (* we need to replace all the parsed_text *) - res,String.length parsed_text + res,"",String.length parsed_text | _ -> HLog.error "The result of the urichooser should be only 1 uri, not:\n"; @@ -287,7 +287,54 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [], parsed_text_length + [], "", parsed_text_length + | TA.Inline (_,suri) -> + let dbd = LibraryDb.instance () in + let uris = + let sql_pat = + (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in + let query = + sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ + "SELECT source FROM %s WHERE source LIKE \"%s\"") + (MetadataTypes.name_tbl ()) sql_pat + MetadataTypes.library_name_tbl sql_pat in + let result = HMysql.exec dbd query in + HMysql.map result + (function cols -> + match cols.(0) with + Some s -> UriManager.uri_of_string s + | _ -> assert false) + in +prerr_endline "Inizio sorting"; + let sorted_uris = MetadataDeps.topological_sort ~dbd uris in +prerr_endline "Fine sorting"; + let sorted_uris_without_xpointer = + HExtlib.filter_map + (function uri -> + let s = + Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" + (UriManager.string_of_uri uri) in + try + ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); + None + with + Not_found -> + Some (UriManager.uri_of_string s) + ) sorted_uris + in + let declarative = + String.concat "\n\n" + (List.map + (fun uri -> +prerr_endline ("Stampo " ^ UriManager.string_of_uri uri); + try + ObjPp.obj_to_string 80 + (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) + with + _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri + ) sorted_uris_without_xpointer) + in + [],declarative,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 @@ -320,7 +367,7 @@ script ex loc guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with - MatitaTypes.Cancel -> [], 0 + MatitaTypes.Cancel -> [], "", 0 | GrafiteEngine.Macro (_loc,lazy_macro) -> let context = match user_goal with @@ -357,13 +404,13 @@ 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,lexicon_status),parsed_text],"", parsed_text_length | 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 let s = String.sub unparsed_text parsed_text_length remain_len in - let s,len = + let s,text,len = try eval_statement include_paths buffer guistuff lexicon_status grafite_status user_goal script (`Raw s) @@ -376,10 +423,11 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status (GrafiteDisambiguator.DisambiguationError (offset+parsed_text_length, errorll)) in + assert (text=""); (* no macros inside comments, please! *) (match s with | (statuses,text)::tl -> - (statuses,parsed_text ^ text)::tl,parsed_text_length + len - | [] -> [], 0) + (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 @@ -468,7 +516,7 @@ object (self) method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in HLog.debug ("evaluating: " ^ first_line s ^ " ..."); - let (entries, parsed_len) = + let entries, newtext, parsed_len = try eval_statement include_paths buffer guistuff self#lexicon_status self#grafite_status userGoal self (`Raw s) @@ -492,7 +540,8 @@ object (self) buffer#insert ~iter:start new_text; end; end; - self#moveMark (Glib.Utf8.length new_text); + self#moveMark (Glib.Utf8.length new_text); + buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext; (* here we need to set the Goal in case we are going to cursor (or to bottom) and we will face a macro *) match self#grafite_status.proof_status with