(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Extend
open Pcoq
open Topconstr
open Ast
open Genarg
open Libnames

(* State of the grammar extensions *)

type all_grammar_command =
  | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
  | Delimiters of (scope_name * prod_item list * prod_item list)
  | Grammar of grammar_command
  | TacticGrammar of
      (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr)
      list

let subst_all_grammar_command subst = function
  | Notation _ -> anomaly "Notation not in GRAMMAR summary"
  | Delimiters _ -> anomaly "Delimiters not in GRAMMAR summary"
  | Grammar gc -> Grammar (subst_grammar_command subst gc)
  | TacticGrammar g -> TacticGrammar g (* TODO ... *)

let (grammar_state : all_grammar_command list ref) = ref []


(**************************************************************************)
let canonise_assoc = function
  | None -> Gramext.LeftA (* camlp4 rule *)
  | Some Gramext.NonA -> Gramext.RightA
  | Some a -> a

let assoc_level = function
  | Gramext.LeftA -> "L"
  | _ -> ""

let constr_level assoc = function
  | 8 -> assert (assoc <> Some Gramext.LeftA); "top"
  | n -> (string_of_int n)^(assoc_level (canonise_assoc assoc))

let constr_prod_level = function
  | 8 -> "top"
  | n -> string_of_int n

let numeric_levels =
  ref [8,Some Gramext.RightA; 1,Some Gramext.RightA; 0,Some Gramext.RightA]

(* At a same level, LeftA takes precedence over RightA and NoneA *)
(* In case, several associativity exists for a level, we make two levels, *)
(* first LeftA, then RightA and NoneA together *)
exception Found of Gramext.g_assoc option

let eq_assoc a b = match (canonise_assoc a, canonise_assoc b) with
  | Gramext.LeftA, Gramext.LeftA -> true
  | Gramext.LeftA, _ -> false
  | _, Gramext.LeftA -> false
  | _ -> true
 
let find_position assoc = function
  | None -> None, Some (canonise_assoc assoc)
  | Some n ->
      if n = 8 & canonise_assoc assoc = Gramext.LeftA then 
	error "Left associativity not allowed at level 8";
      let after = ref (8,Some Gramext.RightA) in
      let rec add_level q = function
        | (p,_ as pa)::l when p > n -> pa :: add_level pa l
        | (p,a as pa)::l as l' when p = n ->
	    if eq_assoc a assoc then raise (Found a);
	    (* Maybe this was (p,Left) and p occurs a second time *)
	    if canonise_assoc a = Gramext.LeftA then
	      match l with
		| (p,a)::_ as l' when p = n -> raise (Found a)
		| _ -> after := pa; (n,assoc)::l'
	    else
	      (* This was not (p,LeftA) hence assoc is LeftA *)
	      (after := q; (n,assoc)::l')
	| l ->
	    after := q; (n,assoc)::l
      in
      try
        numeric_levels := add_level (8,Some Gramext.RightA) !numeric_levels;
        Some (Gramext.After (constr_level (snd !after) (fst !after))),
	Some (canonise_assoc assoc)
      with
          Found a -> Some (Gramext.Level (constr_level a n)),
	  Some (canonise_assoc a)

(* Interpretation of the right hand side of grammar rules *)

(* When reporting errors, we add the name of the grammar rule that failed *)
let specify_name name e =
  match e with
    | UserError(lab,strm) ->
        UserError(lab, (str"during interpretation of grammar rule " ++
                          str name ++ str"," ++ spc () ++ strm))
    | Anomaly(lab,strm) ->
        Anomaly(lab, (str"during interpretation of grammar rule " ++
                        str name ++ str"," ++ spc () ++ strm))
    | Failure s ->
        Failure("during interpretation of grammar rule "^name^", "^s)
    | e -> e

(* Translation of environments: a production
 *   [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
 * is written (with camlp4 conventions):
 *   (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
 * where v1..vi are the values generated by non-terminals nt1..nti.
 * Since the actions are executed by substituting an environment,
 * make_act builds the following closure:
 *
 *      ((fun env ->
 *          (fun vi -> 
 *             (fun env -> ...
 *           
 *                  (fun v1 ->
 *                     (fun env -> gram_action .. env act)
 *                     ((x1,v1)::env))
 *                  ...)
 *             ((xi,vi)::env)))
 *         [])
 *)

open Names

let make_act f pil =
  let rec make env = function
    | [] ->
	Gramext.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gramext.action (fun _ -> make env tl)
    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
        Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
    | Some (p, ETReference) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
    | Some (p, ETIdent) :: tl -> (* non-terminal *)
        Gramext.action (fun (v:identifier) ->
	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
    | Some (p, ETPattern) :: tl -> 
	failwith "Unexpected entry of type cases pattern" in
  make [] (List.rev pil)

let make_cases_pattern_act f pil =
  let rec make env = function
    | [] ->
	Gramext.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gramext.action (fun _ -> make env tl)
    | Some (p, ETPattern) :: tl -> (* non-terminal *)
        Gramext.action (fun v -> make ((p,v) :: env) tl)
    | Some (p, ETReference) :: tl -> (* non-terminal *)
        Gramext.action (fun v -> make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
    | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
	error "ident and constr entry not admitted in patterns cases syntax extensions" in
  make [] (List.rev pil)

(* Grammar extension command. Rules are assumed correct.
 * Type-checking of grammar rules is done during the translation of
 * ast to the type grammar_command.  We only check that the existing
 * entries have the type assumed in the grammar command (these types
 * annotations are added when type-checking the command, function
 * Extend.of_ast) *)

let rec build_prod_item univ assoc = function
  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc s)
  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc s)
  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc s)
  | ProdPrimitive typ ->
      match get_constr_production_entry assoc typ with
	| (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj)
	| (eobj,Some lev) -> 
	    Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev)

let symbol_of_prod_item univ assoc = function
  | Term tok -> (Gramext.Stoken tok, None)
  | NonTerm (nt, ovar) ->
      let eobj = build_prod_item univ assoc nt in
      (eobj, ovar)

let make_rule univ assoc etyp rule =
  let pil = List.map (symbol_of_prod_item univ assoc) rule.gr_production in
  let (symbs,ntl) = List.split pil in
  let f loc env = match rule.gr_action, env with
    | AVar p, [p',a] when p=p' -> a
    | AApp (AVar f,[AVar a]), [f',v;a',w] when f=f' & a=a' ->
        CApp (loc,v,[w,None])
    | AApp (AVar f,[AVar a]), [a',w;f',v] when f=f' & a=a' ->
        CApp (loc,v,[w,None])
    | pat,_ -> CGrammar (loc, pat, env) in
  let act = match etyp with
    | ETPattern -> 
        (* Ugly *)
        let f loc env = match rule.gr_action, env with
          | AVar p, [p',a] when p=p' -> a
          | _ -> error "Unable to handle this grammar extension of pattern" in
        make_cases_pattern_act f ntl
    | _ -> make_act f ntl in
  (symbs, act)

(* Rules of a level are entered in reverse order, so that the first rules
   are applied before the last ones *)
let extend_entry univ (te, etyp, pos, name, ass, rls) =
  let rules = List.rev (List.map (make_rule univ ass etyp) rls) in
  grammar_extend te pos [(name, ass, rules)]

(* Defines new entries. If the entry already exists, check its type *)
let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} =
  let typ = explicitize_entry (fst univ) n in
  let e,lev = get_constr_entry typ in
  let pos,ass = find_position ass lev in
  let name = option_app (constr_level ass) lev in
  (e,typ,pos,name,ass,rls)

(* Add a bunch of grammar rules. Does not check if it is well formed *)
let extend_grammar_rules gram =
  let univ = get_univ gram.gc_univ in
  let tl = List.map (define_entry univ) gram.gc_entries in
  List.iter (extend_entry univ) tl

(* Add a grammar rules for tactics *)
type grammar_tactic_production =
  | TacTerm of string
  | TacNonTerm of loc * (Gram.te Gramext.g_symbol * argument_type) * string option

let make_prod_item = function
  | TacTerm s -> (Gramext.Stoken (Extend.terminal s), None)
  | TacNonTerm (_,(nont,t), po) ->
      (nont, option_app (fun p -> (p,t)) po)

let make_gen_act f pil =
  let rec make env = function
    | [] -> 
	Gramext.action (fun loc -> f loc env)
    | None :: tl -> (* parse a non-binding item *)
        Gramext.action (fun _ -> make env tl)
    | Some (p, t) :: tl -> (* non-terminal *)
        Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
  make [] (List.rev pil)

let extend_constr entry pos (level,assoc) make_act pt =
  let univ = get_univ "constr" in
  let pil = List.map (symbol_of_prod_item univ assoc) pt in
  let (symbs,ntl) = List.split pil in
  let act = make_act ntl in
  grammar_extend entry pos [(level, assoc, [symbs, act])]

let extend_constr_notation (n,assoc,ntn,rule) =
  let mkact loc env = CNotation (loc,ntn,env) in
  let (e,level) = get_constr_entry (ETConstr (n,())) in
  let pos,assoc = find_position assoc level in
  extend_constr e pos (option_app (constr_level assoc) level,assoc) 
    (make_act mkact) rule

let extend_constr_delimiters (sc,rule,pat_rule) =
  let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
  extend_constr Constr.constr (Some (Gramext.Level "0"))
    (None,None)
    (make_act mkact) rule;
  let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
  extend_constr Constr.pattern None (None,None)
    (make_cases_pattern_act mkact) pat_rule

(* These grammars are not a removable *)
let make_rule univ f g (s,pt) =
  let hd = Gramext.Stoken ("IDENT", s) in
  let pil = (hd,None) :: List.map g pt in
  let (symbs,ntl) = List.split pil in
  let act = make_gen_act f ntl in
  (symbs, act)

let extend_tactic_grammar s gl =
  let univ = get_univ "tactic" in
  let make_act loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
  let rules = List.map (make_rule univ make_act make_prod_item) gl in
  Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]

let extend_vernac_command_grammar s gl =
  let univ = get_univ "vernac" in
  let make_act loc l = Vernacexpr.VernacExtend (s,List.map snd l) in
  let rules = List.map (make_rule univ make_act make_prod_item) gl in
  Gram.extend Vernac_.command None [(None, None, List.rev rules)]

let rec interp_entry_name u s =
  let l = String.length s in
  if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
    let t, g = interp_entry_name u (String.sub s 3 (l-8)) in
    List1ArgType t, Gramext.Slist1 g
  else if l > 5 & String.sub s (l-5) 5 = "_list" then
    let t, g = interp_entry_name u (String.sub s 0 (l-5)) in
    List0ArgType t, Gramext.Slist0 g
  else if l > 4 & String.sub s (l-4) 4 = "_opt" then
    let t, g = interp_entry_name u (String.sub s 0 (l-4)) in
    OptArgType t, Gramext.Sopt g
  else
    let e = get_entry (get_univ u) s in
    let o = object_of_typed_entry e in
    let t = type_of_typed_entry e in
    t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)

let qualified_nterm current_univ = function
  | NtQual (univ, en) -> (univ, en)
  | NtShort en -> (current_univ, en)

let make_vprod_item univ = function
  | VTerm s -> (Gramext.Stoken (Extend.terminal s), None)
  | VNonTerm (loc, nt, po) ->
      let (u,nt) = qualified_nterm univ nt in
      let (etyp, e) = interp_entry_name u nt in
      e, option_app (fun p -> (p,etyp)) po

let add_tactic_entries gl =
  let univ = get_univ "tactic" in
  let make_act s tac loc l = Tacexpr.TacAlias (s,l,tac) in
  let f (s,l,tac) =
    make_rule univ (make_act s tac) (make_vprod_item "tactic") l in
  let rules = List.map f gl in
  grammar_extend Tactic.simple_tactic None [(None, None, List.rev rules)]

let extend_grammar gram =
  (match gram with
  | Notation a -> extend_constr_notation a
  | Delimiters a -> extend_constr_delimiters a
  | Grammar g -> extend_grammar_rules g
  | TacticGrammar l -> add_tactic_entries l);
  grammar_state := gram :: !grammar_state


(* Summary functions: the state of the lexer is included in that of the parser.
   Because the grammar affects the set of keywords when adding or removing
   grammar rules. *)
type frozen_t = all_grammar_command list * Lexer.frozen_t

let freeze () = (!grammar_state, Lexer.freeze ())

(* We compare the current state of the grammar and the state to unfreeze, 
   by computing the longest common suffixes *)
let factorize_grams l1 l2 =
  if l1 == l2 then ([], [], l1) else list_share_tails l1 l2

let number_of_entries gcl =
  List.fold_left
    (fun n -> function
      | Notation _ -> n + 1
      | Delimiters _ -> n + 2 (* One rule for constr, one for pattern *)
      | Grammar gc -> n + (List.length gc.gc_entries)
      | TacticGrammar l -> n + 1)
    0 gcl

let unfreeze (grams, lex) =
  let (undo, redo, common) = factorize_grams !grammar_state grams in
  remove_grammars (number_of_entries undo);
  grammar_state := common;
  Lexer.unfreeze lex;
  List.iter extend_grammar (List.rev redo)
    
let init_grammar () =
  remove_grammars (number_of_entries !grammar_state);
  grammar_state := []

let _ = Lexer.init ()

let init () =
  init_grammar ()