X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=89e56bafc266310c0335985d7f61c19d95cc8b4d;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=890f5d75fd4071f5482c5fd00dfec2e530ef669c;hpb=a772e377c1ca7c43c3e1e25eb47479fc3c5ceb9e;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 890f5d75f..89e56bafc 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -60,8 +60,8 @@ 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";; @@ -85,8 +85,8 @@ 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";; @@ -319,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 = @@ -352,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 @@ -368,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 @@ -401,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 ;; @@ -1335,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 ^ @@ -2274,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;; @@ -2414,14 +2436,13 @@ let show_query_results results = window#show () ;; -let - refine_constraints (must_obj,must_rel,must_sort) (only_obj,only_rel,only_sort) -= +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." ~border_width:2 () in + ~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 @@ -2431,23 +2452,32 @@ let ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let onlyb = GButton.toggle_button ~label:"Enforce \"only\" constraints" - ~active:false ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) - () + ~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 + 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 - (* Rel constraints *) 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 + ~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 @@ -2464,9 +2494,9 @@ let | Some depth' -> let mutable_ref = ref (Some depth') in let depthb = - GButton.toggle_button ~label:(string_of_int depth') - ~active:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) - () + 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 @@ -2476,6 +2506,99 @@ let )) ; 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 = @@ -2495,18 +2618,24 @@ let if !chosen then let chosen_must_rel = List.map -(* - (function (position,ref_depth) -> position,!ref_depth) rel_constraints -*) -(function (position,ref_depth) -> prerr_endline ("### " ^ position ^ " " ^ match !ref_depth with None -> "NULL" | Some d -> string_of_int d) ; position,!ref_depth) rel_constraints + (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 - (must_obj,chosen_must_rel,must_sort), - (if !use_only then + (chosen_must_obj,chosen_must_rel,chosen_must_sort), + (if !use_only then (*CSC: ???????????????????????? I assume that must and only are the same... *) - only_obj,Some chosen_must_rel,only_sort - else - None,None,None - ) + Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort + else + None,None,None + ) else raise NoChoice ;; @@ -2517,9 +2646,9 @@ 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 - let must,only = MQueryLevels2.get_constraints expr in - let must',only' = refine_constraints must only in - let results = MQueryGenerator.searchPattern must' only' 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 -> @@ -2963,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" @@ -3056,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) ;