X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=f81dffc8543df69c1760235f6c12647bf3cb44f7;hb=3fcde61beded58d18775c13906b9741ba4735864;hp=4363b3beee623f7e22db32dd5658746c8b89859c;hpb=4cbd4cadc2e71d4d25469dd7dddf05088baacb62;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 4363b3bee..f81dffc85 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -27,7 +27,7 @@ (* *) (* PROJECT HELM *) (* *) -(* Claudio Sacerdoti Coen *) +(* Claudio Sacerdoti Coen *) (* 06/01/2002 *) (* *) (* *) @@ -60,43 +60,42 @@ let htmlfooter = "" ;; -let prooffile = "/public/natile/currentproof";; -let prooffiletype = "/public/natile/currentprooftype";; - -(* SACERDOT -let prooffile = "/public/natile/currentproof";; -let prooffiletype = "/public/natile/currentprooftype";; -*) - -(* TASSI -let prooffile = "//miohelm/tmp/currentproof";; -let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; -*) +let prooffile = + try + Sys.getenv "GTOPLEVEL_PROOFFILE" + with + Not_found -> "/public/currentproof" +;; -(* GALATA -let prooffile = "/home/galata/miohelm/currentproof";; -let prooffiletype = "/home/galata/miohelm/currentprooftype";; -*) +let prooffiletype = + try + Sys.getenv "GTOPLEVEL_PROOFFILETYPE" + with + Not_found -> "/public/currentprooftype" +;; (*CSC: the getter should handle the innertypes, not the FS *) -let innertypesfile = "/public/natile/innertypes";; -let constanttypefile = "/public/natile/constanttype";; - -(* SACERDOT -let innertypesfile = "/public/natile/innertypes";; -let constanttypefile = "/public/natile/constanttype";; -*) +let innertypesfile = + try + Sys.getenv "GTOPLEVEL_INNERTYPESFILE" + with + Not_found -> "/public/innertypes" +;; -(* TASSI -let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; -let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; -*) +let constanttypefile = + try + Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE" + with + Not_found -> "/public/constanttype" +;; -(* GALATA -let innertypesfile = "/home/galata/miohelm/innertypes";; -let constanttypefile = "/home/galata/miohelm/constanttype";; -*) +let postgresqlconnectionstring = + try + Sys.getenv "POSTGRESQL_CONNECTION_STRING" + with + Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" +;; let empty_id_to_uris = ([],function _ -> None);; @@ -171,33 +170,6 @@ let argspec = in Arg.parse argspec ignore "" -(* A WIDGET TO ENTER CIC TERMS *) - -class term_editor ?packing ?width ?height ?isnotempty_callback () = - let input = GEdit.text ~editable:true ?width ?height ?packing () in - let _ = - match isnotempty_callback with - None -> () - | Some callback -> - ignore(input#connect#changed (function () -> callback (input#length > 0))) - in -object(self) - method coerce = input#coerce - method reset = - input#delete_text 0 input#length - (* CSC: txt is now a string, but should be of type Cic.term *) - method set_term txt = - self#reset ; - ignore ((input#insert_text txt) ~pos:0) - (* CSC: this method should disappear *) - method get_as_string = - input#get_chars 0 input#length - method get_term ~context ~metasenv = - let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in - CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf -end -;; - (* MISC FUNCTIONS *) exception IllFormedUri of string;; @@ -292,7 +264,6 @@ let check_window outputhtml uris = in try let mml = !mml_of_cic_term_ref 111 expr in -prerr_endline ("### " ^ CicPp.ppterm expr) ; mmlwidget#load_tree ~dom:mml with e -> @@ -309,10 +280,12 @@ prerr_endline ("### " ^ CicPp.ppterm expr) ; exception NoChoice;; let - interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris + interactive_user_uri_choice ~selection_mode ?(ok="Ok") + ?(enable_button_for_non_vars=false) ~title ~msg uris = let choices = ref [] in let chosen = ref false in + let use_only_constants = ref false in let window = GWindow.dialog ~modal:true ~title ~width:600 () in let lMessage = @@ -342,6 +315,13 @@ let GButton.button ~label:ok ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = okb#misc#set_sensitive false in + let nonvarsb = + GButton.button + ~packing: + (function w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Try constants only" () in let checkb = GButton.button ~label:"Check" ~packing:(hbox#pack ~padding:5) () in @@ -358,6 +338,13 @@ let ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore + (nonvarsb#connect#clicked + (function () -> + use_only_constants := true ; + chosen := true ; + window#destroy () + )) ; ignore (checkb#connect#clicked check_callback) ; ignore (clist#connect#select_row @@ -391,8 +378,13 @@ let window#set_position `CENTER ; window#show () ; GMain.Main.main () ; - if !chosen && List.length !choices > 0 then - !choices + if !chosen then + if !use_only_constants then + List.filter + (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris + else + if List.length !choices > 0 then !choices else raise NoChoice else raise NoChoice ;; @@ -1130,8 +1122,7 @@ let ("

" ^ Printexc.to_string e ^ "

") ; in let show_in_show_window_uri uri = - CicTypeChecker.typecheck uri ; - let obj = CicEnvironment.get_cooked_obj uri in + let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget (n : Gdome.element) = @@ -1186,22 +1177,6 @@ let locate_callback id = uris ;; -let locate () = - let inputt = ((rendering_window ())#inputt : term_editor) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - try - match - GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" - with - None -> raise NoChoice - | Some input -> - let uri = locate_callback input in - inputt#set_term uri - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; let input_or_locate_uri ~title = let uri = ref None in @@ -1326,6 +1301,7 @@ let locate_one_id id = interactive_user_uri_choice ~selection_mode:`EXTENDED ~ok:"Try every selection." + ~enable_button_for_non_vars:true ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ @@ -1335,6 +1311,7 @@ let locate_one_id id = List.map cic_textual_parser_uri_of_string uris' ;; + exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;; exception AmbiguousInput;; @@ -1385,22 +1362,40 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = let metasenv',expr = mk_metasenv_and_expr resolve in try (*CSC: Bug here: we do not try to typecheck also the metasenv' *) - ignore - (CicTypeChecker.type_of_aux' metasenv context expr) ; - resolve::(filter tl) + let term,_,_,metasenv'' = + CicRefine.type_of_aux' metasenv' context expr + in + (* If metasen <> metasenv'' is a normal condition, we should *) + (* be prepared to apply the returned substitution to the *) + (* whole current proof. *) + if metasenv <> metasenv'' then + begin + prerr_endline + ("+++++ ASSERTION FAILED: " ^ + "a refine operation should not modify the metasenv") ; + (* an assert would raise an exception that could be caught *) + exit 1 + end ; + (resolve,term,metasenv'')::(filter tl) with - _ -> filter tl + CicRefine.MutCaseFixAndCofixRefineNotImplemented -> + (try + let term = CicTypeChecker.type_of_aux' metasenv' context expr in + (resolve,term,metasenv')::(filter tl) + with _ -> filter tl + ) + | _ -> filter tl in filter resolve_ids in - let resolve_id' = + let resolve_id',term,metasenv' = match resolve_ids' with [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput | [resolve_id] -> resolve_id | _ -> let choices = List.map - (function resolve -> + (function (resolve,_,_) -> List.map (function id -> id, @@ -1424,9 +1419,67 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = List.nth resolve_ids' index in id_to_uris := known_ids @ dom', resolve_id' ; - mk_metasenv_and_expr resolve_id' + metasenv',term ;; +(* A WIDGET TO ENTER CIC TERMS *) + +class term_editor ?packing ?width ?height ?isnotempty_callback () = + let input = GEdit.text ~editable:true ?width ?height ?packing () in + let _ = + match isnotempty_callback with + None -> () + | Some callback -> + ignore(input#connect#changed (function () -> callback (input#length > 0))) + in +object(self) + method coerce = input#coerce + method reset = + input#delete_text 0 input#length + (* CSC: txt is now a string, but should be of type Cic.term *) + method set_term txt = + self#reset ; + ignore ((input#insert_text txt) ~pos:0) + (* CSC: this method should disappear *) + method get_as_string = + input#get_chars 0 input#length + method get_metasenv_and_term ~context ~metasenv = + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in + let dom,mk_metasenv_and_expr = + CicTextualParserContext.main + ~context:name_context ~metasenv CicTextualLexer.token lexbuf + in + disambiguate_input context metasenv dom mk_metasenv_and_expr +end +;; + +(* OTHER FUNCTIONS *) + +let locate () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + match + GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" + with + None -> raise NoChoice + | Some input -> + let uri = locate_callback input in + inputt#set_term uri + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + + exception UriAlreadyInUse;; exception NotAUriToAConstant;; @@ -1442,7 +1495,7 @@ let new_inductive () = let get_base_uri = ref (function _ -> assert false) in let get_names = ref (function _ -> assert false) in let get_types_and_cons = ref (function _ -> assert false) in - let get_name_context_context_and_subst = ref (function _ -> assert false) in + let get_context_and_subst = ref (function _ -> assert false) in let window = GWindow.window ~width:600 ~modal:true ~position:`CENTER @@ -1587,51 +1640,43 @@ let new_inductive () = let types_and_cons = List.map2 (fun name (newinputt,cons_names_entry) -> - let dom,mk_metasenv_and_expr = - newinputt#get_term ~context:[] ~metasenv:[] in let consnamesstr = cons_names_entry#text in let cons_names = Str.split (Str.regexp " +") consnamesstr in let metasenv,expr = - disambiguate_input [] [] dom mk_metasenv_and_expr + newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] in match metasenv with [] -> expr,cons_names | _ -> raise AmbiguousInput ) names type_widgets in - (* Let's see if so far the definition is well-typed *) let uri = !get_uri () in - let params = [] in - let paramsno = 0 in - let tys = - let i = ref 0 in + let _ = + (* Let's see if so far the definition is well-typed *) + let params = [] in + let paramsno = 0 in + (* To test if the arities of the inductive types are well *) + (* typed, we check the inductive block definition where *) + (* no constructor is given to each type. *) + let tys = List.map2 - (fun name (ty,cons) -> - let cons' = - List.map - (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in - let res = (name, !inductive, ty, cons') in - incr i ; - res - ) names types_and_cons + (fun name (ty,cons) -> (name, !inductive, ty, [])) + names types_and_cons + in + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,paramsno) in -(*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi - anche quando paramsno > 0 ;-(((( - CicTypeChecker.typecheck_mutual_inductive_defs uri - (tys,params,paramsno) ; -*) - get_name_context_context_and_subst := + get_context_and_subst := (function () -> let i = ref 0 in List.fold_left2 - (fun (namecontext,context,subst) name (ty,_) -> + (fun (context,subst) name (ty,_) -> let res = - (Some (Cic.Name name))::namecontext, - (Some (Cic.Name name, Cic.Decl ty))::context, + (Some (Cic.Name name, Cic.Decl ty))::context, (Cic.MutInd (uri,!i,[]))::subst in incr i ; res - ) ([],[],[]) names types_and_cons) ; + ) ([],[]) names types_and_cons) ; let types_and_cons' = List.map2 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) @@ -1692,24 +1737,21 @@ let new_inductive () = (function () -> try chosen := true ; - let namecontext,context,subst= !get_name_context_context_and_subst () in + let context,subst= !get_context_and_subst () in let cons_types = List.map2 (fun name inputt -> - let dom,mk_metasenv_and_expr = - inputt#get_term ~context:namecontext ~metasenv:[] + let metasenv,expr = + inputt#get_metasenv_and_term ~context ~metasenv:[] in - let metasenv,expr = - disambiguate_input context [] dom mk_metasenv_and_expr - in - match metasenv with - [] -> - let undebrujined_expr = - List.fold_left - (fun expr t -> CicSubstitution.subst t expr) expr subst - in - name, undebrujined_expr - | _ -> raise AmbiguousInput + match metasenv with + [] -> + let undebrujined_expr = + List.fold_left + (fun expr t -> CicSubstitution.subst t expr) expr subst + in + name, undebrujined_expr + | _ -> raise AmbiguousInput ) cons cons_type_widgets in get_cons_types := (function () -> cons_types) ; @@ -1773,7 +1815,7 @@ let new_proof () = let notebook = (rendering_window ())#notebook in let chosen = ref false in - let get_parsed = ref (function _ -> assert false) in + let get_metasenv_and_term = ref (function _ -> assert false) in let get_uri = ref (function _ -> assert false) in let non_empty_type = ref false in let window = @@ -1833,7 +1875,7 @@ let new_proof () = (function () -> chosen := true ; try - let parsed = newinputt#get_term [] [] in + let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in let uristr = "cic:" ^ uri_entry#text in let uri = UriManager.uri_of_string uristr in if String.sub uristr (String.length uristr - 4) 4 <> ".con" then @@ -1845,7 +1887,7 @@ let new_proof () = raise UriAlreadyInUse with Getter.Unresolved -> - get_parsed := (function () -> parsed) ; + get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () end @@ -1858,18 +1900,15 @@ let new_proof () = GMain.Main.main () ; if !chosen then try - let dom,mk_metasenv_and_expr = !get_parsed () in - let metasenv,expr = - disambiguate_input [] [] dom mk_metasenv_and_expr - in - let _ = CicTypeChecker.type_of_aux' metasenv [] expr in - ProofEngine.proof := - Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent notebook ; - refresh_proof output ; - !save_set_sensitive true ; - inputt#reset + let metasenv,expr = !get_metasenv_and_term () in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.proof := + Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent notebook ; + refresh_proof output ; + !save_set_sensitive true ; + inputt#reset with RefreshSequentException e -> output_html outputhtml @@ -1886,9 +1925,8 @@ let new_proof () = let check_term_in_scratch scratch_window metasenv context expr = try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in + let ty = CicTypeChecker.type_of_aux' metasenv context expr in let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in -prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; scratch_window#show () ; scratch_window#mmlwidget#load_tree ~dom:mml with @@ -1905,29 +1943,18 @@ let check scratch_window () = None -> [] | Some (_,metasenv,_,_) -> metasenv in - let context,names_context = - let context = - match !ProofEngine.goal with - None -> [] - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - in - context, - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context + let context = + match !ProofEngine.goal with + None -> [] + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context in try - let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in - let (metasenv',expr) = - disambiguate_input context metasenv dom mk_metasenv_and_expr - in - check_term_in_scratch scratch_window metasenv' context expr + let metasenv',expr = inputt#get_metasenv_and_term context metasenv in + check_term_in_scratch scratch_window metasenv' context expr with e -> output_html outputhtml @@ -1994,24 +2021,16 @@ let call_tactic_with_input tactic () = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context - in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) canonical_context in try - let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in - let (metasenv',expr) = - disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr - in - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic expr ; - refresh_sequent notebook ; - refresh_proof output ; - inputt#reset + let metasenv',expr = + inputt#get_metasenv_and_term canonical_context metasenv + in + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic expr ; + refresh_sequent notebook ; + refresh_proof output ; + inputt#reset with RefreshSequentException e -> output_html outputhtml @@ -2124,25 +2143,15 @@ let call_tactic_with_input_and_goal_input tactic () = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) canonical_context + let (metasenv',expr) = + inputt#get_metasenv_and_term canonical_context metasenv in - let dom,mk_metasenv_and_expr = inputt#get_term context metasenv - in - let (metasenv',expr) = - disambiguate_input canonical_context metasenv dom - mk_metasenv_and_expr - in - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic ~goal_input:(Hashtbl.find ids_to_terms id) - ~input:expr ; - refresh_sequent notebook ; - refresh_proof output ; - inputt#reset + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic ~goal_input:(Hashtbl.find ids_to_terms id) + ~input:expr ; + refresh_sequent notebook ; + refresh_proof output ; + inputt#reset | None -> assert false (* "ERROR: No current term!!!" *) with RefreshSequentException e -> @@ -2265,7 +2274,7 @@ let call_tactic_with_hypothesis_input tactic () = let intros = call_tactic ProofEngine.intros;; let exact = call_tactic_with_input ProofEngine.exact;; let apply = call_tactic_with_input ProofEngine.apply;; -let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;; +let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;; let elimtype = call_tactic_with_input ProofEngine.elim_type;; let whd = call_tactic_with_goal_input ProofEngine.whd;; let reduce = call_tactic_with_goal_input ProofEngine.reduce;; @@ -2281,6 +2290,8 @@ let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;; let clear = call_tactic_with_hypothesis_input ProofEngine.clear;; let fourier = call_tactic ProofEngine.fourier;; let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;; +let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;; +let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;; let reflexivity = call_tactic ProofEngine.reflexivity;; let symmetry = call_tactic ProofEngine.symmetry;; let transitivity = call_tactic_with_input ProofEngine.transitivity;; @@ -2292,7 +2303,7 @@ let assumption = call_tactic ProofEngine.assumption;; let generalize = call_tactic_with_goal_input ProofEngine.generalize;; let absurd = call_tactic_with_input ProofEngine.absurd;; let contradiction = call_tactic ProofEngine.contradiction;; -(* Galla: come dare alla tattica la lista di termini da decomporre? +(* Galla chiede: come dare alla tattica la lista di termini da decomporre? let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;; *) @@ -2362,24 +2373,337 @@ let open_ () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let show_query_results results = + let window = + GWindow.window + ~modal:false ~title:"Query results." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Click on a URI to show that object" + ~packing:hbox#add () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in + ignore + (List.map + (function (uri,_) -> + let n = + clist#append [uri] + in + clist#set_row ~selectable:false n + ) results + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + let (uristr,_) = List.nth results row in + match + cic_textual_parser_uri_of_string + (wrong_xpointer_format_from_wrong_xpointer_format' uristr) + with + CicTextualParser0.ConUri uri + | CicTextualParser0.VarUri uri + | CicTextualParser0.IndTyUri (uri,_) + | CicTextualParser0.IndConUri (uri,_,_) -> + show_in_show_window_uri uri + ) + ) ; + window#show () +;; + +let refine_constraints (must_obj,must_rel,must_sort) = + let chosen = ref false in + let use_only = ref false in + let window = + GWindow.window + ~modal:true ~title:"Constraints refinement." + ~width:800 ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "\"Only\" constraints can be enforced or not." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let onlyb = + GButton.toggle_button ~label:"Enforce \"only\" constraints" + ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ; + (* Notebook for the constraints choice *) + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + (* Rel constraints *) + let label = + GMisc.label + ~text: "Constraints on Rels" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Rels." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_rel + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let rel_constraints = + List.map + (function (position,depth) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:position + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> position, ref None + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button + ~label:("depth = " ^ string_of_int depth') ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + position, mutable_ref + ) must_rel in + (* Sort constraints *) + let label = + GMisc.label + ~text: "Constraints on Sorts" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Sorts." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_sort + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let sort_constraints = + List.map + (function (position,depth,sort) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(sort ^ " " ^ position) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> position, ref None, sort + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button ~label:("depth = " ^ string_of_int depth') + ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + position, mutable_ref, sort + ) must_sort in + (* Obj constraints *) + let label = + GMisc.label + ~text: "Constraints on constants" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on constants." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_obj + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let obj_constraints = + List.map + (function (uri,position,depth) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(uri ^ " " ^ position) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> uri, position, ref None + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button ~label:("depth = " ^ string_of_int depth') + ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + uri, position, mutable_ref + ) must_obj in + (* Confirm/abort buttons *) + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())); + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + if !chosen then + let chosen_must_rel = + List.map + (function (position,ref_depth) -> position,!ref_depth) rel_constraints in + let chosen_must_sort = + List.map + (function (position,ref_depth,sort) -> position,!ref_depth,sort) + sort_constraints + in + let chosen_must_obj = + List.map + (function (uri,position,ref_depth) -> uri,position,!ref_depth) + obj_constraints + in + (chosen_must_obj,chosen_must_rel,chosen_must_sort), + (if !use_only then +(*CSC: ???????????????????????? I assume that must and only are the same... *) + Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort + else + None,None,None + ) + else + raise NoChoice +;; let completeSearchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in - let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in - let must,can = MQueryLevels2.get_constraints expr in - let result = MQueryGenerator.searchPattern must can in + let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in + let must = MQueryLevels2.get_constraints expr in + let must',only = refine_constraints must in + let results = MQueryGenerator.searchPattern must' only in + show_query_results results + with + e -> output_html outputhtml - ("

" ^ MQueryUtil.text_of_result result "\n" ^ "

") + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +let insertQuery () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + let chosen = ref None in + let window = + GWindow.window + ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let label = + GMisc.label ~text:"Insert Query. For Experts Only." + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let input = GEdit.text ~editable:true + ~packing:scrolled_window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let loadb = + GButton.button ~label:"Load from file..." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ; + ignore + (loadb#connect#clicked + (function () -> + match + GToolbox.select_file ~title:"Select Query File" () + with + None -> () + | Some filename -> + let inch = open_in filename in + let rec read_file () = + try + let line = input_line inch in + line ^ "\n" ^ read_file () + with + End_of_file -> "" + in + let text = read_file () in + input#delete_text 0 input#length ; + ignore (input#insert_text text ~pos:0))) ; + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + match !chosen with + None -> () + | Some q -> + let results = + Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q)) + in + show_query_results results with e -> output_html outputhtml ("

" ^ Printexc.to_string e ^ "

") ; ;; -let choose_must list_of_must can = +let choose_must list_of_must only = let chosen = ref None in let user_constraints = ref [] in let window = @@ -2445,7 +2769,7 @@ let choose_must list_of_must can = GMisc.label ~text:"Select the constraints that must be satisfied and press OK." ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let expected_height = 25 * (List.length can + 2) in + let expected_height = 25 * (List.length only + 2) in let height = if expected_height > 400 then 400 else expected_height in let scrolled_window = GBin.scrolled_window ~border_width:10 ~height ~width:600 @@ -2463,19 +2787,19 @@ let choose_must list_of_must can = [uri; if position then "MainConclusion" else "Conclusion"] in clist#set_row ~selectable:true n - ) can + ) only ) ; clist#columns_autosize () ; ignore (clist#connect#select_row (fun ~row ~column ~event -> - user_constraints := (List.nth can row)::!user_constraints)) ; + user_constraints := (List.nth only row)::!user_constraints)) ; ignore (clist#connect#unselect_row (fun ~row ~column ~event -> user_constraints := List.filter - (function uri -> uri != (List.nth can row)) !user_constraints)) ; + (function uri -> uri != (List.nth only row)) !user_constraints)) ; in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -2517,16 +2841,22 @@ let searchPattern () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in - let must = choose_must list_of_must can in + let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in + let must = choose_must list_of_must only in let torigth_restriction (u,b) = - let p = if b then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" - else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in - (u,p,None) + let p = + if b then + "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + else + "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" + in + (u,p,None) in let rigth_must = List.map torigth_restriction must in - let rigth_can = Some (List.map torigth_restriction can) in - let result = MQueryGenerator.searchPattern (rigth_must,[],[]) (rigth_can,None,None) in + let rigth_only = Some (List.map torigth_restriction only) in + let result = + MQueryGenerator.searchPattern + (rigth_must,[],[]) (rigth_only,None,None) in let uris = List.map (function uri,_ -> @@ -2809,8 +3139,8 @@ object(self) let applyb = GButton.button ~label:"Apply" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimsimplintrosb = - GButton.button ~label:"ElimSimplIntros" + let elimintrossimplb = + GButton.button ~label:"ElimIntrosSimpl" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let elimtypeb = GButton.button ~label:"ElimType" @@ -2824,11 +3154,11 @@ object(self) let simplb = GButton.button ~label:"Simpl" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let foldwhdb = - GButton.button ~label:"Fold_whd" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let hbox4 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let foldwhdb = + GButton.button ~label:"Fold_whd" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let foldreduceb = GButton.button ~label:"Fold_reduce" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in @@ -2847,37 +3177,43 @@ object(self) let ringb = GButton.button ~label:"Ring" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let hbox5 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let clearbodyb = GButton.button ~label:"ClearBody" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let clearb = GButton.button ~label:"Clear" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let hbox5 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let fourierb = GButton.button ~label:"Fourier" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let rewritesimplb = GButton.button ~label:"RewriteSimpl ->" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let rewritebacksimplb = + GButton.button ~label:"RewriteSimpl <-" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let replaceb = + GButton.button ~label:"Replace" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let hbox6 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let reflexivityb = GButton.button ~label:"Reflexivity" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let symmetryb = GButton.button ~label:"Symmetry" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let transitivityb = GButton.button ~label:"Transitivity" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let existsb = GButton.button ~label:"Exists" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let splitb = GButton.button ~label:"Split" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let hbox6 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let leftb = GButton.button ~label:"Left" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in @@ -2887,22 +3223,24 @@ object(self) let assumptionb = GButton.button ~label:"Assumption" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let hbox7 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let generalizeb = GButton.button ~label:"Generalize" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let absurdb = GButton.button ~label:"Absurd" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let contradictionb = GButton.button ~label:"Contradiction" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let searchpatternb = GButton.button ~label:"SearchPattern_Apply" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in ignore(exactb#connect#clicked exact) ; ignore(applyb#connect#clicked apply) ; - ignore(elimsimplintrosb#connect#clicked elimsimplintros) ; + ignore(elimintrossimplb#connect#clicked elimintrossimpl) ; ignore(elimtypeb#connect#clicked elimtype) ; ignore(whdb#connect#clicked whd) ; ignore(reduceb#connect#clicked reduce) ; @@ -2918,6 +3256,8 @@ object(self) ignore(clearb#connect#clicked clear) ; ignore(fourierb#connect#clicked fourier) ; ignore(rewritesimplb#connect#clicked rewritesimpl) ; + ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ; + ignore(replaceb#connect#clicked replace) ; ignore(reflexivityb#connect#clicked reflexivity) ; ignore(symmetryb#connect#clicked symmetry) ; ignore(transitivityb#connect#clicked transitivity) ; @@ -3099,6 +3439,9 @@ class rendering_window output (notebook : notebook) = let show_menu_item = factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show in + let insert_query_item = + factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U + ~callback:insertQuery in (* settings menu *) let settings_menu = factory0#add_submenu "Settings" in let factory3 = new GMenu.factory settings_menu ~accel_group in @@ -3191,9 +3534,7 @@ let _ = if !usedb then begin Mqint.set_database Mqint.postgres_db ; - (* Mqint.init "dbname=helm_mowgli" ; *) - (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *) - Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"; + Mqint.init postgresqlconnectionstring ; end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ;