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