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

 }