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