X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=89e56bafc266310c0335985d7f61c19d95cc8b4d;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=a3e369057eea263c1522069e422297062efbe924;hpb=15d5b7a1d16dd2f25d3f09ac3575c63e4c792818;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index a3e369057..89e56bafc 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,14 +60,19 @@ let htmlfooter = "" ;; -let prooffile = "/public/sacerdot/currentproof";; -let prooffiletype = "/public/sacerdot/currentprooftype";; +let prooffile = "/public/natile/currentproof";; +let prooffiletype = "/public/natile/currentprooftype";; (* SACERDOT let prooffile = "/public/sacerdot/currentproof";; let prooffiletype = "/public/sacerdot/currentprooftype";; *) +(* NATILE +let prooffile = "/public/natile/currentproof";; +let prooffiletype = "/public/natile/currentprooftype";; +*) + (* TASSI let prooffile = "//miohelm/tmp/currentproof";; let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; @@ -80,14 +85,19 @@ let prooffiletype = "/home/galata/miohelm/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) -let innertypesfile = "/public/sacerdot/innertypes";; -let constanttypefile = "/public/sacerdot/constanttype";; +let innertypesfile = "/public/natile/innertypes";; +let constanttypefile = "/public/natile/constanttype";; (* SACERDOT let innertypesfile = "/public/sacerdot/innertypes";; let constanttypefile = "/public/sacerdot/constanttype";; *) +(* NATILE +let innertypesfile = "/public/natile/innertypes";; +let constanttypefile = "/public/natile/constanttype";; +*) + (* TASSI let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; @@ -309,10 +319,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 +354,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 +377,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 +417,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 +1161,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) = @@ -1326,6 +1356,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 ^ @@ -2265,7 +2296,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;; @@ -2362,6 +2393,252 @@ 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 @@ -2369,14 +2646,17 @@ let completeSearchPattern () = try let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in - ignore (MQueryLevels2.get_constraints expr) + 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 ("

" ^ 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 = @@ -2442,7 +2722,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 @@ -2460,19 +2740,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 @@ -2514,9 +2794,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 result = MQueryGenerator.searchPattern metasenv ey ty 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) + in + let rigth_must = List.map torigth_restriction must 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,_ -> @@ -2799,8 +3092,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" @@ -2892,7 +3185,7 @@ object(self) 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) ;