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