helm/ocaml/cic_proof_checking/cicSubstitution.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 CannotSubstInMeta;;
  27 exception RelToHiddenHypothesis;;
  28 exception ReferenceToVariable;;
  29 exception ReferenceToConstant;;
  30 exception ReferenceToCurrentProof;;
  31 exception ReferenceToInductiveDefinition;;
  32
  33 let debug_print = fun _ -> ()
  34
  35 let lift_from k n =
  36  let rec liftaux k =
  37   let module C = Cic in
  38    function
  39       C.Rel m ->
  40        if m < k then
  41         C.Rel m
  42        else
  43         C.Rel (m + n)
  44     | C.Var (uri,exp_named_subst) ->
  45        let exp_named_subst' =
  46         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  47        in
  48         C.Var (uri,exp_named_subst')
  49     | C.Meta (i,l) ->
  50        let l' =
  51         List.map
  52          (function
  53              None -> None
  54            | Some t -> Some (liftaux k t)
  55          ) l
  56        in
  57         C.Meta(i,l')
  58     | C.Sort _ as t -> t
  59     | C.Implicit _ as t -> t
  60     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
  61     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
  62     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
  63     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
  64     | C.Appl l -> C.Appl (List.map (liftaux k) l)
  65     | C.Const (uri,exp_named_subst) ->
  66        let exp_named_subst' =
  67         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  68        in
  69         C.Const (uri,exp_named_subst')
  70     | C.MutInd (uri,tyno,exp_named_subst) ->
  71        let exp_named_subst' =
  72         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  73        in
  74         C.MutInd (uri,tyno,exp_named_subst')
  75     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  76        let exp_named_subst' =
  77         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  78        in
  79         C.MutConstruct (uri,tyno,consno,exp_named_subst')
  80     | C.MutCase (sp,i,outty,t,pl) ->
  81        C.MutCase (sp, i, liftaux k outty, liftaux k t,
  82         List.map (liftaux k) pl)
  83     | C.Fix (i, fl) ->
  84        let len = List.length fl in
  85        let liftedfl =
  86         List.map
  87          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
  88           fl
  89        in
  90         C.Fix (i, liftedfl)
  91     | C.CoFix (i, fl) ->
  92        let len = List.length fl in
  93        let liftedfl =
  94         List.map
  95          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
  96           fl
  97        in
  98         C.CoFix (i, liftedfl)
  99  in
 100  liftaux k
 101
 102 let lift n t =
 103   if n = 0 then
 104    t
 105   else
 106    lift_from 1 n t
 107 ;;
 108
 109 let subst arg =
 110  let rec substaux k =
 111   let module C = Cic in
 112    function
 113       C.Rel n as t ->
 114        (match n with
 115            n when n = k -> lift (k - 1) arg
 116          | n when n < k -> t
 117          | _            -> C.Rel (n - 1)
 118        )
 119     | C.Var (uri,exp_named_subst) ->
 120        let exp_named_subst' =
 121         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 122        in
 123         C.Var (uri,exp_named_subst')
 124     | C.Meta (i, l) as t ->
 125        let l' =
 126         List.map
 127          (function
 128              None -> None
 129            | Some t -> Some (substaux k t)
 130          ) l
 131        in
 132         C.Meta(i,l')
 133     | C.Sort _ as t -> t
 134     | C.Implicit _ as t -> t
 135     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 136     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
 137     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
 138     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
 139     | C.Appl (he::tl) ->
 140        (* Invariant: no Appl applied to another Appl *)
 141        let tl' = List.map (substaux k) tl in
 142         begin
 143          match substaux k he with
 144             C.Appl l -> C.Appl (l@tl')
 145           | _ as he' -> C.Appl (he'::tl')
 146         end
 147     | C.Appl _ -> assert false
 148     | C.Const (uri,exp_named_subst)  ->
 149        let exp_named_subst' =
 150         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 151        in
 152         C.Const (uri,exp_named_subst')
 153     | C.MutInd (uri,typeno,exp_named_subst) ->
 154        let exp_named_subst' =
 155         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 156        in
 157         C.MutInd (uri,typeno,exp_named_subst')
 158     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 159        let exp_named_subst' =
 160         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 161        in
 162         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 163     | C.MutCase (sp,i,outt,t,pl) ->
 164        C.MutCase (sp,i,substaux k outt, substaux k t,
 165         List.map (substaux k) pl)
 166     | C.Fix (i,fl) ->
 167        let len = List.length fl in
 168        let substitutedfl =
 169         List.map
 170          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 171           fl
 172        in
 173         C.Fix (i, substitutedfl)
 174     | C.CoFix (i,fl) ->
 175        let len = List.length fl in
 176        let substitutedfl =
 177         List.map
 178          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 179           fl
 180        in
 181         C.CoFix (i, substitutedfl)
 182  in
 183   substaux 1
 184 ;;
 185
 186 (*CSC: i controlli di tipo debbono essere svolti da destra a             *)
 187 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b         *)
 188 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma     *)
 189 (*CSC: dovrebbe diventare da sinistra verso destra:                      *)
 190 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H                       *)
 191 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
 192 let subst_vars exp_named_subst =
 193 (*
 194 debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
 195 *)
 196  let rec substaux k =
 197   let module C = Cic in
 198    function
 199       C.Rel _ as t -> t
 200     | C.Var (uri,exp_named_subst') ->
 201        (try
 202          let (_,arg) =
 203           List.find
 204            (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
 205          in
 206           lift (k -1) arg
 207         with
 208          Not_found ->
 209           let params =
 210            let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 211            (match obj with
 212                C.Constant _ -> raise ReferenceToConstant
 213              | C.Variable (_,_,_,params,_) -> params
 214              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 215              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 216            )
 217           in
 218 (*
 219 debug_print (lazy "\n\n---- BEGIN ") ;
 220 debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
 221 debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
 222 debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
 223 *)
 224            let exp_named_subst'' =
 225             substaux_in_exp_named_subst uri k exp_named_subst' params
 226            in
 227 (*
 228 debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
 229 debug_print (lazy "---- END\n\n ") ;
 230 *)
 231             C.Var (uri,exp_named_subst'')
 232        )
 233     | C.Meta (i, l) as t ->
 234        let l' =
 235         List.map
 236          (function
 237              None -> None
 238            | Some t -> Some (substaux k t)
 239          ) l
 240        in
 241         C.Meta(i,l')
 242     | C.Sort _ as t -> t
 243     | C.Implicit _ as t -> t
 244     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 245     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
 246     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
 247     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
 248     | C.Appl (he::tl) ->
 249        (* Invariant: no Appl applied to another Appl *)
 250        let tl' = List.map (substaux k) tl in
 251         begin
 252          match substaux k he with
 253             C.Appl l -> C.Appl (l@tl')
 254           | _ as he' -> C.Appl (he'::tl')
 255         end
 256     | C.Appl _ -> assert false
 257     | C.Const (uri,exp_named_subst')  ->
 258        let params =
 259         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 260         (match obj with
 261             C.Constant (_,_,_,params,_) -> params
 262           | C.Variable _ -> raise ReferenceToVariable
 263           | C.CurrentProof (_,_,_,_,params,_) -> params
 264           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 265         )
 266        in
 267         let exp_named_subst'' =
 268          substaux_in_exp_named_subst uri k exp_named_subst' params
 269         in
 270          C.Const (uri,exp_named_subst'')
 271     | C.MutInd (uri,typeno,exp_named_subst') ->
 272        let params =
 273         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 274         (match obj with
 275             C.Constant _ -> raise ReferenceToConstant
 276           | C.Variable _ -> raise ReferenceToVariable
 277           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 278           | C.InductiveDefinition (_,params,_,_) -> params
 279         )
 280        in
 281         let exp_named_subst'' =
 282          substaux_in_exp_named_subst uri k exp_named_subst' params
 283         in
 284          C.MutInd (uri,typeno,exp_named_subst'')
 285     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
 286        let params =
 287         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 288         (match obj with
 289             C.Constant _ -> raise ReferenceToConstant
 290           | C.Variable _ -> raise ReferenceToVariable
 291           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 292           | C.InductiveDefinition (_,params,_,_) -> params
 293         )
 294        in
 295         let exp_named_subst'' =
 296          substaux_in_exp_named_subst uri k exp_named_subst' params
 297         in
 298          C.MutConstruct (uri,typeno,consno,exp_named_subst'')
 299     | C.MutCase (sp,i,outt,t,pl) ->
 300        C.MutCase (sp,i,substaux k outt, substaux k t,
 301         List.map (substaux k) pl)
 302     | C.Fix (i,fl) ->
 303        let len = List.length fl in
 304        let substitutedfl =
 305         List.map
 306          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 307           fl
 308        in
 309         C.Fix (i, substitutedfl)
 310     | C.CoFix (i,fl) ->
 311        let len = List.length fl in
 312        let substitutedfl =
 313         List.map
 314          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 315           fl
 316        in
 317         C.CoFix (i, substitutedfl)
 318  and substaux_in_exp_named_subst uri k exp_named_subst' params =
 319 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
 320 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
 321   let rec filter_and_lift =
 322    function
 323       [] -> []
 324     | (uri,t)::tl when
 325         List.for_all
 326          (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
 327         &&
 328          List.mem uri params
 329        ->
 330         (uri,lift (k-1) t)::(filter_and_lift tl)
 331     | _::tl -> filter_and_lift tl
 332 (*
 333     | (uri,_)::tl ->
 334 debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
 335 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
 336 exp_named_subst' then debug_print (lazy "---- OK1") ;
 337 debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
 338 if List.mem uri params then debug_print (lazy "---- OK2") ;
 339         filter_and_lift tl
 340 *)
 341   in
 342    List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
 343     (filter_and_lift exp_named_subst)
 344  in
 345   substaux 1
 346 ;;
 347
 348 (* subst_meta [t_1 ; ... ; t_n] t                                *)
 349 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
 350 (* [t_i] is lifted as usual when it crosses an abstraction      *)
 351 let subst_meta l t =
 352  let module C = Cic in
 353   if l = [] then t else
 354    let rec aux k = function
 355       C.Rel n as t ->
 356         if n <= k then t else
 357          (try
 358            match List.nth l (n-k-1) with
 359               None -> raise RelToHiddenHypothesis
 360             | Some t -> lift k t
 361           with
 362            (Failure _) -> assert false
 363          )
 364     | C.Var (uri,exp_named_subst) ->
 365        let exp_named_subst' =
 366         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 367        in
 368         C.Var (uri,exp_named_subst')
 369     | C.Meta (i,l) ->
 370        let l' =
 371         List.map
 372          (function
 373              None -> None
 374            | Some t ->
 375               try
 376                Some (aux k t)
 377               with
 378                RelToHiddenHypothesis -> None
 379          ) l
 380        in
 381         C.Meta(i,l')
 382     | C.Sort _ as t -> t
 383     | C.Implicit _ as t -> t
 384     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
 385     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
 386     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
 387     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
 388     | C.Appl l -> C.Appl (List.map (aux k) l)
 389     | C.Const (uri,exp_named_subst) ->
 390        let exp_named_subst' =
 391         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 392        in
 393         C.Const (uri,exp_named_subst')
 394     | C.MutInd (uri,typeno,exp_named_subst) ->
 395        let exp_named_subst' =
 396         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 397        in
 398         C.MutInd (uri,typeno,exp_named_subst')
 399     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 400        let exp_named_subst' =
 401         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 402        in
 403         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 404     | C.MutCase (sp,i,outt,t,pl) ->
 405        C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
 406     | C.Fix (i,fl) ->
 407        let len = List.length fl in
 408        let substitutedfl =
 409         List.map
 410          (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
 411           fl
 412        in
 413         C.Fix (i, substitutedfl)
 414     | C.CoFix (i,fl) ->
 415        let len = List.length fl in
 416        let substitutedfl =
 417         List.map
 418          (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
 419           fl
 420        in
 421         C.CoFix (i, substitutedfl)
 422  in
 423   aux 0 t
 424 ;;
 425