From: Stefano Zacchiroli Date: Tue, 27 Jan 2004 17:08:31 +0000 (+0000) Subject: s/List.find.../CicUtil.lookup_meta/ X-Git-Tag: V_0_2_3~131 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git s/List.find.../CicUtil.lookup_meta/ --- diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 9e91eeb07..15d7968d3 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -31,7 +31,7 @@ let rec injection_tac ~term ~status:((proof, goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -83,7 +83,7 @@ and injection1_tac ~term ~i ~status:((proof, goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -151,7 +151,7 @@ prerr_endline ("XXXX cominciamo!") ; ~start: (fun ~status:((proof,goal) as status) -> let _,metasenv,_,_ = proof in - let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,gty = CicUtil.lookup_meta goal metasenv in prerr_endline ("XXXX goal " ^ string_of_int goal) ; prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ; prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ; @@ -207,7 +207,7 @@ let discriminate'_tac ~term ~status:((proof, goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -291,21 +291,9 @@ prerr_endline ("XXXX nth funzionano ") ; (match goals' with [goal'] -> let _,metasenv',_,_ = proof' in - let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in -prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ; -prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; -prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; -prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; -ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ; -prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); t2])) ; + let _,context',gty' = + CicUtil.lookup_meta goal' metasenv' + in T.then_ ~start: (P.change_tac @@ -375,7 +363,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,gty = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> @@ -431,7 +419,7 @@ let discriminate_tac ~term ~status:((proof, goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -516,21 +504,9 @@ prerr_endline ("XXXX nth funzionano ") ; (match goals' with [goal'] -> let _,metasenv',_,_ = proof' in - let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in -prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ; -prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; -prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ; -prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; -ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ; -prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); t2'])) ; + let _,context',gty' = + CicUtil.lookup_meta goal' metasenv' + in T.then_ ~start: (P.change_tac diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index b6141094f..cd401a2ec 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -44,7 +44,7 @@ let induction_tac ~term ~status:((proof,goal) as status) = let module S = ProofEngineStructuralRules in let module U = UriManager in let (_,metasenv,_,_) = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,ty = CicUtil.lookup_meta goal metasenv in let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *) T.then_ ~start:(T.repeat_tactic @@ -137,7 +137,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof let module T = Tacticals in let module S = ProofEngineStructuralRules in let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,ty = CicUtil.lookup_meta goal metasenv in let old_context_len = List.length context in let termty = CicTypeChecker.type_of_aux' metasenv context term in @@ -178,7 +178,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); if nr_of_hyp_still_to_elim <> 0 then let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let old_context_len = List.length context in let termty = CicTypeChecker.type_of_aux' metasenv context term' in warn ("elim_clear termty= " ^ CicPp.ppterm termty); @@ -193,7 +193,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof (* clear the hyp that has just been eliminated *) (fun ~status:((proof,goal) as status) -> let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let new_context_len = List.length context in warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 3af6b861d..48d5ea9a6 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -28,7 +28,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = let module C = Cic in let module U = UriManager in let curi,metasenv,pbo,pty = proof in - let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,gty = CicUtil.lookup_meta goal metasenv in let eq_ind_r,ty,t1,t2 = match CicTypeChecker.type_of_aux' metasenv context equality with C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] @@ -89,7 +89,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = let module C = Cic in let module U = UriManager in let curi,metasenv,pbo,pty = proof in - let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,gty = CicUtil.lookup_meta goal metasenv in let eq_ind_r,ty,t1,t2 = match CicTypeChecker.type_of_aux' metasenv context equality with C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] @@ -154,7 +154,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let wty = CicTypeChecker.type_of_aux' metasenv context what in try if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) @@ -200,7 +200,7 @@ let symmetry_tac ~status:(proof, goal) = let module R = CicReduction in let module U = UriManager in let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> PrimitiveTactics.apply_tac ~status:(proof,goal) @@ -220,7 +220,7 @@ let transitivity_tac ~term ~status:((proof, goal) as status) = let module U = UriManager in let module T = Tacticals in let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> T.thens diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 537ef3f5d..eeda7a862 100644 --- 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"); diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml index 6318f4890..b425f219a 100644 --- a/helm/ocaml/tactics/introductionTactics.ml +++ b/helm/ocaml/tactics/introductionTactics.ml @@ -28,7 +28,7 @@ let constructor_tac ~n ~status:(proof, goal) = let module C = Cic in let module R = CicReduction in let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.MutInd (uri, typeno, exp_named_subst)) | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index 25c29918f..12848ad26 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -29,7 +29,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) = let module U = UriManager in let module P = PrimitiveTactics in let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,ty = CicUtil.lookup_meta goal metasenv in if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *) then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c1297a0e5..518c6f86a 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -229,7 +229,7 @@ let apply_tac ~term ~status:(proof, goal) = let module R = CicReduction in let module C = Cic in let (_,metasenv,_,_) = 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 newmeta = new_meta_of_proof ~proof in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -318,7 +318,7 @@ let intros_tac let module C = Cic in let module R = CicReduction in let (_,metasenv,_,_) = 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 newmeta = new_meta_of_proof ~proof in let (context',ty',bo') = lambda_abstract context newmeta ty mk_fresh_name_callback @@ -334,7 +334,7 @@ let cut_tac = let module C = Cic 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 newmeta1 = new_meta_of_proof ~proof in let newmeta2 = newmeta1 + 1 in let fresh_name = @@ -366,7 +366,7 @@ let letin_tac = let module C = Cic 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 _ = CicTypeChecker.type_of_aux' metasenv context term in let newmeta = new_meta_of_proof ~proof in let fresh_name = @@ -389,7 +389,7 @@ let letin_tac let exact_tac ~term ~status:(proof, goal) = (* Assumption: the term bo must be closed in the current context *) let (_,metasenv,_,_) = 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 module T = CicTypeChecker in let module R = CicReduction in if R.are_convertible context (T.type_of_aux' metasenv context term) ty then @@ -410,7 +410,7 @@ let elim_tac ~term ~status:(proof, goal) = let module R = CicReduction in let module C = Cic in let (curi,metasenv,_,_) = 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 termty = T.type_of_aux' metasenv context term in let uri,exp_named_subst,typeno,args = match termty with @@ -450,7 +450,7 @@ let elim_tac ~term ~status:(proof, goal) = (* way. *) let meta_of_corpse = let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas + CicUtil.lookup_meta (lastmeta - 1) newmetas in let irl = CicMkImplicit.identity_relocation_list_for_metavariable @@ -549,7 +549,7 @@ exception NotConvertible (*CSC: Is that evident? Is that right? Or should it be changed? *) let change_tac ~what ~with_what ~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 (* are_convertible works only on well-typed terms *) ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; if CicReduction.are_convertible context what with_what then diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 07ddf3a9e..7f4a89fb8 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -33,7 +33,7 @@ let clearbody ~hyp ~status:(proof, goal) = | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body -> let curi,metasenv,pbo,pty = proof in - let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,_,_ = CicUtil.lookup_meta goal metasenv in let string_of_name = function C.Name n -> n @@ -98,7 +98,7 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) = | Some (n_to_clear, _) -> let curi,metasenv,pbo,pty = proof in let metano,context,ty = - List.find (function (m,_,_) -> m=goal) metasenv + CicUtil.lookup_meta goal metasenv in let string_of_name = function diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 55eacc234..5a567b84a 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -26,7 +26,7 @@ (* let reduction_tac ~reduction ~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 new_ty = reduction context ty in let new_metasenv = List.map @@ -42,7 +42,7 @@ let reduction_tac ~reduction ~status:(proof,goal) = (* The default of term is the thesis of the goal to be prooved *) let reduction_tac ~also_in_hypotheses ~reduction ~terms ~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 terms = match terms with None -> [ty] | Some l -> l in @@ -95,7 +95,7 @@ let whd_tac = reduction_tac ~reduction:CicReduction.whd ;; let fold_tac ~reduction ~also_in_hypotheses ~term ~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 term' = reduction context term in (* We don't know if [term] is a subterm of [ty] or a subterm of *) (* the type of one metavariable. So we replace it everywhere. *) diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index 8e592e61d..bd9c15136 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -125,20 +125,6 @@ let cic_is_const ?(uri: uri option = None) term = *) let uri_of_proof ~proof:(uri, _, _, _) = uri - (** - @param metano meta list index - @param metasenv meta list (environment) - @raise Failure if metano is not found in metasenv - @return conjecture corresponding to metano in metasenv - *) -let conj_of_metano metano = - try - List.find (function (m, _, _) -> m = metano) - with Not_found -> - failwith ( - "Ring.conj_of_metano: " ^ - (string_of_int metano) ^ " no such meta") - (** @param status current proof engine status @raise Failure if proof is None @@ -153,7 +139,7 @@ let metasenv_of_status ~status:((_,m,_,_), _) = m *) let context_of_status ~status:(proof, goal as status) = let metasenv = metasenv_of_status ~status:status in - let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in + let _, context, _ = CicUtil.lookup_meta goal metasenv in context (** CIC TERM CONSTRUCTORS *) @@ -448,7 +434,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) = | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in let (_, metasenv, _, _) = proof in - let (_, context, _) = conj_of_metano goal metasenv in + let (_, context, _) = CicUtil.lookup_meta goal metasenv in let proof',goal' = aux count context status in assert (goal = goal') ; proof',[goal'] @@ -464,7 +450,7 @@ let ring_tac ~status:((proof, goal) as status) = let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in let r = Reals.r in let metasenv = metasenv_of_status ~status in - let (metano, context, ty) = conj_of_metano goal metasenv in + let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) match (build_segments ~terms:[t1; t2]) with | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 06333d231..7270b70b3 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -40,7 +40,7 @@ module G = MQueryGenerator (* search arguments on which Apply tactic doesn't fail *) let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status = let ((_, metasenv, _, _), metano) = status in - let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in + let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in let must = choose_must list_of_must only in let result = diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 57660310b..8414698e7 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -222,7 +222,7 @@ let thens' ~start ~continuations ~status = let prova_tac = let apply_T_tac ~status:((proof,goal) as status) = let curi,metasenv,pbo,pty = proof in - let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,gty = CicUtil.lookup_meta goal metasenv in let rel = let rec find n = function diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 395768db9..04959e696 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -33,7 +33,7 @@ let assumption_tac ~status:((proof,goal) as status) = let module R = CicReduction in let module S = CicSubstitution in let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function hd::tl -> (match hd with @@ -66,7 +66,7 @@ let generalize_tac let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,ty = CicUtil.lookup_meta goal metasenv in let typ = match terms with [] -> assert false