| IPCR (* detect convertible rewriting *)
type ('term,'lazy_term) macro =
- (* Whelp's stuff *)
- | WHint of loc * 'term
- | WMatch of loc * 'term
- | WInstance of loc * 'term
- | WLocate of loc * string
- | WElim of loc * 'term
(* real macros *)
| Eval of loc * 'lazy_term reduction * 'term
| Check of loc * 'term
in
let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
function
- (* Whelp *)
- | WInstance (_, term) -> "whelp instance " ^ term_pp term
- | WHint (_, t) -> "whelp hint " ^ term_pp t
- | WLocate (_, s) -> "whelp locate \"" ^ s ^ "\""
- | WElim (_, t) -> "whelp elim " ^ term_pp t
- | WMatch (_, term) -> "whelp match " ^ term_pp term
(* real macros *)
| Eval (_, kind, term) ->
Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term)
let disambiguate_reduction_kind =
disambiguate_reduction_kind text prefix_len lexicon_status_ref in
match macro with
- | GrafiteAst.WMatch (loc,term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.WMatch (loc,term)
- | GrafiteAst.WInstance (loc,term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.WInstance (loc,term)
- | GrafiteAst.WElim (loc,term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.WElim (loc,term)
- | GrafiteAst.WHint (loc,term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.WHint (loc,term)
| GrafiteAst.Check (loc,term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Check (loc,term)
disambiguate_auto_params disambiguate_term metasenv context params in
metasenv, GrafiteAst.AutoInteractive (loc, params)
| GrafiteAst.Hint _
- | GrafiteAst.WLocate _
| GrafiteAst.Inline _ as macro ->
metasenv,macro
if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
| IDENT "auto"; params = auto_params ->
G.AutoInteractive (loc,params)
- | [ IDENT "whelp"; "match" ] ; t = term ->
- G.WMatch (loc,t)
- | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
- G.WInstance (loc,t)
- | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
- G.WLocate (loc,id)
- | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
- G.WElim (loc, t)
- | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
- G.WHint (loc,t)
]
];
alias_spec: [
<property name="use_underline">True</property>
<child>
<widget class="GtkMenu" id="BrowserViewMenu_menu">
- <child>
- <widget class="GtkMenuItem" id="DepGraphMenuItem">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">View the graph of objects on which the current one depends on</property>
- <property name="label" translatable="yes">(Direct) Dependencies</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
- <child>
- <widget class="GtkMenuItem" id="InvDepGraphMenuItem">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">View the graph of objects which depends on the current one</property>
- <property name="label" translatable="yes">(Inverse) Dependencies</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
<child>
<widget class="GtkMenuItem" id="univMenuItem">
<property name="visible">True</property>
<property name="position">1</property>
</packing>
</child>
- <child>
- <widget class="GtkHBox" id="whelpBarBox">
- <property name="visible">True</property>
- <property name="border_width">3</property>
- <property name="spacing">6</property>
- <child>
- <widget class="GtkImage" id="WhelpBarImage">
- <property name="visible">True</property>
- <property name="stock">gtk-missing-image</property>
- </widget>
- <packing>
- <property name="expand">False</property>
- </packing>
- </child>
- <child>
- <widget class="GtkEntry" id="queryInputText">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="invisible_char">*</property>
- </widget>
- <packing>
- <property name="position">1</property>
- </packing>
- </child>
- <child>
- <widget class="GtkVBox" id="whelpBarComboVbox">
- <property name="visible">True</property>
- <child>
- <widget class="GtkAlignment" id="alignment4">
- <property name="visible">True</property>
- <child>
- <placeholder/>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="position">2</property>
- </packing>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="position">2</property>
- </packing>
- </child>
<child>
<widget class="GtkNotebook" id="mathOrListNotebook">
<property name="visible">True</property>
class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
()
=
- let whelp_RE = Pcre.regexp "^\\s*whelp" in
let uri_RE =
Pcre.regexp
"^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
in
let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
- let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in
- let whelp_query_RE = Pcre.regexp
- "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$"
- in
- let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in
- let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
let gui = get_gui () in
let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
- let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
- let combo,_ = GEdit.combo_box_text ~strings:queries () in
- let activate_combo_query input q =
- let q' = String.lowercase q in
- let rec aux i = function
- | [] -> failwith ("Whelp query '" ^ q ^ "' not found")
- | h::_ when String.lowercase h = q' -> i
- | _::tl -> aux (i+1) tl
- in
- win#queryInputText#set_text input;
- combo#set_active (aux 0 queries);
- in
let searchText =
GSourceView2.source_view ~auto_indent:false ~editable:false ()
in
ignore(win#entrySearch#connect#activate ~callback);
ignore(win#buttonSearch#connect#clicked ~callback);
in
- let set_whelp_query txt =
- let query, arg =
- try
- let q = Pcre.extract ~rex:whelp_query_RE txt in
- q.(1), q.(3)
- with Not_found -> failwith "Malformed Whelp query"
- in
- activate_combo_query arg query;
- in
let toplevel = win#toplevel in
let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
let fail message =
val dep_contextual_menu = GMenu.menu ()
initializer
- activate_combo_query "" "locate";
- win#whelpBarComboVbox#add combo#coerce;
- let start_query () =
- let query =
- try
- String.lowercase (List.nth queries combo#active)
- with Not_found -> assert false in
- let input = win#queryInputText#text in
- let statement =
- if query = "locate" then
- "whelp " ^ query ^ " \"" ^ input ^ "\"."
- else
- "whelp " ^ query ^ " (" ^ input ^ ")."
- in
- (MatitaScript.current ())#advance ~statement ()
- in
- ignore(win#queryInputText#connect#activate ~callback:start_query);
- ignore(combo#connect#changed ~callback:start_query);
- win#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png");
win#mathOrListNotebook#set_show_tabs false;
win#browserForwardButton#misc#set_sensitive false;
win#browserBackButton#misc#set_sensitive false;
| button when button = right_button ->
dep_contextual_menu#popup ~button ~time
| _ -> ());
- connect_menu_item win#depGraphMenuItem (fun () ->
- match self#currentCicUri with
- | Some uri -> self#load (`Metadata (`Deps (`Fwd, uri)))
- | None -> ());
- connect_menu_item win#invDepGraphMenuItem (fun () ->
- match self#currentCicUri with
- | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
- | None -> ());
connect_menu_item win#browserCloseMenuItem (fun () ->
let my_id = Oo.id self in
cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
(** @return None if no object uri can be built from the current entry *)
method private currentCicUri =
match current_entry with
- | `Uri uri
- | `Metadata (`Deps (_, uri)) -> Some uri
+ | `Uri uri -> Some uri
| _ -> None
val model =
self#_loadTermNCic term metasenv subst ctx
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
- | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
- self#dependencies dir uri ()
| `Uri uri -> self#_loadUriManagerUri uri
| `NRef nref -> self#_loadNReference nref
- | `Univs uri -> self#_loadUnivs uri
- | `Whelp (query, results) ->
- set_whelp_query query;
- self#_loadList (List.map (fun r -> "obj",
- UriManager.string_of_uri r) results));
+ | `Univs uri -> self#_loadUnivs uri);
self#setEntry entry
end)
(** this is what the browser does when you enter a string an hit enter *)
method loadInput txt =
- let parse_metadata s =
- let subs = Pcre.extract ~rex:metadata_RE s in
- let uri = UriManager.uri_of_string ("cic:/" ^ subs.(3)) in
- match subs.(1), subs.(2) with
- | "deps", "forward" -> `Deps (`Fwd, uri)
- | "deps", "backward" -> `Deps (`Back, uri)
- | _ -> assert false
- in
let txt = HExtlib.trim_blanks txt in
(* (* ZACK: what the heck? *)
let fix_uri txt =
(UriManager.strip_xpointer (UriManager.uri_of_string txt))
in
*)
- if is_whelp txt then begin
- set_whelp_query txt;
- (MatitaScript.current ())#advance ~statement:(txt ^ ".") ()
- end else begin
let entry =
match txt with
| txt when is_uri txt ->
`Uri (UriManager.uri_of_string ((*fix_uri*) txt))
| txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
- | txt when is_metadata txt -> `Metadata (parse_metadata txt)
- | "hbugs:/tutors/" -> `HBugs `Tutors
| txt ->
(try
MatitaTypes.entry_of_string txt
in
self#_load entry;
self#_historyAdd entry
- end
(** {2 methods accessing underlying GtkMathView} *)
(* 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
match mac with
- (* WHELP's stuff *)
- | TA.WMatch (loc, term) ->
- 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
- | 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
- | 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
- | TA.WElim (loc, term) ->
- let uri =
- match term with
- | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
- | _ -> failwith "Not a MutInd"
- in
- 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
- | TA.WHint (loc, term) ->
- let _subst = [] in
- let s = ((None,[0,[],term], _subst, lazy (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
(* REAL macro *)
- | TA.Hint (loc, rewrite) ->
- let user_goal' =
- match user_goal with
- Some n -> n
- | None -> raise NoUnfinishedProof
- in
- let proof = GrafiteTypes.get_current_proof grafite_status in
- let proof_status = proof,user_goal' in
- if rewrite then
- let l = MQ.equations_for_goal ~dbd proof_status in
- let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in
- let entry =
- `Whelp (pp_macro [] [] (TA.WHint(loc, Cic.Implicit None)), l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- else
- let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
- let selected = guistuff.urichooser l in
- (match selected with
- | [] -> [], "", parsed_text_length
- | [uri] ->
- let suri = UriManager.string_of_uri uri in
- let ast loc =
- TA.Executable (loc, (TA.Tactic (loc,
- Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
- TA.Dot loc))) in
- let text =
- comment parsed_text ^ "\n" ^
- pp_eager_statement_ast (ast HExtlib.dummy_floc)
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- in
- 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 =
- eval_statement include_paths buffer guistuff
- grafite_status user_goal script statement
- in
- (* we need to replace all the parsed_text *)
- res,"",String.length parsed_text
- | _ ->
- HLog.error
- "The result of the urichooser should be only 1 uri, not:\n";
- List.iter (
- fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
- ) selected;
- assert false)
+ | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false
| TA.Eval (_, kind, term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
let context =
| `Cic of Cic.term * Cic.metasenv
| `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
| `Dir of string (* "directory" in cic uris namespace *)
- | `HBugs of [ `Tutors ] (* list of available HBugs tutors *)
- | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
| `Uri of UriManager.uri (* cic object uri *)
| `NRef of NReference.reference (* cic object uri *)
- | `Whelp of string * UriManager.uri list (* query and results *)
| `Univs of UriManager.uri
]
| `Cic (_, _) -> "term:"
| `NCic (_, _, _, _) -> "nterm:"
| `Dir uri -> uri
- | `HBugs `Tutors -> "hbugs:/tutors/"
- | `Metadata meta ->
- "metadata:/" ^
- (match meta with
- | `Deps (dir, uri) ->
- "deps/" ^
- let suri =
- let suri = UriManager.string_of_uri uri in
- let len = String.length suri in
- String.sub suri 4 (len - 4) in (* strip "cic:" prefix *)
- (match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri)
| `Uri uri -> UriManager.string_of_uri uri
| `NRef nref -> NReference.string_of_reference nref
- | `Whelp (query, _) -> query
| `Univs uri -> "univs:" ^ UriManager.string_of_uri uri
let entry_of_string = function
| `Cic of Cic.term * Cic.metasenv
| `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
| `Dir of string
- | `HBugs of [ `Tutors ]
- | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
| `Uri of UriManager.uri
| `NRef of NReference.reference
- | `Whelp of string * UriManager.uri list
| `Univs of UriManager.uri
]
projects / helm.git / commitdiff