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