s/List.find.../CicUtil.lookup_meta/

[helm.git] / helm / ocaml / tactics / fourierR.ml

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 537ef3f5d986f06286ca7ea341cb9d2c750bed0f..eeda7a862a83ce2d9a6771ff5d3c7d6f57f14e07 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -597,7 +597,7 @@ let tac_zero_inf_pos (n,d) ~status =
    let pall str ~status:(proof,goal) t =
      debug ("tac "^str^" :\n" );
      let curi,metasenv,pbo,pty = proof in
-     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      debug ("th = "^ CicPp.ppterm t ^"\n"); 
      debug ("ty = "^ CicPp.ppterm ty^"\n"); 
    in
@@ -678,7 +678,7 @@ let tac_zero_inf_false gl (n,d) ~status=
      (debug "2\n";let r = (Tacticals.then_ ~start:(
        fun ~status:(proof,goal as status) -> 
        let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+       let metano,context,ty = CicUtil.lookup_meta goal metasenv in
          debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
          ^ CicPp.ppterm ty ^"\n");
        let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
@@ -698,7 +698,7 @@ let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
 debug("stat tac_zero_infeq_false\n");
 let r = 
      let curi,metasenv,pbo,pty = proof in
-     let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      
      debug("faccio fold di " ^ CicPp.ppterm
             (Cic.Appl
@@ -736,7 +736,7 @@ let r =
 
 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
@@ -757,7 +757,7 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
    
 let my_cut ~term:c ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
 debug("my_cut di "^CicPp.ppterm c^"\n");
 
@@ -784,7 +784,7 @@ let exact = PrimitiveTactics.exact_tac;;
 let tac_use h ~status:(proof,goal as status) = 
 debug("Inizio TC_USE\n");
 let curi,metasenv,pbo,pty = proof in
-let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
 debug ("ty = "^ CicPp.ppterm ty^"\n"); 
 
@@ -899,7 +899,7 @@ debug("inizio EQ\n");
  let module C = Cic in
   let proof,goal = status in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
    let irl =
@@ -925,7 +925,7 @@ let tcl_fail a ~status:(proof,goal) =
 (* Galla: moved in variousTactics.ml 
 let assumption_tac ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let num = ref 0 in
   let tac_list = List.map 
        ( fun x -> num := !num + 1;
@@ -955,9 +955,7 @@ let contradiction_tac ~status:(proof,goal)=
 
 let rec fourier ~status:(s_proof,s_goal)=
   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
-  let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) 
-   s_metasenv in
-       
+  let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
   debug_pcontext s_context;
 
@@ -998,7 +996,7 @@ theoreme,so let's parse our thesis *)
    (* now we have all the right environment *)
    
    let curi,metasenv,pbo,pty = proof in
-   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
 
    (* now we want to convert hp to inequations, but first we must lift
@@ -1087,8 +1085,7 @@ theoreme,so let's parse our thesis *)
              fun ~status -> 
              debug ("inizio t1 strict\n");
              let curi,metasenv,pbo,pty = proof in
-             let metano,context,ty = List.find 
-              (function (m,_,_) -> m=goal) metasenv in
+             let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
              debug ("ty = "^ CicPp.ppterm ty^"\n"); 
               PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
@@ -1124,8 +1121,7 @@ theoreme,so let's parse our thesis *)
                fun ~status -> 
                debug("INIZIO TAC 1 2\n");
                let curi,metasenv,pbo,pty = proof in
-               let metano,context,ty = List.find (function (m,_,_) -> m=goal) 
-                metasenv in
+               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
                debug ("ty = "^ CicPp.ppterm ty^"\n"); 
                 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
@@ -1163,8 +1159,7 @@ theoreme,so let's parse our thesis *)
          ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_  
           ~start:(fun ~status:(proof,goal as status) ->
              let curi,metasenv,pbo,pty = proof in
-             let metano,context,ty = List.find (function (m,_,_) -> m=goal) 
-             metasenv in
+             let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              PrimitiveTactics.change_tac ~what:ty 
              ~with_what:(Cic.Appl [ _not; ineq]) ~status)
           ~continuation:(Tacticals.then_ 
@@ -1203,8 +1198,7 @@ theoreme,so let's parse our thesis *)
                  (
                  fun ~status:(proof,goal as status) ->
                   let curi,metasenv,pbo,pty = proof in
-                  let metano,context,ty = List.find (function (m,_,_) -> m=
-                   goal) metasenv in
+                  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                   (* check if ty is of type *)
                   let w1 = 
                     debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");