helm/ocaml/cic_omdoc/content2cic.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 (***************************************************************************)
  27 (*                                                                         *)
  28 (*                            PROJECT HELM                                 *)
  29 (*                                                                         *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                     *)
  31 (*                              17/06/2003                                 *)
  32 (*                                                                         *)
  33 (***************************************************************************)
  34
  35 exception TO_DO;;
  36
  37 let proof2cic term2cic p =
  38   let rec proof2cic premise_env p =
  39     let module C = Cic in
  40     let module Con = Content in
  41       let rec extend_premise_env current_env =
  42         function
  43             [] -> current_env
  44           | p::atl ->
  45               extend_premise_env
  46               ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
  47       let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
  48       let body = conclude2cic new_premise_env p.Con.proof_conclude in
  49       context2cic premise_env p.Con.proof_context body
  50
  51   and context2cic premise_env context body =
  52     List.fold_right (ce2cic premise_env) context body
  53
  54   and ce2cic premise_env ce target =
  55     let module C = Cic in
  56     let module Con = Content in
  57       match ce with
  58         `Declaration d ->
  59           (match d.Con.dec_name with
  60               Some s ->
  61                 C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
  62             | None ->
  63                 C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
  64       | `Hypothesis h ->
  65           (match h.Con.dec_name with
  66               Some s ->
  67                 C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
  68             | None ->
  69                 C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
  70       | `Proof p ->
  71           (match p.Con.proof_name with
  72               Some s ->
  73                 C.LetIn (C.Name s, proof2cic premise_env p, target)
  74             | None ->
  75                 C.LetIn (C.Anonymous, proof2cic premise_env p, target))
  76       | `Definition d ->
  77            (match d.Con.def_name with
  78               Some s ->
  79                 C.LetIn (C.Name s, proof2cic premise_env p, target)
  80             | None ->
  81                 C.LetIn (C.Anonymous, proof2cic premise_env p, target))
  82       | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
  83             (match target with
  84                C.Rel n ->
  85                  (match kind with
  86                     `Recursive l ->
  87                       let funs =
  88                         List.map2
  89                           (fun n bo ->
  90                              match bo with
  91                                `Proof bo ->
  92                                   (match
  93                                     bo.Con.proof_conclude.Con.conclude_conclusion,
  94                                     bo.Con.proof_name
  95                                    with
  96                                       Some ty, Some name ->
  97                                        (name,n,term2cic ty,proof2cic premise_env bo)
  98                                     | _,_ -> assert false)
  99                              | _ -> assert false)
 100                           l defs in
 101                       C.Fix (n, funs)
 102                   | `CoRecursive ->
 103                      let funs =
 104                         List.map
 105                           (function bo ->
 106                              match bo with
 107                               `Proof bo ->
 108                                  (match
 109                                     bo.Con.proof_conclude.Con.conclude_conclusion,
 110                                     bo.Con.proof_name
 111                                   with
 112                                      Some ty, Some name ->
 113                                       (name,term2cic ty,proof2cic premise_env bo)
 114                                    | _,_ -> assert false)
 115                              | _ -> assert false)
 116                            defs in
 117                       C.CoFix (n, funs)
 118                   | _ -> (* no inductive types in local contexts *)
 119                        assert false)
 120              | _ -> assert false)
 121
 122   and conclude2cic premise_env conclude =
 123     let module C = Cic in
 124     let module Con = Content in
 125     if conclude.Con.conclude_method = "TD_Conversion" then
 126       (match conclude.Con.conclude_args with
 127          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 128        | _ -> prerr_endline "1"; assert false)
 129     else if conclude.Con.conclude_method = "BU_Conversion" then
 130       (match conclude.Con.conclude_args with
 131          [Con.Premise prem] ->
 132            (try List.assoc prem.Con.premise_xref premise_env
 133             with Not_found ->
 134               prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
 135               raise Not_found)
 136        | _ -> prerr_endline "2"; assert false)
 137     else if conclude.Con.conclude_method = "Exact" then
 138       (match conclude.Con.conclude_args with
 139          [Con.Term t] -> term2cic t
 140        | [Con.Premise prem] ->
 141            (match prem.Con.premise_n with
 142               None -> assert false
 143             | Some n -> C.Rel n)
 144        | _ -> prerr_endline "3"; assert false)
 145     else if conclude.Con.conclude_method = "Intros+LetTac" then
 146       (match conclude.Con.conclude_args with
 147          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 148        | _ -> prerr_endline "4"; assert false)
 149     else if (conclude.Con.conclude_method = "ByInduction") then
 150       (match (List.tl conclude.Con.conclude_args) with
 151          Con.Term (C.AAppl
 152             id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
 153            let subst =
 154              List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
 155            let cargs = args2cic premise_env args in
 156            let cparams_and_IP = List.map term2cic params_and_IP in
 157            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
 158        | _ -> prerr_endline "5"; assert false)
 159     else if (conclude.Con.conclude_method = "Rewrite") then
 160       (match conclude.Con.conclude_args with
 161          Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
 162            let subst =
 163              List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
 164            let  cargs = args2cic premise_env args in
 165            C.Appl (C.Const(uri,subst)::cargs)
 166        | _ -> prerr_endline "6"; assert false)
 167     else if (conclude.Con.conclude_method = "Apply") then
 168       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
 169       C.Appl cargs
 170     else (prerr_endline "7"; assert false)
 171
 172   and args2cic premise_env l =
 173     List.map (arg2cic premise_env) l
 174
 175   and arg2cic premise_env =
 176     let module C = Cic in
 177     let module Con = Content in
 178     function
 179         Con.Aux n -> prerr_endline "8"; assert false
 180       | Con.Premise prem ->
 181           (match prem.Con.premise_n with
 182             Some n ->
 183               C.Rel n
 184             | _ ->
 185               (try List.assoc prem.Con.premise_xref premise_env
 186                with Not_found ->
 187                   prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
 188                   raise Not_found))
 189       | Con.Term t ->
 190           term2cic t
 191       | Con.ArgProof p ->
 192           proof2cic [] p (* empty! *)
 193       | Con.ArgMethod s -> raise TO_DO
 194
 195 in proof2cic [] p
 196 ;;
 197
 198 let proof2cic = proof2cic Deannotate.deannotate_term;;