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

 }