are_convertible on MutCase was no longer checking the match arguments

convertibility.

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 14b858491d8c55c8e4c9010ecb5781836e796845..8b9a0d22e35bc4d2b7d36d70cb4a6291a2178604 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -355,9 +355,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) ->
           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
          else
           let params =
-           let o,_ = 
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-           in
+            let o,_ = 
+              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable (_,_,_,params,_) -> params
@@ -387,9 +387,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) ->
        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
        | C.Const (uri,exp_named_subst) ->
           let params =
-           let o,_ = 
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-           in
+            let o,_ = 
+              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+            in
            (match o with
                C.Constant (_,_,_,params,_) -> params
              | C.Variable _ -> raise ReferenceToVariable
@@ -403,9 +403,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) ->
             C.Const (uri,exp_named_subst')
        | C.MutInd (uri,i,exp_named_subst) ->
           let params =
-           let o,_ = 
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-           in
+            let o,_ = 
+              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
@@ -419,9 +419,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) ->
             C.MutInd (uri,i,exp_named_subst')
        | C.MutConstruct (uri,i,j,exp_named_subst) ->
           let params =
-           let o,_ = 
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-           in
+            let o,_ = 
+              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
@@ -546,8 +546,8 @@ if List.mem uri params then debug_print "---- OK2" ;
           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
          else
           ( let o,_ = 
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-           in
+              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+            in
             match o with
               C.Constant _ -> raise ReferenceToConstant
             | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -562,9 +562,9 @@ if List.mem uri params then debug_print "---- OK2" ;
           )
      | (k, e, ens, (C.Meta (n,l) as t), s) ->
         (try 
-          let (_, term,_) = CicUtil.lookup_subst n subst in
+           let (_, term,_) = CicUtil.lookup_subst n subst in
            reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
-        with  CicUtil.Subst_not_found _ ->
+         with  CicUtil.Subst_not_found _ ->
            let t' = unwind k e ens t in
            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
@@ -607,9 +607,9 @@ if List.mem uri params then debug_print "---- OK2" ;
            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
         (let o,_ = 
-          CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-        in
-         match o with
+           CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+         in
+          match o with
             C.Constant (_,Some body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
@@ -664,13 +664,13 @@ if List.mem uri params then debug_print "---- OK2" ;
               reduce (k, e, ens, (List.nth pl (j-1)), s)
            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
               let (arity, r) =
-               let o,_ = 
-                 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
-               in
-                 match o with
+                let o,_ = 
+                  CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
+                in
+                  match o with
                       C.InductiveDefinition (tl,ingredients,r,_) ->
-                       let (_,_,arity,_) = List.nth tl i in
-                         (arity,r)
+                        let (_,_,arity,_) = List.nth tl i in
+                          (arity,r)
                     | _ -> raise WrongUriToInductiveDefinition
               in
                let ts =
@@ -685,7 +685,7 @@ if List.mem uri params then debug_print "---- OK2" ;
                in
                 (* ts are already unwinded because they are a sublist of tl *)
                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
-          | C.Cast _ | C.Implicit _ ->
+           | C.Cast _ | C.Implicit _ ->
               raise (Impossible 2) (* we don't trust our whd ;-) *)
            | _ ->
              let t' = unwind k e ens t in
@@ -721,7 +721,7 @@ if List.mem uri params then debug_print "---- OK2" ;
                       (name,recindex,unwind k e ens typ,
                         unwind' leng k e ens body)
                      in
-                     List.map unwind_fl fl
+                      List.map unwind_fl fl
                     in
                      let new_env =
                       let counter = ref 0 in
@@ -841,142 +841,142 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
               with
                Invalid_argument _ -> false,ugraph
              )
-           else
-             false,ugraph
+            else
+              false,ugraph
         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
-           if n1 = n2 then
-             let b2, ugraph1 = 
-               let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
-               let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
-                 List.fold_left2
-                   (fun (b,ugraph) t1 t2 ->
-                      if b then 
-                        match t1,t2 with
-                            None,_
-                          | _,None  -> true,ugraph
-                          | Some t1',Some t2' -> 
-                              aux test_equality_only context t1' t2' ugraph
-                      else
-                        false,ugraph
-                   ) (true,ugraph) l1 l2
-             in
-               if b2 then true,ugraph1 else false,ugraph 
-           else
-             false,ugraph
+            if n1 = n2 then
+              let b2, ugraph1 = 
+                let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+                let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+                  List.fold_left2
+                    (fun (b,ugraph) t1 t2 ->
+                       if b then 
+                         match t1,t2 with
+                             None,_
+                           | _,None  -> true,ugraph
+                           | Some t1',Some t2' -> 
+                               aux test_equality_only context t1' t2' ugraph
+                       else
+                         false,ugraph
+                    ) (true,ugraph) l1 l2
+              in
+                if b2 then true,ugraph1 else false,ugraph 
+            else
+              false,ugraph
+          (* TASSI: CONSTRAINTS *)
+        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+            true,(CicUniv.add_eq t2 t1 ugraph)
+          (* TASSI: CONSTRAINTS *)
+        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+            true,(CicUniv.add_ge t2 t1 ugraph)
+          (* TASSI: CONSTRAINTS *)
+        | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
           (* TASSI: CONSTRAINTS *)
-       | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-           true,(CicUniv.add_eq t2 t1 ugraph)
-         (* TASSI: CONSTRAINTS *)
-       | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-           true,(CicUniv.add_ge t2 t1 ugraph)
-         (* TASSI: CONSTRAINTS *)
-       | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-         (* TASSI: CONSTRAINTS *)
         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           let b',ugraph' = aux true context s1 s2 ugraph in
-           if b' then 
+            let b',ugraph' = aux true context s1 s2 ugraph in
+            if b' then 
               aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
-               t1 t2 ugraph'
-           else
-             false,ugraph
+                t1 t2 ugraph'
+            else
+              false,ugraph
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
            if b' then
-            aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
-              t1 t2 ugraph'
-          else
-            false,ugraph
+             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
+               t1 t2 ugraph'
+           else
+             false,ugraph
         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
-          if b' then
+           if b' then
             aux test_equality_only
              ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
-          else
-            false,ugraph
+           else
+             false,ugraph
         | (C.Appl l1, C.Appl l2) ->
            (try
              List.fold_right2
                (fun  x y (b,ugraph) -> 
-                if b then
-                  aux test_equality_only context x y ugraph
-                else
-                  false,ugraph) l1 l2 (true,ugraph)
+                 if b then
+                   aux test_equality_only context x y ugraph
+                 else
+                   false,ugraph) l1 l2 (true,ugraph)
             with
              Invalid_argument _ -> false,ugraph
            )
         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
             let b' = U.eq uri1 uri2 in
-           if b' then
+            if b' then
              (try
                List.fold_right2
                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                 if b && U.eq uri1 uri2 then
-                   aux test_equality_only context x y ugraph 
-                 else
-                   false,ugraph
+                  if b && U.eq uri1 uri2 then
+                    aux test_equality_only context x y ugraph 
+                  else
+                    false,ugraph
                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
               with
                Invalid_argument _ -> false,ugraph
              )
-           else
-             false,ugraph
+            else
+              false,ugraph
         | (C.MutInd (uri1,i1,exp_named_subst1),
            C.MutInd (uri2,i2,exp_named_subst2)
           ) ->
             let b' = U.eq uri1 uri2 && i1 = i2 in
-           if b' then
+            if b' then
              (try
                List.fold_right2
                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
                   if b && U.eq uri1 uri2 then
-                   aux test_equality_only context x y ugraph
-                 else
-                  false,ugraph
+                    aux test_equality_only context x y ugraph
+                  else
+                   false,ugraph
                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
               with
                Invalid_argument _ -> false,ugraph
              )
-           else 
-             false,ugraph
+            else 
+              false,ugraph
         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
           ) ->
             let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
-           if b' then
+            if b' then
              (try
                List.fold_right2
                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                 if b && U.eq uri1 uri2 then
-                   aux test_equality_only context x y ugraph
-                 else
-                   false,ugraph
+                  if b && U.eq uri1 uri2 then
+                    aux test_equality_only context x y ugraph
+                  else
+                    false,ugraph
                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
               with
                Invalid_argument _ -> false,ugraph
              )
-           else
-             false,ugraph
+            else
+              false,ugraph
         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
            C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
             let b' = U.eq uri1 uri2 && i1 = i2 in
-           if b' then
+            if b' then
              let b'',ugraph''=aux test_equality_only context 
-                outtype1 outtype2 ugraph in
-            if b'' then 
-              let b''',ugraph'''= aux test_equality_only context 
-                  term1 term2 ugraph'' in
-              List.fold_right2
-                (fun x y (b,ugraph) -> 
-                  if b then
-                    aux test_equality_only context x y ugraph 
-                  else 
-                    false,ugraph)
-                pl1 pl2 (true,ugraph''')
-            else
-              false,ugraph
-           else
-             false,ugraph
+                 outtype1 outtype2 ugraph in
+             if b'' then 
+               let b''',ugraph'''= aux test_equality_only context 
+                   term1 term2 ugraph'' in
+               List.fold_right2
+                 (fun x y (b,ugraph) -> 
+                   if b then
+                     aux test_equality_only context x y ugraph 
+                   else 
+                     false,ugraph)
+                 pl1 pl2 (b''',ugraph''')
+             else
+               false,ugraph
+            else
+              false,ugraph
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
             let tys =
               List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
@@ -985,17 +985,17 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
              List.fold_right2
               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
                 if b && recindex1 = recindex2 then
-                 let b',ugraph' = aux test_equality_only context ty1 ty2 
-                     ugraph in
-                 if b' then
-                   aux test_equality_only (tys@context) bo1 bo2 ugraph'
-                 else
-                   false,ugraph
-               else
-                 false,ugraph)
-            fl1 fl2 (true,ugraph)
-           else
-             false,ugraph
+                  let b',ugraph' = aux test_equality_only context ty1 ty2 
+                      ugraph in
+                  if b' then
+                    aux test_equality_only (tys@context) bo1 bo2 ugraph'
+                  else
+                    false,ugraph
+                else
+                  false,ugraph)
+             fl1 fl2 (true,ugraph)
+            else
+              false,ugraph
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
            let tys =
             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
@@ -1003,18 +1003,18 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
             if i1 = i2 then
               List.fold_right2
               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
-               if b then
-                 let b',ugraph' = aux test_equality_only context ty1 ty2 
-                     ugraph in
-                 if b' then
-                   aux test_equality_only (tys@context) bo1 bo2 ugraph'
-                 else
-                   false,ugraph
-               else
-                 false,ugraph)
-            fl1 fl2 (true,ugraph)
-           else
-             false,ugraph
+                if b then
+                  let b',ugraph' = aux test_equality_only context ty1 ty2 
+                      ugraph in
+                  if b' then
+                    aux test_equality_only (tys@context) bo1 bo2 ugraph'
+                  else
+                    false,ugraph
+                else
+                  false,ugraph)
+             fl1 fl2 (true,ugraph)
+            else
+              false,ugraph
         | (C.Cast _, _) | (_, C.Cast _)
         | (C.Implicit _, _) | (_, C.Implicit _) ->
             assert false
@@ -1025,11 +1025,11 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
      debug t1 [t2] "PREWHD";
      (* 
      (match t1 with 
-        Cic.Meta _ -> 
-          debug_print (CicPp.ppterm t1);
-          debug_print (CicPp.ppterm (whd ~subst context t1));
-          debug_print (CicPp.ppterm t2);
-          debug_print (CicPp.ppterm (whd ~subst context t2))
+         Cic.Meta _ -> 
+           debug_print (CicPp.ppterm t1);
+           debug_print (CicPp.ppterm (whd ~subst context t1));
+           debug_print (CicPp.ppterm t2);
+           debug_print (CicPp.ppterm (whd ~subst context t2))
        | _ -> ()); *)
      let t1' = whd ~subst context t1 in
      let t2' = whd ~subst context t2 in