helm/ocaml/cic_unification/cicUnification.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 UnificationFailed;;
  27 exception Free;;
  28 exception OccurCheck;;
  29 exception RelToHiddenHypothesis;;
  30 exception OpenTerm;;
  31
  32 (**** DELIFT ****)
  33
  34 (* the delift function takes in input an ordered list of optional terms       *)
  35 (* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with   *)
  36 (* rel(k). Typically, the list of optional terms is the explicit substitution *)(* that is applied to a metavariable occurrence and the result of the delift  *)
  37 (* function is a term the implicit variable can be substituted with to make   *)
  38 (* the term [t] unifiable with the metavariable occurrence.                   *)
  39 (* In general, the problem is undecidable if we consider equivalence in place *)
  40 (* of alpha convertibility. Our implementation, though, is even weaker than   *)
  41 (* alpha convertibility, since it replace the term [tk] if and only if [tk]   *)
  42 (* is a Rel (missing all the other cases). Does this matter in practice?      *)
  43
  44 exception NotInTheList;;
  45
  46 let position n =
  47   let rec aux k =
  48    function
  49        [] -> raise NotInTheList
  50      | (Some (Cic.Rel m))::_ when m=n -> k
  51      | _::tl -> aux (k+1) tl in
  52   aux 1
  53 ;;
  54
  55 (*CSC: this restriction function is utterly wrong, since it does not check  *)
  56 (*CSC: that the variable that is going to be restricted does not occur free *)
  57 (*CSC: in a part of the sequent that is not going to be restricted.         *)
  58 (*CSC: In particular, the whole approach is wrong; if restriction can fail  *)
  59 (*CSC: (as indeed it is the case), we can not collect all the restrictions  *)
  60 (*CSC: and restrict everything at the end ;-(                               *)
  61 let restrict to_be_restricted =
  62   let rec erase i n =
  63     function
  64         [] -> []
  65       |        _::tl when List.mem (n,i) to_be_restricted ->
  66           None::(erase (i+1) n tl)
  67       | he::tl -> he::(erase (i+1) n tl) in
  68   let rec aux =
  69     function
  70         [] -> []
  71       |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
  72   aux
  73 ;;
  74
  75
  76 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
  77 let delift context metasenv l t =
  78  let module S = CicSubstitution in
  79   let to_be_restricted = ref [] in
  80   let rec deliftaux k =
  81    let module C = Cic in
  82     function
  83        C.Rel m ->
  84          if m <=k then
  85           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
  86                     (*CSC: deliftato la regola per il LetIn                 *)
  87                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
  88          else
  89           (match List.nth context (m-k-1) with
  90             Some (_,C.Def (t,_)) ->
  91              (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
  92              (*CSC: first order unification. Does it help or does it harm? *)
  93              deliftaux k (S.lift m t)
  94           | Some (_,C.Decl t) ->
  95              (*CSC: The following check seems to be wrong!             *)
  96              (*CSC: B:Set |- ?2 : Set                                  *)
  97              (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x                 *)
  98              (*CSC: Why should I restrict ?2 over B? The instantiation *)
  99              (*CSC: ?1 := A is perfectly reasonable and well-typed.    *)
 100              (*CSC: Thus I comment out the following two lines that    *)
 101              (*CSC: are the incriminated ones.                         *)
 102              (*(* It may augment to_be_restricted *)
 103                ignore (deliftaux k (S.lift m t)) ;*)
 104              (*CSC: end of bug commented out                           *)
 105              C.Rel ((position (m-k) l) + k)
 106           | None -> raise RelToHiddenHypothesis)
 107      | C.Var (uri,exp_named_subst) ->
 108         let exp_named_subst' =
 109          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 110         in
 111          C.Var (uri,exp_named_subst')
 112      | C.Meta (i, l1) as t ->
 113         let rec deliftl j =
 114          function
 115             [] -> []
 116           | None::tl -> None::(deliftl (j+1) tl)
 117           | (Some t)::tl ->
 118              let l1' = (deliftl (j+1) tl) in
 119               try
 120                Some (deliftaux k t)::l1'
 121               with
 122                  RelToHiddenHypothesis
 123                | NotInTheList ->
 124                   to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
 125         in
 126          let l' = deliftl 1 l1 in
 127           C.Meta(i,l')
 128      | C.Sort _ as t -> t
 129      | C.Implicit as t -> t
 130      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
 131      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
 132      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
 133      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
 134      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
 135      | C.Const (uri,exp_named_subst) ->
 136         let exp_named_subst' =
 137          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 138         in
 139          C.Const (uri,exp_named_subst')
 140      | C.MutInd (uri,typeno,exp_named_subst) ->
 141         let exp_named_subst' =
 142          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 143         in
 144          C.MutInd (uri,typeno,exp_named_subst')
 145      | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 146         let exp_named_subst' =
 147          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 148         in
 149          C.MutConstruct (uri,typeno,consno,exp_named_subst')
 150      | C.MutCase (sp,i,outty,t,pl) ->
 151         C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
 152          List.map (deliftaux k) pl)
 153      | C.Fix (i, fl) ->
 154         let len = List.length fl in
 155         let liftedfl =
 156          List.map
 157           (fun (name, i, ty, bo) ->
 158            (name, i, deliftaux k ty, deliftaux (k+len) bo))
 159            fl
 160         in
 161          C.Fix (i, liftedfl)
 162      | C.CoFix (i, fl) ->
 163         let len = List.length fl in
 164         let liftedfl =
 165          List.map
 166           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 167            fl
 168         in
 169          C.CoFix (i, liftedfl)
 170   in
 171    let res =
 172     try
 173      deliftaux 0 t
 174     with
 175      NotInTheList ->
 176       (* This is the case where we fail even first order unification. *)
 177       (* The reason is that our delift function is weaker than first  *)
 178       (* order (in the sense of alpha-conversion). See comment above  *)
 179       (* related to the delift function.                              *)
 180 prerr_endline "!!!!!!!!!!! First Order UnificationFailed, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
 181       raise UnificationFailed
 182    in
 183     res, restrict !to_be_restricted metasenv
 184 ;;
 185
 186 (**** END OF DELIFT ****)
 187
 188 type substitution = (int * Cic.term) list
 189
 190 (* NUOVA UNIFICAZIONE *)
 191 (* A substitution is a (int * Cic.term) list that associates a
 192    metavariable i with its body.
 193    A metaenv is a (int * Cic.term) list that associate a metavariable
 194    i with is type.
 195    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 196    a new substitution which is _NOT_ unwinded. It must be unwinded before
 197    applying it. *)
 198
 199 let rec fo_unif_subst subst context metasenv t1 t2 =
 200  let module C = Cic in
 201  let module R = CicReduction in
 202  let module S = CicSubstitution in
 203   match (t1, t2) with
 204      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 205        let ok =
 206         List.fold_left2
 207          (fun b t1 t2 ->
 208            b &&
 209             match t1,t2 with
 210                None,_
 211              | _,None -> true
 212              | Some t1', Some t2' ->
 213                 (* First possibility:  restriction    *)
 214                 (* Second possibility: unification    *)
 215                 (* Third possibility:  convertibility *)
 216                 R.are_convertible context t1' t2'
 217          ) true ln lm
 218        in
 219         if ok then subst,metasenv else raise UnificationFailed
 220    | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
 221        fo_unif_subst subst context metasenv t2 t1
 222    | (C.Meta (n,l), t)
 223    | (t, C.Meta (n,l)) ->
 224        let subst',metasenv' =
 225         try
 226          let oldt = (List.assoc n subst) in
 227          let lifted_oldt = S.lift_meta l oldt in
 228           fo_unif_subst subst context metasenv lifted_oldt t
 229         with Not_found ->
 230          let t',metasenv' = delift context metasenv l t in
 231           (n, t')::subst, metasenv'
 232        in
 233         let (_,_,meta_type) =
 234          List.find (function (m,_,_) -> m=n) metasenv' in
 235         let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
 236          fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
 237    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 238    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 239       if UriManager.eq uri1 uri2 then
 240        fo_unif_subst_exp_named_subst subst context metasenv
 241         exp_named_subst1 exp_named_subst2
 242       else
 243        raise UnificationFailed
 244    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 245       if UriManager.eq uri1 uri2 && i1 = i2 then
 246        fo_unif_subst_exp_named_subst subst context metasenv
 247         exp_named_subst1 exp_named_subst2
 248       else
 249        raise UnificationFailed
 250    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 251      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 252       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 253        fo_unif_subst_exp_named_subst subst context metasenv
 254         exp_named_subst1 exp_named_subst2
 255       else
 256        raise UnificationFailed
 257    | (C.Rel _, _)
 258    | (_,  C.Rel _)
 259    | (C.Sort _ ,_)
 260    | (_, C.Sort _)
 261    | (C.Implicit, _)
 262    | (_, C.Implicit) ->
 263        if R.are_convertible context t1 t2 then
 264         subst, metasenv
 265        else
 266         raise UnificationFailed
 267    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
 268    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
 269    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 270        let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
 271         fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 272    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 273        let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
 274         fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 275    | (C.LetIn (_,s1,t1), t2)
 276    | (t2, C.LetIn (_,s1,t1)) ->
 277        fo_unif_subst subst context metasenv t2 (S.subst s1 t1)
 278    | (C.Appl l1, C.Appl l2) ->
 279        let lr1 = List.rev l1 in
 280        let lr2 = List.rev l2 in
 281        let rec fo_unif_l subst metasenv =
 282         function
 283            [],_
 284          | _,[] -> assert false
 285          | ([h1],[h2]) ->
 286              fo_unif_subst subst context metasenv h1 h2
 287          | ([h],l)
 288          | (l,[h]) ->
 289              fo_unif_subst subst context metasenv h (C.Appl (List.rev l))
 290          | ((h1::l1),(h2::l2)) ->
 291             let subst', metasenv' =
 292              fo_unif_subst subst context metasenv h1 h2
 293             in
 294              fo_unif_l subst' metasenv' (l1,l2)
 295        in
 296         fo_unif_l subst metasenv (lr1, lr2)
 297    | (C.Const _, _)
 298    | (_, C.Const _)
 299    | (C.MutInd  _, _)
 300    | (_, C.MutInd _)
 301    | (C.MutConstruct _, _)
 302    | (_, C.MutConstruct _) ->
 303       if R.are_convertible context t1 t2 then
 304        subst, metasenv
 305       else
 306        raise UnificationFailed
 307    | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))->
 308        let subst', metasenv' =
 309         fo_unif_subst subst context metasenv outt1 outt2 in
 310        let subst'',metasenv'' =
 311         fo_unif_subst subst' context metasenv' t1 t2 in
 312        List.fold_left2
 313         (function (subst,metasenv) ->
 314           fo_unif_subst subst context metasenv
 315         ) (subst'',metasenv'') pl1 pl2
 316    | (C.Fix _, _)
 317    | (_, C.Fix _)
 318    | (C.CoFix _, _)
 319    | (_, C.CoFix _) ->
 320        if R.are_convertible context t1 t2 then
 321         subst, metasenv
 322        else
 323         raise UnificationFailed
 324    | (_,_) ->
 325        if R.are_convertible context t1 t2 then
 326         subst, metasenv
 327        else
 328         raise UnificationFailed
 329
 330 and fo_unif_subst_exp_named_subst subst context metasenv
 331  exp_named_subst1 exp_named_subst2
 332 =
 333 try
 334  List.fold_left2
 335   (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
 336     assert (uri1=uri2) ;
 337     fo_unif_subst subst context metasenv t1 t2
 338   ) (subst,metasenv) exp_named_subst1 exp_named_subst2
 339 with
 340 e ->
 341 let uri = UriManager.uri_of_string "cic:/dummy.var" in
 342 prerr_endline ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
 343 " <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
 344 ;;
 345
 346 let unwind metasenv subst unwinded t =
 347  let unwinded = ref unwinded in
 348  let frozen = ref [] in
 349  let rec um_aux metasenv =
 350   let module C = Cic in
 351   let module S = CicSubstitution in
 352    function
 353       C.Rel _ as t -> t,metasenv
 354     | C.Var _  as t -> t,metasenv
 355     | C.Meta (i,l) ->
 356         (try
 357           S.lift_meta l (List.assoc i !unwinded), metasenv
 358          with Not_found ->
 359            if List.mem i !frozen then raise OccurCheck
 360            else
 361             let saved_frozen = !frozen in
 362             frozen := i::!frozen ;
 363             let res =
 364              try
 365               let t = List.assoc i subst in
 366               let t',metasenv' = um_aux metasenv t in
 367               let _,metasenv'' =
 368                let (_,canonical_context,_) =
 369                 List.find (function (m,_,_) -> m=i) metasenv
 370                in
 371                 delift canonical_context metasenv' l t'
 372               in
 373                unwinded := (i,t')::!unwinded ;
 374                S.lift_meta l t', metasenv'
 375              with
 376               Not_found ->
 377                (* not constrained variable, i.e. free in subst*)
 378                let l',metasenv' =
 379                 List.fold_right
 380                  (fun t (tl,metasenv) ->
 381                    match t with
 382                       None -> None::tl,metasenv
 383                     | Some t ->
 384                        let t',metasenv' = um_aux metasenv t in
 385                         (Some t')::tl, metasenv'
 386                  ) l ([],metasenv)
 387                in
 388                 C.Meta (i,l'), metasenv'
 389             in
 390             frozen := saved_frozen ;
 391             res
 392         )
 393     | C.Sort _
 394     | C.Implicit as t -> t,metasenv
 395     | C.Cast (te,ty) ->
 396        let te',metasenv' = um_aux metasenv te in
 397        let ty',metasenv'' = um_aux metasenv' ty in
 398        C.Cast (te',ty'),metasenv''
 399     | C.Prod (n,s,t) ->
 400        let s',metasenv' = um_aux metasenv s in
 401        let t',metasenv'' = um_aux metasenv' t in
 402        C.Prod (n, s', t'), metasenv''
 403     | C.Lambda (n,s,t) ->
 404        let s',metasenv' = um_aux metasenv s in
 405        let t',metasenv'' = um_aux metasenv' t in
 406        C.Lambda (n, s', t'), metasenv''
 407     | C.LetIn (n,s,t) ->
 408        let s',metasenv' = um_aux metasenv s in
 409        let t',metasenv'' = um_aux metasenv' t in
 410        C.LetIn (n, s', t'), metasenv''
 411     | C.Appl (he::tl) ->
 412        let tl',metasenv' =
 413         List.fold_right
 414          (fun t (tl,metasenv) ->
 415            let t',metasenv' = um_aux metasenv t in
 416             t'::tl, metasenv'
 417          ) tl ([],metasenv)
 418        in
 419         begin
 420          match um_aux metasenv' he with
 421             (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
 422           | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
 423         end
 424     | C.Appl _ -> assert false
 425     | C.Const (uri,exp_named_subst) ->
 426        let exp_named_subst', metasenv' =
 427         List.fold_right
 428          (fun (uri,t) (tl,metasenv) ->
 429            let t',metasenv' = um_aux metasenv t in
 430             (uri,t')::tl, metasenv'
 431          ) exp_named_subst ([],metasenv)
 432        in
 433         C.Const (uri,exp_named_subst'),metasenv'
 434     | C.MutInd (uri,typeno,exp_named_subst) ->
 435        let exp_named_subst', metasenv' =
 436         List.fold_right
 437          (fun (uri,t) (tl,metasenv) ->
 438            let t',metasenv' = um_aux metasenv t in
 439             (uri,t')::tl, metasenv'
 440          ) exp_named_subst ([],metasenv)
 441        in
 442         C.MutInd (uri,typeno,exp_named_subst'),metasenv'
 443     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 444        let exp_named_subst', metasenv' =
 445         List.fold_right
 446          (fun (uri,t) (tl,metasenv) ->
 447            let t',metasenv' = um_aux metasenv t in
 448             (uri,t')::tl, metasenv'
 449          ) exp_named_subst ([],metasenv)
 450        in
 451         C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
 452     | C.MutCase (sp,i,outty,t,pl) ->
 453        let outty',metasenv' = um_aux metasenv outty in
 454        let t',metasenv'' = um_aux metasenv' t in
 455        let pl',metasenv''' =
 456         List.fold_right
 457          (fun p (pl,metasenv) ->
 458            let p',metasenv' = um_aux metasenv p in
 459             p'::pl, metasenv'
 460          ) pl ([],metasenv'')
 461        in
 462         C.MutCase (sp, i, outty', t', pl'),metasenv'''
 463     | C.Fix (i, fl) ->
 464        let len = List.length fl in
 465        let liftedfl,metasenv' =
 466         List.fold_right
 467          (fun (name, i, ty, bo) (fl,metasenv) ->
 468            let ty',metasenv' = um_aux metasenv ty in
 469            let bo',metasenv'' = um_aux metasenv' bo in
 470             (name, i, ty', bo')::fl,metasenv''
 471          ) fl ([],metasenv)
 472        in
 473         C.Fix (i, liftedfl),metasenv'
 474     | C.CoFix (i, fl) ->
 475        let len = List.length fl in
 476        let liftedfl,metasenv' =
 477         List.fold_right
 478          (fun (name, ty, bo) (fl,metasenv) ->
 479            let ty',metasenv' = um_aux metasenv ty in
 480            let bo',metasenv'' = um_aux metasenv' bo in
 481             (name, ty', bo')::fl,metasenv''
 482          ) fl ([],metasenv)
 483        in
 484         C.CoFix (i, liftedfl),metasenv'
 485  in
 486   let t',metasenv' = um_aux metasenv t in
 487    t',metasenv',!unwinded
 488 ;;
 489
 490 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
 491 (* performs as (apply_subst subst t) until it finds an application of   *)
 492 (* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
 493 (* a new beta-redex; in this case up to [reductions_no] consecutive     *)
 494 (* beta-reductions are performed.                                       *)
 495 (* Hint: this function is usually called when [reductions_no]           *)
 496 (*  eta-expansions have been performed and the head of the new          *)
 497 (*  application has been unified with (META [meta_to_reduce]):          *)
 498 (*  during the unwinding the eta-expansions are undone.                 *)
 499
 500 let apply_subst_reducing subst meta_to_reduce t =
 501  let unwinded = ref subst in
 502  let rec um_aux =
 503   let module C = Cic in
 504   let module S = CicSubstitution in
 505    function
 506       C.Rel _
 507     | C.Var _  as t -> t
 508     | C.Meta (i,l) as t ->
 509        (try
 510          S.lift_meta l (List.assoc i !unwinded)
 511         with Not_found ->
 512           C.Meta (i,l))
 513     | C.Sort _ as t -> t
 514     | C.Implicit as t -> t
 515     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
 516     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
 517     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
 518     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
 519     | C.Appl (he::tl) ->
 520        let tl' = List.map um_aux tl in
 521         let t' =
 522          match um_aux he with
 523             C.Appl l -> C.Appl (l@tl')
 524           | _ as he' -> C.Appl (he'::tl')
 525         in
 526          begin
 527           match meta_to_reduce,he with
 528              Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
 529               let rec beta_reduce =
 530                function
 531                   (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
 532                     let he'' = CicSubstitution.subst he' t in
 533                      if tl' = [] then
 534                       he''
 535                      else
 536                       beta_reduce (n-1,C.Appl(he''::tl'))
 537                 | (_,t) -> t
 538               in
 539                beta_reduce (reductions_no,t')
 540            | _,_ -> t'
 541          end
 542     | C.Appl _ -> assert false
 543     | C.Const (uri,exp_named_subst) ->
 544        let exp_named_subst' =
 545         List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
 546        in
 547         C.Const (uri,exp_named_subst')
 548     | C.MutInd (uri,typeno,exp_named_subst) ->
 549        let exp_named_subst' =
 550         List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
 551        in
 552         C.MutInd (uri,typeno,exp_named_subst')
 553     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 554        let exp_named_subst' =
 555         List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
 556        in
 557         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 558     | C.MutCase (sp,i,outty,t,pl) ->
 559        C.MutCase (sp, i, um_aux outty, um_aux t,
 560         List.map um_aux pl)
 561     | C.Fix (i, fl) ->
 562        let len = List.length fl in
 563        let liftedfl =
 564         List.map
 565          (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
 566           fl
 567        in
 568         C.Fix (i, liftedfl)
 569     | C.CoFix (i, fl) ->
 570        let len = List.length fl in
 571        let liftedfl =
 572         List.map
 573          (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
 574           fl
 575        in
 576         C.CoFix (i, liftedfl)
 577  in
 578    um_aux t
 579 ;;
 580
 581 (* UNWIND THE MGU INSIDE THE MGU *)
 582 let unwind_subst metasenv subst =
 583  let identity_relocation_list_for_metavariable i =
 584   let (_,canonical_context,_) =
 585    List.find (function (m,_,_) -> m=i) metasenv
 586   in
 587    let canonical_context_length = List.length canonical_context in
 588     let rec aux =
 589      function
 590         n when n > canonical_context_length -> []
 591       | n -> (Some (Cic.Rel n))::(aux (n+1))
 592     in
 593      aux 1
 594  in
 595   List.fold_left
 596    (fun (unwinded,metasenv) (i,_) ->
 597      let identity_relocation_list =
 598       identity_relocation_list_for_metavariable i
 599      in
 600       let (_,metasenv',subst') =
 601        unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
 602       in
 603        subst',metasenv'
 604    ) ([],metasenv) subst
 605 ;;
 606
 607 let apply_subst subst t =
 608  (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
 609  let metasenv = [] in
 610   let (t',_,_) = unwind metasenv [] subst t in
 611    t'
 612 ;;
 613
 614 (* A substitution is a (int * Cic.term) list that associates a               *)
 615 (* metavariable i with its body.                                             *)
 616 (* metasenv is of type Cic.metasenv                                          *)
 617 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 618 (* a new substitution which is already unwinded and ready to be applied and  *)
 619 (* a new metasenv in which some hypothesis in the contexts of the            *)
 620 (* metavariables may have been restricted.                                   *)
 621 let fo_unif metasenv context t1 t2 =
 622  let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
 623   unwind_subst metasenv' subst_to_unwind
 624 ;;