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