/*  THIS IS A PARTIAL TRANSLATION FROM Isabelle2016-1 ...

     Title:      Pure/Syntax/ast.ML

     Author:     Markus Wenzel, TU Muenchen

 Abstract syntax trees, translation rules, matching and normalization of asts.

 */

 package isac.gui.mawen.syntax

 import isac.gui.mawen.scalaterm.Util

 import isac.gui.mawen.syntax.isabelle.XLibrary

 import scala.collection.immutable.TreeMap

 object Ast {

   sealed abstract class Ast

   case class Constant(name: String) extends Ast // operator 

   case class Variable(name: String) extends Ast 

   case class Appl(name: List[Ast]) extends Ast  // invariant: List[Ast].length > 1

   /*the list of subasts of an Appl node has to contain at least 2 elements, i.e.

   there are no empty asts or nullary applications; use mk_appl for convenience*/

   def mk_appl(f : Ast, args : List[Ast]) : Ast =

   args match {

     case Nil => f

     case _ => Appl(f :: args)

   }

   def is_atom(a : Ast) = a match {

     case Constant(_) => true

     case Variable(_) => true

     case Appl(_) => false

   }

   def prefix_string_of(ast : Ast) : String = ast match {

     case Constant(str) =>  XSyntax.isa_ast(str)

     case Variable(str) =>  str

     case Appl(names) => {

       names.map { x => prefix_string_of(x) }.mkString(" ")

     }

   }

   //the root "_list" has been dropped in to_str (how handle lists of lists ?)

   def to_list(args: Ast, prior: Int, l_r: String): String = args match {

     case Variable(v) => to_str(Variable(v), 0, "none")

     case Appl(List(Constant("_args"), a, arg)) =>

       to_str(a, 0, "none") + ", " + to_list(arg, 0, "none")

     case ast => to_str(ast, 0, "none") //the last element

   }

   def to_tuple(ast: Ast, prior: Int, l_r: String): String = ast match {

     case Appl(List(Constant("_tuple"), a1, a2)) =>

       "(" + to_str(a1, 0, "none") + to_tuple(a2, 0, "none")

     case Appl(List(Constant("_tuple_args"), a1, a2)) =>

       ", " + to_str(a1, 0, "none") + to_tuple(a2, 0, "none")

     case Appl(List(Constant("_tuple_arg"), arg)) =>

       ", " + to_str(arg, 0, "none") + ")"

     case ast => to_str(ast, 0, "none") //the last element

   }

   // set parentheses according to priority and to left/right associativity

   def to_binop(str: String, a1: Ast, a2: Ast, prior: Int, l_r: String): String = { val pri = XSyntax.isa_prior(str)

     if (prior > pri) {

        XSyntax.isa_fix(str) match {

        case "infixl" => XLibrary.enclose("(", ")", to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right"))

        case "infixr" => XLibrary.enclose("(", ")", to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right"))

        case "prefix" => XLibrary.enclose("(", ")", XSyntax.isa_math(str) + to_str(a1, pri, "left") + to_str(a2, pri, "right"))}

     }else{

        XSyntax.isa_fix(str) match {

        case "infixl" => {

          if (prior == pri & l_r == "right") {

            XLibrary.enclose("(", ")", to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right"))

          }else{

            to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right")

          }

        }

        case "infixr" => {

          if (prior == pri & l_r == "left") {

            XLibrary.enclose("(", ")", to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right"))

          }else{

            to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right")

          }

        }

        case "prefix" => XSyntax.isa_math(str) + to_str(a1, pri, "none") + " " + to_str(a2, pri, "none")}

     } }

   /* transform an Ast into a String, which corresponds to Isabelle's 

    * pretty_printing within Isac's Knowledge, restricted for prototyping.

    */

   def to_str (ast: Ast, prior: Int, l_r: String): String = ast match {

     case Constant("GAP") => "#"

     case Constant(str) => XSyntax.isa_math(str)

     case Variable(str) => XLibrary.cut_long_ident(str)

     case Appl(List(Variable(str), a)) => //ONLY univariate functions expected

       if (Set("Probl" /*prelim.test*/, "Problem").contains(str))

         XSyntax.isa_math(str) + to_tuple(a, 0, "none")

       else

         to_str(Variable(str), 0, "none") + XLibrary.enclose(" (", ")", to_str(a, 0, "none"))

     case Appl(List(Constant("CURSOR"), a)) => to_str(a, prior, "none")

     case Appl(List(a, Constant("CURSOR"))) => to_str(a, prior, "none")

     case Appl(List(Constant("_list"), a)) => XLibrary.enclose("[", "]", to_list(a, prior, "none"))

     case Appl(List(Constant("_tuple"), a1, a2)) => to_tuple(Appl(List(Constant("_tuple"), a1, a2)), prior, "none")

     case Appl(List(Constant(str), a))  if str.startsWith("BOX") => to_str(a, prior, "none") 

     case Appl(List(Constant(str), a)) => {

       val uniop = XSyntax.isa_math(str)

       if (Set("Diff ", "Integrate ", "solve ").contains(uniop)) uniop + to_tuple(a, 0, "none")

       else if (prior == 99 & XSyntax.isa_prior(str) == 99) //FIXME: handles "d_d x (! sin(_) !)" as special case

         XLibrary.enclose("(", ")", uniop + XLibrary.enclose("(", ")", to_str(a, 0, "none")))

       else

         uniop + XLibrary.enclose("(", ")", to_str(a, 0, "none"))

       }

     case Appl(List(Constant(str), a)) if str.startsWith("BOX") => to_str(a, prior, "none")

     case Appl(List(Constant(str), a1, a2)) => to_binop(str, a1, a2, prior, l_r)

     case Appl(asts) => XLibrary.strs_to_str(asts.map(x => {

       val str = Ast.to_str(x, 0, "none"); if (is_atom(x)) str else XLibrary.enclose("(", ")", str)

       }))

   }    

   // infix: "left" or "right" associativity ---------vvvv

   def math_string_of(t: Ast): String = to_str(t, 0, "none")

   /*

     fun string_of (Ast.Constant str) = "Constant" ^ enclose "(" ")" (quote str)

       | string_of (Ast.Variable str) = "Variable" ^ enclose "(" ")" (quote str)

       | string_of (Ast.Appl asts) = "Appl " ^ enclose "[" "]" (commas (map string_of asts))

    */

   def raw_string_of (ast: Ast): String = ast match {

     case Constant(str) => "Constant" + XLibrary.enclose("(", ")", XLibrary.quote(str))

     case Variable(str) => "Variable" + XLibrary.enclose("(", ")", XLibrary.quote(str))

     case Appl(asts) =>

       "Appl" + XLibrary.enclose("(List(", "))", XLibrary.commas(asts.map ( x => raw_string_of(x) )))

   }

   /*

    * translation from Isabelle2016-1 ~~/src/Pure/Syntax/ast.ML

    * "match" is a Scala keyword

   (*  match = fn: ast -> ast -> (ast Symtab.table * ast list) option*)

   fun match ast pat =

     let

       exception NO_MATCH;

       (*  mtch = fn: ast -> ast -> ast Symtab.table -> ast Symtab.table *)

       fun mtch (Constant a) (Constant b) env =

             if a = b then env else raise NO_MATCH

         | mtch (Variable a) (Constant b) env =

             if a = b then env else raise NO_MATCH

         | mtch ast (Variable x) env = Symtab.update (x, ast) env

                                            (*update: key * 'a -> 'a table -> 'a table*)

         | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env

         | mtch _ _ _ = raise NO_MATCH

       (*  mtch_lst = fn: ast list -> ast list -> ast Symtab.table -> ast Symtab.table *)

       and mtch_lst (ast :: asts) (pat :: pats) env =

             mtch_lst asts pats (mtch ast pat env)

         | mtch_lst [] [] env = env

         | mtch_lst _ _ _ = raise NO_MATCH;

       (*   ast * (ast list) *)

       val (head, args) =

         (case (ast, pat) of

           (Appl asts, Appl pats) =>

             let val a = length asts and p = length pats in

               if a > p then (Appl (take p asts), drop p asts)

               else (ast, [])

             end

         | _ => (ast, []));

     in

         (* (ast Symtab.table          * ast list) *)

       SOME (mtch head pat Symtab.empty, args    ) handle NO_MATCH => NONE

     end;

    */

   def matches (ast_pat: Tuple2[Ast, Ast]) : Option[(TreeMap[String, Ast], List[Ast])] = {

     case class NO_MATCH() extends Exception()

     def mtch (ast_pat: Tuple2[Ast, Ast], env: TreeMap[String, Ast])

       : TreeMap[String, Ast] = ast_pat match {

         case ((Ast.Constant(a), Ast.Constant(b))) => 

           if (a == b) env else throw new NO_MATCH

         case ((Ast.Variable(a), Ast.Constant(b))) =>

           if (a == b) env else throw new NO_MATCH

         case ((ast, Ast.Variable(x))) => env + ((x, ast))

         case ((Appl(asts), Appl(pats))) => mtch_lst ((asts, pats), env)

         case (_) => throw new NO_MATCH

     }

     def mtch_lst (asts_pats: Tuple2[List[Ast], List[Ast]], env: TreeMap[String, Ast])

       : TreeMap[String, Ast] = asts_pats match {

         case ((ast :: asts, pat :: pats)) =>

           mtch_lst ((asts, pats), mtch ((ast, pat), env))

         case ((List(), List())) => env

         case (_) => throw new NO_MATCH      

     }

     val (head, args) = ast_pat match {

       case ((Appl(asts), Appl(pats))) => {

         val a = asts.length

         val p = pats.length

         if (a > p) {(Ast.Appl(asts.take(p)), asts.drop(p))}

         else (ast_pat._1, List())

       }

       case ((_,_)) => (ast_pat._1, List())

     }

     try {

       Some (mtch ((head, ast_pat._2), new TreeMap()), args)

     } catch {

       case c: NO_MATCH => None

     }

   }

   /*

   translation from Isabelle2016-1 ~~/src/Pure/Syntax/ast.ML

    *

   (*      = fn: Proof.context -> (string -> (ast * ast) list) -> ast -> ast*)

   fun normalize ctxt get_rules pre_ast =

     let

       val trace = Config.get ctxt trace;

       val stats = Config.get ctxt stats;

       val passes = Unsynchronized.ref 0;

       val failed_matches = Unsynchronized.ref 0;

       val changes = Unsynchronized.ref 0;

       (* = fn: ast Symtab.table -> ast -> ast*)

       fun subst _ (ast as Constant _) = ast

         | subst env (Variable x) = the (Symtab.lookup env x)

         | subst env (Appl asts) = Appl (map (subst env) asts);

       (*      = fn: (ast * ast) list -> ast -> ast option*)

       fun try_rules ((lhs, rhs) :: pats) ast =

             (case match ast lhs of

               SOME (env, args) =>

                 (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))

             | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))

         | try_rules [] _ = NONE;

       (* = fn: ast -> ast option *)

       val try_headless_rules = try_rules (get_rules "");

       (* = fn: ast -> string -> ast option *)

       fun try ast a =

         (case try_rules (get_rules a) ast of

           NONE => try_headless_rules ast

         | some => some);

       (* = fn: ast -> ast option *)

       fun rewrite (ast as Constant a) = try ast a

         | rewrite (ast as Variable a) = try ast a

         | rewrite (ast as Appl (Constant a :: _)) = try ast a

         | rewrite (ast as Appl (Variable a :: _)) = try ast a

         | rewrite ast = try_headless_rules ast;

       (* = fn: ast -> ast -> unit *)

       fun rewrote old_ast new_ast =

         if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast)))

         else ();

       (* = fn: ast -> ast *)

       fun norm_root ast =

         (case rewrite ast of

           SOME new_ast => (rewrote ast new_ast; norm_root new_ast)

         | NONE => ast);

       (* = fn: ast -> ast *)

       fun norm ast =

         (case norm_root ast of

           Appl sub_asts =>

             let

               val old_changes = ! changes;

               val new_ast = Appl (map norm sub_asts);

             in

               if old_changes = ! changes then new_ast else norm_root new_ast

             end

         | atomic_ast => atomic_ast);

       (* = fn: ast -> ast *)

       fun normal ast =

         let

           val old_changes = ! changes;

           val new_ast = norm ast;

         in

           Unsynchronized.inc passes;

           if old_changes = ! changes then new_ast else normal new_ast

         end;

       val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();

       val post_ast = normal pre_ast;

       val _ =

         if trace orelse stats then

           tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^

             string_of_int (! passes) ^ " passes, " ^

             string_of_int (! changes) ^ " changes, " ^

             string_of_int (! failed_matches) ^ " matches failed")

         else ();

     in post_ast end;

   * 

   * The translation to Scala drops the (logical) context and simplifies Symtab.table.

   * In case Scala code is copied, the respective source is indicated.

   */

   //~~/src/Pure/PIDE/document.scala

   // private def fail[A]: A = throw new State.Fail(this)

   // def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)

   private def fail[A]: A = throw new Exception()

   def normalize(get_rules: String => List[Tuple2[Ast, Ast]], pre_ast: Ast) = {

     //def get_rules(key: String) = XSyntax.print_rules(key)  //used BEFORE made local to normalize

     var failed_matches = 0

     var changes = 0

     def subst(env: TreeMap[String, Ast]) (ast: Ast) : Ast = ast match {

       case Constant(x) => Constant(x)

       case Variable(x) => env.getOrElse(x, fail)

       case Appl(asts) => Appl(asts.map(x => subst(env)(x)))

     }

     def try_rules(rules: List[Tuple2[Ast, Ast]], ast: Ast): Option[Ast] = rules match {

       case ((lhs, rhs) :: pats) => {

         matches(ast, lhs) match {    //matches <- match ..Scala keyword

           case Some((env, args)) => {

             changes = changes + 1

             Some(mk_appl(subst(env)(rhs), args))

           }

           case None => {

             failed_matches = failed_matches + 1

             try_rules(pats, ast)

           }

         }

       }

       case Nil => { None }

     }    

     def try_headless_rules(ast: Ast) = try_rules(get_rules(""), ast)

     //   try is a Scala keyword

     def xtry(ast: Ast, a: String): Option[Ast] =

       try_rules (get_rules(a), ast) match {

         case None => try_headless_rules(ast)

         case some => some

       }

     def rewrite(ast: Ast) = ast match {

       case Constant(a) => xtry(ast, a)

       case Variable(a) => xtry(ast, a)

       case Appl (Constant(a) :: _) => xtry(ast, a)

       case Appl (Variable(a) :: _) => xtry(ast, a)

       case a => try_headless_rules(a)

     }

     def rewrote (old_ast: Ast, new_ast: Ast) = {

       println("###scala rewrote:")

       println("###scala old_ast: " + Ast.raw_string_of(old_ast))

       println("###scala new_ast: " + Ast.raw_string_of(new_ast))

     }

     def norm_root(ast: Ast): Ast =

       rewrite(ast) match {

         case Some(new_ast) => {

           //rewrote (ast, new_ast)

           norm_root(new_ast)}

         case None => ast

     }

     def norm(ast: Ast): Ast =

       norm_root(ast) match {

         case Appl(sub_asts) => {

           val old_changes = changes

           val new_ast = Appl(sub_asts.map(x => norm(x)))

           if (old_changes == changes)

             new_ast

           else

             norm_root(new_ast)

         }

         case atomic_ast => atomic_ast

       }

     def normal(ast: Ast): Ast = {

       val old_changes = changes

       val new_ast = norm(ast)

       if (old_changes == changes)

         new_ast

       else

         normal(new_ast)

     }

     normal(pre_ast)

   } //def normalize

   //\\=================================================================//

   case class AST_NO_KEY(message: String = "") extends Exception(message)

   def upd_list (asts: List[Ast], i: Integer, ast: Ast) = asts.updated(i - 1, ast)

   /* add ast to ast <code>upd</code> at a position given by <code>key</code>.

    * This is the only function modifying an immutable ast,

    * because "remove" means: add Constant("GAP") at <code>key</code>

    */

   def add (key: List[Int], ad: Ast, ast: Ast): Ast = ast match {

     case Appl(asts) => {

       if (key.length == 1)

         Appl(upd_list(asts, key.head, ad))

       else {

         if (key.isEmpty)

           throw new AST_NO_KEY("Index out of range of list")

         else {

           val uu = add(key.tail, ad, asts(key.head -1))

           Appl(upd_list(asts, key.head, uu)) }}}

     case const_var => const_var

   }

   // get a sub-term at key of an ast.

   def get_value (key: List[Int], ast: Ast): Ast = ast match {

     case Appl(asts) =>

       if (key.isEmpty) Appl(asts)

       else if (asts.length < key.head - 1)

         throw new AST_NO_KEY("NOT existent key=" + key)

       else  get_value (key.tail, asts(key.head - 1))

     case const_var => 

       if (key.isEmpty) const_var 

       else throw new AST_NO_KEY("NOT existent key=" + key)

   }

 }