helm/ocaml/acic_content/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 (* $Id$ *)
  36
  37 exception TO_DO;;
  38
  39 let proof2cic deannotate p =
  40   let rec proof2cic premise_env p =
  41     let module C = Cic in
  42     let module Con = Content in
  43       let rec extend_premise_env current_env =
  44         function
  45             [] -> current_env
  46           | p::atl ->
  47               extend_premise_env
  48               ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
  49       let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
  50       let body = conclude2cic new_premise_env p.Con.proof_conclude in
  51       context2cic premise_env p.Con.proof_context body
  52
  53   and context2cic premise_env context body =
  54     List.fold_right (ce2cic premise_env) context body
  55
  56   and ce2cic premise_env ce target =
  57     let module C = Cic in
  58     let module Con = Content in
  59       match ce with
  60         `Declaration d ->
  61           (match d.Con.dec_name with
  62               Some s ->
  63                 C.Lambda (C.Name s, deannotate d.Con.dec_type, target)
  64             | None ->
  65                 C.Lambda (C.Anonymous, deannotate d.Con.dec_type, target))
  66       | `Hypothesis h ->
  67           (match h.Con.dec_name with
  68               Some s ->
  69                 C.Lambda (C.Name s, deannotate h.Con.dec_type, target)
  70             | None ->
  71                 C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
  72       | `Proof p ->
  73           (match p.Con.proof_name with
  74               Some s ->
  75                 C.LetIn (C.Name s, proof2cic premise_env p, target)
  76             | None ->
  77                 C.LetIn (C.Anonymous, proof2cic premise_env p, target))
  78       | `Definition d ->
  79            (match d.Con.def_name with
  80               Some s ->
  81                 C.LetIn (C.Name s, proof2cic premise_env p, target)
  82             | None ->
  83                 C.LetIn (C.Anonymous, proof2cic premise_env p, target))
  84       | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
  85             (match target with
  86                C.Rel n ->
  87                  (match kind with
  88                     `Recursive l ->
  89                       let funs =
  90                         List.map2
  91                           (fun n bo ->
  92                              match bo with
  93                                `Proof bo ->
  94                                   (match
  95                                     bo.Con.proof_conclude.Con.conclude_conclusion,
  96                                     bo.Con.proof_name
  97                                    with
  98                                       Some ty, Some name ->
  99                                        (name,n,deannotate ty,
 100                                          proof2cic premise_env bo)
 101                                     | _,_ -> assert false)
 102                              | _ -> assert false)
 103                           l defs in
 104                       C.Fix (n, funs)
 105                   | `CoRecursive ->
 106                      let funs =
 107                         List.map
 108                           (function bo ->
 109                              match bo with
 110                               `Proof bo ->
 111                                  (match
 112                                     bo.Con.proof_conclude.Con.conclude_conclusion,
 113                                     bo.Con.proof_name
 114                                   with
 115                                      Some ty, Some name ->
 116                                       (name,deannotate ty,
 117                                         proof2cic premise_env bo)
 118                                    | _,_ -> assert false)
 119                              | _ -> assert false)
 120                            defs in
 121                       C.CoFix (n, funs)
 122                   | _ -> (* no inductive types in local contexts *)
 123                        assert false)
 124              | _ -> assert false)
 125
 126   and conclude2cic premise_env conclude =
 127     let module C = Cic in
 128     let module Con = Content in
 129     if conclude.Con.conclude_method = "TD_Conversion" then
 130       (match conclude.Con.conclude_args with
 131          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 132        | _ -> prerr_endline "1"; assert false)
 133     else if conclude.Con.conclude_method = "BU_Conversion" then
 134       (match conclude.Con.conclude_args with
 135          [Con.Premise prem] ->
 136            (try List.assoc prem.Con.premise_xref premise_env
 137             with Not_found ->
 138               prerr_endline
 139                ("Not_found in BU_Conversion: " ^ prem.Con.premise_xref);
 140               raise Not_found)
 141        | _ -> prerr_endline "2"; assert false)
 142     else if conclude.Con.conclude_method = "Exact" then
 143       (match conclude.Con.conclude_args with
 144          [Con.Term t] -> deannotate t
 145        | [Con.Premise prem] ->
 146            (match prem.Con.premise_n with
 147               None -> assert false
 148             | Some n -> C.Rel n)
 149        | _ -> prerr_endline "3"; assert false)
 150     else if conclude.Con.conclude_method = "Intros+LetTac" then
 151       (match conclude.Con.conclude_args with
 152          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 153        | _ -> prerr_endline "4"; assert false)
 154     else if (conclude.Con.conclude_method = "ByInduction" ||
 155              conclude.Con.conclude_method = "AndInd" ||
 156              conclude.Con.conclude_method = "Exists" ||
 157              conclude.Con.conclude_method = "FalseInd") then
 158       (match (List.tl conclude.Con.conclude_args) with
 159          Con.Term (C.AAppl (
 160             id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
 161            let subst =
 162              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
 163            let cargs = args2cic premise_env args in
 164            let cparams_and_IP = List.map deannotate params_and_IP in
 165            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
 166        | _ -> prerr_endline "5"; assert false)
 167     else if (conclude.Con.conclude_method = "Rewrite") then
 168       (match conclude.Con.conclude_args with
 169          Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
 170            let subst =
 171              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
 172            let  cargs = args2cic premise_env args in
 173            C.Appl (C.Const(uri,subst)::cargs)
 174        | _ -> prerr_endline "6"; assert false)
 175     else if (conclude.Con.conclude_method = "Case") then
 176       (match conclude.Con.conclude_args with
 177         Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
 178            C.MutCase
 179             (UriManager.uri_of_string uri,
 180              int_of_string notype, deannotate ty,
 181              List.assoc prem.Con.premise_xref premise_env,
 182              List.map
 183                (function
 184                    Con.ArgProof p -> proof2cic [] p
 185                  | _ -> prerr_endline "7a"; assert false) patterns)
 186       | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
 187             (UriManager.uri_of_string uri,
 188              int_of_string notype, deannotate ty, deannotate te,
 189              List.map
 190                (function
 191                    (Con.ArgProof p) -> proof2cic [] p
 192                  | _ -> prerr_endline "7a"; assert false) patterns)
 193       | _ -> (prerr_endline "7"; assert false))
 194     else if (conclude.Con.conclude_method = "Apply") then
 195       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
 196       C.Appl cargs
 197     else (prerr_endline "8"; assert false)
 198
 199   and args2cic premise_env l =
 200     List.map (arg2cic premise_env) l
 201
 202   and arg2cic premise_env =
 203     let module C = Cic in
 204     let module Con = Content in
 205     function
 206         Con.Aux n -> prerr_endline "8"; assert false
 207       | Con.Premise prem ->
 208           (match prem.Con.premise_n with
 209               Some n -> C.Rel n
 210             | None ->
 211               (try List.assoc prem.Con.premise_xref premise_env
 212                with Not_found ->
 213                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
 214                   raise Not_found))
 215       | Con.Lemma lemma ->
 216          CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
 217       | Con.Term t -> deannotate t
 218       | Con.ArgProof p -> proof2cic [] p (* empty! *)
 219       | Con.ArgMethod s -> raise TO_DO
 220
 221 in proof2cic [] p
 222 ;;
 223
 224 exception ToDo;;
 225
 226 let cobj2obj deannotate (id,params,metasenv,obj) =
 227  let module K = Content in
 228  match obj with
 229     `Def (Content.Const,ty,`Proof bo) ->
 230       (match metasenv with
 231           None ->
 232            Cic.Constant
 233             (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
 234         | Some metasenv' ->
 235            let metasenv'' =
 236             List.map
 237              (function (_,i,canonical_context,term) ->
 238                let canonical_context' =
 239                 List.map
 240                  (function
 241                      None -> None
 242                    | Some (`Declaration d)
 243                    | Some (`Hypothesis d) ->
 244                      (match d with
 245                         {K.dec_name = Some n ; K.dec_type = t} ->
 246                           Some (Cic.Name n, Cic.Decl (deannotate t))
 247                       | _ -> assert false)
 248                    | Some (`Definition d) ->
 249                       (match d with
 250                           {K.def_name = Some n ; K.def_term = t} ->
 251                             Some (Cic.Name n, Cic.Def ((deannotate t),None))
 252                         | _ -> assert false)
 253                    | Some (`Proof d) ->
 254                       (match d with
 255                           {K.proof_name = Some n } ->
 256                             Some (Cic.Name n,
 257                               Cic.Def ((proof2cic deannotate d),None))
 258                         | _ -> assert false)
 259                  ) canonical_context
 260                in
 261                 (i,canonical_context',deannotate term)
 262              ) metasenv'
 263            in
 264             Cic.CurrentProof
 265              (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
 266               []))
 267   | _ -> raise ToDo
 268 ;;
 269
 270 let cobj2obj = cobj2obj Deannotate.deannotate_term;;