]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/gTopLevel.ml
First experimental commit of the notation (partial!) for real numbers.
[helm.git] / helm / gTopLevel / gTopLevel.ml
index 4878088b709748ef9bc5d0168965420ebe5985a9..89e56bafc266310c0335985d7f61c19d95cc8b4d 100644 (file)
@@ -27,7 +27,7 @@
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
 (*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                Claudio Sacerdoti Coen <natile@cs.unibo.it>               *)
 (*                                 06/01/2002                                 *)
 (*                                                                            *)
 (*                                                                            *)
@@ -60,14 +60,19 @@ let htmlfooter =
  "</html>"
 ;;
 
-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
        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
   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,13 +2296,14 @@ 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;;
 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
+let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
 let cut = call_tactic_with_input ProofEngine.cut;;
 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
 let letin = call_tactic_with_input ProofEngine.letin;;
@@ -2361,6 +2393,252 @@ let open_ () =
         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+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
@@ -2368,35 +2646,145 @@ 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
      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let choose_must list_of_must only =
+ let chosen = ref None in
+ let user_constraints = ref [] in
+ let window =
+  GWindow.window
+   ~modal:true ~title:"Query refinement." ~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:
+    ("You can now specify the genericity of the query. " ^
+     "The more generic the slower.")
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+  GMisc.label
+   ~text:
+    "Suggestion: start with faster queries before moving to more generic ones."
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let notebook =
+  GPack.notebook ~scrollable:true
+   ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let _ =
+  let page = ref 0 in
+  let last = List.length list_of_must in
+  List.map
+   (function must ->
+     incr page ;
+     let label =
+      GMisc.label ~text:
+       (if !page = 1 then "More generic" else
+         if !page = last then "More precise" else "          ") () in
+     let expected_height = 25 * (List.length must + 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:(notebook#append_page ~tab_label:label#coerce) () in
+     let clist =
+        GList.clist ~columns:2 ~packing:scrolled_window#add
+         ~titles:["URI" ; "Position"] ()
+     in
+      ignore
+       (List.map
+         (function (uri,position) ->
+           let n =
+            clist#append 
+             [uri; if position then "MainConclusion" else "Conclusion"]
+           in
+            clist#set_row ~selectable:false n
+         ) must
+       ) ;
+      clist#columns_autosize ()
+   ) list_of_must in
+ let _ =
+  let label = GMisc.label ~text:"User provided" () 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:"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 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
+    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+  let clist =
+   GList.clist ~columns:2 ~packing:scrolled_window#add
+    ~selection_mode:`EXTENDED
+    ~titles:["URI" ; "Position"] ()
+  in
+   ignore
+    (List.map
+      (function (uri,position) ->
+        let n =
+         clist#append 
+          [uri; if position then "MainConclusion" else "Conclusion"]
+        in
+         clist#set_row ~selectable:true n
+      ) only
+    ) ;
+   clist#columns_autosize () ;
+   ignore
+    (clist#connect#select_row
+      (fun ~row ~column ~event ->
+        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 only row)) !user_constraints)) ;
+ 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 cancelb =
+  GButton.button ~label:"Abort"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+  (okb#connect#clicked
+    (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
+ window#set_position `CENTER ;
+ window#show () ;
+ GMain.Main.main () ;
+ match !chosen with
+    None -> raise NoChoice
+  | Some n ->
+     if n = List.length list_of_must then
+      (* user provided constraints *)
+      !user_constraints
+     else
+      List.nth list_of_must n
+;;
+
 let searchPattern () =
  let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
-   let rec get_level ?(last_invalid=false) () =
-    match
-     GToolbox.input_string
-      ~title:"Insert the strictness parameter for the query:"
-      ((if last_invalid then
-         "Invalid input (must be a non-negative natural number). Insert again "
-        else
-         "Insert "
-       ) ^ "the strictness parameter for the query:")
-    with
-       None -> raise NoChoice
-     | Some n ->
-        try
-         int_of_string n
-        with
-         _ -> get_level ~last_invalid:true ()
-   in
-    let level = get_level () in
     let metasenv =
      match !ProofEngine.proof with
         None -> assert false
@@ -2406,10 +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 len = List.length list_of_must in
-         let must = if level < len then List.nth list_of_must level else 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,_ ->
@@ -2417,9 +2817,6 @@ let searchPattern () =
             ) result in
           let html =
            " <h1>Backward Query: </h1>" ^
-           " <h2>Levels: </h2> " ^
-           MQueryLevels.string_of_levels
-            (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
           " <pre>" ^ get_last_query result ^ "</pre>"
           in
            output_html outputhtml html ;
@@ -2695,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"
@@ -2710,14 +3107,17 @@ object(self)
    let simplb =
     GButton.button ~label:"Simpl"
      ~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
+     ~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 foldreduceb =
     GButton.button ~label:"Fold_reduce"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let foldsimplb =
+    GButton.button ~label:"Fold_simpl"
+     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
    let cutb =
     GButton.button ~label:"Cut"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2785,13 +3185,14 @@ 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) ;
    ignore(simplb#connect#clicked simpl) ;
    ignore(foldwhdb#connect#clicked fold_whd) ;
    ignore(foldreduceb#connect#clicked fold_reduce) ;
+   ignore(foldsimplb#connect#clicked fold_simpl) ;
    ignore(cutb#connect#clicked cut) ;
    ignore(changeb#connect#clicked change) ;
    ignore(letinb#connect#clicked letin) ;