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