first moogle template checkin

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index c413d4694e266ae35a48f76f18bf1878217689f2..dd2e68d09e8afcaf582ee88f10a7481cc63cfd0d 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -23,19 +23,20 @@
  * http://cs.unibo.it/helm/.
  *)
 
+open HelmLibraryObjects
 
-let rec injection_tac ~term ~status:((proof, goal) as status) = 
+let rec injection_tac ~term status = 
+  let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
   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])
-             when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
-             or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+             when (U.eq equri Logic.eq_URI) -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
@@ -71,10 +72,11 @@ let rec injection_tac ~term ~status:((proof, goal) as status) =
             | _ -> raise (ProofEngineTypes.Fail "Injection: not a projectable equality")
            )
         | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation")
-      ) ~status
+      ) status
 
 
-and injection1_tac ~term ~i ~status:((proof, goal) as status) = 
+and injection1_tac ~term ~i status = 
+let (proof, goal) = status in
 (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
   let module C = Cic in
   let module S = CicSubstitution in
@@ -82,12 +84,11 @@ 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])
-            when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
-            or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+            when (U.eq equri Logic.eq_URI) -> (
           match tty with (* some inductive type *)
              (C.MutInd (turi,typeno,exp_named_subst))
            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -148,9 +149,10 @@ prerr_endline ("XXXX cominciamo!") ;
                    ;
                    T.then_ 
                     ~start:
-                      (fun ~status:((proof,goal) as status) ->    
+                      (fun status ->    
+                        let (proof, goal) = status 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
 prerr_endline ("XXXX goal " ^ string_of_int goal) ;
 prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ;
 prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ;
@@ -179,7 +181,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ;
                                   );
                                   t1]
                                 )
-                       ~status
+                       status
                       )
                     ~continuation:
                       (T.then_
@@ -187,7 +189,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ;
                         ~continuation:EqualityTactics.reflexivity_tac
                       )
                   ]     
-                 ~status
+                 status
            | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
           )
        | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
@@ -200,18 +202,18 @@ exception TwoDifferentSubtermsFound of int
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
-let discriminate'_tac ~term ~status:((proof, goal) as status) = 
+let discriminate'_tac ~term status = 
+  let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
   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]) 
-          when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) 
-            or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+          when (U.eq equri Logic.eq_URI) -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -275,8 +277,8 @@ prerr_endline ("XXXX nth funzionano ") ;
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
-                                     else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[]))
+                                     then (C.MutInd(Logic.false_URI,0,[]))
+                                     else (C.MutInd(Logic.true_URI,0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -285,27 +287,15 @@ prerr_endline ("XXXX nth funzionano ") ;
 
                     let (proof',goals') = 
                      EliminationTactics.elim_type_tac 
-                      ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
-                      ~status 
+                      ~term:(C.MutInd(Logic.false_URI,0,[]))
+                      status 
                     in
                      (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 
@@ -340,7 +330,7 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic
                                    ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               )
-                             ~status:(proof',goal')
+                             (proof',goal')
                        | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
                      )    
             | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
@@ -349,11 +339,11 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic
 ;;
 
 
-let discriminate_tac ~term ~status =
+let discriminate_tac ~term status =
   Tacticals.then_
    ~start:(* (injection_tac ~term) *) Tacticals.id_tac
    ~continuation:(discriminate'_tac ~term) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
-   ~status
+   status
 ;;
 
 
@@ -366,7 +356,7 @@ e' vera o no e lo risolve *)
 
 
 
-let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~status
+let compare_tac ~term status = Tacticals.id_tac status
 (*
 (* term is in the form t1=t2; the tactic leaves two goals: in the first you have to          *)
 (* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2  *)
@@ -375,7 +365,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")) ->
@@ -396,7 +386,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat
                ~continuations:[
                  T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
                  decide_equality_tac]  
-               ~status
+               status
       | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
           let term' = (* (t1=t2) \/ ~(t1=t2) *)
            C.Appl [
@@ -414,7 +404,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat
                ~continuations:[
                  T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
                  decide_equality_tac]  
-               ~status
+               status
       | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") 
 *)
 ;;
@@ -425,13 +415,14 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat
 
 exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int) 
 
-let discriminate_tac ~term ~status:((proof, goal) as status) =
+let discriminate_tac ~term status =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
+  let (proof, goal) = status 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]) 
@@ -511,26 +502,14 @@ prerr_endline ("XXXX nth funzionano ") ;
                     let (proof',goals') = 
                      EliminationTactics.elim_type_tac 
                       ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ) 
-                      ~status 
+                      status 
                     in
                      (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 
@@ -569,7 +548,7 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic
                                    ~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               )
-                             ~status:(proof',goal')
+                             (proof',goal')
                        | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
                      )    
             | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")