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 _ as t -> t
 107      | C.Abst _  as t -> t
 108      | C.MutInd _ as t -> t
 109      | C.MutConstruct _ as t -> t
 110      | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 111         C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
 112          List.map (deliftaux k) pl)
 113      | C.Fix (i, fl) ->
 114         let len = List.length fl in
 115         let liftedfl =
 116          List.map
 117           (fun (name, i, ty, bo) ->
 118            (name, i, deliftaux k ty, deliftaux (k+len) bo))
 119            fl
 120         in
 121          C.Fix (i, liftedfl)
 122      | C.CoFix (i, fl) ->
 123         let len = List.length fl in
 124         let liftedfl =
 125          List.map
 126           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 127            fl
 128         in
 129          C.CoFix (i, liftedfl)
 130   in
 131     let res = deliftaux 0 t in
 132     res, restrict !to_be_restricted metasenv
 133 ;;
 134
 135 (**** END OF DELIFT ****)
 136
 137 type substitution = (int * Cic.term) list
 138
 139 (* NUOVA UNIFICAZIONE *)
 140 (* A substitution is a (int * Cic.term) list that associates a
 141    metavariable i with its body.
 142    A metaenv is a (int * Cic.term) list that associate a metavariable
 143    i with is type.
 144    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 145    a new substitution which is _NOT_ unwinded. It must be unwinded before
 146    applying it. *)
 147
 148 let fo_unif_new metasenv context t1 t2 =
 149     let module C = Cic in
 150     let module R = CicReduction in
 151     let module S = CicSubstitution in
 152     let rec fo_unif_aux subst context metasenv t1 t2 =
 153     match (t1, t2) with
 154          (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 155            let ok =
 156             List.fold_left2
 157              (fun b t1 t2 ->
 158                b &&
 159                 match t1,t2 with
 160                   None,_
 161                 | _,None -> true
 162                 | Some t1', Some t2' ->
 163                    (* First possibility:  restriction    *)
 164                    (* Second possibility: unification    *)
 165                    (* Third possibility:  convertibility *)
 166                    R.are_convertible context t1' t2'
 167              ) true ln lm
 168            in
 169             if ok then subst,metasenv else
 170              raise UnificationFailed
 171        | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
 172            fo_unif_aux subst context metasenv t2 t1
 173        | (C.Meta (n,l), t)
 174        | (t, C.Meta (n,l)) ->
 175            let subst',metasenv' =
 176              try
 177                let oldt = (List.assoc n subst) in
 178                let lifted_oldt = S.lift_meta l oldt in
 179                fo_unif_aux subst context metasenv lifted_oldt t
 180              with Not_found ->
 181 prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ;
 182 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
 183 prerr_endline "<DELIFT2" ; flush stderr ;
 184                let t',metasenv' = delift context metasenv l t in
 185                (n, t')::subst, metasenv'
 186            in
 187             let (_,_,meta_type) =
 188               List.find (function (m,_,_) -> m=n) metasenv' in
 189             let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
 190              fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt
 191        | (C.Rel _, _)
 192        | (_,  C.Rel _)
 193        | (C.Var _, _)
 194        | (_, C.Var _)
 195        | (C.Sort _ ,_)
 196        | (_, C.Sort _)
 197        | (C.Implicit, _)
 198        | (_, C.Implicit) ->
 199            if R.are_convertible context t1 t2 then subst, metasenv
 200            else raise UnificationFailed
 201        | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2
 202        | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te
 203        | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 204            let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in
 205            fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 206        | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 207            let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in
 208            fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 209        | (C.LetIn (_,s1,t1), t2)
 210        | (t2, C.LetIn (_,s1,t1)) ->
 211            fo_unif_aux subst context metasenv t2 (S.subst s1 t1)
 212        | (C.Appl l1, C.Appl l2) ->
 213            let lr1 = List.rev l1 in
 214            let lr2 = List.rev l2 in
 215            let rec fo_unif_l subst metasenv = function
 216                [],_
 217              | _,[] -> assert false
 218              | ([h1],[h2]) ->
 219                  fo_unif_aux subst context metasenv h1 h2
 220              | ([h],l)
 221              | (l,[h]) ->
 222                  fo_unif_aux subst context metasenv h (C.Appl (List.rev l))
 223              | ((h1::l1),(h2::l2)) ->
 224                  let subst', metasenv' =
 225                    fo_unif_aux subst context metasenv h1 h2
 226                  in
 227                  fo_unif_l subst' metasenv' (l1,l2)
 228            in
 229             fo_unif_l subst metasenv (lr1, lr2)
 230        | (C.Const _, _)
 231        | (_, C.Const _)
 232        | (C.Abst _, _)
 233        | (_, C.Abst _)
 234        | (C.MutInd  _, _)
 235        | (_, C.MutInd _)
 236        | (C.MutConstruct _, _)
 237        | (_, C.MutConstruct _) ->
 238            if R.are_convertible context t1 t2 then subst, metasenv
 239            else raise UnificationFailed
 240        | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
 241          let subst', metasenv' =
 242            fo_unif_aux subst context metasenv outt1 outt2 in
 243          let subst'',metasenv'' =
 244            fo_unif_aux subst' context metasenv' t1 t2 in
 245          List.fold_left2
 246            (function (subst,metasenv) ->
 247              fo_unif_aux subst context metasenv
 248            ) (subst'',metasenv'') pl1 pl2
 249        | (C.Fix _, _)
 250        | (_, C.Fix _)
 251        | (C.CoFix _, _)
 252        | (_, C.CoFix _) ->
 253            if R.are_convertible context t1 t2 then subst, metasenv
 254            else raise UnificationFailed
 255        | (_,_) -> raise UnificationFailed
 256    in fo_unif_aux [] context metasenv t1 t2;;
 257
 258 (*CSC: ???????????????
 259 (* m is the index of a metavariable to restrict, k is nesting depth
 260 of the occurrence m, and l is its relocation list. canonical_context
 261 is the context of the metavariable we are instantiating - containing
 262 m - Only rel in the domain of canonical_context are accessible.
 263 This function takes in input a metasenv and gives back a metasenv.
 264 A rel(j) in the canonical context of m, is rel(List.nth l j) for the
 265 instance of m under consideration, that is rel (List.nth l j) - k
 266 in canonical_context. *)
 267
 268 let restrict canonical_context m k l =
 269   let rec erase i =
 270     function
 271         [] -> []
 272       | None::tl -> None::(erase (i+1) tl)
 273       | he::tl ->
 274           let i' = (List.nth l (i-1)) in
 275           if i' <= k
 276            then he::(erase (i+1) tl) (* local variable *)
 277            else
 278             let acc =
 279               (try List.nth canonical_context (i'-k-1)
 280                with Failure _ -> None) in
 281             if acc = None
 282              then None::(erase (i+1) tl)
 283              else he::(erase (i+1) tl) in
 284   let rec aux =
 285     function
 286         [] -> []
 287       | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
 288       | hd::tl -> hd::(aux tl)
 289   in
 290    aux
 291 ;;
 292
 293
 294 let check_accessibility metasenv i =
 295   let module C = Cic in
 296   let module S = CicSubstitution in
 297   let (_,canonical_context,_) =
 298     List.find (function (m,_,_) -> m=i) metasenv in
 299    List.map
 300     (function t ->
 301       let =
 302        delift canonical_context metasenv ? t
 303     ) canonical_context
 304 CSCSCS
 305
 306
 307
 308   let rec aux metasenv k =
 309     function
 310       C.Rel i ->
 311        if i <= k then
 312         metasenv
 313        else
 314         (try
 315           match List.nth canonical_context (i-k-1) with
 316             Some (_,C.Decl t)
 317           | Some (_,C.Def t) -> aux metasenv k (S.lift i t)
 318           | None -> raise RelToHiddenHypothesis
 319           with
 320            Failure _ -> raise OpenTerm
 321         )
 322     | C.Var _  -> metasenv
 323     | C.Meta (i,l) -> restrict canonical_context i k l metasenv
 324     | C.Sort _ -> metasenv
 325     | C.Implicit -> metasenv
 326     | C.Cast (te,ty) ->
 327         let metasenv' = aux metasenv k te in
 328         aux metasenv' k ty
 329     | C.Prod (_,s,t)
 330     | C.Lambda (_,s,t)
 331     | C.LetIn (_,s,t) ->
 332         let metasenv' = aux metasenv k s in
 333         aux metasenv' (k+1) t
 334     | C.Appl l ->
 335         List.fold_left
 336           (function metasenv -> aux metasenv k) metasenv l
 337     | C.Const _
 338     | C.Abst _
 339     | C.MutInd _
 340     | C.MutConstruct _ -> metasenv
 341     | C.MutCase (_,_,_,outty,t,pl) ->
 342         let metasenv' = aux metasenv k outty in
 343         let metasenv'' = aux metasenv' k t in
 344         List.fold_left
 345           (function metasenv -> aux metasenv k) metasenv'' pl
 346     | C.Fix (i, fl) ->
 347        let len = List.length fl in
 348        List.fold_left
 349          (fun metasenv f ->
 350            let (_,_,ty,bo) = f in
 351            let metasenv' = aux metasenv k ty in
 352            aux metasenv' (k+len) bo
 353          ) metasenv fl
 354     | C.CoFix (i, fl) ->
 355         let len = List.length fl in
 356         List.fold_left
 357          (fun metasenv f ->
 358            let (_,ty,bo) = f in
 359            let metasenv' = aux metasenv k ty in
 360            aux metasenv' (k+len) bo
 361          ) metasenv fl
 362   in aux metasenv 0
 363 ;;
 364 *)
 365
 366
 367 let unwind metasenv subst unwinded t =
 368  let unwinded = ref unwinded in
 369  let frozen = ref [] in
 370  let rec um_aux metasenv =
 371   let module C = Cic in
 372   let module S = CicSubstitution in
 373    function
 374       C.Rel _ as t -> t,metasenv
 375     | C.Var _  as t -> t,metasenv
 376     | C.Meta (i,l) ->
 377         (try
 378           S.lift_meta l (List.assoc i !unwinded), metasenv
 379          with Not_found ->
 380            if List.mem i !frozen then raise OccurCheck
 381            else
 382             let saved_frozen = !frozen in
 383             frozen := i::!frozen ;
 384             let res =
 385              try
 386               let t = List.assoc i subst in
 387               let t',metasenv' = um_aux metasenv t in
 388               let _,metasenv'' =
 389                let (_,canonical_context,_) =
 390                 List.find (function (m,_,_) -> m=i) metasenv
 391                in
 392 prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ;
 393 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
 394 prerr_endline "<DELIFT" ; flush stderr ;
 395                 delift canonical_context metasenv' l t'
 396               in
 397                unwinded := (i,t')::!unwinded ;
 398                S.lift_meta l t', metasenv'
 399              with
 400               Not_found ->
 401                (* not constrained variable, i.e. free in subst*)
 402                let l',metasenv' =
 403                 List.fold_right
 404                  (fun t (tl,metasenv) ->
 405                    match t with
 406                       None -> None::tl,metasenv
 407                     | Some t ->
 408                        let t',metasenv' = um_aux metasenv t in
 409                         (Some t')::tl, metasenv'
 410                  ) l ([],metasenv)
 411                in
 412                 C.Meta (i,l'), metasenv'
 413             in
 414             frozen := saved_frozen ;
 415             res
 416         )
 417     | C.Sort _
 418     | C.Implicit as t -> t,metasenv
 419     | C.Cast (te,ty) ->
 420        let te',metasenv' = um_aux metasenv te in
 421        let ty',metasenv'' = um_aux metasenv' ty in
 422        C.Cast (te',ty'),metasenv''
 423     | C.Prod (n,s,t) ->
 424        let s',metasenv' = um_aux metasenv s in
 425        let t',metasenv'' = um_aux metasenv' t in
 426        C.Prod (n, s', t'), metasenv''
 427     | C.Lambda (n,s,t) ->
 428        let s',metasenv' = um_aux metasenv s in
 429        let t',metasenv'' = um_aux metasenv' t in
 430        C.Lambda (n, s', t'), metasenv''
 431     | C.LetIn (n,s,t) ->
 432        let s',metasenv' = um_aux metasenv s in
 433        let t',metasenv'' = um_aux metasenv' t in
 434        C.LetIn (n, s', t'), metasenv''
 435     | C.Appl (he::tl) ->
 436        let tl',metasenv' =
 437         List.fold_right
 438          (fun t (tl,metasenv) ->
 439            let t',metasenv' = um_aux metasenv t in
 440             t'::tl, metasenv'
 441          ) tl ([],metasenv)
 442        in
 443         begin
 444          match um_aux metasenv' he with
 445             (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
 446           | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
 447         end
 448     | C.Appl _ -> assert false
 449     | C.Const _
 450     | C.Abst _
 451     | C.MutInd _
 452     | C.MutConstruct _ as t -> t,metasenv
 453     | C.MutCase (sp,cookingsno,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, cookingsno, 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  let unwinded = ref subst in
 503  let rec um_aux =
 504   let module C = Cic in
 505   let module S = CicSubstitution in
 506    function
 507       C.Rel _
 508     | C.Var _  as t -> t
 509     | C.Meta (i,l) as t ->
 510        (try
 511          S.lift_meta l (List.assoc i !unwinded)
 512         with Not_found ->
 513           C.Meta (i,l))
 514     | C.Sort _ as t -> t
 515     | C.Implicit as t -> t
 516     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
 517     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
 518     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
 519     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
 520     | C.Appl (he::tl) ->
 521        let tl' = List.map um_aux tl in
 522         let t' =
 523          match um_aux he with
 524             C.Appl l -> C.Appl (l@tl')
 525           | _ as he' -> C.Appl (he'::tl')
 526         in
 527          begin
 528           match meta_to_reduce,he with
 529              Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
 530               let rec beta_reduce =
 531                function
 532                   (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
 533                     let he'' = CicSubstitution.subst he' t in
 534                      if tl' = [] then
 535                       he''
 536                      else
 537                       beta_reduce (n-1,C.Appl(he''::tl'))
 538                 | (_,t) -> t
 539               in
 540                beta_reduce (reductions_no,t')
 541            | _,_ -> t'
 542          end
 543     | C.Appl _ -> assert false
 544     | C.Const _ as t -> t
 545     | C.Abst _  as t -> t
 546     | C.MutInd _ as t -> t
 547     | C.MutConstruct _ as t -> t
 548     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 549        C.MutCase (sp, cookingsno, i, um_aux outty, um_aux t,
 550         List.map um_aux pl)
 551     | C.Fix (i, fl) ->
 552        let len = List.length fl in
 553        let liftedfl =
 554         List.map
 555          (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
 556           fl
 557        in
 558         C.Fix (i, liftedfl)
 559     | C.CoFix (i, fl) ->
 560        let len = List.length fl in
 561        let liftedfl =
 562         List.map
 563          (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
 564           fl
 565        in
 566         C.CoFix (i, liftedfl)
 567  in
 568    um_aux t
 569 ;;
 570
 571 (* UNWIND THE MGU INSIDE THE MGU *)
 572 let unwind_subst metasenv subst =
 573  let identity_relocation_list_for_metavariable i =
 574   let (_,canonical_context,_) =
 575    List.find (function (m,_,_) -> m=i) metasenv
 576   in
 577    let canonical_context_length = List.length canonical_context in
 578     let rec aux =
 579      function
 580         n when n > canonical_context_length -> []
 581       | n -> (Some (Cic.Rel n))::(aux (n+1))
 582     in
 583      aux 1
 584  in
 585   List.fold_left
 586    (fun (unwinded,metasenv) (i,_) ->
 587      let identity_relocation_list =
 588       identity_relocation_list_for_metavariable i
 589      in
 590       let (_,metasenv',subst') =
 591        unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
 592       in
 593        subst',metasenv'
 594    ) ([],metasenv) subst
 595 ;;
 596
 597 let apply_subst subst t =
 598  (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
 599  let metasenv = [] in
 600   let (t',_,_) = unwind metasenv [] subst t in
 601    t'
 602 ;;
 603
 604 (* A substitution is a (int * Cic.term) list that associates a               *)
 605 (* metavariable i with its body.                                             *)
 606 (* metasenv is of type Cic.metasenv                                          *)
 607 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 608 (* a new substitution which is already unwinded and ready to be applied and  *)
 609 (* a new metasenv in which some hypothesis in the contexts of the            *)
 610 (* metavariables may have been restricted.                                   *)
 611 let fo_unif metasenv context t1 t2 =
 612 prerr_endline "INIZIO FASE 1" ; flush stderr ;
 613  let subst_to_unwind,metasenv' = fo_unif_new metasenv context t1 t2 in
 614 prerr_endline "FINE FASE 1" ; flush stderr ;
 615 let res =
 616   unwind_subst metasenv' subst_to_unwind
 617 in
 618 prerr_endline "FINE FASE 2" ; flush stderr ; res
 619 ;;