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" ||
 153              conclude.Con.conclude_method = "AndInd" ||
 154              conclude.Con.conclude_method = "Exists" ||
 155              conclude.Con.conclude_method = "FalseInd") then
 156       (match (List.tl conclude.Con.conclude_args) with
 157          Con.Term (C.AAppl (
 158             id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
 159            let subst =
 160              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
 161            let cargs = args2cic premise_env args in
 162            let cparams_and_IP = List.map deannotate params_and_IP in
 163            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
 164        | _ -> prerr_endline "5"; assert false)
 165     else if (conclude.Con.conclude_method = "Rewrite") then
 166       (match conclude.Con.conclude_args with
 167          Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
 168            let subst =
 169              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
 170            let  cargs = args2cic premise_env args in
 171            C.Appl (C.Const(uri,subst)::cargs)
 172        | _ -> prerr_endline "6"; assert false)
 173     else if (conclude.Con.conclude_method = "Case") then
 174       (match conclude.Con.conclude_args with
 175         Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
 176            C.MutCase
 177             (UriManager.uri_of_string uri,
 178              int_of_string notype, deannotate ty,
 179              List.assoc prem.Con.premise_xref premise_env,
 180              List.map
 181                (function
 182                    Con.ArgProof p -> proof2cic [] p
 183                  | _ -> prerr_endline "7a"; assert false) patterns)
 184       | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
 185             (UriManager.uri_of_string uri,
 186              int_of_string notype, deannotate ty, deannotate te,
 187              List.map
 188                (function
 189                    (Con.ArgProof p) -> proof2cic [] p
 190                  | _ -> prerr_endline "7a"; assert false) patterns)
 191       | _ -> (prerr_endline "7"; assert false))
 192     else if (conclude.Con.conclude_method = "Apply") then
 193       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
 194       C.Appl cargs
 195     else (prerr_endline "8"; assert false)
 196
 197   and args2cic premise_env l =
 198     List.map (arg2cic premise_env) l
 199
 200   and arg2cic premise_env =
 201     let module C = Cic in
 202     let module Con = Content in
 203     function
 204         Con.Aux n -> prerr_endline "8"; assert false
 205       | Con.Premise prem ->
 206           (match prem.Con.premise_n with
 207               Some n -> C.Rel n
 208             | None ->
 209               (try List.assoc prem.Con.premise_xref premise_env
 210                with Not_found ->
 211                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
 212                   raise Not_found))
 213       | Con.Lemma lemma ->
 214          CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
 215       | Con.Term t -> deannotate t
 216       | Con.ArgProof p -> proof2cic [] p (* empty! *)
 217       | Con.ArgMethod s -> raise TO_DO
 218
 219 in proof2cic [] p
 220 ;;
 221
 222 exception ToDo;;
 223
 224 let cobj2obj deannotate (id,params,metasenv,obj) =
 225  let module K = Content in
 226  match obj with
 227     `Def (Content.Const,ty,`Proof bo) ->
 228       (match metasenv with
 229           None ->
 230            Cic.Constant
 231             (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
 232         | Some metasenv' ->
 233            let metasenv'' =
 234             List.map
 235              (function (_,i,canonical_context,term) ->
 236                let canonical_context' =
 237                 List.map
 238                  (function
 239                      None -> None
 240                    | Some (`Declaration d)
 241                    | Some (`Hypothesis d) ->
 242                      (match d with
 243                         {K.dec_name = Some n ; K.dec_type = t} ->
 244                           Some (Cic.Name n, Cic.Decl (deannotate t))
 245                       | _ -> assert false)
 246                    | Some (`Definition d) ->
 247                       (match d with
 248                           {K.def_name = Some n ; K.def_term = t} ->
 249                             Some (Cic.Name n, Cic.Def ((deannotate t),None))
 250                         | _ -> assert false)
 251                    | Some (`Proof d) ->
 252                       (match d with
 253                           {K.proof_name = Some n } ->
 254                             Some (Cic.Name n,
 255                               Cic.Def ((proof2cic deannotate d),None))
 256                         | _ -> assert false)
 257                  ) canonical_context
 258                in
 259                 (i,canonical_context',deannotate term)
 260              ) metasenv'
 261            in
 262             Cic.CurrentProof
 263              (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
 264               []))
 265   | _ -> raise ToDo
 266 ;;
 267
 268 let cobj2obj = cobj2obj Deannotate.deannotate_term;;