X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=0cfd8f07cfe620ed9e2fe58438b6c7d97744b5c6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=491fe5224f2098cf1fc87765a52c62e5e99db4f4;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 491fe5224..0cfd8f07c 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -31,16 +31,20 @@ open ProofEngineTypes
 let proof = ref (None : proof option)
 let goal = ref (None : goal option)
 
+let get_proof () = !proof;;
+let set_proof p = proof := p;;
+
 let get_current_status_as_xml () =
-  match !proof with
+  match get_proof () with
      None -> assert false
    | Some (uri, metasenv, bo, ty) ->
+      let uri = match uri with Some uri -> uri | None -> assert false in
       let currentproof =
        (*CSC: Wrong: [] is just plainly wrong *)
-       Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+       Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])
       in
        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
-        Cic2acic.acic_object_of_cic_object currentproof
+        Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
        in
         let xml, bodyxml =
          match
@@ -54,12 +58,13 @@ let get_current_status_as_xml () =
 ;;
 
 let apply_tactic ~tactic =
- match !proof,!goal with
+ let module PET = ProofEngineTypes in
+ match get_proof (),!goal with
   | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
-     let (newproof, newgoals) = tactic ~status:(proof', goal') in
-      proof := Some newproof;
+     let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in
+      set_proof (Some newproof);
       goal :=
        (match newgoals, newproof with
            goal::_, _ -> Some goal
@@ -80,7 +85,7 @@ let metas_in_term term =
       C.Rel _ -> []
     | C.Meta (n,_) -> [n]
     | C.Sort _
-    | C.Implicit -> []
+    | C.Implicit _ -> []
     | C.Cast (te,ty) -> (aux te) @ (aux ty)
     | C.Prod (_,s,t) -> (aux s) @ (aux t)
     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
@@ -115,14 +120,16 @@ let metas_in_term term =
 (* are efficiency reasons.                                                   *)
 let perforate context term ty =
  let module C = Cic in
-  match !proof with
+  match get_proof () with
      None -> assert false
    | Some (uri,metasenv,bo,gty as proof') ->
-      let newmeta = new_meta proof' in
+      let newmeta = new_meta_of_proof proof' in
        (* We push the new meta at the end of the list for pretty-printing *)
        (* purposes: in this way metas are ordered.                        *)
        let metasenv' = metasenv@[newmeta,context,ty] in
-        let irl = identity_relocation_list_for_metavariable context in
+        let irl =
+          CicMkImplicit.identity_relocation_list_for_metavariable context
+        in
 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
         let bo' =
          ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
@@ -137,7 +144,7 @@ let perforate context term ty =
           let metasenv'' =
            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
           in
-           proof := Some (uri,metasenv'',bo',gty) ;
+           set_proof (Some (uri,metasenv'',bo',gty)) ;
            goal := Some newmeta
 
 
@@ -148,7 +155,7 @@ let perforate context term ty =
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function terms ty =
  let metasenv =
-  match !proof with
+  match get_proof () with
      None -> []
    | Some (_,metasenv,_,_) -> metasenv
  in
@@ -176,9 +183,9 @@ let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros ?mk_fresh_name_callback () =
  apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
 let cut ?mk_fresh_name_callback term =
- apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term)
+ apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback ~term)
 let letin ?mk_fresh_name_callback term =
- apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term)
+ apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 let elim_intros_simpl term =
   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
@@ -221,6 +228,10 @@ let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
 let fourier () = apply_tactic FourierR.fourier_tac
 
+(* let auto ~dbd () = apply_tactic (AutoTactic.auto_tac ~dbd) *)
+let auto ~dbd () = apply_tactic (AutoTactic.auto_tac_new ~dbd)
+
+
 let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
 let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
 let replace ~goal_input:what ~input:with_what =