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 ho ->
  83             raise TO_DO
  84
  85   and conclude2cic premise_env conclude =
  86     let module C = Cic in
  87     let module Con = Content in
  88     if conclude.Con.conclude_method = "TD_Conversion" then
  89       (match conclude.Con.conclude_args with
  90          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
  91        | _ -> prerr_endline "1"; assert false)
  92     else if conclude.Con.conclude_method = "BU_Conversion" then
  93       (match conclude.Con.conclude_args with
  94          [Con.Premise prem] ->
  95            (try List.assoc prem.Con.premise_xref premise_env
  96             with Not_found ->
  97               prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
  98               raise Not_found)
  99        | _ -> prerr_endline "2"; assert false)
 100     else if conclude.Con.conclude_method = "Exact" then
 101       (match conclude.Con.conclude_args with
 102          [Con.Term t] -> term2cic t
 103        | _ -> prerr_endline "3"; assert false)
 104     else if conclude.Con.conclude_method = "Intros+LetTac" then
 105       (match conclude.Con.conclude_args with
 106          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
 107        | _ -> prerr_endline "4"; assert false)
 108     else if (conclude.Con.conclude_method = "ByInduction") then
 109       (match (List.tl conclude.Con.conclude_args) with
 110          Con.Term (C.AAppl
 111             id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
 112            let subst =
 113              List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
 114            let cargs = args2cic premise_env args in
 115            let cparams_and_IP = List.map term2cic params_and_IP in
 116            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
 117        | _ -> prerr_endline "5"; assert false)
 118     else if (conclude.Con.conclude_method = "Rewrite") then
 119       (match conclude.Con.conclude_args with
 120          Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
 121            let subst =
 122              List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
 123            let  cargs = args2cic premise_env args in
 124            C.Appl (C.Const(uri,subst)::cargs)
 125        | _ -> prerr_endline "6"; assert false)
 126     else if (conclude.Con.conclude_method = "Apply") then
 127       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
 128       C.Appl cargs
 129     else (prerr_endline "7"; assert false)
 130
 131   and args2cic premise_env l =
 132     List.map (arg2cic premise_env) l
 133
 134   and arg2cic premise_env =
 135     let module C = Cic in
 136     let module Con = Content in
 137     function
 138         Con.Aux n -> prerr_endline "8"; assert false
 139       | Con.Premise prem ->
 140           (match prem.Con.premise_n with
 141             Some n ->
 142               C.Rel n
 143             | _ ->
 144               (try List.assoc prem.Con.premise_xref premise_env
 145                with Not_found ->
 146                   prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
 147                   raise Not_found))
 148       | Con.Term t ->
 149           term2cic t
 150       | Con.ArgProof p ->
 151           proof2cic [] p (* empty! *)
 152       | Con.ArgMethod s -> raise TO_DO
 153
 154 in proof2cic [] p
 155 ;;
 156
 157
 158
 159
 160
 161