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 deannotate 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, deannotate d.Con.dec_type, target)
  62             | None ->
  63                 C.Lambda (C.Anonymous, deannotate d.Con.dec_type, target))
  64       | `Hypothesis h ->
  65           (match h.Con.dec_name with
  66               Some s ->
  67                 C.Lambda (C.Name s, deannotate h.Con.dec_type, target)
  68             | None ->
  69                 C.Lambda (C.Anonymous, deannotate 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,deannotate ty,
  98                                          proof2cic premise_env bo)
  99                                     | _,_ -> assert false)
 100                              | _ -> assert false)
 101                           l defs in
 102                       C.Fix (n, funs)
 103                   | `CoRecursive ->
 104                      let funs =
 105                         List.map
 106                           (function bo ->
 107                              match bo with
 108                               `Proof bo ->
 109                                  (match
 110                                     bo.Con.proof_conclude.Con.conclude_conclusion,
 111                                     bo.Con.proof_name
 112                                   with
 113                                      Some ty, Some name ->
 114                                       (name,deannotate ty,
 115                                         proof2cic premise_env bo)
 116                                    | _,_ -> assert false)
 117                              | _ -> assert false)
 118                            defs in
 119                       C.CoFix (n, funs)
 120                   | _ -> (* no inductive types in local contexts *)
 121                        assert false)
 122              | _ -> assert false)
 123
 124   and conclude2cic premise_env conclude =
 125     let module C = Cic in
 126     let module Con = Content in
 127     if conclude.Con.conclude_method = "TD_Conversion" then
 128       (match conclude.Con.conclude_args with
 129          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 130        | _ -> prerr_endline "1"; assert false)
 131     else if conclude.Con.conclude_method = "BU_Conversion" then
 132       (match conclude.Con.conclude_args with
 133          [Con.Premise prem] ->
 134            (try List.assoc prem.Con.premise_xref premise_env
 135             with Not_found ->
 136               prerr_endline
 137                ("Not_found in BU_Conversion: " ^ prem.Con.premise_xref);
 138               raise Not_found)
 139        | _ -> prerr_endline "2"; assert false)
 140     else if conclude.Con.conclude_method = "Exact" then
 141       (match conclude.Con.conclude_args with
 142          [Con.Term t] -> deannotate t
 143        | [Con.Premise prem] ->
 144            (match prem.Con.premise_n with
 145               None -> assert false
 146             | Some n -> C.Rel n)
 147        | _ -> prerr_endline "3"; assert false)
 148     else if conclude.Con.conclude_method = "Intros+LetTac" then
 149       (match conclude.Con.conclude_args with
 150          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 151        | _ -> prerr_endline "4"; assert false)
 152     else if (conclude.Con.conclude_method = "ByInduction") then
 153       (match (List.tl conclude.Con.conclude_args) with
 154          Con.Term (C.AAppl
 155             id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
 156            let subst =
 157              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
 158            let cargs = args2cic premise_env args in
 159            let cparams_and_IP = List.map deannotate params_and_IP in
 160            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
 161        | _ -> prerr_endline "5"; assert false)
 162     else if (conclude.Con.conclude_method = "Rewrite") then
 163       (match conclude.Con.conclude_args with
 164          Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
 165            let subst =
 166              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
 167            let  cargs = args2cic premise_env args in
 168            C.Appl (C.Const(uri,subst)::cargs)
 169        | _ -> prerr_endline "6"; assert false)
 170     else if (conclude.Con.conclude_method = "Case") then
 171       (match conclude.Con.conclude_args with
 172         Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
 173            C.MutCase
 174             (UriManager.uri_of_string uri,
 175              int_of_string notype, deannotate ty,
 176              List.assoc prem.Con.premise_xref premise_env,
 177              List.map
 178                (function
 179                    Con.ArgProof p -> proof2cic [] p
 180                  | _ -> prerr_endline "7a"; assert false) patterns)
 181       | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
 182             (UriManager.uri_of_string uri,
 183              int_of_string notype, deannotate ty, deannotate te,
 184              List.map
 185                (function
 186                    (Con.ArgProof p) -> proof2cic [] p
 187                  | _ -> prerr_endline "7a"; assert false) patterns)
 188       | _ -> (prerr_endline "7"; assert false))
 189     else if (conclude.Con.conclude_method = "Apply") then
 190       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
 191       C.Appl cargs
 192     else (prerr_endline "8"; assert false)
 193
 194   and args2cic premise_env l =
 195     List.map (arg2cic premise_env) l
 196
 197   and arg2cic premise_env =
 198     let module C = Cic in
 199     let module Con = Content in
 200     function
 201         Con.Aux n -> prerr_endline "8"; assert false
 202       | Con.Premise prem ->
 203           (match prem.Con.premise_n with
 204               Some n -> C.Rel n
 205             | None ->
 206               (try List.assoc prem.Con.premise_xref premise_env
 207                with Not_found ->
 208                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
 209                   raise Not_found))
 210       | Con.Lemma lemma ->
 211           MQueryMisc.term_of_cic_textual_parser_uri
 212            (MQueryMisc.cic_textual_parser_uri_of_string
 213             (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
 214               lemma.Con.lemma_uri))
 215       | Con.Term t ->
 216           deannotate t
 217       | Con.ArgProof p ->
 218           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))
 252                         | _ -> assert false)
 253                    | _,Some (`Proof d) ->
 254                       (match d with
 255                           {K.proof_name = Some n } ->
 256                             Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
 257                         | _ -> assert false)
 258                  ) canonical_context
 259                in
 260                 (i,canonical_context',deannotate term)
 261              ) metasenv'
 262            in
 263             Cic.CurrentProof
 264              (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
 265   | _ -> raise ToDo
 266 ;;
 267
 268 let cobj2obj = cobj2obj Deannotate.deannotate_term;;