(* Copyright (C) 2004, 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://helm.cs.unibo.it/
 *)

open Printf

module Ast = CicAst

let symbol_table = Hashtbl.create 1024

let get_types uri =
  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
    match o with
      | Cic.InductiveDefinition (l,_,_,_) -> l 
      | _ -> assert false

let name_of_inductive_type uri i = 
  let types = get_types uri in
  let (name, _, _, _) = try List.nth types i with Not_found -> assert false in
  name

  (* returns <name, type> pairs *)
let constructors_of_inductive_type uri i =
  let types = get_types uri in
  let (_, _, _, constructors) = 
    try List.nth types i with Not_found -> assert false
  in
  constructors

  (* returns name only *)
let constructor_of_inductive_type uri i j =
  (try
    fst (List.nth (constructors_of_inductive_type uri i) (j-1))
  with Not_found -> assert false)

let ast_of_acic ids_to_inner_sorts acic =
  let ids_to_uris = Hashtbl.create 503 in
  let register_uri id uri = Hashtbl.add ids_to_uris id uri in
  let sort_of_id id =
    try
      Hashtbl.find ids_to_inner_sorts id
    with Not_found -> assert false
  in
  let idref id t = Ast.AttributedTerm (`IdRef id, t) in
  let rec aux =
    function
    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
    | Cic.AVar (id,uri,subst) ->
        register_uri id (UriManager.string_of_uri uri);
        idref id
          (Ast.Ident (UriManager.name_of_uri uri, astsubst_of_cicsubst subst))
    | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
    | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
    | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *)
    | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
    | Cic.AImplicit _ -> assert false
    | Cic.AProd (id,n,s,t) ->
        let binder_kind =
          match sort_of_id id with
          | `Set | `Type | `Meta -> `Pi
          | `Prop | `CProp -> `Forall
        in
        idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
    | Cic.ACast (id,v,t) ->
        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); aux v; aux t])
    | Cic.ALambda (id,n,s,t) ->
        idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t))
    | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t))
    | Cic.AAppl (aid,Cic.AConst (sid,uri,subst)::tl) ->
        let uri_str = UriManager.string_of_uri uri in
        register_uri sid uri_str;
        (try 
          let f = Hashtbl.find symbol_table uri_str in
          f aid sid tl aux
        with Not_found ->
          idref aid
            (Ast.Appl (idref sid
              (Ast.Ident (UriManager.name_of_uri uri,
                astsubst_of_cicsubst subst)) :: (List.map aux tl))))
    | Cic.AAppl (aid,Cic.AMutInd (sid,uri,i,subst)::tl) ->
        let name = name_of_inductive_type uri i in
        let uri_str = UriManager.string_of_uri uri in
        let puri_str =
         uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
        register_uri sid puri_str;
        (try 
          (let f = Hashtbl.find symbol_table puri_str in
           f aid sid tl aux)
         with Not_found ->
           idref aid
            (Ast.Appl (idref sid
              (Ast.Ident (name,
                astsubst_of_cicsubst subst)) :: (List.map aux tl))))
    | Cic.AAppl (id,li) -> idref id (Ast.Appl (List.map aux li))
    | Cic.AConst (id,uri,subst) ->
        let uri_str = UriManager.string_of_uri uri in
        register_uri id uri_str;
        (try
          let f = Hashtbl.find symbol_table uri_str in
          f "dummy" id [] aux
        with Not_found ->
          idref id
            (Ast.Ident
              (UriManager.name_of_uri uri, astsubst_of_cicsubst subst)))
    | Cic.AMutInd (id,uri,i,subst) ->
        let name = name_of_inductive_type uri i in
        let uri_str = UriManager.string_of_uri uri in
        let puri_str =
         uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
        register_uri id puri_str;
        (try
          let f = Hashtbl.find symbol_table puri_str in
          f "dummy" id [] aux
        with Not_found ->
          idref id (Ast.Ident (name, astsubst_of_cicsubst subst)))
    | Cic.AMutConstruct (id,uri,i,j,subst) ->
        let name = constructor_of_inductive_type uri i j in
        let uri_str = UriManager.string_of_uri uri in
        let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in
        register_uri id puri_str;
        (try
          let f = Hashtbl.find symbol_table puri_str in
          f "dummy" id [] aux
        with Not_found ->
          idref id (Ast.Ident (name, astsubst_of_cicsubst subst)))
    | Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
        let name = name_of_inductive_type uri typeno in
        let constructors = constructors_of_inductive_type uri typeno in
        let rec eat_branch ty pat =
          match (ty, pat) with
          | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
              let (cv, rhs) = eat_branch t t' in
              (name, Some (aux s)) :: cv, rhs
          | _, _ -> [], aux pat
        in
        let patterns =
          List.map2
            (fun (name, ty) pat ->
              let (capture_variables, rhs) = eat_branch ty pat in
              ((name, capture_variables), rhs))
            constructors patterns
        in
        idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns))
    | Cic.AFix (id, no, funs) -> 
        let defs = 
          List.map
            (fun (_, n, decr_idx, ty, bo) ->
              ((Cic.Name n, Some (aux ty)), aux bo, decr_idx))
            funs
        in
        let name =
          try
            (match List.nth defs no with
            | (Cic.Name n, _), _, _ -> n
            | _ -> assert false)
          with Not_found -> assert false
        in
        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
    | Cic.ACoFix (id, no, funs) -> 
        let defs = 
          List.map
            (fun (_, n, ty, bo) -> ((Cic.Name n, Some (aux ty)), aux bo, 0))
            funs
        in
        let name =
          try
            (match List.nth defs no with
            | (Cic.Name n, _), _, _ -> n
            | _ -> assert false)
          with Not_found -> assert false
        in
        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))

  and astsubst_of_cicsubst subst =
    Some
      (List.map (fun (uri, annterm) ->
        (UriManager.name_of_uri uri, aux annterm))
        subst)

  and astcontext_of_ciccontext context =
    List.map
      (function
        | None -> None
        | Some annterm -> Some (aux annterm))
      context

  in
  aux acic, ids_to_uris

let _ = (** fill symbol_table *)
  let add_symbol name uri =
    Hashtbl.add symbol_table uri
      (fun aid sid args acic2ast ->
        Ast.AttributedTerm (`IdRef aid,
          Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, 0)) ::
            List.map acic2ast args)))
  in
    (* eq *)
  Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
    (fun aid sid args acic2ast ->
      Ast.AttributedTerm (`IdRef aid,
        Ast.Appl (
          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", 0)) ::
          List.map acic2ast (List.tl args))));
    (* exists *)
  Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI 
    (fun aid sid args acic2ast ->
     match (List.tl args) with
       [Cic.ALambda (_,Cic.Name n,s,t)] ->
         Ast.AttributedTerm (`IdRef aid,
          Ast.Binder (`Exists, (Cic.Name n, Some (acic2ast s)), acic2ast t))
    | _ -> raise Not_found);
  add_symbol "and" HelmLibraryObjects.Logic.and_XURI;
  add_symbol "or" HelmLibraryObjects.Logic.or_XURI;
  add_symbol "iff" HelmLibraryObjects.Logic.iff_SURI;
  add_symbol "not" HelmLibraryObjects.Logic.not_SURI;
  add_symbol "inv" HelmLibraryObjects.Reals.rinv_SURI;
  add_symbol "opp" HelmLibraryObjects.Reals.ropp_SURI;
  add_symbol "leq" HelmLibraryObjects.Peano.le_XURI;
  add_symbol "leq" HelmLibraryObjects.Reals.rle_SURI;
  add_symbol "lt" HelmLibraryObjects.Peano.lt_SURI;
  add_symbol "lt" HelmLibraryObjects.Reals.rlt_SURI;
  add_symbol "geq" HelmLibraryObjects.Peano.ge_SURI;
  add_symbol "geq" HelmLibraryObjects.Reals.rge_SURI;
  add_symbol "gt" HelmLibraryObjects.Peano.gt_SURI;
  add_symbol "gt" HelmLibraryObjects.Reals.rgt_SURI;
  add_symbol "plus" HelmLibraryObjects.Peano.plus_SURI;
  add_symbol "plus" HelmLibraryObjects.BinInt.zplus_SURI;
  add_symbol "times" HelmLibraryObjects.Peano.mult_SURI;
  add_symbol "times" HelmLibraryObjects.Reals.rmult_SURI;
  add_symbol "minus" HelmLibraryObjects.Peano.minus_SURI;
  add_symbol "minus" HelmLibraryObjects.Reals.rminus_SURI;
  add_symbol "div" HelmLibraryObjects.Reals.rdiv_SURI;
  Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
  (fun aid sid args acic2ast ->
    Ast.AttributedTerm (`IdRef sid, Ast.Num ("0", 0)));
  Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
  (fun aid sid args acic2ast ->
    Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", 0)));
    (* plus *)
  Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
    (fun aid sid args acic2ast ->
     let appl () =
       Ast.AttributedTerm (`IdRef aid,
        Ast.Appl (
          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", 0)) ::
          List.map acic2ast args))
     in
      let rec aux acc = function
        | [ Cic.AConst (nid, uri, []); n] when
            UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
              (match n with
              | Cic.AConst (_, uri, []) when
                 UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
                   Ast.AttributedTerm (`IdRef aid,
                    Ast.Num (string_of_int (acc + 2), 0))
              | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
                  UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
                    aux (acc + 1) args
              | _ -> appl ())
        | _ -> appl ()
      in
      aux 0 args)