helm/ocaml/cic_proof_checking/cicElim.ml

   1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 let fresh_binder =
  29   let counter = ref ~-1 in
  30   function
  31     | true ->
  32         incr counter;
  33         Cic.Name ("elim" ^ string_of_int !counter)
  34     | _ -> Cic.Anonymous
  35
  36   (** verifies if a given inductive type occurs in a term in target position *)
  37 let rec recursive uri typeno subst = function
  38   | Cic.Prod (_, _, target) -> recursive uri typeno subst target
  39   | Cic.MutInd (uri', typeno', subst')
  40   | Cic.Appl (Cic.MutInd  (uri', typeno', subst') :: _) ->
  41       UriManager.eq uri uri' && typeno = typeno' && subst = subst'
  42 (*   | Cic.Appl args -> List.exists (recursive uri typeno subst) args *)
  43   | _ -> false
  44
  45 let unfold_appl = function
  46   | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl)
  47   | t -> t
  48
  49 let rec split l n =
  50  match (l,n) with
  51     (l,0) -> ([], l)
  52   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  53   | (_,_) -> assert false
  54
  55   (** build elimination principle part related to a single constructor
  56   * @param paramsno number of Prod to ignore in this constructor (i.e. number of
  57   * inductive parameters)
  58   * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *)
  59 let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
  60   assert (subst = []);
  61   match t with
  62   | Cic.MutInd (uri', typeno', subst') when
  63     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
  64       if dependent then
  65         (match args with
  66         | [] -> assert false
  67         | [arg] -> unfold_appl (Cic.Appl [p; arg])
  68         | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)]))
  69       else
  70         p
  71   | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when
  72     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
  73       let (lparams, rparams) = split tl paramsno in
  74       if dependent then
  75         (match args with
  76         | [] -> assert false
  77         | [arg] -> unfold_appl (Cic.Appl (p :: rparams @ [arg]))
  78         | _ ->
  79             unfold_appl (Cic.Appl (p ::
  80               rparams @ [unfold_appl (Cic.Appl args)])))
  81       else  (* non dependent *)
  82         (match rparams with
  83         | [] -> p
  84         | _ -> Cic.Appl (p :: rparams))
  85   | Cic.Prod (binder, src, tgt) ->
  86       if recursive uri typeno subst src then
  87         let args = List.map (CicSubstitution.lift 2) args in
  88         let phi =
  89           let src = CicSubstitution.lift 1 src in
  90           delta (uri, typeno, subst) dependent paramsno consno src
  91             (CicSubstitution.lift 1 p) [Cic.Rel 1]
  92         in
  93         let tgt = CicSubstitution.lift 1 tgt in
  94         Cic.Prod (fresh_binder dependent, src,
  95           Cic.Prod (Cic.Anonymous, phi,
  96             delta (uri, typeno, subst) dependent paramsno consno tgt
  97               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
  98       else  (* non recursive *)
  99         let args = List.map (CicSubstitution.lift 1) args in
 100         Cic.Prod (fresh_binder dependent, src,
 101           delta (uri, typeno, subst) dependent paramsno consno tgt
 102             (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
 103   | _ -> assert false
 104
 105 let rec strip_left_params consno leftno = function
 106   | t when leftno = 0 -> t (* no need to lift, the term is (hopefully) closed *)
 107   | Cic.Prod (_, _, tgt) (* when leftno > 0 *) ->
 108       (* after stripping the parameters we lift of consno. consno is 1 based so,
 109       * the first constructor will be lifted by 1 (for P), the second by 2 (1
 110       * for P and 1 for the 1st constructor), and so on *)
 111       if leftno = 1 then
 112         CicSubstitution.lift consno tgt
 113       else
 114         strip_left_params consno (leftno - 1) tgt
 115   | _ -> assert false
 116
 117 let delta (ury, typeno, subst) dependent paramsno consno t p args =
 118   let t = strip_left_params consno paramsno t in
 119   delta (ury, typeno, subst) dependent paramsno consno t p args
 120
 121 let rec add_params indno ty eliminator =
 122   if indno = 0 then
 123     eliminator
 124   else
 125     match ty with
 126     | Cic.Prod (binder, src, tgt) ->
 127         Cic.Prod (binder, src, add_params (indno - 1) tgt eliminator)
 128     | _ -> assert false
 129
 130 let rec mk_rels consno = function
 131   | 0 -> []
 132   | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1)
 133
 134 let rec strip_pi = function
 135   | Cic.Prod (_, _, tgt) -> strip_pi tgt
 136   | t -> t
 137
 138 let rec count_pi = function
 139   | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
 140   | t -> 0
 141
 142 let rec type_of_p sort dependent leftno indty = function
 143   | Cic.Prod (n, src, tgt) when leftno = 0 ->
 144       Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
 145   | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
 146   | t ->
 147       if dependent then
 148         Cic.Prod (Cic.Anonymous, indty, Cic.Sort sort)
 149       else
 150         Cic.Sort sort
 151
 152 let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
 153   | Cic.Prod (_, src, tgt) when strip = 0 ->
 154       Cic.Prod (fresh_binder true,
 155         CicSubstitution.lift_from (liftfrom + 1) liftno src,
 156         add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
 157   | Cic.Prod (_, _, tgt) ->
 158       add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
 159   | t ->
 160       if dependent then
 161         Cic.Prod (fresh_binder dependent,
 162           CicSubstitution.lift_from (rightno + 1) liftno indty,
 163           Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
 164       else
 165         Cic.Prod (Cic.Anonymous,
 166           CicSubstitution.lift_from (rightno + 1) liftno indty,
 167           if rightno = 0 then
 168             Cic.Rel (1 + liftno + rightno)
 169           else
 170             Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno))
 171
 172 let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
 173 function
 174   | Cic.Prod (_, src, tgt) when strip = 0 ->
 175       Cic.Lambda (fresh_binder true,
 176         CicSubstitution.lift_from (liftfrom + 1) liftno src,
 177         add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
 178           case tgt)
 179   | Cic.Prod (_, _, tgt) ->
 180       add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty
 181         case tgt
 182   | t ->
 183       Cic.Lambda (fresh_binder true,
 184         CicSubstitution.lift_from (rightno + 1) liftno indty,
 185         case)
 186
 187 exception Failure of string
 188
 189 let string_of_sort = function
 190   | Cic.Prop -> "Prop"
 191   | Cic.CProp -> "CProp"
 192   | Cic.Set -> "Set"
 193   | Cic.Type _ -> "Type"
 194
 195 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
 196   let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
 197   let subst = [] in
 198   match obj with
 199   | Cic.InductiveDefinition (indTypes, params, leftno) ->
 200       let (name, inductive, ty, constructors) =
 201         try
 202           List.nth indTypes typeno
 203         with Failure _ -> assert false
 204       in
 205       let paramsno = count_pi ty in (* number of (left or right) parameters *)
 206       let rightno = paramsno - leftno in
 207       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
 208       let conslen = List.length constructors in
 209       let consno = ref (conslen + 1) in
 210       if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
 211         raise (Failure (sprintf "can't eliminate from Prop to %s"
 212           (string_of_sort sort)));
 213       let indty =
 214         let indty = Cic.MutInd (uri, typeno, subst) in
 215         if paramsno = 0 then
 216           indty
 217         else
 218           Cic.Appl (indty :: mk_rels 0 paramsno)
 219       in
 220       let mk_constructor consno =
 221         let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
 222         if leftno = 0 then
 223           constructor
 224         else
 225           Cic.Appl (constructor :: mk_rels consno leftno)
 226       in
 227       let eliminator =
 228         let p_ty = type_of_p sort dependent leftno indty ty in
 229         let final_ty =
 230           add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
 231         in
 232         Cic.Prod (Cic.Name "P", p_ty,
 233           (List.fold_right
 234             (fun (_, constructor) acc ->
 235               decr consno;
 236               let p = Cic.Rel !consno in
 237               Cic.Prod (Cic.Anonymous,
 238                 (delta (uri, typeno, subst) dependent leftno !consno
 239                   constructor p [mk_constructor !consno]),
 240                 acc))
 241             constructors final_ty))
 242       in
 243       add_params leftno ty eliminator
 244   | _ -> assert false
 245
 246 let rec branch (uri, typeno, subst) insource paramsno t fix head args =
 247   assert (subst = []);
 248   match t with
 249   | Cic.MutInd (uri', typeno', subst') when
 250     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
 251       let head = if insource then fix else head in
 252       (match args with
 253       | [] -> head
 254       | _ -> Cic.Appl (head :: args))
 255   | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when
 256     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
 257       let (lparams, rparams) = split tl paramsno in
 258       (match args with
 259       | [] when insource && rparams = [] -> fix
 260       | [] when insource -> Cic.Appl (fix :: rparams)
 261       | _ when insource -> Cic.Appl (fix :: rparams @ args)
 262       | _ -> Cic.Appl (head :: rparams @ args))
 263   | Cic.Prod (binder, src, tgt) ->
 264       if recursive uri typeno subst src then
 265         let args = List.map (CicSubstitution.lift 1) args in
 266         let phi =
 267           let fix = CicSubstitution.lift 1 fix in
 268           branch (uri, typeno, subst) true paramsno src fix head
 269             (args @ [Cic.Rel 1])
 270         in
 271         let tgt = CicSubstitution.lift 1 tgt in
 272         Cic.Lambda (fresh_binder true, src,
 273           branch (uri, typeno, subst) insource paramsno tgt
 274             (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
 275             (args @ [Cic.Rel 1; phi]))
 276       else  (* non recursive *)
 277         let args = List.map (CicSubstitution.lift 1) args in
 278         Cic.Lambda (fresh_binder true, src,
 279           branch (uri, typeno, subst) insource paramsno tgt
 280           (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
 281             (args @ [Cic.Rel 1]))
 282   | _ -> assert false
 283
 284 let branch (uri, typeno, subst) insource liftno paramsno t fix head args =
 285   let t = strip_left_params liftno paramsno t in
 286   branch (uri, typeno, subst) insource paramsno t fix head args
 287
 288 let body_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
 289   let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
 290   let subst = [] in
 291   match obj with
 292   | Cic.InductiveDefinition (indTypes, params, leftno) ->
 293       let (name, inductive, ty, constructors) =
 294         try
 295           List.nth indTypes typeno
 296         with Failure _ -> assert false
 297       in
 298       let paramsno = count_pi ty in (* number of (left or right) parameters *)
 299       let rightno = paramsno - leftno in
 300       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
 301       let conslen = List.length constructors in
 302       let consno = ref (conslen + 1) in
 303       if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
 304         raise (Failure (sprintf "can't eliminate from Prop to %s"
 305           (string_of_sort sort)));
 306       let indty =
 307         let indty = Cic.MutInd (uri, typeno, subst) in
 308         if paramsno = 0 then
 309           indty
 310         else
 311           Cic.Appl (indty :: mk_rels 0 paramsno)
 312       in
 313       let mk_constructor consno =
 314         let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
 315         if leftno = 0 then
 316           constructor
 317         else
 318           Cic.Appl (constructor :: mk_rels consno leftno)
 319       in
 320       let eliminator =
 321         let p_ty = type_of_p sort dependent leftno indty ty in
 322         let final_ty =
 323           add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
 324         in
 325         let fix = Cic.Rel (rightno + 2) in
 326         let (_, branches) =
 327           List.fold_right
 328             (fun (_, ty) (shift, branches) ->
 329               let head = Cic.Rel (rightno + shift + 2) in
 330               let b =
 331                 branch (uri, typeno, subst) false (rightno + conslen + 3) leftno
 332                   ty fix head []
 333               in
 334               (shift + 1,  b :: branches))
 335             constructors (1, [])
 336         in
 337         let case =
 338           Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 3), Cic.Rel 1,
 339             branches)
 340         in
 341         let fix_body =
 342           add_right_lambda dependent leftno (conslen + 1) 1 rightno
 343             indty case ty
 344         in
 345         let fix = Cic.Fix (0, ["f", 0, final_ty, fix_body]) in
 346         Cic.Lambda (Cic.Name "P", p_ty,
 347           (List.fold_right
 348             (fun (_, constructor) acc ->
 349               decr consno;
 350               let p = Cic.Rel !consno in
 351               Cic.Lambda (fresh_binder true,
 352                 (delta (uri, typeno, subst) dependent leftno !consno
 353                   constructor p [mk_constructor !consno]),
 354                 acc))
 355             constructors fix))
 356       in
 357       add_params leftno ty eliminator
 358   | _ -> assert false
 359