semanticPrimitives.lem

open import Pervasives
open import Lib
import List_extra
import String
import String_extra
open import Ast
open import Ffi

(* The type that a constructor builds is either a named datatype or an exception.
 * For exceptions, we also keep the module that the exception was declared in. *)
type tid_or_exn =
  | TypeId of id typeN
  | TypeExn of id conN

val type_defs_to_new_tdecs : maybe modN -> type_def -> set tid_or_exn
let type_defs_to_new_tdecs mn tdefs =
  Set.fromList (List.map (fun (tvs,tn,ctors) -> TypeId (mk_id mn tn)) tdefs)

type alist_mod_env 'k 'v = alist modN (alist 'k 'v) * alist 'k 'v

let merge_alist_mod_env (menv1,env1) (menv2,env2) =
  (menv1 ++ menv2, env1 ++ env2)

let lookup_alist_mod_env id (mcenv,cenv) =
  match id with
    | Short x -> lookup x cenv
    | Long x y ->
        match lookup x mcenv with
          | Nothing -> Nothing
          | Just cenv -> lookup y cenv
        end
  end

(* Maps each constructor to its arity and which type it is from *)
type flat_env_ctor = alist conN (nat * tid_or_exn)
type env_ctor = alist_mod_env conN (nat * tid_or_exn)

type environment 'v =
  <| v : alist varN 'v
   ; c : alist_mod_env conN (nat * tid_or_exn)
   ; m : alist modN (alist varN 'v)
   |>

(* Value forms *)
type v =
  | Litv of lit
  (* Constructor application. *)
  | Conv of maybe (conN * tid_or_exn) * list v
  (* Function closures
     The environment is used for the free variables in the function *)
  | Closure of environment v * varN * exp
  (* Function closure for recursive functions
   * See Closure and Letrec above
   * The last variable name indicates which function from the mutually
   * recursive bundle this closure value represents *)
  | Recclosure of environment v * list (varN * varN * exp) * varN
  | Loc of nat
  | Vectorv of list v

let Bindv = Conv (Just("Bind",TypeExn(Short"Bind"))) []

(* These are alists rather than finite maps because the type of values (v above)
 * recurs through them, and HOL4 does not easily support that kind of data type
 * (although Isabelle/HOL does) *)
type env_val = alist varN v
type env_mod = alist modN env_val

(* The result of evaluation *)
type abort =
  | Rtype_error
  | Rtimeout_error

type error_result 'a =
  | Rraise of 'a (* Should only be a value of type exn *)
  | Rabort of abort

type result 'a 'b =
  | Rval of 'a
  | Rerr of error_result 'b

(* Stores *)
type store_v 'a =
  (* A ref cell *)
    Refv of 'a
  (* A byte array *)
  | W8array of list word8
  (* An array of values *)
  | Varray of list 'a

val store_v_same_type : forall 'a. store_v 'a -> store_v 'a -> bool
let store_v_same_type v1 v2 =
  match (v1,v2) with
  | (Refv _, Refv _) -> true
  | (W8array _,W8array _) -> true
  | (Varray _,Varray _) -> true
  | _ -> false
  end

(* The nth item in the list is the value at location n *)
type store 'a = list (store_v 'a)

val empty_store : forall 'a. store 'a
let empty_store = []

val store_lookup : forall 'a. nat -> store 'a -> maybe (store_v 'a)
let store_lookup l st =
  if l < List.length st then
    Just (List_extra.nth st l)
  else
    Nothing

val store_alloc : forall 'a. store_v 'a -> store 'a -> store 'a * nat
let store_alloc v st =
  ((st ++ [v]), List.length st)

val store_assign : forall 'a. nat -> store_v 'a -> store 'a -> maybe (store 'a)
let store_assign n v st =
  if n < List.length st &&
     store_v_same_type (List_extra.nth st n) v
  then
    Just (List.update st n v)
  else
    Nothing

val lookup_var_id : id varN -> environment v -> maybe v
let lookup_var_id id env =
  match id with
    | Short x -> lookup x env.v
    | Long x y ->
        match lookup x env.m with
          | Nothing -> Nothing
          | Just env -> lookup y env
        end
  end

type state 'ffi =
  <| clock : nat
   ; refs  : store v
   ; ffi : ffi_state 'ffi
   ; defined_types : set tid_or_exn
   ; defined_mods : set modN
   |>

(* Other primitives *)
(* Check that a constructor is properly applied *)
val do_con_check : env_ctor -> maybe (id conN) -> nat -> bool
let do_con_check cenv n_opt l =
  match n_opt with
    | Nothing -> true
    | Just n ->
        match lookup_alist_mod_env n cenv with
          | Nothing -> false
          | Just (l',ns) -> l = l'
        end
  end

val build_conv : env_ctor -> maybe (id conN) -> list v -> maybe v
let build_conv envC cn vs =
  match cn with
    | Nothing ->
        Just (Conv Nothing vs)
    | Just id ->
        match lookup_alist_mod_env id envC with
          | Nothing -> Nothing
          | Just (len,t) -> Just (Conv (Just (id_to_n id, t)) vs)
        end
  end

val lit_same_type : lit -> lit -> bool
let lit_same_type l1 l2 =
  match (l1,l2) with
    | (IntLit _, IntLit _) -> true
    | (Char _, Char _) -> true
    | (StrLit _, StrLit _) -> true
    | (Word8 _, Word8 _) -> true
    | (Word64 _, Word64 _) -> true
    | _ -> false
  end

type match_result 'a =
  | No_match
  | Match_type_error
  | Match of 'a

val same_tid : tid_or_exn -> tid_or_exn -> bool
let rec same_tid (TypeId tn1) (TypeId tn2) = tn1 = tn2
and same_tid (TypeExn _) (TypeExn _) = true
and same_tid _ _ = false

val same_ctor : conN * tid_or_exn -> conN * tid_or_exn -> bool
let rec same_ctor (cn1, TypeExn mn1) (cn2, TypeExn mn2) = cn1 = cn2 && mn1 = mn2
and same_ctor (cn1, _) (cn2, _) = cn1 = cn2

val ctor_same_type : maybe (conN * tid_or_exn) -> maybe (conN * tid_or_exn) -> bool
let ctor_same_type c1 c2 =
  match (c1,c2) with
    | (Nothing, Nothing) -> true
    | (Just (_,t1), Just (_,t2)) -> same_tid t1 t2
    | _ -> false
  end

(* A big-step pattern matcher.  If the value matches the pattern, return an
 * environment with the pattern variables bound to the corresponding sub-terms
 * of the value; this environment extends the environment given as an argument.
 * No_match is returned when there is no match, but any constructors
 * encountered in determining the match failure are applied to the correct
 * number of arguments, and constructors in corresponding positions in the
 * pattern and value come from the same type.  Match_type_error is returned
 * when one of these conditions is violated *)
val pmatch : env_ctor -> store v -> pat -> v -> env_val -> match_result env_val
let rec
pmatch envC s (Pvar x) v' env = Match ((x,v')::env)
and
pmatch envC s (Plit l) (Litv l') env =
  if l = l' then
    Match env
  else if lit_same_type l l' then
    No_match
  else
    Match_type_error
and
pmatch envC s (Pcon (Just n) ps) (Conv (Just (n', t')) vs) env =
  match lookup_alist_mod_env n envC with
    | Just (l, t)->
        if same_tid t t' && List.length ps = l then
          if same_ctor (id_to_n n, t) (n',t') then
            pmatch_list envC s ps vs env
          else
            No_match
        else
          Match_type_error
    | _ -> Match_type_error
  end
and
pmatch envC s (Pcon Nothing ps) (Conv Nothing vs) env =
  if List.length ps = List.length vs then
    pmatch_list envC s ps vs env
  else
    Match_type_error
and
pmatch envC s (Pref p) (Loc lnum) env =
  match store_lookup lnum s with
    | Just (Refv v) -> pmatch envC s p v env
    | Just _ -> Match_type_error
    | Nothing -> Match_type_error
  end
and
pmatch envC s (Ptannot p t) v env =
  pmatch envC s p v env
and
pmatch envC _ _ _ env = Match_type_error
and
pmatch_list envC s [] [] env = Match env
and
pmatch_list envC s (p::ps) (v::vs) env =
  match pmatch envC s p v env with
    | No_match -> No_match
    | Match_type_error -> Match_type_error
    | Match env' -> pmatch_list envC s ps vs env'
  end
and
pmatch_list envC s _ _ env = Match_type_error

(* Bind each function of a mutually recursive set of functions to its closure *)
val build_rec_env : list (varN * varN * exp) -> environment v -> env_val -> env_val
let build_rec_env funs cl_env add_to_env =
  foldr
    (fun (f,x,e) env' -> (f, Recclosure cl_env funs f) :: env')
    add_to_env
    funs

(* Lookup in the list of mutually recursive functions *)
val find_recfun : forall 'a 'b. varN -> list (varN * 'a * 'b) -> maybe ('a * 'b)
let rec find_recfun n funs =
  match funs with
    | [] -> Nothing
    | (f,x,e) :: funs ->
        if f = n then
          Just (x,e)
        else
          find_recfun n funs
  end

declare termination_argument find_recfun = automatic

type eq_result =
  | Eq_val of bool
  | Eq_type_error

val do_eq : v -> v -> eq_result
let rec
do_eq (Litv l1) (Litv l2) =
  if lit_same_type l1 l2 then Eq_val (l1 = l2)
  else Eq_type_error
and
do_eq (Loc l1) (Loc l2) = Eq_val (l1 = l2)
and
do_eq (Conv cn1 vs1) (Conv cn2 vs2) =
  if cn1 = cn2 && (List.length vs1 = List.length vs2) then
    do_eq_list vs1 vs2
  else if ctor_same_type cn1 cn2 then
    Eq_val false
  else
    Eq_type_error
and
do_eq (Vectorv vs1) (Vectorv vs2) =
  if List.length vs1 = List.length vs2 then
    do_eq_list vs1 vs2
  else
    Eq_val false
and
do_eq (Closure _ _ _) (Closure _ _ _) = Eq_val true
and
do_eq (Closure _ _ _) (Recclosure _ _ _) = Eq_val true
and
do_eq (Recclosure _ _ _) (Closure _ _ _) = Eq_val true
and
do_eq (Recclosure _ _ _) (Recclosure _ _ _) = Eq_val true
and
do_eq _ _ = Eq_type_error
and
do_eq_list [] [] = Eq_val true
and
do_eq_list (v1::vs1) (v2::vs2) =
  match do_eq v1 v2 with
    | Eq_type_error -> Eq_type_error
    | Eq_val r ->
        if not r then
          Eq_val false
        else
          do_eq_list vs1 vs2
  end
and
do_eq_list _ _ = Eq_val false

val prim_exn : conN -> v
let prim_exn cn = Conv (Just (cn, TypeExn (Short cn))) []

(* Do an application *)
val do_opapp : list v -> maybe (environment v * exp)
let do_opapp vs =
  match vs with
  | [Closure env n e; v] ->
      Just (<| env with v = (n,v)::env.v |>, e)
  | [Recclosure env funs n; v] ->
      if allDistinct (List.map (fun (f,x,e) -> f) funs) then
        match find_recfun n funs with
          | Just (n,e) -> Just (<| env with v = (n,v)::build_rec_env funs env env.v |>, e)
          | Nothing -> Nothing
        end
      else
        Nothing
  | _ -> Nothing
  end

(* If a value represents a list, get that list. Otherwise return Nothing *)
val v_to_list : v -> maybe (list v)
let rec v_to_list (Conv (Just (cn, TypeId (Short tn))) []) =
  if cn = "nil" && tn = "list" then
    Just []
  else
    Nothing
and v_to_list (Conv (Just (cn,TypeId (Short tn))) [v1;v2]) =
  if cn = "::"  && tn = "list" then
    match v_to_list v2 with
      | Just vs -> Just (v1::vs)
      | Nothing -> Nothing
    end
  else
    Nothing
and v_to_list _ = Nothing

val v_to_char_list : v -> maybe (list char)
let rec v_to_char_list (Conv (Just (cn, TypeId (Short tn))) []) =
  if cn = "nil" && tn = "list" then
    Just []
  else
    Nothing
and v_to_char_list (Conv (Just (cn,TypeId (Short tn))) [Litv (Char c);v]) =
  if cn = "::"  && tn = "list" then
    match v_to_char_list v with
      | Just cs -> Just (c::cs)
      | Nothing -> Nothing
    end
  else
    Nothing
and v_to_char_list _ = Nothing

val opn_lookup : opn -> integer -> integer -> integer
let opn_lookup n : integer -> integer -> integer = match n with
  | Plus -> (+)
  | Minus -> (-)
  | Times -> ( * )
  | Divide -> (/)
  | Modulo -> (mod)
end

val opb_lookup : opb -> integer -> integer -> bool
let opb_lookup n : integer -> integer -> bool = match n with
  | Lt -> (<)
  | Gt -> (>)
  | Leq -> (<=)
  | Geq -> (>=)
end

val opw8_lookup : opw -> word8 -> word8 -> word8
let opw8_lookup op = match op with
  | Andw -> W8and
  | Orw -> W8or
  | Xor -> W8xor
  | Add -> W8add
  | Sub -> W8sub
end

val opw64_lookup : opw -> word64 -> word64 -> word64
let opw64_lookup op = match op with
  | Andw -> W64and
  | Orw -> W64or
  | Xor -> W64xor
  | Add -> W64add
  | Sub -> W64sub
end

val shift8_lookup : shift -> word8 -> nat -> word8
let shift8_lookup sh = match sh with
  | Lsl -> W8lsl
  | Lsr -> W8lsr
  | Asr -> W8asr
end

val shift64_lookup : shift -> word64 -> nat -> word64
let shift64_lookup sh = match sh with
  | Lsl -> W64lsl
  | Lsr -> W64lsr
  | Asr -> W64asr
end

val Boolv : bool -> v
let Boolv b = if b
  then Conv (Just ("true", TypeId (Short "bool"))) []
  else Conv (Just ("false", TypeId (Short "bool"))) []

type exp_or_val =
  | Exp of exp
  | Val of v

type store_ffi 'ffi 'v = store 'v * ffi_state 'ffi

val do_app : forall 'ffi. store_ffi 'ffi v -> op -> list v -> maybe (store_ffi 'ffi v * result v v)
let do_app ((s:store v),(t:ffi_state 'ffi)) op vs =
  match (op, vs) with
    | (Opn op, [Litv (IntLit n1); Litv (IntLit n2)]) ->
        if (op = Divide || (op = Modulo)) && (n2 = 0) then
          Just ((s,t), Rerr (Rraise (prim_exn "Div")))
        else
          Just ((s,t), Rval (Litv (IntLit (opn_lookup op n1 n2))))
    | (Opb op, [Litv (IntLit n1); Litv (IntLit n2)]) ->
        Just ((s,t), Rval (Boolv (opb_lookup op n1 n2)))
    | (Opw W8 op, [Litv (Word8 w1); Litv (Word8 w2)]) ->
        Just ((s,t), Rval (Litv (Word8 (opw8_lookup op w1 w2))))
    | (Opw W64 op, [Litv (Word64 w1); Litv (Word64 w2)]) ->
        Just ((s,t), Rval (Litv (Word64 (opw64_lookup op w1 w2))))
    | (Shift W8 op n, [Litv (Word8 w)]) ->
        Just ((s,t), Rval (Litv (Word8 (shift8_lookup op w n))))
    | (Shift W64 op n, [Litv (Word64 w)]) ->
        Just ((s,t), Rval (Litv (Word64 (shift64_lookup op w n))))
    | (Equality, [v1; v2]) ->
        match do_eq v1 v2 with
          | Eq_type_error -> Nothing
          | Eq_val b -> Just ((s,t), Rval (Boolv b))
        end
    | (Opassign, [Loc lnum; v]) ->
        match store_assign lnum (Refv v) s with
          | Just s' -> Just ((s',t), Rval (Conv Nothing []))
          | Nothing -> Nothing
        end
    | (Opref, [v]) ->
        let (s',n) = store_alloc (Refv v) s in
          Just ((s',t), Rval (Loc n))
    | (Opderef, [Loc n]) ->
        match store_lookup n s with
          | Just (Refv v) -> Just ((s,t),Rval v)
          | _ -> Nothing
        end
    | (Aw8alloc, [Litv (IntLit n); Litv (Word8 w)]) ->
        if n < 0 then
          Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
        else
          let (s',lnum) =
            store_alloc (W8array (List.replicate (natFromInteger n) w)) s
          in
            Just ((s',t), Rval (Loc lnum))
    | (Aw8sub, [Loc lnum; Litv (IntLit i)]) ->
        match store_lookup lnum s with
          | Just (W8array ws) ->
              if i < 0 then
                Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
              else
                let n = natFromInteger i in
                  if n >= List.length ws then
                    Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
                  else
                    Just ((s,t), Rval (Litv (Word8 (List_extra.nth ws n))))
          | _ -> Nothing
        end
    | (Aw8length, [Loc n]) ->
        match store_lookup n s with
          | Just (W8array ws) ->
              Just ((s,t),Rval (Litv(IntLit(integerFromNat(List.length ws)))))
          | _ -> Nothing
         end
    | (Aw8update, [Loc lnum; Litv(IntLit i); Litv(Word8 w)]) ->
        match store_lookup lnum s with
        | Just (W8array ws) ->
            if i < 0 then
              Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
            else
              let n = natFromInteger i in
                if n >= List.length ws then
                  Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
                else
                  match store_assign lnum (W8array (List.update ws n w)) s with
                    | Nothing -> Nothing
                    | Just s' -> Just ((s',t), Rval (Conv Nothing []))
                  end
        | _ -> Nothing
      end
    | (WordFromInt W8, [Litv(IntLit i)]) ->
        Just ((s,t), Rval (Litv (Word8 (word8FromInteger i))))
    | (WordFromInt W64, [Litv(IntLit i)]) ->
        Just ((s,t), Rval (Litv (Word64 (word64FromInteger i))))
    | (WordToInt W8, [Litv (Word8 w)]) ->
        Just ((s,t), Rval (Litv (IntLit (integerFromNat(natFromWord8 w)))))
    | (WordToInt W64, [Litv (Word64 w)]) ->
        Just ((s,t), Rval (Litv (IntLit (integerFromNat(natFromWord64 w)))))
    | (Ord, [Litv (Char c)]) ->
          Just ((s,t), Rval (Litv(IntLit(integerFromNat(String_extra.ord c)))))
    | (Chr, [Litv (IntLit i)]) ->
        Just ((s,t),
          if i < 0 || i > 255 then
            Rerr (Rraise (prim_exn "Chr"))
          else
            Rval (Litv(Char(String_extra.chr(natFromInteger i)))))
    | (Chopb op, [Litv (Char c1); Litv (Char c2)]) ->
        Just ((s,t), Rval (Boolv (opb_lookup op (integerFromNat(String_extra.ord c1)) (integerFromNat(String_extra.ord c2)))))
    | (Implode, [v]) ->
          match v_to_char_list v with
          | Just ls ->
              Just ((s,t), Rval (Litv (StrLit (toString ls))))
          | Nothing -> Nothing
          end
    | (Strsub, [Litv (StrLit str); Litv (IntLit i)]) ->
        if i < 0 then
          Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
        else
          let n = natFromInteger i in
            if n >= stringLength str then
              Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
            else
              Just ((s,t), Rval (Litv (Char (List_extra.nth (toCharList str) n))))
    | (Strlen, [Litv (StrLit str)]) ->
        Just ((s,t), Rval (Litv(IntLit(integerFromNat(stringLength str)))))
    | (VfromList, [v]) ->
          match v_to_list v with
            | Just vs ->
                Just ((s,t), Rval (Vectorv vs))
            | Nothing -> Nothing
          end
    | (Vsub, [Vectorv vs; Litv (IntLit i)]) ->
        if i < 0 then
          Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
        else
          let n = natFromInteger i in
            if n >= List.length vs then
              Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
            else
              Just ((s,t), Rval (List_extra.nth vs n))
    | (Vlength, [Vectorv vs]) ->
        Just ((s,t), Rval (Litv (IntLit (integerFromNat (List.length vs)))))
    | (Aalloc, [Litv (IntLit n); v]) ->
        if n < 0 then
          Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
        else
          let (s',lnum) =
            store_alloc (Varray (List.replicate (natFromInteger n) v)) s
          in
            Just ((s',t), Rval (Loc lnum))
    | (Asub, [Loc lnum; Litv (IntLit i)]) ->
        match store_lookup lnum s with
          | Just (Varray vs) ->
              if i < 0 then
                Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
              else
                let n = natFromInteger i in
                  if n >= List.length vs then
                    Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
                  else
                    Just ((s,t), Rval (List_extra.nth vs n))
          | _ -> Nothing
        end
    | (Alength, [Loc n]) ->
        match store_lookup n s with
          | Just (Varray ws) ->
              Just ((s,t),Rval (Litv(IntLit(integerFromNat(List.length ws)))))
          | _ -> Nothing
         end
    | (Aupdate, [Loc lnum; Litv (IntLit i); v]) ->
        match store_lookup lnum s with
        | Just (Varray vs) ->
            if i < 0 then
              Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
            else
              let n = natFromInteger i in
                if n >= List.length vs then
                  Just ((s,t), Rerr (Rraise (prim_exn "Subscript")))
                else
                  match store_assign lnum (Varray (List.update vs n v)) s with
                    | Nothing -> Nothing
                    | Just s' -> Just ((s',t), Rval (Conv Nothing []))
                  end
        | _ -> Nothing
      end
    | (FFI n, [Loc lnum]) ->
        match store_lookup lnum s with
        | Just (W8array ws) ->
            match call_FFI t n ws with
            | (t', ws') ->
               match store_assign lnum (W8array ws') s with
               | Just s' -> Just ((s', t'), Rval (Conv Nothing []))
               | Nothing -> Nothing
               end
            end
        | _ -> Nothing
        end
    | _ -> Nothing
  end

(* Do a logical operation *)
val do_log : lop -> v -> exp -> maybe exp_or_val
let do_log l v e =
  match (l, v) with
    | (And, Conv (Just ("true", TypeId (Short "bool"))) []) -> Just (Exp e)
    | (Or, Conv (Just ("false", TypeId (Short "bool"))) []) -> Just (Exp e)
    | (_, Conv (Just ("true", TypeId (Short "bool"))) []) -> Just (Val v)
    | (_, Conv (Just ("false", TypeId (Short "bool"))) []) -> Just (Val v)
    | _ -> Nothing
  end

(* Do an if-then-else *)
val do_if : v -> exp -> exp -> maybe exp
let do_if v e1 e2 =
  if v = (Boolv true) then
    Just e1
  else if v = (Boolv false) then
    Just e2
  else
    Nothing

(* Semantic helpers for definitions *)

(* Build a constructor environment for the type definition tds *)
val build_tdefs : maybe modN -> list (list tvarN * typeN * list (conN * list t)) -> flat_env_ctor
let build_tdefs mn tds =
  List.reverse
    (List.concat
      (List.map
        (fun (tvs, tn, condefs) ->
           List.map
             (fun (conN, ts) ->
                (conN, (List.length ts, TypeId (mk_id mn tn))))
             condefs)
        tds))

(* Checks that no constructor is defined twice in a type *)
val check_dup_ctors : list (list tvarN * typeN * list (conN * list t)) -> bool
let check_dup_ctors tds =
  List.allDistinct [ n | forall ((tvs, tn, condefs) MEM tds) ((n, ts) MEM condefs) | true ]

val combine_dec_result : forall 'a 'b 'c. alist 'a 'b -> result (alist 'a 'b) 'c -> result (alist 'a 'b) 'c
let combine_dec_result env r =
  match r with
    | Rerr e -> Rerr e
    | Rval env' -> Rval (env'++env)
  end

val combine_mod_result : forall 'a 'b 'c 'd 'e. alist 'a 'b -> alist 'c 'd -> result (alist 'a 'b * alist 'c 'd) 'e -> result (alist 'a 'b * alist 'c 'd) 'e
let combine_mod_result menv env r =
  match r with
    | Rerr e -> Rerr e
    | Rval (menv',env') -> Rval (menv'++menv, env'++env)
  end

val extend_dec_env : env_val -> flat_env_ctor -> environment v -> environment v
let extend_dec_env new_v new_c env =
  <| m = env.m; c = merge_alist_mod_env ([],new_c) env.c; v = new_v ++ env.v |>

val extend_top_env : env_mod -> env_val -> env_ctor -> environment v -> environment v
let extend_top_env new_m new_v new_c env =
  <| m = new_m ++ env.m; c = merge_alist_mod_env new_c env.c; v = new_v ++ env.v |>

val decs_to_types : list dec -> list typeN
let decs_to_types ds =
  List.concat (List.map (fun d ->
        match d with
          | Dtype tds -> List.map (fun (tvs,tn,ctors) -> tn) tds
          | _ -> [] end)
     ds)

val no_dup_types : list dec -> bool
let no_dup_types ds =
  List.allDistinct (decs_to_types ds)

val prog_to_mods : list top -> list modN
let prog_to_mods tops =
  List.concat (List.map (fun top ->
        match top with
          | Tmod mn _ _ -> [mn]
          | _ -> [] end)
     tops)

val no_dup_mods : list top -> set modN -> bool
let no_dup_mods tops defined_mods =
  List.allDistinct (prog_to_mods tops) &&
  disjoint (Set.fromList (prog_to_mods tops)) defined_mods

val prog_to_top_types : list top -> list typeN
let prog_to_top_types tops =
  List.concat (List.map (fun top ->
        match top with
          | Tdec d -> decs_to_types [d]
          | _ -> [] end)
     tops)

val no_dup_top_types : list top -> set tid_or_exn -> bool
let no_dup_top_types tops defined_types =
  List.allDistinct (prog_to_top_types tops) &&
  disjoint (Set.fromList (List.map (fun tn -> TypeId (Short tn)) (prog_to_top_types tops))) defined_types


(* conversions to strings *)

import Show_extra

let rec
id_to_string (Short s) = s
and
id_to_string (Long x y) = x^"."^y

let tc_to_string tc =
  match tc with
    TC_name id -> id_to_string id
  | TC_int -> "<int>"
  | TC_char -> "<char>"
  | TC_string -> "<string>"
  | TC_ref -> "<ref>"
  | TC_word8 -> "<word8>"
  | TC_word64 -> "<word64>"
  | TC_word8array -> "<word8array>"
  | TC_exn -> "<exn>"
  | TC_vector -> "<vector>"
  | TC_array -> "<array>"
  end

val int_to_string : integer -> string
let int_to_string z =
  if z < 0 then "~"^(show (naturalFromInteger (~ z)))
  else show (naturalFromInteger z)

let rec
string_escape [] = ""
and
string_escape (c::cs) =
  (if c = #'\n' then "\\n"
   else if c = #'\t' then "\\t"
   else if c = #'\\' then "\\\\"
   else String.toString [c])
  ^(string_escape cs)

let string_to_string s =
  "\""^(string_escape (String.toCharList s))^"\""