helm/ocaml/cic_proof_checking/cicReductionMachine.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 exception CicReductionInternalError;;
  27 exception WrongUriToInductiveDefinition;;
  28 exception Impossible of int;;
  29 exception ReferenceToConstant;;
  30 exception ReferenceToVariable;;
  31 exception ReferenceToCurrentProof;;
  32 exception ReferenceToInductiveDefinition;;
  33
  34 let fdebug = ref 1;;
  35 let debug t env s =
  36  let rec debug_aux t i =
  37   let module C = Cic in
  38   let module U = UriManager in
  39    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  40  in
  41   if !fdebug = 0 then
  42    begin
  43     print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
  44     flush stdout
  45    end
  46 ;;
  47
  48 type env = Cic.term list;;
  49 type stack = Cic.term list;;
  50 type config =
  51  int * env * Cic.term Cic.explicit_named_substitution * Cic.term * stack;;
  52
  53 let lazily = true;;
  54
  55 (* k is the length of the environment e *)
  56 (* m is the current depth inside the term *)
  57 let unwind' m k e ens t =
  58  let module C = Cic in
  59  let module S = CicSubstitution in
  60   if k = 0 && ens = [] then
  61    t
  62   else
  63    let rec unwind_aux m =
  64     function
  65        C.Rel n as t ->
  66         if n <= m then t else
  67          let d =
  68           try
  69            Some (List.nth e (n-m-1))
  70           with _ -> None
  71          in
  72           (match d with
  73               Some t' ->
  74                if m = 0 then t' else S.lift m t'
  75             | None -> C.Rel (n-k)
  76           )
  77      | C.Var (uri,exp_named_subst) ->
  78 (*
  79 prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
  80 *)
  81        if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
  82         CicSubstitution.lift m (List.assq uri ens)
  83        else
  84         let params =
  85          (match CicEnvironment.get_obj uri with
  86              C.Constant _ -> raise ReferenceToConstant
  87            | C.Variable (_,_,_,params) -> params
  88            | C.CurrentProof _ -> raise ReferenceToCurrentProof
  89            | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
  90          )
  91         in
  92          let exp_named_subst' =
  93           substaux_in_exp_named_subst params exp_named_subst m
  94          in
  95           C.Var (uri,exp_named_subst')
  96      | C.Meta (i,l) ->
  97         let l' =
  98          List.map
  99           (function
 100               None -> None
 101             | Some t -> Some (unwind_aux m t)
 102           ) l
 103         in
 104          C.Meta (i, l')
 105      | C.Sort _ as t -> t
 106      | C.Implicit as t -> t
 107      | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *)
 108      | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
 109      | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
 110      | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
 111      | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
 112      | C.Const (uri,exp_named_subst) ->
 113         let params =
 114          (match CicEnvironment.get_obj uri with
 115              C.Constant (_,_,_,params) -> params
 116            | C.Variable _ -> raise ReferenceToVariable
 117            | C.CurrentProof (_,_,_,_,params) -> params
 118            | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 119          )
 120         in
 121          let exp_named_subst' =
 122           substaux_in_exp_named_subst params exp_named_subst m
 123          in
 124           C.Const (uri,exp_named_subst')
 125      | C.MutInd (uri,i,exp_named_subst) ->
 126         let params =
 127          (match CicEnvironment.get_obj uri with
 128              C.Constant _ -> raise ReferenceToConstant
 129            | C.Variable _ -> raise ReferenceToVariable
 130            | C.CurrentProof _ -> raise ReferenceToCurrentProof
 131            | C.InductiveDefinition (_,params,_) -> params
 132          )
 133         in
 134          let exp_named_subst' =
 135           substaux_in_exp_named_subst params exp_named_subst m
 136          in
 137           C.MutInd (uri,i,exp_named_subst')
 138      | C.MutConstruct (uri,i,j,exp_named_subst) ->
 139         let params =
 140          (match CicEnvironment.get_obj uri with
 141              C.Constant _ -> raise ReferenceToConstant
 142            | C.Variable _ -> raise ReferenceToVariable
 143            | C.CurrentProof _ -> raise ReferenceToCurrentProof
 144            | C.InductiveDefinition (_,params,_) -> params
 145          )
 146         in
 147          let exp_named_subst' =
 148           substaux_in_exp_named_subst params exp_named_subst m
 149          in
 150           C.MutConstruct (uri,i,j,exp_named_subst')
 151      | C.MutCase (sp,i,outt,t,pl) ->
 152         C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
 153          List.map (unwind_aux m) pl)
 154      | C.Fix (i,fl) ->
 155         let len = List.length fl in
 156         let substitutedfl =
 157          List.map
 158           (fun (name,i,ty,bo) ->
 159             (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
 160            fl
 161         in
 162          C.Fix (i, substitutedfl)
 163      | C.CoFix (i,fl) ->
 164         let len = List.length fl in
 165         let substitutedfl =
 166          List.map
 167           (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
 168            fl
 169         in
 170          C.CoFix (i, substitutedfl)
 171    and substaux_in_exp_named_subst params exp_named_subst' m  =
 172 (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
 173     let ens' =
 174      List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 175 (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
 176       List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
 177     in
 178     let rec filter_and_lift =
 179      function
 180         [] -> []
 181       | uri::tl ->
 182          let r = filter_and_lift tl in
 183           (try
 184             (uri,(List.assq uri ens'))::r
 185            with
 186             Not_found -> r
 187           )
 188     in
 189      filter_and_lift params
 190 *)
 191
 192 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
 193 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
 194
 195 (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
 196 (*CSC: codice altamente inefficiente *)
 197     let rec filter_and_lift already_instantiated =
 198      function
 199         [] -> []
 200       | (uri,t)::tl when
 201           List.for_all
 202            (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
 203           &&
 204            not (List.mem uri already_instantiated)
 205           &&
 206            List.mem uri params
 207          ->
 208           (uri,CicSubstitution.lift m t) ::
 209            (filter_and_lift (uri::already_instantiated) tl)
 210       | _::tl -> filter_and_lift already_instantiated tl
 211 (*
 212     | (uri,_)::tl ->
 213 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
 214 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
 215 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
 216 if List.mem uri params then prerr_endline "---- OK2" ;
 217         filter_and_lift tl
 218 *)
 219     in
 220      List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 221       (filter_and_lift [] (List.rev ens))
 222    in
 223     unwind_aux m t
 224 ;;
 225
 226 let unwind =
 227  unwind' 0
 228 ;;
 229
 230 let reduce context : config -> Cic.term =
 231  let module C = Cic in
 232  let module S = CicSubstitution in
 233  let rec reduce =
 234   function
 235      (k, e, _, (C.Rel n as t), s) ->
 236       let d =
 237        try
 238         Some (List.nth e (n-1))
 239        with
 240         _ ->
 241          try
 242           begin
 243            match List.nth context (n - 1 - k) with
 244               None -> assert false
 245             | Some (_,C.Decl _) -> None
 246             | Some (_,C.Def x) -> Some (S.lift (n - k) x)
 247           end
 248          with
 249           _ -> None
 250       in
 251        (match d with
 252            Some t' -> reduce (0,[],[],t',s)
 253          | None ->
 254             if s = [] then
 255              C.Rel (n-k)
 256             else C.Appl (C.Rel (n-k)::s)
 257        )
 258    | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
 259        if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
 260         reduce (0, [], [], List.assq uri ens, s)
 261        else
 262         (match CicEnvironment.get_obj uri with
 263             C.Constant _ -> raise ReferenceToConstant
 264           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 265           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 266           | C.Variable (_,None,_,_) ->
 267              let t' = unwind k e ens t in
 268               if s = [] then t' else C.Appl (t'::s)
 269           | C.Variable (_,Some body,_,_) ->
 270              let ens' = push_exp_named_subst k e ens exp_named_subst in
 271               reduce (0, [], ens', body, s)
 272         )
 273    | (k, e, ens, (C.Meta _ as t), s) ->
 274       let t' = unwind k e ens t in
 275        if s = [] then t' else C.Appl (t'::s)
 276    | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
 277    | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *)
 278    | (k, e, ens, (C.Cast (te,ty) as t), s) ->
 279       reduce (k, e, ens, te, s) (* s should be empty *)
 280    | (k, e, ens, (C.Prod _ as t), s) -> unwind k e ens t (* s should be empty *)
 281    | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
 282    | (k, e, ens, C.Lambda (_,_,t), p::s) ->
 283        reduce (k+1, p::e, ens, t,s)
 284    (* lazy *)
 285    | (k, e, ens, (C.LetIn (_,m,t) as t'), s) when lazily ->
 286       let m' = unwind k e ens m in reduce (k+1, m'::e, ens, t, s)
 287    (* strict *)
 288    | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
 289       let m' = reduce (k,e,ens,m,[]) in reduce (k+1,m'::e,ens,t,s)
 290    | (_, _, _, C.Appl [], _) -> raise (Impossible 1)
 291    (* lazy *)
 292    | (k, e, ens, C.Appl (he::tl), s) when lazily ->
 293       let tl' = List.map (unwind k e ens) tl in
 294        reduce (k, e, ens, he, (List.append tl' s))
 295    (* strict, but constants are NOT unfolded *)
 296    | (k, e, ens, C.Appl (he::tl), s) ->
 297       (* constants are NOT unfolded *)
 298       let red =
 299        function
 300           C.Const _ as t -> unwind k e ens t
 301         | t -> reduce (k,e,ens,t,[])
 302       in
 303        let tl' = List.map red tl in
 304         reduce (k, e, ens, he , List.append tl' s)
 305 (*
 306    | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
 307    | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
 308    | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
 309    | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
 310 (* strict evaluation, but constants are NOT unfolded *)
 311       let red =
 312        function
 313           C.Const _ as t -> unwind k e ens t
 314         | t -> reduce (k,e,ens,t,[])
 315       in
 316        let tl' = List.map red tl in
 317         reduce (k, e, ens, he , List.append tl' s)
 318    | (k, e, ens, C.Appl l, s) ->
 319        C.Appl (List.append (List.map (unwind k e ens) l) s)
 320 *)
 321    | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
 322       (match CicEnvironment.get_obj uri with
 323           C.Constant (_,Some body,_,_) ->
 324            let ens' = push_exp_named_subst k e ens exp_named_subst in
 325             (* constants are closed *)
 326             reduce (0, [], ens', body, s)
 327         | C.Constant (_,None,_,_) ->
 328            let t' = unwind k e ens t in
 329             if s = [] then t' else C.Appl (t'::s)
 330         | C.Variable _ -> raise ReferenceToVariable
 331         | C.CurrentProof (_,_,body,_,_) ->
 332            let ens' = push_exp_named_subst k e ens exp_named_subst in
 333             (* constants are closed *)
 334             reduce (0, [], ens', body, s)
 335         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 336       )
 337    | (k, e, ens, (C.MutInd _ as t),s) ->
 338       let t' = unwind k e ens t in
 339        if s = [] then t' else C.Appl (t'::s)
 340    | (k, e, ens, (C.MutConstruct _ as t),s) ->
 341        let t' = unwind k e ens t in
 342         if s = [] then t' else C.Appl (t'::s)
 343    | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
 344       let decofix =
 345        function
 346           C.CoFix (i,fl) as t ->
 347            let (_,_,body) = List.nth fl i in
 348             let body' =
 349              let counter = ref (List.length fl) in
 350               List.fold_right
 351                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 352                fl
 353                body
 354             in
 355              (* the term is the result of a reduction; *)
 356              (* so it is already unwinded.             *)
 357              reduce (0,[],[],body',[])
 358         | C.Appl (C.CoFix (i,fl) :: tl) ->
 359            let (_,_,body) = List.nth fl i in
 360             let body' =
 361              let counter = ref (List.length fl) in
 362               List.fold_right
 363                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 364                fl
 365                body
 366             in
 367              (* the term is the result of a reduction; *)
 368              (* so it is already unwinded.             *)
 369              reduce (0,[],[],body',tl)
 370         | t -> t
 371       in
 372        (match decofix (reduce (k,e,ens,term,[])) with
 373            C.MutConstruct (_,_,j,_) ->
 374             reduce (k, e, ens, (List.nth pl (j-1)), s)
 375          | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 376             let (arity, r) =
 377              match CicEnvironment.get_obj mutind with
 378                 C.InductiveDefinition (tl,ingredients,r) ->
 379                   let (_,_,arity,_) = List.nth tl i in
 380                    (arity,r)
 381               | _ -> raise WrongUriToInductiveDefinition
 382             in
 383              let ts =
 384               let num_to_eat = r in
 385                let rec eat_first =
 386                 function
 387                    (0,l) -> l
 388                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 389                  | _ -> raise (Impossible 5)
 390                in
 391                 eat_first (num_to_eat,tl)
 392              in
 393               (* ts are already unwinded because they are a sublist of tl *)
 394               reduce (k, e, ens, (List.nth pl (j-1)),(ts@s))
 395          | C.Cast _ | C.Implicit ->
 396             raise (Impossible 2) (* we don't trust our whd ;-) *)
 397          | _ ->
 398            let t' = unwind k e ens t in
 399             if s = [] then t' else C.Appl (t'::s)
 400        )
 401    | (k, e, ens, (C.Fix (i,fl) as t), s) ->
 402       let (_,recindex,_,body) = List.nth fl i in
 403        let recparam =
 404         try
 405          Some (List.nth s recindex)
 406         with
 407          _ -> None
 408        in
 409         (match recparam with
 410             Some recparam ->
 411              (match reduce (0,[],[],recparam,[]) with
 412                  (* match recparam with *)
 413                  C.MutConstruct _
 414                | C.Appl ((C.MutConstruct _)::_) ->
 415                   (* OLD
 416                   let body' =
 417                    let counter = ref (List.length fl) in
 418                     List.fold_right
 419                      (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 420                      fl
 421                      body
 422                   in
 423                    reduce (k, e, ens, body', s) *)
 424                   (* NEW *)
 425                   let leng = List.length fl in
 426                   let fl' =
 427                    let unwind_fl (name,recindex,typ,body) =
 428                     (name,recindex,unwind k e ens typ,
 429                       unwind' leng k e ens body)
 430                    in
 431                     List.map unwind_fl fl
 432                   in
 433                    let new_env =
 434                     let counter = ref 0 in
 435                     let rec build_env e =
 436                      if !counter = leng then e
 437                      else
 438                       (incr counter ; build_env ((C.Fix (!counter -1, fl'))::e))
 439                     in
 440                      build_env e
 441                    in
 442                     reduce (k+leng, new_env, ens, body, s)
 443                | _ ->
 444                  let t' = unwind k e ens t in
 445                   if s = [] then t' else C.Appl (t'::s)
 446              )
 447           | None ->
 448              let t' = unwind k e ens t in
 449               if s = [] then t' else C.Appl (t'::s)
 450         )
 451    | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
 452       let t' = unwind k e ens t in
 453        if s = [] then t' else C.Appl (t'::s)
 454  and push_exp_named_subst k e ens =
 455   function
 456      [] -> ens
 457    | (uri,t)::tl -> push_exp_named_subst k e ((uri,unwind k e ens t)::ens) tl
 458  in
 459   reduce
 460 ;;
 461
 462 let rec whd context t = reduce context (0, [], [], t, []);;
 463
 464 (* DEBUGGING ONLY
 465 let whd context t =
 466  let res = whd context t in
 467  let rescsc = CicReductionNaif.whd context t in
 468   if not (CicReductionNaif.are_convertible context res rescsc) then
 469    begin
 470     prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
 471     flush stderr ;
 472     prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
 473     flush stderr ;
 474     prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
 475     flush stderr ;
 476 CicReductionNaif.fdebug := 0 ;
 477 let _ =  CicReductionNaif.are_convertible context res rescsc in
 478     assert false ;
 479    end
 480   else
 481    res
 482 ;;
 483 *)
 484
 485
 486 (* t1, t2 must be well-typed *)
 487 let are_convertible =
 488  let module U = UriManager in
 489  let rec aux context t1 t2 =
 490   let aux2 t1 t2 =
 491    (* this trivial euristic cuts down the total time of about five times ;-) *)
 492    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 493    if t1 = t2 then
 494     true
 495    else
 496     begin
 497      let module C = Cic in
 498        match (t1,t2) with
 499           (C.Rel n1, C.Rel n2) -> n1 = n2
 500         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 501             U.eq uri1 uri2 &&
 502              (try
 503                List.fold_right2
 504                 (fun (uri1,x) (uri2,y) b ->
 505                   U.eq uri1 uri2 && aux context x y && b
 506                 ) exp_named_subst1 exp_named_subst2 true
 507               with
 508                Invalid_argument _ -> false
 509              )
 510         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 511             n1 = n2 &&
 512              List.fold_left2
 513               (fun b t1 t2 ->
 514                 b &&
 515                  match t1,t2 with
 516                     None,_
 517                   | _,None  -> true
 518                   | Some t1',Some t2' -> aux context t1' t2'
 519               ) true l1 l2
 520         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
 521         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 522            aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
 523         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 524            aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
 525         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 526            aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
 527         | (C.Appl l1, C.Appl l2) ->
 528            (try
 529              List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true
 530             with
 531              Invalid_argument _ -> false
 532            )
 533         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 534             U.eq uri1 uri2 &&
 535              (try
 536                List.fold_right2
 537                 (fun (uri1,x) (uri2,y) b ->
 538                   U.eq uri1 uri2 && aux context x y && b
 539                 ) exp_named_subst1 exp_named_subst2 true
 540               with
 541                Invalid_argument _ -> false
 542              )
 543         | (C.MutInd (uri1,i1,exp_named_subst1),
 544            C.MutInd (uri2,i2,exp_named_subst2)
 545           ) ->
 546             U.eq uri1 uri2 && i1 = i2 &&
 547              (try
 548                List.fold_right2
 549                 (fun (uri1,x) (uri2,y) b ->
 550                   U.eq uri1 uri2 && aux context x y && b
 551                 ) exp_named_subst1 exp_named_subst2 true
 552               with
 553                Invalid_argument _ -> false
 554              )
 555         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 556            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 557           ) ->
 558             U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
 559              (try
 560                List.fold_right2
 561                 (fun (uri1,x) (uri2,y) b ->
 562                   U.eq uri1 uri2 && aux context x y && b
 563                 ) exp_named_subst1 exp_named_subst2 true
 564               with
 565                Invalid_argument _ -> false
 566              )
 567         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 568            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 569             U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 &&
 570              aux context term1 term2 &&
 571              List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true
 572         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 573            let tys =
 574             List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 575            in
 576             i1 = i2 &&
 577              List.fold_right2
 578               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
 579                 b && recindex1 = recindex2 && aux context ty1 ty2 &&
 580                  aux (tys@context) bo1 bo2)
 581               fl1 fl2 true
 582         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 583            let tys =
 584             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 585            in
 586             i1 = i2 &&
 587              List.fold_right2
 588               (fun (_,ty1,bo1) (_,ty2,bo2) b ->
 589                 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
 590               fl1 fl2 true
 591         | (C.Cast _, _) | (_, C.Cast _)
 592         | (C.Implicit, _) | (_, C.Implicit) ->
 593            raise (Impossible 3) (* we don't trust our whd ;-) *)
 594         | (_,_) -> false
 595     end
 596   in
 597    if aux2 t1 t2 then true
 598    else
 599     begin
 600      debug t1 [t2] "PREWHD";
 601      let t1' = whd context t1 in
 602      let t2' = whd context t2 in
 603       debug t1' [t2'] "POSTWHD";
 604       aux2 t1' t2'
 605     end
 606  in
 607   aux
 608 ;;