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