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