(* parse, elaborate, and translate to FLINT
 * optionally call Absyn->Absyn match compiler on elaborated code
 *)

signature TRANSMAIN = 
sig
    (* First argument is NONE to get declaration(s) from stdin
     * or SOME(filename)
     *
     * Second argument is true to call "post-elaboration" (the 
     * Absyn -> Absyn match compiler) before translating.
     *)

    (* translate first declaration to FLINT, then quit *)
    val transMain1 : string option * bool -> 
                    {flint:FLINT.prog, 
		     imports:(PersStamps.persstamp * 
			      ImportTree.importTree) list}
    (* Translate all declarations in input *)
    val transMain : string option * bool -> 
                    {flint:FLINT.prog, 
		     imports:(PersStamps.persstamp * 
			      ImportTree.importTree) list}
    val debug : bool ref
    val pre_mcomp : (Absyn.dec) option ref
    val post_mcomp: (Absyn.dec) option ref
end (* sig *)



structure TransMain : TRANSMAIN = 
struct
  val debug = ref false
  val pre_mcomp : Absyn.dec option ref = ref NONE
  val post_mcomp : Absyn.dec option ref = ref NONE
local
    structure SigMatch = SigMatchFn (structure EV = EvalEntity)
    structure Typecheck = TypecheckFn (val ii_ispure = InlInfo.pureInfo
                                       val ii2ty = InstantiateParam.ii2ty)
    structure ElabMod = ElabModFn (structure SM = SigMatch
                                   structure Typecheck = Typecheck)
    structure ElabTop = ElabTopFn (structure ElabMod = ElabMod)
    structure PU = PEUtil
in
    exception BadParseResult of MLParser.parseResult
    exception ElaborationError

    val {exportLvars=_,exportPid=_,newenv=initenv,pickle=_,pid=_} =
        Pup.pickBase(SavedEnv.makeSavedEnv ())

    fun transMainP parse (strOpt, doPostElab) = 
        (let
	   val {exportLvars=_,exportPid=_,newenv=initenv,pickle=_,pid=_} =
	     Pup.pickBase(SavedEnv.makeSavedEnv ())

            val source = ParserInterface.whichSource strOpt
            val astdec = parse source
            val cinfo = CompInfo.mkCompInfo {source = source, 
                                             transform = fn x : Absyn.dec => x,
                                             mkMkStamp = Stamps.newGenerator}
	    val (dec, newenv) = ElabTop.elabTop (astdec, initenv, cinfo)
	    val staticenv = StaticEnv.atop (initenv, newenv)
	    val {exportLvars, ...} = PickUnpick.pickUnpick {context = initenv,
							    env = newenv,
							    guid = ""}

            val _ = if CompInfo.anyErrors cinfo
                    then raise PU.ElaborationError
                    else ()
	    val rootdec = if doPostElab
			  then 
			    let
			      val _ = 
				if !debug then pre_mcomp := SOME dec else ()
			      val dec' = PostElab.transDec {rootdec = dec, 
							    env = staticenv,
							    compInfo = cinfo}
			      val _ = 
				if !debug then post_mcomp := SOME dec' else ()
			    in dec' end
			  else dec
        in
	    Translate.transDec {compInfo = cinfo, cproto_conv = "cpc", 
				env = staticenv, exportLvars = exportLvars,
				rootdec = rootdec}
        end handle x => raise x)

    val transMain1 = transMainP ParserInterface.parseOne

    val transMain = transMainP ParserInterface.parseAll
end (* local *)
end (* struct *)