Added universes handling. The PRE_UNIVERSES tag may help ;)

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index ceaccdcefaed715d9a636da8c34f222a1099447f..66a860a451115e14a8d745c5dd205cd87cd7bb56 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -32,10 +32,11 @@ let rec injection_tac ~term =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,_ = CicUtil.lookup_meta goal metasenv in
-     let termty = (CicTypeChecker.type_of_aux' metasenv context term) in  
-      ProofEngineTypes.apply_tactic
+  let _,metasenv,_,_ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let termty,_ = (* TASSI: FIXME *)
+    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in  
+    ProofEngineTypes.apply_tactic
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
              when (U.eq equri Logic.eq_URI) -> (
@@ -88,11 +89,12 @@ and injection1_tac ~term ~i =
    let module U = UriManager in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
-    let _,metasenv,_,_ = proof 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])
+   let _,metasenv,_,_ = proof in
+   let _,context,_ = CicUtil.lookup_meta goal metasenv in
+   let termty,_ = (* TASSI: FIXME *)
+     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+     match termty with (* an equality *)
+         (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
              when (U.eq equri Logic.eq_URI) -> (
            match tty with (* some inductive type *)
               (C.MutInd (turi,typeno,exp_named_subst))
@@ -110,13 +112,16 @@ and injection1_tac ~term ~i =
                     (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2
                  | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai")
                in
-                let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in
+                let tty',_ = 
+                 CicTypeChecker.type_of_aux' metasenv context t1' 
+                   CicUniv.empty_ugraph  in
  prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ;
  prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
  prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
  prerr_endline ("XXXX consno " ^ string_of_int consno) ;
                 let pattern =
-                      match (CicEnvironment.get_obj turi) with
+                      match fst(CicEnvironment.get_obj turi 
+                                 CicUniv.empty_ugraph ) with
                          C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx)  ->
                           let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
                            let i_constr_id,_ = List.nth constructor_list (consno - 1) in
@@ -218,9 +223,10 @@ let discriminate'_tac ~term =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,_ = CicUtil.lookup_meta goal metasenv in
-     let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
+  let _,metasenv,_,_ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let termty,_ = 
+    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
           when (U.eq equri Logic.eq_URI) -> (
@@ -269,7 +275,8 @@ prerr_endline ("XXXX consno2 " ^ (string_of_int consno2)) ;
 
                    let pattern = 
                      (* a list of "True" except for the element in position consno2 which is "False" *)
-                     match (CicEnvironment.get_obj turi) with
+                     match fst(CicEnvironment.get_obj turi 
+                                CicUniv.empty_ugraph) with
                         C.InductiveDefinition (ind_type_list,_,nr_ind_params)  ->
 prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ;
                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in 
@@ -327,17 +334,21 @@ prerr_endline ("XXXX nth funzionano ") ;
                               )
                              ~continuation:
                               (
-prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2])));
+let u = CicUniv.empty_ugraph in
+prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2]) u)));
 prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2])) ;
 prerr_endline ("XXXX equri: " ^ U.string_of_uri equri) ;
 prerr_endline ("XXXX tty : " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1)) ;
-prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2)) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1) <> tty then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1)) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t2) <> tty then prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2)) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1) <> (CicTypeChecker.type_of_aux' metasenv' context' t2) 
- then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1)) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2)) ;
-prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term));
+prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ;
+prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
+if (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <> tty then 
+prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ;
+if (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u)) <> tty then 
+prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
+if (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <> 
+(fst (CicTypeChecker.type_of_aux' metasenv' context' t2 u)) 
+ then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
+prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' term u)));
                                  T.then_
                                    ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
@@ -490,7 +501,8 @@ prerr_endline ("XXXX consno2' " ^ (string_of_int consno2')) ;
 
                    let pattern = 
                      (* a list of "True" except for the element in position consno2' which is "False" *)
-                     match (CicEnvironment.get_obj turi) with
+                     match fst(CicEnvironment.get_obj turi 
+                                 CicUniv.empty_ugraph) with
                         C.InductiveDefinition (ind_type_list,_,nr_ind_params)  ->
 prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ;
                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in