(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(***************************************************************************)
(*                                                                         *)
(*                            PROJECT HELM                                 *)
(*                                                                         *)
(*                Andrea Asperti <asperti@cs.unibo.it>                     *)
(*                              17/06/2003                                 *)
(*                                                                         *)
(***************************************************************************)

exception TO_DO;;

let proof2cic term2cic p =
  let rec proof2cic premise_env p =
    let module C = Cic in 
    let module Con = Content in
      let rec extend_premise_env current_env = 
	function
            [] -> current_env
	  | p::atl ->
              extend_premise_env 
              ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
      let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
      let body = conclude2cic new_premise_env p.Con.proof_conclude in
      context2cic premise_env p.Con.proof_context body

  and context2cic premise_env context body =
    List.fold_right (ce2cic premise_env) context body

  and ce2cic premise_env ce target =
    let module C = Cic in
    let module Con = Content in
      match ce with
        `Declaration d -> 
          (match d.Con.dec_name with
              Some s ->
                C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
            | None -> 
                C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
      | `Hypothesis h ->
          (match h.Con.dec_name with
              Some s ->
                C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
            | None -> 
                C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
      | `Proof p -> 
          (match p.Con.proof_name with
              Some s ->
                C.LetIn (C.Name s, proof2cic premise_env p, target)
            | None -> 
                C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
      | `Definition d -> 
           (match d.Con.def_name with
              Some s ->
                C.LetIn (C.Name s, proof2cic premise_env p, target)
            | None -> 
                C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
      | `Joint ho -> 
            raise TO_DO 

  and conclude2cic premise_env conclude =
    let module C = Cic in 
    let module Con = Content in
    if conclude.Con.conclude_method = "TD_Conversion" then
      (match conclude.Con.conclude_args with
         [Con.ArgProof p] -> proof2cic [] p (* empty! *)
       | _ -> prerr_endline "1"; assert false)
    else if conclude.Con.conclude_method = "BU_Conversion" then
      (match conclude.Con.conclude_args with
         [Con.Premise prem] -> 
           (try List.assoc prem.Con.premise_xref premise_env
            with Not_found -> 
              prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
              raise Not_found)
       | _ -> prerr_endline "2"; assert false)
    else if conclude.Con.conclude_method = "Exact" then
      (match conclude.Con.conclude_args with
         [Con.Term t] -> term2cic t
       | _ -> prerr_endline "3"; assert false)
    else if conclude.Con.conclude_method = "Intros+LetTac" then
      (match conclude.Con.conclude_args with
         [Con.ArgProof p] -> proof2cic [] p (* empty! *)
       | _ -> prerr_endline "4"; assert false)
    else if (conclude.Con.conclude_method = "ByInduction") then
      (match (List.tl conclude.Con.conclude_args) with
         Con.Term (C.AAppl 
            id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
           let subst =
             List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in 
           let cargs = args2cic premise_env args in
           let cparams_and_IP = List.map term2cic params_and_IP in
           C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
       | _ -> prerr_endline "5"; assert false)
    else if (conclude.Con.conclude_method = "Rewrite") then
      (match conclude.Con.conclude_args with
         Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
           let subst =
             List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
           let  cargs = args2cic premise_env args in
           C.Appl (C.Const(uri,subst)::cargs)
       | _ -> prerr_endline "6"; assert false)
    else if (conclude.Con.conclude_method = "Apply") then
      let cargs = (args2cic premise_env conclude.Con.conclude_args) in
      C.Appl cargs 
    else (prerr_endline "7"; assert false)

  and args2cic premise_env l =
    List.map (arg2cic premise_env) l

  and arg2cic premise_env =
    let module C = Cic in
    let module Con = Content in
    function
        Con.Aux n -> prerr_endline "8"; assert false
      | Con.Premise prem ->
          (match prem.Con.premise_n with
            Some n -> 
              C.Rel n
            | _ ->
              (try List.assoc prem.Con.premise_xref premise_env
               with Not_found -> 
                  prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
                  raise Not_found))
      | Con.Term t -> 
          term2cic t
      | Con.ArgProof p ->
          proof2cic [] p (* empty! *)
      | Con.ArgMethod s -> raise TO_DO

in proof2cic [] p
;;

let proof2cic = proof2cic Deannotate.deannotate_term;;