#ifndef TCENV_H
#define TCENV_H

#include "core.h"
#include "list.h"
#include "set.h"
#include "dict.h"
#include "absyn.h"
#include "position.h"

namespace Tcenv {

using Core;
using List;
using Set;
using Dict;
using Absyn;
using Position;

extern struct Var_info {
  scope sc;
  tqual tq;
  typ   t;
  bool  is_used;
};
typedef struct Var_info @var_info;

/* Flags that control whether an operation (e.g., break) is okay */
extern struct Ok_ctrl;
typedef struct Ok_ctrl @ok_ctrl;

/* Used to tell what an ordinary identifer refers to */
extern enum Resolved {
  UnknownRes;
  LocalRes(var_info);
  GlobalRes(qvar,var_info);
  StructRes(structdecl);
  EnumRes(enumdecl,enumfield);
  XenumRes(xenumdecl,enumfield);
};
typedef enum Resolved resolved;

/* Global environments -- what's declared in a global scope */
extern struct Genv {
  Set<var>              namespaces;
  Dict<var,structdecl>  structdecls;
  Dict<var,enumdecl>    enumdecls;
  Dict<var,xenumdecl>   xenumdecls;
  Dict<var,typedefdecl> typedefs;
  Dict<var,resolved>    ordinaries;
  list<list<var>>       availables; // "using" namespaces
};
typedef struct Genv @genv;

/* Local function environments */
extern struct Fenv {
  list<var>             labels;
  Dict<var,var_info>    locals;
  ok_ctrl               ok;
  Set<var>              uv; // maybe-unassigned variables
  typ                   return_typ;
  Dict<var,typedefdecl> typedefs;
  list<tvar>            type_vars; // type variables that can occur free
};
typedef struct Fenv @fenv; 

/* Models the nesting of the RTCG constructs */
extern enum Frames<`a> {
  Outermost(`a);
  Frame(`a,enum Frames<`a>);
  Hidden(`a,enum Frames<`a>);
};
typedef enum Frames<`a> frames<`a>;

/* Type environments */
extern struct Tenv {
  list<var>            ns; // current namespace
  Dict<list<var>,genv> ae; // absolute environment
  Opt_t<frames<fenv>>  le; // local environment, == null except in functions
};
typedef struct Tenv @tenv;

extern tenv set_in_loop(tenv);
extern tenv set_in_switch(tenv);
extern tenv clear_fallthru(tenv);
extern bool is_ok_continue(tenv);
extern bool is_ok_break(tenv);
extern bool is_ok_fallthru(tenv);

extern ok_ctrl default_ok_ctrl();
 
extern tenv enter_ns(tenv, var);
extern genv genv_concat(genv, genv);
extern genv genv_copy(genv);

/* lookup functions */
extern list<var>   resolve_namespace(tenv,segment,list<var>);
extern genv        lookup_namespace(tenv,segment,list<var>);
extern resolved    lookup_ordinary(tenv,segment,qvar);
extern structdecl  lookup_structdecl(tenv,segment,qvar);
extern enumdecl    lookup_enumdecl(tenv,segment,qvar);
extern Opt_t<xenumdecl> lookup_xenumdecl(tenv,segment,qvar);
extern typedefdecl lookup_typedefdecl(tenv,segment,qvar);
extern list<tvar>  lookup_type_vars(tenv);

extern Opt_t<$(tqual,typ)@> lookup_struct_field(structdecl,var);

extern tenv add_local_var(segment,tenv,var,tqual,typ,bool);

extern tenv add_type_vars(segment,tenv,list<tvar>);

// what we synthesize when type-checking a statement or expression:
extern struct Synth;
typedef struct Synth @synth;
// whether the statement/expr may implicitly fall through to the next
extern bool synth_may_implicit_fallthru(synth);
// whether the statement/expr explicitly falls through to the next
extern bool synth_may_explicit_fallthru(synth);
// the type of the expression (only call on synth's generated by exps)
extern typ synth_typ(synth);
// given a synth, set the type to t -- IMPERATIVE!!!
extern synth synth_set_typ(synth s,typ t);

// we refine the flow-through edge for boolean expressions to the "on true"
// and "on false" cases.  
extern enum Unassigned {
  Always(Set<var>);  // unassigned after expression
  Boolean(Set<var>,Set<var>); // unassigned when true, when false
};
typedef enum Unassigned unassigned;

extern unassigned merge_unassigned(unassigned, unassigned);

// make the unassigned set in the resulting tenv come from the 
// "fallthrough" edge of the synth
extern tenv layer_synth(tenv,synth);
// give back two environments -- one when the exp is true and one when false
extern $(tenv,tenv)@ bool_layer_synth(tenv,synth);
// synth we get for most expressions and atomic statements -- implicit 
// fallthru with no forward jump, and all currently unassigned variables as
// unassigned on the normal edge, empty set of unassigned variables on
// the forward jump edge.
extern synth standard_synth(tenv, typ);
// synth we get on error in expressions (type is wild)
 extern synth wild_synth(tenv);
// synth we get for most statements -- standard_synth with void type
extern synth skip_synth(tenv te);
// synth we get upon return, continue, raise -- no fallthru or forward jump,
// no unassigned variables on either the normal or forward jump edge.
extern synth empty_synth(tenv te);
// synth we get upon a break, goto, or raise -- forward jump with no 
// fallthru, all currently unassigned variables on the forward jump edge, the
// empty set on the normal edge.
extern synth forward_jump_synth(tenv te);
// synth we get for sequencing.  We merge the normal and jump edges
// according to whether or not s1 may fallthru to s2.
extern synth seq_synth(synth s1, synth s2);
// synth we get upon join of two if statements or switch cases etc.
extern synth join_synth(synth s1, synth s2);
// after joining all of the switch cases' synths, we treat the 
// unassigned variables on the "forward jump" edge as unassigned
// on the outgoing normal control flow edge, because any case's break is
// a forward jump to the bottom of the switch statement.  
extern synth switch_bottom(synth s);
// after a loop, the synth is the join of the "false" part of the
// test expression, and the forward_jump part of the statement
extern synth loop_synth(synth e, synth s);
// an explicit fallthru -- similar to skip but ctrl indicates explicit fallthru
extern synth fallthru_synth(tenv te);
// add the set v to both edges of the synth
extern synth add_var_synth(Set<var> v, synth s);
// remove v from the fall-through edge of the synth (if any)
extern synth initialize_var_synth(synth s, var v);
// remove all of the variables on the fall-through edge
extern synth drop_fallthru_synth(synth s);
// set of variables unassigned on fallthru edge
extern Set<var> maybe_unassigned(synth);
// set of variables unassigned on "true"/"false" branches respectively
extern $(Set<var>,Set<var>)@ maybe_unassigned_bool(synth);

extern Set<var> get_unassigned(tenv);
extern tenv     set_unassigned(tenv, Set<var>);
extern tenv     add_label(tenv, var);
extern typ      return_typ(tenv);

extern tenv code_gen_tenv(fndecl, tenv);

extern tenv tc_init();
extern genv empty_genv();

}
#endif
