(* Copyright (C) 2004-2005, 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 CicNotationPt

  (* TODO ensure that names generated by fresh_var do not clash with user's *)
let fresh_name =
  let index = ref ~-1 in
  fun () ->
    incr index;
    "fresh" ^ string_of_int !index

let visit_ast ?(special_k = fun _ -> assert false) k =
  let rec aux = function

    | Appl terms -> Appl (List.map k terms)
    | Binder (kind, var, body) ->
        Binder (kind, aux_capture_variable var, k body) 
    | Case (term, indtype, typ, patterns) ->
        Case (k term, indtype, aux_opt typ, aux_patterns patterns)
    | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
    | LetRec (kind, definitions, term) ->
        let definitions =
          List.map
            (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
            definitions
        in
        LetRec (kind, definitions, k term)
    | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
    | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
    | Meta (index, substs) -> Meta (index, List.map aux_opt substs)

    | (AttributedTerm _
      | Layout _
      | Literal _
      | Magic _
      | Variable _) as t -> special_k t

    | (Ident _
      | Implicit
      | Num _
      | Sort _
      | Symbol _
      | Uri _
      | UserInput) as t -> t

  and aux_opt = function
    | None -> None
    | Some term -> Some (k term)

  and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt

  and aux_patterns patterns = List.map aux_pattern patterns

  and aux_pattern ((head, vars), term) =
    ((head, List.map aux_capture_variable vars), k term)

  and aux_subst (name, term) = (name, k term)

  and aux_substs substs = List.map aux_subst substs

  in

  aux

let visit_layout k = function
  | Sub (t1, t2) -> Sub (k t1, k t2)
  | Sup (t1, t2) -> Sup (k t1, k t2)
  | Below (t1, t2) -> Below (k t1, k t2)
  | Above (t1, t2) -> Above (k t1, k t2)
  | Over (t1, t2) -> Over (k t1, k t2)
  | Atop (t1, t2) -> Atop (k t1, k t2)
  | Frac (t1, t2) -> Frac (k t1, k t2)
  | Sqrt t -> Sqrt (k t)
  | Root (arg, index) -> Root (k arg, k index)
  | Break -> Break
  | Box (kind, terms) -> Box (kind, List.map k terms)

let visit_magic k = function
  | List0 (t, l) -> List0 (k t, l)
  | List1 (t, l) -> List1 (k t, l )
  | Opt t -> Opt (k t)
  | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
  | Default (t1, t2) -> Default (k t1, k t2)

let rec strip_attributes t =
  prerr_endline "strip_attributes";
  let special_k = function
    | AttributedTerm (_, term) -> strip_attributes term
    | Magic m -> Magic (visit_magic strip_attributes m)
    | Variable _ as t -> t
    | t -> assert false
  in
  visit_ast ~special_k strip_attributes t