- added (hack) apply_tac_verbose (for auto)

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e70946564a53b64b1d3b754b0e3b854429210993..4c6a6588b5094eda5bf1ea7eb9f8314465576222 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -62,7 +62,7 @@ let _ =
 (* GLOBAL CONSTANTS *)
 
 let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
+let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -468,6 +468,12 @@ let qed () =
  match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,[],bo,ty) ->
+     let uri = match uri with Some uri -> uri | _ -> assert false in
+     (* we want to typecheck in the ENV *)
+     (*let old_working = CicUniv.get_working () in
+     CicUniv.set_working (CicUniv.get_global ());*)
+     CicUniv.directly_to_env_begin () ;
+     prerr_endline "-------------> QED";
      if
       CicReduction.are_convertible []
        (CicTypeChecker.type_of_aux' [] [] bo) ty
@@ -483,7 +489,16 @@ let qed () =
         let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
          make_dirs pathname ;
          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
-          pathname
+          pathname;
+       (* add the object to the env *)
+       CicEnvironment.add_type_checked_term uri (
+        Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+       (* FIXME: the variable list!! *)
+       (*
+       CicUniv.qed (); (* now the env has the right constraints *)*)
+       CicUniv.directly_to_env_end();
+       CicUniv.reset_working ();
+     prerr_endline "-------------> FINE";
       end
      else
       raise WrongProof
@@ -565,8 +580,9 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        else
         Hbugs.notify () ;
        (*CSC: Wrong: [] is just plainly wrong *)
-       uri,
-        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+        let uri = match uri with Some uri -> uri | _ -> assert false in
+        (uri,
+         Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
   in
    ignore (output#load_proof uri currentproof)
  with
@@ -620,7 +636,10 @@ let refresh_goals ?(empty_notebook=true) notebook =
           begin
            notebook#set_current_page
             ~may_skip_switch_page_event:true metano ;
-           notebook#proofw#load_sequent metasenv currentsequent
+prerr_endline "CIAO CIAO" ;
+prerr_endline ("SEQUENTE CORRENTE: " ^ SequentPp.TextualPp.print_sequent currentsequent) ;
+           notebook#proofw#load_sequent metasenv currentsequent ;
+prerr_endline "pASSO CIAO CIAO"
           end
  with
   e ->
@@ -691,7 +710,7 @@ let load_unfinished_proof () =
         match CicParser.obj_of_xml proof_file_type (Some proof_file) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
-            ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+            ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
             refresh_proof output ;
             set_proof_engine_goal
              (match metasenv with
@@ -876,7 +895,7 @@ let
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;
-       mmlwidget#load_doc mml ;
+       mmlwidget#load_root mml#get_documentElement ;
     with
      e ->
       HelmLogger.log
@@ -886,7 +905,7 @@ let
    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 option) _ =
+   let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
     match n with
        None -> ()
      | Some n' ->
@@ -1056,7 +1075,7 @@ module DisambiguateCallbacks =
     interactive_user_uri_choice ~selection_mode ?ok
      ?enable_button_for_non_vars ~title ~msg
   let interactive_interpretation_choice = interactive_interpretation_choice
-  let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
+  let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title
  end
 ;;
 
@@ -1512,7 +1531,7 @@ let new_proof () =
    let metasenv,expr = !get_metasenv_and_term () in
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
      ProofEngine.set_proof
-      (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+      (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr));
      set_proof_engine_goal (Some 1) ;
      refresh_goals notebook ;
      refresh_proof output ;
@@ -1591,7 +1610,8 @@ let open_ () =
  let notebook = (rendering_window ())#notebook in
    try
     let uri = input_or_locate_uri ~title:"Open" in
-     CicTypeChecker.typecheck uri ;
+     ignore(CicTypeChecker.typecheck uri);
+     (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
      let metasenv,bo,ty =
       match CicEnvironment.get_cooked_obj uri with
          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
@@ -1600,7 +1620,7 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+      ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
       set_proof_engine_goal None ;
       refresh_goals notebook ;
       refresh_proof output ;
@@ -2852,13 +2872,16 @@ end
 (* MAIN *)
 
 let initialize_everything () =
+prerr_endline "STO PER CREARE LA PROOF WINDOW" ;
   let output =
     TermViewer.proof_viewer
      ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
      ~width:350 ~height:280 ()
   in
+prerr_endline "CREATA" ;
   let notebook = new notebook in
   let rendering_window' = new rendering_window output notebook in
+prerr_endline "OK" ;
   rendering_window'#set_auto_disambiguation !auto_disambiguation;
   set_rendering_window rendering_window';
   let print_error_as_html prefix msg =
@@ -2876,6 +2899,7 @@ let initialize_everything () =
 ;;
 
 let main () =
+prerr_endline "CIAO" ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  MQIC.close mqi_handle;