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