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

    Title:      Pure/Syntax/syntax_phases.ML

    Author:     Makarius

Main phases of inner syntax processing, with standard implementations

of parse/unparse operations.

CODE OMITTED IN THE TRANSLATION IS INDICATED BY (**) IN ORIGINAL ML.

*/

package isac.gui.mawen.syntax

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

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

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

object Syntax_Phases {

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

     CODE OMITTED IN THE TRANSLATION IS INDICATED BY (**) IN ORIGINAL ML:

  (* simple_ast_of *)

  (* = fn: Proof.context -> term -> Ast.ast*)

  fun simple_ast_of (*ctxt*)_ =

    let

     (* = fn: string -> string*)

     (*val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";*)

     (* = fn: term -> Ast.ast*)

     fun ast_of (Const (c, _)) = Ast.Constant c

        | ast_of (Free (x, _)) = Ast.Variable x

        | ast_of (Var (xi, _)) = Ast.Variable ((*tune_var*) (Term.string_of_vname xi))

        | ast_of (t as _ $ _) =

            let val (f, args) = strip_comb t

            in Ast.mk_appl (ast_of f) (map ast_of args) end

        | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]

        | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";

    in ast_of end;

   *

   * Constant GETS AN ABBREVIATED STRING PROBABLY USEFUL FOR ast_to_term

   */

  def simple_ast_of(/* ctxt : ???,*/ t : Term) : Ast.Ast = {

    def ast_of(tm : Term) : Ast.Ast =

    tm match {

      case Const(c, _) => Ast.Constant(c)

      case Free(c, _) => Ast.Variable(c)

      case Var(xi, _) => Ast.Variable(XTerm.string_of_vname(xi))

      case App(t1, t2) => {

        val (f, args) = XTerm.strip_comb(App(t1, t2))

        Ast.mk_appl(ast_of(f), args.map(t => ast_of(t)))

      }

      case Bound(i) =>

        Ast.Appl(List(Ast.Constant("_loose"), Ast.Variable("B." ++ XLibrary.string_of_int(i.intValue))))

      case Abs(_, _, _) => throw new AstException("simple_ast_of: Abs")

    }

    ast_of(t)

  }

  // still NO ast-translations, compare ~~/src/Pure/Syntax/syntax_phases.ML

  def term_to_ast(tm : Term) : Ast.Ast = 

    Ast.normalize(XSyntax.print_rules, simple_ast_of(tm))

  // we do NOT submit Term to Isabelle_Isac, only String (and let parse again)

  def ast_to_term(ast: Ast.Ast) : Term = Const("DUMMY", Type("DUMMY"))

}