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
  30 type substitution = (int * Cic.term) list
  31
  32 (*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *)
  33 (*CSC: lift? O creare una proofEngineSubstitution?                          *)
  34 (* the function delift n m un-lifts a lambda term m of n level of abstractions.
  35    It returns an exception Free if M contains a free variable in the range 1--n *)
  36 let delift n =
  37  let rec deliftaux k =
  38   let module C = Cic in
  39    function
  40       C.Rel m ->
  41        if m < k then C.Rel m else
  42        if m < k+n then raise Free
  43        else C.Rel (m - n)
  44     | C.Var _  as t -> t
  45     | C.Meta _ as t -> t
  46     | C.Sort _ as t -> t
  47     | C.Implicit as t -> t
  48     | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
  49     | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
  50     | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
  51     | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
  52     | C.Appl l -> C.Appl (List.map (deliftaux k) l)
  53     | C.Const _ as t -> t
  54     | C.Abst _  as t -> t
  55     | C.MutInd _ as t -> t
  56     | C.MutConstruct _ as t -> t
  57     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
  58        C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
  59         List.map (deliftaux k) pl)
  60     | C.Fix (i, fl) ->
  61        let len = List.length fl in
  62        let liftedfl =
  63         List.map
  64          (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo))
  65           fl
  66        in
  67         C.Fix (i, liftedfl)
  68     | C.CoFix (i, fl) ->
  69        let len = List.length fl in
  70        let liftedfl =
  71         List.map
  72          (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
  73           fl
  74        in
  75         C.CoFix (i, liftedfl)
  76  in
  77   if n = 0 then
  78    (function t -> t)
  79   else
  80    deliftaux 1
  81 ;;
  82
  83 (* NUOVA UNIFICAZIONE *)
  84 (* A substitution is a (int * Cic.term) list that associates a
  85    metavariable i with its body.
  86    A metaenv is a (int * Cic.term) list that associate a metavariable
  87    i with is type.
  88    fo_unif_new takes a metasenv, a context,
  89    two terms t1 and t2 and gives back a new
  90    substitution which is _NOT_ unwinded. It must be unwinded before
  91    applying it. *)
  92
  93 let fo_unif_new metasenv context t1 t2 =
  94     let module C = Cic in
  95     let module R = CicReduction in
  96     let module S = CicSubstitution in
  97     let rec fo_unif_aux subst k t1 t2 =
  98     match (t1, t2) with
  99       (C.Meta n, C.Meta m) -> if n == m then subst
 100                        else let subst'=
 101                          let tn = try List.assoc n subst
 102                                   with Not_found -> C.Meta n in
 103                          let tm = try List.assoc m subst
 104                                   with Not_found -> C.Meta m in
 105                          (match (tn, tm) with
 106                            (C.Meta n, C.Meta m) -> if n==m then subst
 107                                                  else if n<m
 108                                                  then (m, C.Meta n)::subst
 109                                                  else (n, C.Meta m)::subst
 110                          | (C.Meta n, tm) -> (n, tm)::subst
 111                          | (tn, C.Meta m) -> (m, tn)::subst
 112                          | (tn,tm) -> fo_unif_aux subst 0 tn tm) in
 113                          (* unify types first *)
 114                          let tyn = List.assoc n metasenv in
 115                          let tym = List.assoc m metasenv in
 116                          fo_unif_aux subst' 0 tyn tym
 117        | (C.Meta n, t)
 118        | (t, C.Meta n) ->   (* unify types first *)
 119                             let t' = delift k t in
 120                             let subst' =
 121                             (try fo_unif_aux subst 0 (List.assoc n subst) t'
 122                              with Not_found -> (n, t')::subst) in
 123                             let tyn = List.assoc n metasenv in
 124                             let tyt = CicTypeChecker.type_of_aux' metasenv context t' in
 125                             fo_unif_aux subst' 0 tyn tyt
 126        | (C.Rel _, _)
 127        | (_,  C.Rel _)
 128        | (C.Var _, _)
 129        | (_, C.Var _)
 130        | (C.Sort _ ,_)
 131        | (_, C.Sort _)
 132        | (C.Implicit, _)
 133        | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
 134                             else raise UnificationFailed
 135        | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
 136        | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
 137        | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) ->
 138                            let subst' = fo_unif_aux subst k s1 s2 in
 139                            fo_unif_aux subst' (k+1) t1 t2
 140        | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) ->
 141                                 let subst' = fo_unif_aux subst k s1 s2 in
 142                                 fo_unif_aux subst' (k+1) t1 t2
 143        | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2
 144        | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2)
 145        | (C.Appl l1, C.Appl l2) ->
 146                           let lr1 = List.rev l1 in
 147                           let lr2 = List.rev l2 in
 148                           let rec fo_unif_l subst = function
 149                               [],_
 150                             | _,[] -> assert false
 151                             | ([h1],[h2]) -> fo_unif_aux subst k h1 h2
 152                             | ([h],l)
 153                             | (l,[h]) -> fo_unif_aux subst k h (C.Appl l)
 154                             | ((h1::l1),(h2::l2)) ->
 155                                 let subst' = fo_unif_aux subst k h1 h2 in
 156                                 fo_unif_l subst' (l1,l2)
 157                           in
 158                           fo_unif_l subst (lr1, lr2)
 159        | (C.Const _, _)
 160        | (_, C.Const _)
 161        | (C.Abst _, _)
 162        | (_, C.Abst _)
 163        | (C.MutInd  _, _)
 164        | (_, C.MutInd _)
 165        | (C.MutConstruct _, _)
 166        | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
 167                                    else raise UnificationFailed
 168        | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
 169                       let subst' = fo_unif_aux subst k outt1 outt2 in
 170                       let subst'' = fo_unif_aux subst' k t1 t2 in
 171                       List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2
 172        | (C.Fix _, _)
 173        | (_, C.Fix _)
 174        | (C.CoFix _, _)
 175        | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
 176                            else raise UnificationFailed
 177        | (_,_) -> raise UnificationFailed
 178    in fo_unif_aux [] 0 t1 t2;;
 179
 180 (* unwind mgu mark m applies mgu to the term m; mark is an array of integers
 181 mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
 182 and is 1 if it has been succesfully unwinded. Meeting the value 2 during
 183 the computation is an error: occur-check *)
 184
 185 let unwind subst unwinded t =
 186  let unwinded = ref unwinded in
 187  let frozen = ref [] in
 188  let rec um_aux k =
 189   let module C = Cic in
 190   let module S = CicSubstitution in
 191    function
 192       C.Rel _ as t -> t
 193     | C.Var _  as t -> t
 194     | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
 195                        with Not_found ->
 196                          if List.mem i !frozen then
 197                            raise OccurCheck
 198                          else
 199                            let saved_frozen = !frozen in
 200                             frozen := i::!frozen ;
 201                             let res =
 202                              try
 203                               let t = List.assoc i subst in
 204                                let t' = um_aux 0 t in
 205                                 unwinded := (i,t)::!unwinded ;
 206                                 S.lift k t'
 207                              with
 208                               Not_found ->
 209                                (* not constrained variable, i.e. free in subst *)
 210                                C.Meta i
 211                             in
 212                              frozen := saved_frozen ;
 213                              res
 214                       )
 215     | C.Sort _ as t -> t
 216     | C.Implicit as t -> t
 217     | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
 218     | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
 219     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
 220     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
 221     | C.Appl (he::tl) ->
 222        let tl' = List.map (um_aux k) tl in
 223         begin
 224          match um_aux k he with
 225             C.Appl l -> C.Appl (l@tl')
 226           | _ as he' -> C.Appl (he'::tl')
 227         end
 228     | C.Appl _ -> assert false
 229     | C.Const _ as t -> t
 230     | C.Abst _  as t -> t
 231     | C.MutInd _ as t -> t
 232     | C.MutConstruct _ as t -> t
 233     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 234        C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
 235         List.map (um_aux k) pl)
 236     | C.Fix (i, fl) ->
 237        let len = List.length fl in
 238        let liftedfl =
 239         List.map
 240          (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
 241           fl
 242        in
 243         C.Fix (i, liftedfl)
 244     | C.CoFix (i, fl) ->
 245        let len = List.length fl in
 246        let liftedfl =
 247         List.map
 248          (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
 249           fl
 250        in
 251         C.CoFix (i, liftedfl)
 252  in
 253    um_aux 0 t,!unwinded
 254 ;;
 255
 256 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
 257 (* performs as (apply_subst subst t) until it finds an application of   *)
 258 (* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
 259 (* a new beta-redex; in this case up to [reductions_no] consecutive     *)
 260 (* beta-reductions are performed.                                       *)
 261 (* Hint: this function is usually called when [reductions_no]           *)
 262 (*  eta-expansions have been performed and the head of the new          *)
 263 (*  application has been unified with (META [meta_to_reduce]):          *)
 264 (*  during the unwinding the eta-expansions are undone.                 *)
 265
 266 let apply_subst_reducing subst meta_to_reduce t =
 267  let unwinded = ref subst in
 268  let rec um_aux k =
 269   let module C = Cic in
 270   let module S = CicSubstitution in
 271    function
 272       C.Rel _ as t -> t
 273     | C.Var _  as t -> t
 274     | C.Meta i as t ->
 275        (try
 276          S.lift k (List.assoc i !unwinded)
 277         with Not_found ->
 278           C.Meta i)
 279     | C.Sort _ as t -> t
 280     | C.Implicit as t -> t
 281     | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
 282     | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
 283     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
 284     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
 285     | C.Appl (he::tl) ->
 286        let tl' = List.map (um_aux k) tl in
 287         let t' =
 288          match um_aux k he with
 289             C.Appl l -> C.Appl (l@tl')
 290           | _ as he' -> C.Appl (he'::tl')
 291         in
 292          begin
 293           match meta_to_reduce with
 294              Some (mtr,reductions_no) when he = C.Meta mtr ->
 295               let rec beta_reduce =
 296                function
 297                   (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
 298                     let he'' = CicSubstitution.subst he' t in
 299                      if tl' = [] then
 300                       he''
 301                      else
 302                       beta_reduce (n-1,C.Appl(he''::tl'))
 303                 | (_,t) -> t
 304               in
 305                beta_reduce (reductions_no,t')
 306            | _ -> t'
 307          end
 308     | C.Appl _ -> assert false
 309     | C.Const _ as t -> t
 310     | C.Abst _  as t -> t
 311     | C.MutInd _ as t -> t
 312     | C.MutConstruct _ as t -> t
 313     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 314        C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
 315         List.map (um_aux k) pl)
 316     | C.Fix (i, fl) ->
 317        let len = List.length fl in
 318        let liftedfl =
 319         List.map
 320          (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
 321           fl
 322        in
 323         C.Fix (i, liftedfl)
 324     | C.CoFix (i, fl) ->
 325        let len = List.length fl in
 326        let liftedfl =
 327         List.map
 328          (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
 329           fl
 330        in
 331         C.CoFix (i, liftedfl)
 332  in
 333    um_aux 0 t
 334 ;;
 335
 336 (* UNWIND THE MGU INSIDE THE MGU *)
 337 (* let unwind mgu =
 338     let mark = Array.make (Array.length mgu) 0 in
 339     Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *)
 340
 341 let unwind_subst subst =
 342   List.fold_left
 343    (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst
 344 ;;
 345
 346 let apply_subst subst t =
 347     fst (unwind [] subst t)
 348 ;;
 349
 350 (* A substitution is a (int * Cic.term) list that associates a
 351    metavariable i with its body.
 352    A metaenv is a (int * Cic.term) list that associate a metavariable
 353    i with is type.
 354    fo_unif takes a metasenv, a context,
 355    two terms t1 and t2 and gives back a new
 356    substitution which is already unwinded and ready to be applied. *)
 357 let fo_unif metasenv context t1 t2 =
 358  let subst_to_unwind = fo_unif_new metasenv context t1 t2 in
 359   unwind_subst subst_to_unwind
 360 ;;