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 (*CSC: Vecchia unificazione: exception Impossible;;*)
  28 exception Free;;
  29 exception OccurCheck;;
  30
  31 type substitution = (int * Cic.term) list
  32
  33 (*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *)
  34 (*CSC: lift? O creare una proofEngineSubstitution?                          *)
  35 (* the function delift n m un-lifts a lambda term m of n level of abstractions.
  36    It returns an exception Free if M contains a free variable in the range 1--n *)
  37 let delift n =
  38  let rec deliftaux k =
  39   let module C = Cic in
  40    function
  41       C.Rel m ->
  42        if m < k then C.Rel m else
  43        if m < k+n then raise Free
  44        else C.Rel (m - n)
  45     | C.Var _  as t -> t
  46     | C.Meta _ as t -> t
  47     | C.Sort _ as t -> t
  48     | C.Implicit as t -> t
  49     | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
  50     | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
  51     | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
  52     | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
  53     | C.Appl l -> C.Appl (List.map (deliftaux k) l)
  54     | C.Const _ as t -> t
  55     | C.Abst _  as t -> t
  56     | C.MutInd _ as t -> t
  57     | C.MutConstruct _ as t -> t
  58     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
  59        C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
  60         List.map (deliftaux k) pl)
  61     | C.Fix (i, fl) ->
  62        let len = List.length fl in
  63        let liftedfl =
  64         List.map
  65          (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo))
  66           fl
  67        in
  68         C.Fix (i, liftedfl)
  69     | C.CoFix (i, fl) ->
  70        let len = List.length fl in
  71        let liftedfl =
  72         List.map
  73          (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
  74           fl
  75        in
  76         C.CoFix (i, liftedfl)
  77  in
  78   if n = 0 then
  79    (function t -> t)
  80   else
  81    deliftaux 1
  82 ;;
  83
  84 (* Questa funzione non serve piu'... per il momento la lascio *)
  85 (*
  86 let closed_up_to_n n m =
  87  let rec closed_aux k =
  88   let module C = Cic in
  89    function
  90       C.Rel m -> if m > k then () else raise Free
  91     | C.Var _
  92     | C.Meta _ (* we assume Meta are closed up to k; note that during
  93                   meta-unfolding we shall need to properly lift the
  94                   "body" of Metavariables *)
  95     | C.Sort _
  96     | C.Implicit -> ()
  97     | C.Cast (te,ty) -> closed_aux k te; closed_aux k ty
  98     | C.Prod (n,s,t) -> closed_aux k s; closed_aux (k+1) t
  99     | C.Lambda (n,s,t) -> closed_aux k s; closed_aux (k+1) t
 100     | C.LetIn (n,s,t) -> closed_aux k s; closed_aux (k+1) t
 101     | C.Appl l -> List.iter (closed_aux k) l
 102     | C.Const _
 103     | C.Abst _
 104     | C.MutInd _
 105     | C.MutConstruct _ -> ()
 106     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 107         closed_aux k outty; closed_aux k t;
 108         List.iter (closed_aux k) pl
 109     | C.Fix (i, fl) ->
 110        let len = List.length fl in
 111        List.iter
 112          (fun (name, i, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo)
 113           fl
 114     | C.CoFix (i, fl) ->
 115        let len = List.length fl in
 116        List.iter
 117          (fun (name, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo)
 118           fl
 119  in
 120   if n = 0 then true
 121   else
 122    try closed_aux n m; true
 123    with Free -> false
 124 ;; *)
 125
 126 (* NUOVA UNIFICAZIONE *)
 127 (* A substitution is a (int * Cic.term) list that associates a
 128    metavariable i with its body.
 129    A metaenv is a (int * Cic.term) list that associate a metavariable
 130    i with is type.
 131    fo_unif_new takes a metasenv, a context,
 132    two terms t1 and t2 and gives back a new
 133    substitution which is _NOT_ unwinded. It must be unwinded before
 134    applying it. *)
 135
 136 let fo_unif_new metasenv context t1 t2 =
 137     let module C = Cic in
 138     let module R = CicReduction in
 139     let module S = CicSubstitution in
 140     let rec fo_unif_aux subst k t1 t2 =
 141     match (t1, t2) with
 142       (C.Meta n, C.Meta m) -> if n == m then subst
 143                        else let subst'=
 144                          let tn = try List.assoc n subst
 145                                   with Not_found -> C.Meta n in
 146                          let tm = try List.assoc m subst
 147                                   with Not_found -> C.Meta m in
 148                          (match (tn, tm) with
 149                            (C.Meta n, C.Meta m) -> if n==m then subst
 150                                                  else if n<m
 151                                                  then (m, C.Meta n)::subst
 152                                                  else (n, C.Meta m)::subst
 153                          | (C.Meta n, tm) -> (n, tm)::subst
 154                          | (tn, C.Meta m) -> (m, tn)::subst
 155                          | (tn,tm) -> fo_unif_aux subst 0 tn tm) in
 156                          (* unify types first *)
 157                          let tyn = List.assoc n metasenv in
 158                          let tym = List.assoc m metasenv in
 159                          fo_unif_aux subst' 0 tyn tym
 160        | (C.Meta n, t)
 161        | (t, C.Meta n) ->   (* unify types first *)
 162                             let t' = delift k t in
 163                             let subst' =
 164                             (try fo_unif_aux subst 0 (List.assoc n subst) t'
 165                              with Not_found -> (n, t')::subst) in
 166                             let tyn = List.assoc n metasenv in
 167                             let tyt = CicTypeChecker.type_of_aux' metasenv context t' in
 168                             fo_unif_aux subst' 0 tyn tyt
 169        | (C.Rel _, _)
 170        | (_,  C.Rel _)
 171        | (C.Var _, _)
 172        | (_, C.Var _)
 173        | (C.Sort _ ,_)
 174        | (_, C.Sort _)
 175        | (C.Implicit, _)
 176        | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
 177                             else raise UnificationFailed
 178        | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
 179        | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
 180        | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) ->
 181                            let subst' = fo_unif_aux subst k s1 s2 in
 182                            fo_unif_aux subst' (k+1) t1 t2
 183        | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) ->
 184                                 let subst' = fo_unif_aux subst k s1 s2 in
 185                                 fo_unif_aux subst' (k+1) t1 t2
 186        | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2
 187        | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2)
 188        | (C.Appl l1, C.Appl l2) ->
 189                           let lr1 = List.rev l1 in
 190                           let lr2 = List.rev l2 in
 191                           let rec fo_unif_l subst = function
 192                               [],_
 193                             | _,[] -> assert false
 194                             | ([h1],[h2]) -> fo_unif_aux subst k h1 h2
 195                             | ([h],l)
 196                             | (l,[h]) -> fo_unif_aux subst k h (C.Appl l)
 197                             | ((h1::l1),(h2::l2)) ->
 198                                 let subst' = fo_unif_aux subst k h1 h2 in
 199                                 fo_unif_l subst' (l1,l2)
 200                           in
 201                           fo_unif_l subst (lr1, lr2)
 202        | (C.Const _, _)
 203        | (_, C.Const _)
 204        | (C.Abst _, _)
 205        | (_, C.Abst _)
 206        | (C.MutInd  _, _)
 207        | (_, C.MutInd _)
 208        | (C.MutConstruct _, _)
 209        | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
 210                                    else raise UnificationFailed
 211        | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
 212                       let subst' = fo_unif_aux subst k outt1 outt2 in
 213                       let subst'' = fo_unif_aux subst' k t1 t2 in
 214                       List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2
 215        | (C.Fix _, _)
 216        | (_, C.Fix _)
 217        | (C.CoFix _, _)
 218        | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
 219                            else raise UnificationFailed
 220        | (_,_) -> raise UnificationFailed
 221    in fo_unif_aux [] 0 t1 t2;;
 222
 223 (* VECCHIA UNIFICAZIONE -- molto piu' bella, alas *)
 224 (*
 225 let fo_unif_mgu k t1 t2 mgu =
 226     let module C = Cic in
 227     let module R = CicReduction in
 228     let module S = CicSubstitution in
 229     let rec deref n = match mgu.(n) with
 230          C.Meta m as t -> if n = m then t else (deref m)
 231        | t -> t
 232     in
 233     let rec fo_unif k t1 t2 = match (t1, t2) with
 234        (* aggiungere l'unificazione sui tipi in caso di istanziazione *)
 235          (C.Meta n, C.Meta m) -> if n == m then () else
 236                             let t1' = deref n in
 237                             let t2' = deref m in
 238                             (* deref of metavariables ARE already delifted *)
 239                             (match (t1',t2') with
 240                                (C.Meta n, C.Meta m) -> if n = m then () else
 241                                            if n < m then mgu.(m) <- t1' else
 242                                            if n > m then mgu.(n) <- t2'
 243                              | (C.Meta n, _) -> mgu.(n) <- t2'
 244                              | (_, C.Meta m) -> mgu.(m) <- t1'
 245                              | (_,_) -> fo_unif k t1' t2')
 246        | (C.Meta n, _) ->   let t1' = deref n in
 247                             let t2' =  try delift k t2
 248                                        with Free -> raise UnificationFailed in
 249                             (match t1' with
 250                                C.Meta n -> mgu.(n) <- t2'
 251                              |  _ -> fo_unif k t1' t2')
 252        | (_, C.Meta m) ->   let t2' = deref m in
 253                             let t1' = try delift k t1
 254                                       with Free -> raise UnificationFailed in
 255                             (match t2' with
 256                                C.Meta m -> mgu.(m) <- t1'
 257                              | _ -> fo_unif k t1' t2')
 258        | (C.Rel _, _)
 259        | (_,  C.Rel _)
 260        | (C.Var _, _)
 261        | (_, C.Var _)
 262        | (C.Sort _ ,_)
 263        | (_, C.Sort _)
 264        | (C.Implicit, _)
 265        | (_, C.Implicit) -> if R.are_convertible t1 t2 then ()
 266                             else raise UnificationFailed
 267        | (C.Cast (te,ty), _) -> fo_unif k te t2
 268        | (_, C.Cast (te,ty)) -> fo_unif k t1 te
 269        | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> fo_unif k s1 s2;
 270                                                 fo_unif (k+1) t1 t2
 271        | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> fo_unif k s1 s2;
 272                                                     fo_unif (k+1) t1 t2
 273        | (C.LetIn (_,s1,t1), _) -> fo_unif k (S.subst s1 t1) t2
 274        | (_, C.LetIn (_,s2,t2)) -> fo_unif k t1 (S.subst s2 t2)
 275        | (C.Appl (h1::l1), C.Appl (h2::l2)) ->
 276                           let lr1 = List.rev l1 in
 277                           let lr2 = List.rev l2 in
 278                           let rec fo_unif_aux = function
 279                               ([],l2) -> ([],l2)
 280                             | (l1,[]) -> (l1,[])
 281                             | ((h1::l1),(h2::l2)) -> fo_unif k h1 h2;
 282                                                      fo_unif_aux (l1,l2)
 283                          in
 284                          (match fo_unif_aux (lr1, lr2) with
 285                               ([],[]) -> fo_unif k h1 h2
 286                             | ([],l2) -> fo_unif k h1 (C.Appl (h2::List.rev l2))
 287                             | (l1,[]) -> fo_unif k (C.Appl (h1::List.rev l1)) h2
 288                             | (_,_) -> raise Impossible)
 289        | (C.Const _, _)
 290        | (_, C.Const _)
 291        | (C.Abst _, _)
 292        | (_, C.Abst _)
 293        | (C.MutInd  _, _)
 294        | (_, C.MutInd _)
 295        | (C.MutConstruct _, _)
 296        | (_, C.MutConstruct _) -> print_endline "siamo qui"; flush stdout;
 297                                  if R.are_convertible t1 t2 then ()
 298                                  else raise UnificationFailed
 299        | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
 300                       fo_unif k outt1 outt2;
 301                       fo_unif k t1 t2;
 302                       List.iter2 (fo_unif k) pl1 pl2
 303        | (C.Fix _, _)
 304        | (_, C.Fix _)
 305        | (C.CoFix _, _)
 306        | (_, C.CoFix _) -> if R.are_convertible t1 t2 then ()
 307                            else raise UnificationFailed
 308        | (_,_) -> raise UnificationFailed
 309    in fo_unif k t1 t2;mgu ;;
 310 *)
 311
 312 (* unwind mgu mark m applies mgu to the term m; mark is an array of integers
 313 mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
 314 and is 1 if it has been succesfully unwinded. Meeting the value 2 during
 315 the computation is an error: occur-check *)
 316
 317 let unwind subst unwinded t =
 318  let unwinded = ref unwinded in
 319  let frozen = ref [] in
 320  let rec um_aux k =
 321   let module C = Cic in
 322   let module S = CicSubstitution in
 323    function
 324       C.Rel _ as t -> t
 325     | C.Var _  as t -> t
 326     | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
 327                        with Not_found ->
 328                          if List.mem i !frozen then
 329                            raise OccurCheck
 330                          else
 331                            let saved_frozen = !frozen in
 332                             frozen := i::!frozen ;
 333                             let res =
 334                              try
 335                               let t = List.assoc i subst in
 336                                let t' = um_aux 0 t in
 337                                 unwinded := (i,t)::!unwinded ;
 338                                 S.lift k t'
 339                              with
 340                               Not_found ->
 341                                (* not constrained variable, i.e. free in subst *)
 342                                C.Meta i
 343                             in
 344                              frozen := saved_frozen ;
 345                              res
 346                       )
 347     | C.Sort _ as t -> t
 348     | C.Implicit as t -> t
 349     | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
 350     | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
 351     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
 352     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
 353     | C.Appl (he::tl) ->
 354        let tl' = List.map (um_aux k) tl in
 355         begin
 356          match um_aux k he with
 357             C.Appl l -> C.Appl (l@tl')
 358           | _ as he' -> C.Appl (he'::tl')
 359         end
 360     | C.Appl _ -> assert false
 361     | C.Const _ as t -> t
 362     | C.Abst _  as t -> t
 363     | C.MutInd _ as t -> t
 364     | C.MutConstruct _ as t -> t
 365     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 366        C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
 367         List.map (um_aux k) pl)
 368     | C.Fix (i, fl) ->
 369        let len = List.length fl in
 370        let liftedfl =
 371         List.map
 372          (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
 373           fl
 374        in
 375         C.Fix (i, liftedfl)
 376     | C.CoFix (i, fl) ->
 377        let len = List.length fl in
 378        let liftedfl =
 379         List.map
 380          (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
 381           fl
 382        in
 383         C.CoFix (i, liftedfl)
 384  in
 385    um_aux 0 t,!unwinded
 386 ;;
 387
 388 (*
 389 let unwind_meta mgu mark =
 390  let rec um_aux k =
 391   let module C = Cic in
 392   let module S = CicSubstitution in
 393    function
 394       C.Rel _ as t -> t
 395     | C.Var _  as t -> t
 396     | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else
 397                        if mark.(i)=1 then S.lift k mgu.(i)
 398                        else (match mgu.(i) with
 399                            C.Meta k as t1 -> if k = i then t
 400                                              else (mark.(i) <- 2;
 401                                                    mgu.(i) <- (um_aux 0 t1);
 402                                                    mark.(i) <- 1;
 403                                                    S.lift k mgu.(i))
 404                          | _ -> (mark.(i) <- 2;
 405                                  mgu.(i) <- (um_aux 0 mgu.(i));
 406                                  mark.(i) <- 1;
 407                                  S.lift k mgu.(i)))
 408     | C.Sort _ as t -> t
 409     | C.Implicit as t -> t
 410     | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
 411     | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
 412     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
 413     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
 414     | C.Appl (he::tl) ->
 415        let tl' = List.map (um_aux k) tl in
 416         begin
 417          match um_aux k he with
 418             C.Appl l -> C.Appl (l@tl')
 419           | _ as he' -> C.Appl (he'::tl')
 420         end
 421     | C.Appl _ -> assert false
 422     | C.Const _ as t -> t
 423     | C.Abst _  as t -> t
 424     | C.MutInd _ as t -> t
 425     | C.MutConstruct _ as t -> t
 426     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 427        C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
 428         List.map (um_aux k) pl)
 429     | C.Fix (i, fl) ->
 430        let len = List.length fl in
 431        let liftedfl =
 432         List.map
 433          (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
 434           fl
 435        in
 436         C.Fix (i, liftedfl)
 437     | C.CoFix (i, fl) ->
 438        let len = List.length fl in
 439        let liftedfl =
 440         List.map
 441          (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
 442           fl
 443        in
 444         C.CoFix (i, liftedfl)
 445  in
 446    um_aux 0
 447 ;;
 448 *)
 449
 450 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
 451 (* performs as (apply_subst subst t) until it finds an application of   *)
 452 (* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
 453 (* a new beta-redex; in this case up to [reductions_no] consecutive     *)
 454 (* beta-reductions are performed.                                       *)
 455 (* Hint: this function is usually called when [reductions_no]           *)
 456 (*  eta-expansions have been performed and the head of the new          *)
 457 (*  application has been unified with (META [meta_to_reduce]):          *)
 458 (*  during the unwinding the eta-expansions are undone.                 *)
 459
 460 let apply_subst_reducing subst meta_to_reduce t =
 461  let unwinded = ref subst in
 462  let rec um_aux k =
 463   let module C = Cic in
 464   let module S = CicSubstitution in
 465    function
 466       C.Rel _ as t -> t
 467     | C.Var _  as t -> t
 468     | C.Meta i as t ->
 469        (try
 470          S.lift k (List.assoc i !unwinded)
 471         with Not_found ->
 472           C.Meta i)
 473     | C.Sort _ as t -> t
 474     | C.Implicit as t -> t
 475     | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
 476     | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
 477     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
 478     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
 479     | C.Appl (he::tl) ->
 480        let tl' = List.map (um_aux k) tl in
 481         let t' =
 482          match um_aux k he with
 483             C.Appl l -> C.Appl (l@tl')
 484           | _ as he' -> C.Appl (he'::tl')
 485         in
 486          begin
 487           match meta_to_reduce with
 488              Some (mtr,reductions_no) when he = C.Meta mtr ->
 489               let rec beta_reduce =
 490                function
 491                   (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
 492                     let he'' = CicSubstitution.subst he' t in
 493                      if tl' = [] then
 494                       he''
 495                      else
 496                       beta_reduce (n-1,C.Appl(he''::tl'))
 497                 | (_,t) -> t
 498               in
 499                beta_reduce (reductions_no,t')
 500            | _ -> t'
 501          end
 502     | C.Appl _ -> assert false
 503     | C.Const _ as t -> t
 504     | C.Abst _  as t -> t
 505     | C.MutInd _ as t -> t
 506     | C.MutConstruct _ as t -> t
 507     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 508        C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
 509         List.map (um_aux k) pl)
 510     | C.Fix (i, fl) ->
 511        let len = List.length fl in
 512        let liftedfl =
 513         List.map
 514          (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
 515           fl
 516        in
 517         C.Fix (i, liftedfl)
 518     | C.CoFix (i, fl) ->
 519        let len = List.length fl in
 520        let liftedfl =
 521         List.map
 522          (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
 523           fl
 524        in
 525         C.CoFix (i, liftedfl)
 526  in
 527    um_aux 0 t
 528 ;;
 529
 530 (* unwind mgu mark mm m applies mgu to the term m; mark is an array of integers
 531 mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
 532 and is 1 if it has been succesfully unwinded. Meeting the value 2 during
 533 the computation is an error: occur-check. When the META mm is to be unfolded
 534 and it is applied to something, one-step beta reduction is performed just
 535 after the unfolding. *)
 536
 537 (*
 538 let unwind_meta_reducing mgu mark meta_to_reduce =
 539  let rec um_aux k =
 540   let module C = Cic in
 541   let module S = CicSubstitution in
 542    function
 543       C.Rel _ as t -> t
 544     | C.Var _  as t -> t
 545     | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else
 546                        if mark.(i)=1 then S.lift k mgu.(i)
 547                        else (match mgu.(i) with
 548                            C.Meta k as t1 -> if k = i then t
 549                                              else (mark.(i) <- 2;
 550                                                    mgu.(i) <- (um_aux 0 t1);
 551                                                    mark.(i) <- 1;
 552                                                    S.lift k mgu.(i))
 553                          | _ -> (mark.(i) <- 2;
 554                                  mgu.(i) <- (um_aux 0 mgu.(i));
 555                                  mark.(i) <- 1;
 556                                  S.lift k mgu.(i)))
 557     | C.Sort _ as t -> t
 558     | C.Implicit as t -> t
 559     | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
 560     | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
 561     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
 562     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
 563     | C.Appl (he::tl) ->
 564        let tl' = List.map (um_aux k) tl in
 565         let t' =
 566          match um_aux k he with
 567             C.Appl l -> C.Appl (l@tl')
 568           | _ as he' -> C.Appl (he'::tl')
 569         in
 570          begin
 571           match t', meta_to_reduce with
 572              (C.Appl (C.Lambda (n,s,t)::he'::tl')),Some mtr
 573                when he = C.Meta mtr ->
 574 (*CSC: Sbagliato!!! Effettua beta riduzione solo del primo argomento
 575  *CSC: mentre dovrebbe farla dei primi n, dove n sono quelli eta-astratti
 576 *)
 577                 C.Appl((CicSubstitution.subst he' t)::tl')
 578            | _ -> t'
 579          end
 580     | C.Appl _ -> assert false
 581     | C.Const _ as t -> t
 582     | C.Abst _  as t -> t
 583     | C.MutInd _ as t -> t
 584     | C.MutConstruct _ as t -> t
 585     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 586        C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
 587         List.map (um_aux k) pl)
 588     | C.Fix (i, fl) ->
 589        let len = List.length fl in
 590        let liftedfl =
 591         List.map
 592          (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
 593           fl
 594        in
 595         C.Fix (i, liftedfl)
 596     | C.CoFix (i, fl) ->
 597        let len = List.length fl in
 598        let liftedfl =
 599         List.map
 600          (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
 601           fl
 602        in
 603         C.CoFix (i, liftedfl)
 604  in
 605    um_aux 0
 606 ;; *)
 607
 608 (* UNWIND THE MGU INSIDE THE MGU *)
 609 (* let unwind mgu =
 610     let mark = Array.make (Array.length mgu) 0 in
 611     Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *)
 612
 613 let unwind_subst subst =
 614   List.fold_left
 615    (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst
 616 ;;
 617
 618 let apply_subst subst t =
 619     fst (unwind [] subst t)
 620 ;;
 621
 622 (* A substitution is a (int * Cic.term) list that associates a
 623    metavariable i with its body.
 624    A metaenv is a (int * Cic.term) list that associate a metavariable
 625    i with is type.
 626    fo_unif takes a metasenv, a context,
 627    two terms t1 and t2 and gives back a new
 628    substitution which is already unwinded and ready to be applied. *)
 629 let fo_unif metasenv context t1 t2 =
 630  let subst_to_unwind = fo_unif_new metasenv context t1 t2 in
 631   unwind_subst subst_to_unwind
 632 ;;