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

let debug = true
let debug_print s =
  if debug then begin
    prerr_endline "<NEW_TEXTUAL_PARSER>";
    prerr_endline s;
    prerr_endline "</NEW_TEXTUAL_PARSER>"
  end

let grammar = Grammar.gcreate Lexer.lex

let term = Grammar.Entry.create grammar "term"
(* let tactic = Grammar.Entry.create grammar "tactic" *)
(* let tactical = Grammar.Entry.create grammar "tactical" *)

let return_term loc term = Ast.LocatedTerm (loc, term)
(* let return_term loc term = term *)

let fail (x, y) msg =
  failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)

EXTEND
  GLOBAL: term;
  meta_subst: [
    [ s = SYMBOL "_" -> None
    | t = term -> Some t ]
  ];
  binder: [
    [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
    | SYMBOL <:unicode<pi>> (* π *) -> `Pi
    | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
    | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
    ]
  ];
  substituted_name: [ (* a subs.name is an explicit substitution subject *)
    [ s = [ IDENT | SYMBOL ];
      subst = OPT [
        SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
        LPAREN "[";
        substs = LIST1 [
          i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
        ] SEP SYMBOL ";";
        RPAREN "]" ->
          substs
      ] ->
        (match subst with
        | Some l -> Ast.Ident (s, l)
        | None -> Ast.Ident (s, []))
    ]
  ];
  name: [ (* as substituted_name with no explicit substitution *)
    [ s = [ IDENT | SYMBOL ] -> s ]
  ];
  pattern: [
    [ n = name -> [n]
    | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ]
  ];
  term:
    [ "arrow" RIGHTA
      [ t1 = term; SYMBOL <:unicode<to>>; t2 = term ->
          return_term loc (Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
      ]
    | "eq" LEFTA
      [ t1 = term; SYMBOL "="; t2 = term ->
        return_term loc (Ast.Appl_symbol ("eq", [t1; t2]))
      ]
    | "add" LEFTA     [ (* nothing here by default *) ]
    | "mult" LEFTA    [ (* nothing here by default *) ]
    | "inv" NONA      [ (* nothing here by default *) ]
    | "simple" NONA
      [
        b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
        typ = OPT [ SYMBOL ":"; t = term -> t ];
        SYMBOL "."; body = term ->
          let binder =
            List.fold_right
              (fun var body -> Ast.Binder (b, Cic.Name var, typ, body))
              vars body
          in
          return_term loc binder
      | sort_kind = [
          "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp
        ] ->
          Ast.Sort sort_kind
      | n = substituted_name -> return_term loc n
      | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
          return_term loc (Ast.Appl (head :: args))
      | i = INT -> return_term loc (Ast.Num i)
      | m = META;
        substs = [
          LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->
            substs
        ] ->
            let index =
              try
                int_of_string (String.sub m 1 (String.length m - 1))
              with Failure "int_of_string" ->
                fail loc ("Invalid meta variable number: " ^ m)
            in
            return_term loc (Ast.Meta (index, substs))
        (* actually "in" and "and" are _not_ keywords. Parsing works anyway
         * since applications are required to be bound by parens *)
      | "let"; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *); t1 = term;
        IDENT "in"; t2 = term ->
          return_term loc (Ast.LetIn (name, t1, t2))
      | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
          defs = LIST1 [
          name = IDENT;
          index = OPT [ LPAREN "("; index = INT; RPAREN ")" ->
            int_of_string index
          ];
          typ = OPT [ SYMBOL ":"; typ = term -> typ ];
          SYMBOL <:unicode<def>> (* ≝ *); t1 = term ->
            (name, t1, typ, (match index with None -> 1 | Some i -> i))
        ] SEP (IDENT "and");
        IDENT "in"; body = term ->
          return_term loc (Ast.LetRec (ind_kind, defs, body))
      | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ];
        "match"; t = term;
        SYMBOL ":"; indty = IDENT;
        "with";
        LPAREN "[";
        patterns = LIST0 [
          p = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); t = term -> (p, t)
        ] SEP SYMBOL "|";
        RPAREN "]" ->
          return_term loc (Ast.Case (t, indty, outtyp, patterns))
      | LPAREN "("; t = term; RPAREN ")" -> return_term loc t
      ]
    ];
END

let parse_term = Grammar.Entry.parse term

(*
open Disambiguate_struct
open ProofEngineHelpers

exception UnknownIdentifier of string
exception InductiveTypeExpected 

let list_of_domain dom = Domain.fold (fun s acc -> s :: acc) dom []
let apply_interp (interp: interpretation) item = snd (interp item)

let pre_disambiguate ~context ast =
  let rec aux loc context = function
    | Ast.LocatedTerm (loc, term) -> aux loc context term
    | Ast.Appl terms ->
        let (dom, funs) =
          List.fold_left
            (fun (dom, funs) term ->
              let (dom', f) = aux loc context term in
              (Domain.union dom dom', f :: funs))
            (Domain.empty, [])
            terms
        in
        let f interp =
          Cic.Appl (List.map (fun f -> f interp) (List.rev funs))
        in
        (dom, f)
    | Ast.Appl_symbol (symb, args) ->
        let (dom, funs) =
          List.fold_left
            (fun (dom, funs) term ->
              let (dom', f) = aux loc context term in
              (Domain.union dom dom', f :: funs))
            (Domain.empty, [])
            args
        in
        (Domain.add (Symbol (symb, 0)) dom,
         (fun interp ->
           apply_interp interp (Symbol (symb, 0)) interp
            (List.map (fun f -> f interp) funs)))
    | Ast.Binder (binder_kind, var, typ, body) ->
        let (type_dom, type_f) =
          match typ with
          | Some t -> aux loc context t
          | None -> (Domain.empty, (fun _ -> Cic.Implicit))
        in
        let (dom', body_f) = aux loc (Some var :: context) body in
        let dom'' = Domain.union dom' type_dom in
        (dom'',
         match binder_kind with
         | `Lambda ->
             (fun interp ->
               Cic.Lambda (var, type_f interp, body_f interp))
         | `Pi | `Forall ->
             (fun interp ->
               Cic.Prod (var, type_f interp, body_f interp))
         | `Exists ->
             (fun interp ->
               let typ = type_f interp in
               Cic.Appl
                [ apply_interp interp (Id "ex") interp [];
                  typ;
                  (Cic.Lambda (var, typ, body_f interp)) ]))
    | Ast.Case (term, indty_ident, outtype, branches) ->
        let (term_dom, term_f) = aux loc context term in
        let (outtype_dom, outtype_f) =
          match outtype with
          | Some typ -> aux loc context typ
          | None -> (Domain.empty, (fun _ -> Cic.Implicit))
        in
        let do_branch (pat, term) =
          let rec do_branch' context = function
            | [] -> aux loc context term
            | hd :: tl ->
                let (dom, f) = do_branch' (Some (Cic.Name hd) :: context) tl in
                (dom,
                 (fun interp ->
                   Cic.Lambda (Cic.Name hd, Cic.Implicit, f interp)))
          in
          match pat with
          | _ :: tl -> (* ignoring constructor *)
              do_branch' context tl
          | [] -> assert false
        in
        let (branches_dom, branches_f) =
          List.fold_right
            (fun branch (dom, f) ->
              let (dom', f') = do_branch branch in
              Domain.union dom dom', (fun interp -> f' interp :: f interp))
            branches
            (Domain.empty, (fun _ -> []))
        in
        (Domain.union outtype_dom (Domain.union term_dom branches_dom),
         (fun interp ->
           let (indtype_uri, indtype_no) =
             match apply_interp interp (Id indty_ident) interp [] with
             | Cic.MutInd (uri, tyno, _) -> uri, tyno
             | _ -> assert false
           in
           Cic.MutCase (indtype_uri, indtype_no, outtype_f interp,
            term_f interp, branches_f interp)))
    | Ast.LetIn (var, body, where) ->
        let (body_dom, body_f) = aux loc context body in
        let (where_dom, where_f) = aux loc context where in
        (Domain.union body_dom where_dom,
         fun interp -> Cic.LetIn (Cic.Name var, body_f interp, where_f interp))
    | Ast.LetRec (kind, defs, where) ->
        let context' =
          List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
            context defs
        in
        let (where_dom, where_f) = aux loc context' where in
        let inductiveFuns =
          List.map
            (fun (var, body, typ, decr_idx) ->
              let body_dom, body_f = aux loc context' body in
              let typ_dom, typ_f =
                match typ with
                | None -> (Domain.empty, (fun _ -> Cic.Implicit))
                | Some typ -> aux loc context' typ
              in
              (Domain.union body_dom typ_dom,
               (fun interp ->
                 (var, decr_idx, typ_f interp, body_f interp))))
            defs
        in
        let dom =
          List.fold_left (fun acc (dom, _) -> Domain.union acc dom)
            where_dom inductiveFuns
        in
        let inductiveFuns interp =
          List.map (fun (_, g) -> g interp) inductiveFuns
        in
        let build_term counter funs =
          (* this is the body of the fold_right function below. Rationale: Fix
           * and CoFix cases differs only in an additional index in the
           * indcutiveFun list, see Cic.term *)
          match kind with
          | `Inductive ->
              (fun (var, _, _, _) cic ->
                incr counter;
                Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
          | `CoInductive ->
              let funs =
                List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
              in
              (fun (var, _, _, _) cic ->
                Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
        in
        (dom,
         (fun interp ->
           let counter = ref 0 in
           let funs = inductiveFuns interp in
           List.fold_right (build_term counter funs) funs (where_f interp)))
    | Ast.Ident (name, subst) ->
        (* TODO hanlde explicit substitutions *)
        let rec find acc e = function
          | [] -> raise Not_found
          | Some (Cic.Name hd) :: tl when e = hd -> acc
          | _ :: tl ->  find (acc + 1) e tl
        in
        (try
          let index = find 1 name context in
          if subst <> [] then
            fail loc "Explicit substitutions not allowed here";
          (Domain.empty, fun _ -> Cic.Rel index)
        with Not_found ->
          (Domain.singleton (Id name),
           (fun interp -> apply_interp interp (Id name) interp [])))
    | Ast.Num num ->
        (* TODO check to see if num can be removed from the domain *)
        (Domain.singleton (Num (num, 0)),
          (fun interp -> apply_interp interp (Num (num, 0)) interp []))
    | Ast.Meta (index, subst) ->
        let (dom, funs) =
          List.fold_left
            (fun (dom, funs) term ->
              match term with
              | None -> (dom, (fun _ -> None) :: funs)
              | Some term ->
                  let (dom', f) = aux loc context term in
                  (Domain.union dom dom',
                   (fun interp -> Some (f interp)) :: funs))
            (Domain.empty, [])
            subst
        in
        let f interp =
          Cic.Meta (index, List.map (fun f -> f interp) (List.rev funs))
        in
        (dom, f)
    | Ast.Sort `Prop -> Domain.empty, fun _ -> Cic.Sort Cic.Prop
    | Ast.Sort `Set -> Domain.empty, fun _ -> Cic.Sort Cic.Set
    | Ast.Sort `Type -> Domain.empty, fun _ -> Cic.Sort Cic.Type
    | Ast.Sort `CProp -> Domain.empty, fun _ -> Cic.Sort Cic.CProp
  in
  match ast with
  | Ast.LocatedTerm (loc, term) ->
      let (dom, f) = aux loc context term in
      dom, f
  | _ -> assert false

let main ~context char_stream =
  let term_ast = parse_term char_stream in
  debug_print (Pp.pp_term term_ast);
  pre_disambiguate ~context term_ast
*)