1structure Parse_supportENV =
2struct
3
4  type pretype = Pretype.pretype
5  type preterm = Preterm.preterm
6  type env = {scope : (string * pretype) list,
7              free  : (string * pretype) list,
8              uscore_cnt : int,
9              ptyE : Pretype.Env.t}
10
11  type 'a PSM = env -> ('a * env)
12  type preterm_in_env = preterm PSM
13
14  exception AQincompat of { nm : string, aqty : Type.hol_type,
15                            loc : locn.locn, fv : bool,
16                            unify_error : typecheck_error.error }
17
18  val empty_env =
19      {scope = [], free = [], uscore_cnt = 0, ptyE = Pretype.Env.empty}
20  fun frees (e:env) = #free e
21
22  fun fupd_ptyE f ({scope,free,uscore_cnt,ptyE}:env) : env =
23    {scope=scope, free=free, uscore_cnt=uscore_cnt, ptyE = f ptyE}
24
25  fun fupd_scope f ({scope,free,uscore_cnt,ptyE}:env) : env =
26    {scope=f scope, free=free, uscore_cnt=uscore_cnt, ptyE = ptyE}
27
28  fun fupd_free f ({scope,free,uscore_cnt,ptyE}:env) : env =
29    {scope=scope, free=f free, uscore_cnt=uscore_cnt, ptyE = ptyE}
30
31end
32