(* 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

let symbol_table = Hashtbl.create 1024

let sort_of_string = function
  | "Prop" -> `Prop
  | "Set" -> `Set
  | "Type" -> `Type
  | "CProp" -> `CProp
  | _ -> assert false

let get_types uri =
  match CicEnvironment.get_obj uri with
  | Cic.Constant _ -> assert false
  | Cic.Variable _ -> assert false
  | Cic.CurrentProof _ -> assert false
  | Cic.InductiveDefinition (l,_,_) -> l 

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 ids_to_uris acic =
  let register_uri id uri = Hashtbl.add ids_to_uris id uri in
  let sort_of_id id =
    try
      sort_of_string (Hashtbl.find ids_to_inner_sorts id)
    with Not_found -> assert false
  in
  let module Ast = CicAst in
  let idref id t = Ast.AttributedTerm (`IdRef id, t) in
  let rec aux = function
    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
    | 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)
    | 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 -> `Pi
          | `Prop | `CProp -> `Forall
        in
        idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
    | Cic.ACast (id,v,t) -> idref id (aux v)
    | 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, 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, [])))
    | 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, [])))

  and astsubst_of_cicsubst subst =
    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