/*  THIS IS A DUMMY IMPLEMENTATION OF Isabelle2016-1 ...

    TTitle:      Pure/Syntax/syntax.ML

    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

Standard Isabelle syntax, based on arbitrary context-free grammars

(specified by mixfix declarations).

*/

package isac.gui.mawen.syntax

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

import isac.gui.mawen.syntax.isabelle.XTerm

import isac.gui.mawen.syntax.Ast._  //"._" simplifies "Ast.Ast" to "Ast"

import edu.tum.cs.isabelle.pure._

import scala.collection.immutable.TreeMap

object XSyntax {

 /* Data for presentation of Const which are not contained in (Scala-) Term:

  * _0: string used in ASTs

  * _1: string as shown by Isabelle's pretty printing

  * _2: infixl | infixr | prefix | postfix

  * _3: priority, which determines parentheses to be set

  * 

  * This replaces structure Syntax in Pure/Syntax/syntax.ML etc:

  *   val lookup_const: syntax -> string -> string option

  *   fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;

  */

  val isa_const = Map (

    "HOL.eq" -> ("=", " = ", "infixl", 50),                              //see ~~/src/HOL/HOL.thy

    "Groups.plus_class.plus" -> ("+", " + ", "infixl", 65),              //see ~~/src/HOL/Groups.thy

    "Groups.minus_class.minus" -> ("-", " - ", "infixl", 65),            //see ~~/src/HOL/Groups.thy

    "Groups.plus_class.uminus" -> ("-", " -", "prefix", 80),             //see ~~/src/HOL/Groups.thy

    "Groups.times_class.times" -> ("*", " * ", "infixl", 70),            //see ~~/src/HOL/Groups.thy

    "Fields.inverse_class.divide" -> ("/", " / ", "infixl", 70),         //see ~~/src/HOL/Fields.thy

    "Atools.pow" -> ("^", " ^ ", "infixr", 80),                          //see ~~/src/Tools/isac/Knowledge/Atools.thy

    "Power.power_class.power" -> ("^", " ^ ", "infixr", 80),             //see ~~/src/HOL/Power.thy

    "Transcendental.sin" -> ("sin", "sin ", "prefix", 70),               //see ~~/src/HOL/Transcendental.thy

    "Transcendental.cos" -> ("cos", "cos ", "prefix", 70),               //see ~~/src/HOL/Transcendental.thy

    "Integrate.Integral" -> ("Integral", "Integral ", "prefix", 91)      //see ~~/src/Tools/isac/Knowledge/Integrate.thy

    //...ERROR: implicit conversion found: ...

    )

  /* an exact copy of isa_const with another key:

   * _0: string used in Isabelle Term

   */

  val ast_const = Map (

    "=" -> ("HOL.eq",                      " = ",      "infixl", 50, "CMCSC8", '='.toInt),    //see ~~/src/HOL/HOL.thy

    "+" -> ("Groups.plus_class.plus",      " + ",      "infixl", 65, "CMCSC8", '+'.toInt),    //see ~~/src/HOL/Groups.thy

    "-" -> ("Groups.minus_class.minus",    " - ",      "infixl", 65, "CMCSC8", '-'.toInt),    //see ~~/src/HOL/Groups.thy

    "-" -> ("Groups.plus_class.uminus",    " -",       "prefix", 80, "CMCSC8", '-'.toInt),    //see ~~/src/HOL/Groups.thy

    "*" -> ("Groups.times_class.times",    " * ",      "infixl", 70, "CMCSC8", '*'.toInt),    //see ~~/src/HOL/Groups.thy

    "/" -> ("Fields.inverse_class.divide", " / ",      "infixl", 70, "",        0),           //see ~~/src/HOL/Fields.thy

    "^" -> ("Atools.pow",                  " ^ ",      "infixr", 80, "",        0),           //see ~~/src/Tools/isac/Knowledge/Atools.thy

    "^" -> ("Power.power_class.power",     "  ",       "infixr", 80, "",        0),           //see ~~/src/HOL/Power.thy

    "sin" -> ("Transcendental.sin",        "sin ",     "prefix", 70, "",        0),           //see ~~/src/HOL/Transcendental.thy

    "cos" -> ("Transcendental.cos",        "cos ",     "prefix", 70, "",        0),           //see ~~/src/HOL/Transcendental.thy

    "Integral" -> ("Integrate.Integral",  "Integral ", "prefix", 91, "",        0)            //see ~~/src/Tools/isac/Knowledge/Integrate.thy

    //...ERROR: implicit conversion found: ...

    )

  /* so not every constant needs to be in Util.isa_const */

  def isa_ast(str: String): String = { //key is the String in Term.Const

    isa_const.get(str) match {

      case Some((ast, _, _, _)) => ast 

      case None => str.substring(str.lastIndexOf(".") + 1)}}

  def ast_isa(str: String): String = { //key is the String in Ast.Constant

    ast_const.get(str) match {

      case Some((ast, _, _, _, _, _)) => ast 

      case None => str.substring(str.lastIndexOf(".") + 1)}}

  def isa_math(str: String): String = { //key is the String in Term.Const

    isa_const.get(str) match {

      case Some((_, isa, _, _)) => isa 

      case None => str.substring(str.lastIndexOf(".") + 1) + " "}}

  def ast_math(str: String): String = { //key is the String in Ast.Constant

    ast_const.get(str) match {

      case Some((_, isa, _, _, _, _)) => isa 

      case None => str.substring(str.lastIndexOf(".") + 1) + " "}}

  def isa_fix(str: String): String = { //key is the String in Term.Const

    isa_const.get(str) match {

      case Some((_, _, fix, _)) => fix 

      case None => "prefix"}}

  def ast_fix(str: String): String = { //key is the String in Ast.Constant

    ast_const.get(str) match {

      case Some((_, _, fix, _, _, _)) => fix 

      case None => "prefix"}}

  def isa_prior(str: String): Int = { //key is the String in Term.Const

    isa_const.get(str) match {

      case Some((_, _, _, prior)) => prior 

      case None => 99}}

  def ast_prior(str: String): Int = { //key is the String in Ast.Constant

    ast_const.get(str) match {

      case Some((_, _, _, prior, _, _)) => prior 

      case None => 99}}

  /* ~~/src/Pure/Syntax/syntax.ML:

   *   val print_rules: syntax -> string -> (Ast.ast * Ast.ast) list

   *   fun print_rules (Syntax ({print_ruletab, ...}, _)) = Symtab.lookup_list print_ruletab;

   */

  var symtab = TreeMap(

    "List.list.Cons" -> List(

//ML try_rules lhs: Appl(List(Constant("\<^const>List.list.Cons"), Variable("x"), Constant("\<^const>List.list.Nil"))) 

//ML try_rules rhs: Appl(List(Constant("_list"), Variable("x"))) 

      //rule for the last element

      (Appl(List(                     // lhs

         Constant("List.list.Cons"),

         Variable("x"),

         Constant("List.list.Nil"))),

       Appl(List(                     // rhs

         Constant("_list"),

         Variable("x")))),

//ML try_rules lhs: Appl(List(Constant("\<^const>List.list.Cons"), Variable("x"), Appl(List(Constant("_list"), Variable("xs"))))) 

//ML try_rules rhs: Appl(List(Constant("_list"), Appl(List(Constant("_args"), Variable("x"), Variable("xs")))))

      //rule for earlier elements: rewriting begins at the last element

      (Appl(List(                     // lhs

         Constant("List.list.Cons"),

         Variable("x"),

         Appl(List(

           Constant("_list"),

           Variable("xs"))))),

       Appl(List(                     // rhs

         Constant("_list"),

         Appl(List(Constant("_args"),

           Variable("x"),

           Variable("xs"))))))),

    "Product_Type.Pair" -> List(

//ML try_rules lhs: Appl(List(Constant("\<^const>Product_Type.Pair"), Variable("x"), Variable("y"))) 

//ML try_rules rhs: Appl(List(Constant("_tuple"), Variable("x"), Appl(List(Constant("_tuple_arg"), Variable("y"))))) 

      //rule for the last element

      (Appl(List(Constant("Product_Type.Pair"), Variable("x"), Variable("y"))),

       Appl(List(Constant("_tuple"), Variable("x"), Appl(List(Constant("_tuple_arg"), Variable("y"))))) )

    ),

    "" -> List( //called by Ast.try_headless_rules

//ML try_rules lhs: Appl(List(Constant("_tuple"), Variable("x"), Appl(List(Constant("_tuple_arg"), Appl(List(Constant("_tuple"), Variable("y"), Variable("z"))))))) 

//ML try_rules rhs: Appl(List(Constant("_tuple"), Variable("x"), Appl(List(Constant("_tuple_args"), Variable("y"), Variable("z"))))) 

      (Appl(List(Constant("_tuple"), Variable("x"), Appl(List(Constant("_tuple_arg"), Appl(List(Constant("_tuple"), Variable("y"), Variable("z"))))))),

       Appl(List(Constant("_tuple"), Variable("x"), Appl(List(Constant("_tuple_args"), Variable("y"), Variable("z"))))) ) )

  )

  def print_rules (key: String): List[Tuple2[Ast, Ast]] =

    if (symtab.contains(key)) symtab(key) else List()

}