Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

15 files changed, 645 insertions, 167 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index bd0d7750..bae8381e 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -57,9 +57,37 @@ Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < s
 Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
  l >>= (fun l => if l then r else returnm false).
 
+Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFact (P b)} E) (y : monad rv {b:bool & ArithFact (Q b)} E)
+  `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))}
+  : monad rv {b:bool & ArithFact (R b)} E.
+refine (
+  x >>= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then
+    fun p => y >>= fun '(existT _ y _) => returnm (existT _ y _)
+  else fun p => returnm (existT _ false _)) p
+).
+* constructor. destruct H. destruct a0. change y with (andb true y). auto.
+* constructor. destruct H. change false with (andb false false). apply fact.
+  assumption.
+  congruence.
+Defined.
+
 (*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
 Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
  l >>= (fun l => if l then returnm true else r).
+Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFact (P b)} E) (r : monad rv {b : bool & ArithFact (Q b)} E)
+ `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))}
+ : monad rv {b : bool & ArithFact (R b)} E.
+refine (
+ l >>= fun '(existT _ l (Build_ArithFact _ p)) =>
+  (if l return P l -> _ then fun p => returnm (existT _ true _)
+   else fun p => r >>= fun '(existT _ r _) => returnm (existT _ r _)) p
+).
+* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence.
+* constructor. destruct H. destruct a0. change r with (orb false r). auto.
+Defined.
+
+Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact True} E :=
+  x >>= fun x => returnm (existT _ x (Build_ArithFact _ I)).
 
 (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
 Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 943d850a..e6c5e786 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -45,25 +45,6 @@ End Morphism.
 Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
-(* The informative boolean type. *)
-
-Definition Bool (P : Prop) : Type := {P} + {~P}.
-
-Definition build_Bool {P:Prop} (b:bool) `{ArithFact (b = true <-> P)} : Bool P.
-refine (if sumbool_of_bool b then left _ else right _);
-destruct H; subst;
-intuition.
-Defined.
-
-Definition projBool {P:Prop} (b:Bool P) : bool := if b then true else false.
-
-Lemma projBool_true {P:Prop} {b:Bool P} : projBool b = true <-> P.
-destruct b; simpl; intuition.
-Qed.
-Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P.
-destruct b; simpl; intuition.
-Qed.
-
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
 Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
@@ -1113,11 +1094,6 @@ Ltac extract_properties :=
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
     change (projT1 (existT _ x Hx)) with x in * end.
-(* We could also destruct any remaining Bools, if necessary. *)
-Ltac extract_Bool_props :=
-  repeat match goal with
-  | H:projBool _ = true |- _ => rewrite projBool_true in H
-  | H:projBool _ = false |- _ => rewrite projBool_false in H end.
 (* TODO: hyps, too? *)
 Ltac reduce_list_lengths :=
   repeat match goal with |- context [length_list ?X] => 
@@ -1183,7 +1159,6 @@ Ltac prepare_for_solver :=
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  split_cases;
  extract_properties;
- extract_Bool_props;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  destruct_exists;
@@ -1233,6 +1208,14 @@ prepare_for_solver;
  | constructor; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
+   (* Booleans - and_boolMP *)
+ | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => 
+     constructor; intros l r H1 H2;
+     solve [exists l; destruct l; intuition | exists r; destruct l; intuition]
+   end
+ | match goal with |- context [@eq _ _ _] =>
+     constructor; intuition
+   end
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
 (* Add an indirection so that you can redefine run_solver to fail to get
diff --git a/src/c_backend.ml b/src/c_backend.ml
index a656a097..ab388223 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -71,6 +71,18 @@ let opt_no_main = ref false
 let opt_memo_cache = ref false
 let opt_no_rts = ref false
 let opt_prefix = ref "z"
+let opt_extra_params = ref None
+let opt_extra_arguments = ref None
+
+let extra_params () =
+  match !opt_extra_params with
+  | Some str -> str ^ ", "
+  | _ -> ""
+
+let extra_arguments is_extern =
+  match !opt_extra_arguments with
+  | Some str when not is_extern -> str ^ ", "
+  | _ -> ""
 
 (* Optimization flags *)
 let optimize_primops = ref false
@@ -2588,6 +2600,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_funcall (x, extern, f, args) ->
      let c_args = Util.string_of_list ", " sgen_cval args in
      let ctyp = clexp_ctyp x in
+     let is_extern = Env.is_extern f ctx.tc_env "c" || extern in
      let fname =
        if Env.is_extern f ctx.tc_env "c" then
          Env.get_extern f ctx.tc_env "c"
@@ -2649,9 +2662,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
          string (Printf.sprintf  "  COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
      else
        if is_stack_ctyp ctyp then
-         string (Printf.sprintf "  %s = %s(%s);" (sgen_clexp_pure x) fname c_args)
+         string (Printf.sprintf "  %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args)
        else
-         string (Printf.sprintf "  %s(%s, %s);" fname (sgen_clexp x) c_args)
+         string (Printf.sprintf "  %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args)
 
   | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
      empty
@@ -2867,7 +2880,7 @@ let codegen_type_def ctx = function
          in
          Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty
        in
-       string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_function_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
+       string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline
        ^^ surround 2 0 lbrace
                    (tuple
                     ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline
@@ -3183,9 +3196,9 @@ let codegen_def' ctx = function
      if Env.is_extern id ctx.tc_env "c" then
        empty
      else if is_stack_ctyp ret_ctyp then
-       string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
      else
-       string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_function_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
      if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else ();
@@ -3226,12 +3239,12 @@ let codegen_def' ctx = function
        | None ->
           assert (is_stack_ctyp ret_ctyp);
           (if !opt_static then string "static " else empty)
-          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string args) ^^ hardline
+          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline
        | Some gs ->
           assert (not (is_stack_ctyp ret_ctyp));
           (if !opt_static then string "static " else empty)
           ^^ string "void" ^^ space ^^ codegen_function_id id
-          ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
+          ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
           ^^ hardline
      in
      function_header
diff --git a/src/c_backend.mli b/src/c_backend.mli
index e6cc783c..3b26acdf 100644
--- a/src/c_backend.mli
+++ b/src/c_backend.mli
@@ -53,18 +53,54 @@ open Type_check
 
 (** Global compilation options *)
 
+(** Output a dataflow graph for each generated function in Graphviz
+   (dot) format. *)
 val opt_debug_flow_graphs : bool ref
+
+(** Print the ANF and IR representations of a specific function. *)
 val opt_debug_function : string ref
+
+(** Instrument generated code to output a trace. opt_smt_trace is WIP
+   but intended to enable generating traces suitable for concolic
+   execution with SMT. *)
 val opt_trace : bool ref
 val opt_smt_trace : bool ref
+
+(** Define generated functions as static *)
 val opt_static : bool ref
+
+(** Do not generate a main function *)
 val opt_no_main : bool ref
+
+(** (WIP) Do not include rts.h (the runtime), and do not generate code
+   that requires any setup or teardown routines to be run by a runtime
+   before executing any instruction semantics. *)
 val opt_no_rts : bool ref
+
+(** Ordinarily we use plain z-encoding to name-mangle generated Sail
+   identifiers into a form suitable for C. If opt_prefix is set, then
+   the "z" which is added on the front of each generated C function
+   will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would
+   give sail_my_function rather than zmy_function. *)
 val opt_prefix : string ref
 
-(** [opt_memo_cache] will store the compiled function definitions in
-   file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the
-   original function to be compiled. Enabled using the -memo
+(** opt_extra_params and opt_extra_arguments allow additional state to
+   be threaded through the generated C code by adding an additional
+   parameter to each function type, and then giving an extra argument
+   to each function call. For example we could have
+
+   opt_extra_params := Some "CPUMIPSState *env"
+   opt_extra_arguments := Some "env"
+
+   and every generated function will take a pointer to a QEMU MIPS
+   processor state, and each function will be passed the env argument
+   when it is called. *)
+val opt_extra_params : string option ref
+val opt_extra_arguments : string option ref
+
+(** (WIP) [opt_memo_cache] will store the compiled function
+   definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum
+   of the original function to be compiled. Enabled using the -memo
    flag. Uses Marshal so it's quite picky about the exact version of
    the Sail version. This cache can obviously become stale if the C
    backend changes - it'll load an old version compiled without said
@@ -82,13 +118,14 @@ val optimize_experimental : bool ref
 (** The compilation context. *)
 type ctx
 
-(** Convert a typ to a IR ctyp *)
-val ctyp_of_typ : ctx -> Ast.typ -> ctyp
-
 (** Create a context from a typechecking environment. This environment
    should be the environment returned by typechecking the full AST. *)
 val initial_ctx : Env.t -> ctx
 
+(** Convert a typ to a IR ctyp *)
+val ctyp_of_typ : ctx -> Ast.typ -> ctyp
+
+
 val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list
 
 val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 784929e1..f0472385 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -344,6 +344,7 @@ and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) =
   match ta with
   | A_nexp _
   | A_order _
+  | A_bool _
       -> insts, tyarg
   | A_typ typ ->
      let insts', typ' = inst_src_type insts typ in
@@ -364,6 +365,7 @@ and contains_exist_arg (A_aux (arg,_)) =
   match arg with
   | A_nexp _
   | A_order _
+  | A_bool _
       -> false
   | A_typ typ -> contains_exist typ
 
@@ -2085,19 +2087,26 @@ let split_defs all_errors splits defs =
         | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les))
         | LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id))
         | LEXP_deref e -> re (LEXP_deref (map_exp e))
-      in map_pexp, map_letbind
-    in    
+      in map_exp, map_pexp, map_letbind
+    in
+    let map_exp r = let (f,_,_) = map_fns r in f in
+    let map_pexp r = let (_,f,_) = map_fns r in f in
+    let map_letbind r = let (_,_,f) = map_fns r in f in
+    let map_exp exp =
+      let ref_vars = referenced_vars exp in
+      map_exp ref_vars exp
+    in
     let map_pexp top_pexp =
       (* Construct the set of referenced variables so that we don't accidentally
          make false assumptions about them during constant propagation.  Note that
          we assume there aren't any in the guard. *)
       let (_,_,body,_) = destruct_pexp top_pexp in
       let ref_vars = referenced_vars body in
-      fst (map_fns ref_vars) top_pexp
+      map_pexp ref_vars top_pexp
     in
     let map_letbind (LB_aux (LB_val (_,e),_) as lb) =
       let ref_vars = referenced_vars e in
-      snd (map_fns ref_vars) lb
+      map_letbind ref_vars lb
     in
 
     let map_funcl (FCL_aux (FCL_Funcl (id,pexp),annot)) =
@@ -2128,6 +2137,7 @@ let split_defs all_errors splits defs =
       | DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now"
       | DEF_val lb -> [DEF_val (map_letbind lb)]
       | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd)
+      | DEF_measure (id,pat,exp) -> [DEF_measure (id,pat,map_exp exp)]
     in
     Defs (List.concat (List.map map_def defs))
   in
@@ -2210,6 +2220,7 @@ and sizes_of_typarg (A_aux (ta,_)) =
   match ta with
     A_nexp _
   | A_order _
+  | A_bool _
     -> KidSet.empty
   | A_typ typ -> sizes_of_typ typ
 
@@ -4380,7 +4391,9 @@ let replace_nexp_in_typ env typ orig new_nexp =
     | A_typ typ ->
        let f, typ = aux typ in
        f, A_aux (A_typ typ,l)
-    | A_order _ -> false, typ_arg
+    | A_order _
+    | A_bool _
+      -> false, typ_arg
   in aux typ
 
 let fresh_nexp_kid nexp =
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 430eb40d..d323d639 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -356,7 +356,8 @@ match nc1, nc2 with
 | _, NC_aux (NC_true,_) -> nc1
 | NC_aux (NC_false,_), _ -> nc_not nc2
 | _, NC_aux (NC_false,_) -> nc_not nc1
-| _,_ -> nc_or (nc_and nc1 nc2) (nc_and (nc_not nc1) (nc_not nc2))
+ (* TODO: replace this hacky iff with a proper NC_ constructor *)
+| _,_ -> mk_nc (NC_app (mk_id "iff",[arg_bool nc1; arg_bool nc2]))
 
 (* n_constraint functions are currently just Z3 functions *)
 let doc_nc_fn_prop id =
@@ -370,33 +371,123 @@ let doc_nc_fn id =
   | "not" -> string "negb"
   | s -> string s
 
-type ex_atom_bool = ExBool_simple | ExBool_val of bool | ExBool_complex
+let merge_bool_count = KBindings.union (fun _ m n -> Some (m+n))
 
-let non_trivial_ex_atom_bool l kopts nc atom_nc =
-  let vars = KOptSet.union (kopts_of_constraint nc) (kopts_of_constraint atom_nc) in
-  let exists = KOptSet.of_list kopts in
-  if KOptSet.subset vars exists then
-    let kenv = List.fold_left (fun kenv kopt -> KBindings.add (kopt_kid kopt) (unaux_kind (kopt_kind kopt)) kenv) KBindings.empty kopts in
-    match Constraint.call_smt l kenv (nc_and nc atom_nc),
-          Constraint.call_smt l kenv (nc_and nc (nc_not atom_nc)) with
-    | Sat, Sat -> ExBool_simple
-    | Sat, Unsat -> ExBool_val true
-    | Unsat, Sat -> ExBool_val false
-    | _ -> ExBool_complex
-  else ExBool_complex
-
-type ex_kind = ExNone | ExBool | ExGeneral
-
-let classify_ex_type (Typ_aux (t,l) as t0) =
+let rec count_bool_vars (NC_aux (nc,_)) =
+  let count_arg (A_aux (arg,_)) =
+    match arg with
+    | A_bool nc -> count_bool_vars nc
+    | A_nexp _ | A_typ _ | A_order _ -> KBindings.empty
+  in
+  match nc with
+  | NC_or (nc1,nc2)
+  | NC_and (nc1,nc2)
+    -> merge_bool_count (count_bool_vars nc1) (count_bool_vars nc2)
+  | NC_var kid -> KBindings.singleton kid 1
+  | NC_equal _ | NC_bounded_ge _ | NC_bounded_le _ | NC_not_equal _
+  | NC_set _ | NC_true | NC_false
+    -> KBindings.empty
+  | NC_app (_,args) ->
+     List.fold_left merge_bool_count KBindings.empty (List.map count_arg args)
+
+type atom_bool_prop =
+  Bool_boring
+| Bool_complex of kinded_id list * n_constraint * n_constraint
+
+let simplify_atom_bool l kopts nc atom_nc =
+(*prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*)
+  let counter = ref 0 in
+  let is_bound kid = List.exists (fun kopt -> Kid.compare kid (kopt_kid kopt) == 0) kopts in
+  let bool_vars = merge_bool_count (count_bool_vars nc) (count_bool_vars atom_nc) in
+  let lin_bool_vars = KBindings.filter (fun kid n -> is_bound kid && n = 1) bool_vars in
+  let rec simplify (NC_aux (nc,l) as nc_full) =
+    let is_ex_var news (NC_aux (nc,_)) =
+      match nc with
+      | NC_var kid when KBindings.mem kid lin_bool_vars -> Some kid
+      | NC_var kid when KidSet.mem kid news -> Some kid
+      | _ -> None
+    in
+    let replace kills vars =
+      let v = mk_kid ("simp#" ^ string_of_int !counter) in
+      let kills = KidSet.union kills (KidSet.of_list vars) in
+      counter := !counter + 1;
+      KidSet.singleton v, kills, NC_aux (NC_var v,l)
+    in
+    match nc with
+    | NC_or (nc1,nc2) -> begin
+       let new1, kill1, nc1 = simplify nc1 in
+       let new2, kill2, nc2 = simplify nc2 in
+       let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in
+       match is_ex_var news nc1, is_ex_var news nc2 with
+       | Some kid1, Some kid2 -> replace kills [kid1;kid2]
+       | _ -> news, kills, NC_aux (NC_or (nc1,nc2),l)
+      end
+    | NC_and (nc1,nc2) -> begin
+       let new1, kill1, nc1 = simplify nc1 in
+       let new2, kill2, nc2 = simplify nc2 in
+       let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in
+       match is_ex_var news nc1, is_ex_var news nc2 with
+       | Some kid1, Some kid2 -> replace kills [kid1;kid2]
+       | _ -> news, kills, NC_aux (NC_and (nc1,nc2),l)
+      end
+    | NC_app (Id_aux (Id "not",_) as id,[A_aux (A_bool nc1,al)]) -> begin
+       let new1, kill1, nc1 = simplify nc1 in
+       match is_ex_var new1 nc1 with
+       | Some kid -> replace kill1 [kid]
+       | None -> new1, kill1, NC_aux (NC_app (id,[A_aux (A_bool nc1,al)]),l)
+      end
+    (* We don't currently recurse into general uses of NC_app, but the
+       "boring" cases we really want to get rid of won't contain
+       those. *)
+    | _ -> KidSet.empty, KidSet.empty, nc_full
+  in
+  let new_nc, kill_nc, nc = simplify nc in
+  let new_atom, kill_atom, atom_nc = simplify atom_nc in
+  let new_kids = KidSet.union new_nc new_atom in
+  let kill_kids = KidSet.union kill_nc kill_atom in
+  let kopts =
+    List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @
+      List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts
+  in
+(*prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*)
+  match atom_nc with
+  | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring
+  | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring
+  | _ -> Bool_complex (kopts, nc, atom_nc)
+
+
+type ex_kind = ExNone | ExGeneral
+
+(* Should a Sail type be turned into a dependent pair in Coq?
+   Optionally takes a variable that we're binding (to avoid trivial cases where
+   the type is exactly the boolean we're binding), and whether to turn bools
+   with interesting type-expressions into dependent pairs. *)
+let classify_ex_type ctxt env ?binding ?(rawbools=false) (Typ_aux (t,l) as t0) =
+  let is_binding kid =
+    match binding, KBindings.find_opt kid ctxt.kid_id_renames with
+    | Some id, Some id' when Id.compare id id' == 0 -> true
+    | _ -> false
+  in
+  let simplify_atom_bool l kopts nc atom_nc =
+    match simplify_atom_bool l kopts nc atom_nc with
+    | Bool_boring -> Bool_boring
+    | Bool_complex (_,_,NC_aux (NC_var kid,_)) when is_binding kid -> Bool_boring
+    | Bool_complex (x,y,z) -> Bool_complex (x,y,z)
+  in
   match t with
-  | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin
-      match non_trivial_ex_atom_bool l kopts nc atom_nc with
-      | ExBool_simple -> ExNone, t1
-      | ExBool_val _ -> ExBool, t1
-      | ExBool_complex -> ExGeneral, t1
+  | Typ_exist (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_)) -> begin
+      match simplify_atom_bool l kopts nc atom_nc with
+      | Bool_boring -> ExNone, [], bool_typ
+      | Bool_complex _ -> ExGeneral, [], bool_typ
     end
-  | Typ_exist (_,_,t1) -> ExGeneral,t1
-  | _ -> ExNone,t0
+  | Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]) -> begin
+      match rawbools, simplify_atom_bool l [] nc_true atom_nc with
+      | false, _ -> ExNone, [], bool_typ
+      | _,Bool_boring -> ExNone, [], bool_typ
+      | _,Bool_complex _ -> ExGeneral, [], bool_typ
+    end
+  | Typ_exist (kopts,_,t1) -> ExGeneral,kopts,t1
+  | _ -> ExNone,[],t0
 
 (* When making changes here, check whether they affect coq_nvars_of_typ *)
 let rec doc_typ_fns ctx =
@@ -441,10 +532,17 @@ let rec doc_typ_fns ctx =
          (string "Z")
       | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
          (string "Z")
-      | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool"
-      | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool nc,_)]) ->
-         let tpp = string "Bool" ^^ space ^^ doc_nc_prop ~top:false ctx nc in
-         if atyp_needed then parens tpp else tpp
+      | Typ_app(Id_aux (Id "atom_bool", _), [A_aux (A_bool atom_nc,_)]) ->
+         begin match simplify_atom_bool l [] nc_true atom_nc with
+         | Bool_boring -> string "bool"
+         | Bool_complex (_,_,atom_nc) -> (* simplify won't introduce new kopts *)
+            let var = mk_kid "_bool" in (* TODO collision avoid *)
+            let nc = nice_iff (nc_var var) atom_nc in
+            braces (separate space
+                      [doc_var ctx var; colon; string "bool";
+                       ampersand;
+                       doc_arithfact ctx nc])
+         end
       | Typ_app(id,args) ->
          let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in
          if atyp_needed then parens tpp else tpp
@@ -505,10 +603,9 @@ let rec doc_typ_fns ctx =
                         ampersand;
                         doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc])
           | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin
-             match non_trivial_ex_atom_bool l kopts nc atom_nc with
-             | ExBool_simple -> string "bool"
-             | ExBool_val t -> string "Bool(" ^^ if t then string "True)" else string "False)"
-             | ExBool_complex ->
+             match simplify_atom_bool l kopts nc atom_nc with
+             | Bool_boring -> string "bool"
+             | Bool_complex (kopts,nc,atom_nc) ->
                 let var = mk_kid "_bool" in (* TODO collision avoid *)
                 let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
                 braces (separate space
@@ -814,11 +911,11 @@ let is_ctor env id = match Env.lookup_id id env with
 | Enum _ -> true
 | _ -> false
 
-let is_auto_decomposed_exist env typ =
+let is_auto_decomposed_exist ctxt env ?(rawbools=false) typ =
   let typ = expand_range_type typ in
-  match destruct_exist_plain (Env.expand_synonyms env typ) with
-  | Some (_, _, typ') -> Some typ'
-  | _ -> None
+  match classify_ex_type ctxt env ~rawbools (Env.expand_synonyms env typ) with
+  | ExGeneral, kopts, typ' -> Some (kopts, typ')
+  | ExNone, _, _ -> None
 
 (*Note: vector concatenation, literal vectors, indexed vectors, and record should
   be removed prior to pp. The latter two have never yet been seen
@@ -826,9 +923,11 @@ let is_auto_decomposed_exist env typ =
 let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, typ) =
   let env = env_of_annot (l,annot) in
   let typ = Env.expand_synonyms env typ in
-  match exists_as_pairs, is_auto_decomposed_exist env typ with
-  | true, Some typ' ->
-     let pat_pp = doc_pat ctxt true true (pat, typ') in
+  match exists_as_pairs, is_auto_decomposed_exist ctxt env typ with
+  | true, Some (kopts,typ') ->
+     debug ctxt (lazy ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ'));
+     let ctxt' = { ctxt with bound_nvars = List.fold_left (fun s kopt -> KidSet.add (kopt_kid kopt) s) ctxt.bound_nvars kopts } in
+     let pat_pp = doc_pat ctxt' true true (pat, typ') in
      let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in
      if apat_needed then parens pat_pp else pat_pp
   | _ ->
@@ -1014,10 +1113,8 @@ let replace_atom_return_type ret_typ =
   | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),l) ->
      let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
      Some "build_ex", Typ_aux (Typ_exist ([mk_kopt K_int kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l)
-  (* For informative booleans tweak the type name so that doc_typ knows that the
-     constraint should be output. *)
   | Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) ->
-     Some "build_Bool", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l)
+     Some "build_ex", ret_typ
   | _ -> None, ret_typ
 
 let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) =
@@ -1042,6 +1139,33 @@ let is_prefix s s' =
   String.length s' >= l &&
   String.sub s' 0 l = s
 
+let merge_new_tyvars ctxt old_env pat new_env =
+  let is_new_binding id =
+    match Env.lookup_id ~raw:true id old_env with
+    | Unbound -> true
+    | _ -> false
+  in
+  let new_ids = IdSet.filter is_new_binding (pat_ids pat) in
+  let merge_new_kids id m =
+    let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in
+    debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ ));
+    match destruct_numeric typ, destruct_atom_bool new_env typ with
+    | Some ([],_,Nexp_aux (Nexp_var kid,_)), _
+    | _, Some (NC_aux (NC_var kid,_)) ->
+       begin try
+           let _ = Env.get_typ_var kid old_env in
+           debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env"));
+           m
+         with _ ->
+           debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id));
+           KBindings.add kid id m
+       end
+    | _ ->
+       debug ctxt (lazy (" not suitable type"));
+       m
+  in
+  { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames }
+
 let prefix_recordtype = true
 let report = Reporting.err_unreachable
 let doc_exp, doc_let =
@@ -1068,15 +1192,14 @@ let doc_exp, doc_let =
       match destruct_exist_plain typ with
       | None -> epp
       | Some (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l)) -> begin
-          match non_trivial_ex_atom_bool l kopts nc atom_nc with
-          | ExBool_simple -> epp
-          | ExBool_val t -> wrap_parens (string "build_Bool" ^/^ epp)
-          | ExBool_complex -> wrap_parens (string "build_ex" ^/^ epp)
+          match simplify_atom_bool l kopts nc atom_nc with
+          | Bool_boring -> epp
+          | Bool_complex _ -> wrap_parens (string "build_ex" ^/^ epp)
         end
       | Some _ ->
          wrap_parens (string "build_ex" ^/^ epp)
     in
-    let rec construct_dep_pairs env =
+    let construct_dep_pairs ?(rawbools=false) env =
       let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) =
         match e,t with
         | E_tuple exps, Typ_tup typs
@@ -1085,16 +1208,11 @@ let doc_exp, doc_let =
            parens (separate (string ", ") (List.map2 (aux false) exps typs))
         | _ ->
            let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in
+           debug ctxt (lazy ("Constructing " ^ string_of_exp exp ^ " at type " ^ string_of_typ typ));
            let build_ex, out_typ =
-             match destruct_exist_plain typ' with
-             | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin
-                 match non_trivial_ex_atom_bool l kopts nc atom_nc with
-                 | ExBool_simple -> None, t
-                 | ExBool_val _ -> Some "build_Bool", t
-                 | ExBool_complex -> Some "build_ex", t
-               end
-             | Some (_,_,t) -> Some "build_ex", t
-             | None -> None, typ'
+             match classify_ex_type ctxt (env_of exp) ~rawbools typ' with
+             | ExNone, _, _ -> None, typ'
+             | ExGeneral, _, typ' -> Some "build_ex", typ'
            in
            let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in
            let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in
@@ -1115,7 +1233,7 @@ let doc_exp, doc_let =
              else exp_pp
            in match build_ex with
               | Some s ->
-                let exp_pp = string s ^^ space ^^ exp_pp in
+                let exp_pp = string s ^/^ exp_pp in
                 if want_parens then parens exp_pp else exp_pp
               | None -> exp_pp
       in aux
@@ -1197,14 +1315,31 @@ let doc_exp, doc_let =
     | E_loop _ ->
        raise (report l __POS__ "E_loop should have been rewritten before pretty-printing")
     | E_let(leb,e) ->
-       let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+       let pat = match leb with LB_aux (LB_val (p,_),_) -> p in
+       let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e) in
+       let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in
        if aexp_needed then parens epp else epp
     | E_app(f,args) ->
        begin match f with
        | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
          when effectful (effect_of full_exp) ->
-          let call = doc_id (append_id f "M") in
-          wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
+          let informative = Util.is_some (is_auto_decomposed_exist ctxt (env_of full_exp) (general_typ_of full_exp)) in
+          let suffix = if informative then "MP" else "M" in
+          let call = doc_id (append_id f suffix) in
+          let doc_arg exp =
+            let epp = expY exp in
+            match is_auto_decomposed_exist ctxt (env_of exp) ~rawbools:true (general_typ_of exp) with
+            | Some _ ->
+               if informative then parens (epp ^^ doc_tannot ctxt (env_of exp) true (general_typ_of exp)) else
+               let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in
+               parens (string proj ^/^ epp)
+            | None ->
+               if informative then parens (string "build_trivial_ex" ^/^ epp)
+               else epp
+          in
+          let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in
+          let epp = if informative then epp ^^ doc_tannot ctxt (env_of full_exp) true (general_typ_of full_exp) else epp in
+          wrap_parens epp
        (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "None", _) as none -> doc_id_ctor none
        | Id_aux (Id "foreach#", _) ->
@@ -1435,21 +1570,22 @@ let doc_exp, doc_let =
           let ret_typ_inst =
                subst_unifiers inst ret_typ
           in
-          let packeff,unpack,autocast,projbool =
+          let packeff,unpack,autocast =
             let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in
             let ann_typ = expand_range_type ann_typ in
             let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in
             let ret_typ_inst =
               if is_no_proof_fn env f then ret_typ_inst
               else snd (replace_atom_return_type ret_typ_inst) in
-            let () = 
+            let () =
               debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst));
               debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ))
             in
             let unpack, in_typ =
-              match ret_typ_inst with
-              | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-              | t1 -> false,t1
+              if is_no_proof_fn env f then false, ret_typ_inst else
+                match classify_ex_type ctxt env ~rawbools:true ret_typ_inst with
+                | ExGeneral, _, t1 -> true,t1
+                | ExNone, _, t1 -> false,t1
             in
             let pack,out_typ = 
               match ann_typ with
@@ -1464,23 +1600,17 @@ let doc_exp, doc_let =
                 Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
                  not (similar_nexps ctxt env n1 n2)
               | _ -> false
-            in
-            let projbool =
-              match in_typ with
-              | Typ_aux (Typ_app (Id_aux (Id "atom#bool",_),_),_) -> true
-              | _ -> false
-            in pack,unpack,autocast,projbool
+            in pack,unpack,autocast
           in
           let autocast_id, proj_id =
             if effectful eff
             then "autocast_m", "projT1_m"
             else "autocast",   "projT1" in
-          let epp = if unpack && not (effectful eff) then string proj_id ^^ space ^^ parens epp else epp in
-          let epp = if projbool && not (effectful eff) then string "projBool" ^^ space ^^ parens epp else epp in
+          let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in
           let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
           let epp =
             if effectful eff && packeff && not unpack
-            then string "build_ex_m" ^^ space ^^ parens epp
+            then string "build_ex_m" ^^ break 1 ^^ parens epp
             else epp
           in
           liftR (if aexp_needed then parens (align epp) else epp)
@@ -1545,9 +1675,9 @@ let doc_exp, doc_let =
          debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ));
          debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ))
        in
-       let outer_ex,outer_typ' = classify_ex_type outer_typ in
-       let cast_ex,cast_typ' = classify_ex_type cast_typ in
-       let inner_ex,inner_typ' = classify_ex_type inner_typ in
+       let outer_ex,_,outer_typ' = classify_ex_type ctxt env outer_typ in
+       let cast_ex,_,cast_typ' = classify_ex_type ctxt env ~rawbools:true cast_typ in
+       let inner_ex,_,inner_typ' = classify_ex_type ctxt env inner_typ in
        let autocast =
                 (* Avoid using helper functions which simplify the nexps *)
          is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
@@ -1566,27 +1696,24 @@ let doc_exp, doc_let =
                  otherwise derive the new type from the old one. *)
               if alpha_equivalent env inner_typ cast_typ
               then epp
-              else string "derive_m" ^^ space ^^ epp
+              else string "derive_m" ^/^ epp
            | ExGeneral, ExNone ->
-              string "projT1_m" ^^ space ^^ epp
+              string "projT1_m" ^/^ epp
            | ExNone, ExGeneral ->
-              string "build_ex_m" ^^ space ^^ epp
+              string "build_ex_m" ^/^ epp
            | ExNone, ExNone -> epp
          else match cast_ex with
-              | ExGeneral -> string "build_ex" ^^ space ^^ epp
-              | ExBool -> string "build_Bool" ^^ space ^^ epp
+              | ExGeneral -> string "build_ex" ^/^ epp
               | ExNone -> epp
        in
        let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in
        let epp =
          if effects then
            match cast_ex, outer_ex with
-           | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp
-           | ExBool, ExNone -> string "projBool_m" ^^ space ^^ parens epp
+           | ExGeneral, ExNone -> string "projT1_m" ^/^ parens epp
            | _ -> epp
          else match cast_ex with
-              | ExGeneral -> string "projT1" ^^ space ^^ parens epp
-              | ExBool -> string "projBool" ^^ space ^^ parens epp
+              | ExGeneral -> string "projT1" ^/^ parens epp
               | ExNone -> epp
        in
        let epp =
@@ -1676,7 +1803,7 @@ let doc_exp, doc_let =
        let only_integers e = expY e in
        let epp =
          group ((separate space [string "match"; only_integers e; string "with"]) ^/^
-                  (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^
+                  (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) (typ_of e)) pexps) ^/^
                     (string "end")) in
        if aexp_needed then parens (align epp) else align epp
     | E_try (e, pexps) ->
@@ -1685,7 +1812,7 @@ let doc_exp, doc_let =
          let epp =
            (* TODO capture avoidance for __catch_val *)
            group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^
-                    (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^
+                    (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) exc_typ) pexps) ^/^
                       (string "end)")) in
          if aexp_needed then parens (align epp) else align epp
        else
@@ -1708,11 +1835,12 @@ let doc_exp, doc_let =
            debug ctxt (lazy ("Internal plet, pattern " ^ string_of_pat pat));
            debug ctxt (lazy (" type of e1 " ^ string_of_typ (typ_of e1)))
          in
+         let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e2) in
          match pat, e1, e2 with
          | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)),
            (E_aux (E_assert (assert_e1,assert_e2),_)), _ ->
             let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in
-            let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in
+            let epp = infix 0 1 (string ">>= fun _ =>") epp (top_exp new_ctxt false e2) in
             if aexp_needed then parens (align epp) else align epp
          (* Special case because we don't handle variables with nested existentials well yet.
             TODO: check that id1 is not used in e2' *)
@@ -1727,45 +1855,60 @@ let doc_exp, doc_let =
             let middle =
               match pat' with
               | P_aux (P_id id,_)
-                   when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+                   when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) &&
                           not (is_enum (env_of e1) id) ->
                  separate space [string ">>= fun"; doc_id id; bigarrow]
               | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
-                   when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+                   when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) &&
                           not (is_enum (env_of e1) id) ->
                  separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]              | _ ->
                  separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow]
             in
-            infix 0 1 middle e1_pp (expN e2')
+            infix 0 1 middle e1_pp (top_exp new_ctxt false e2')
          | _ ->
             let epp =
               let middle =
+                let env1 = env_of e1 in
                 match pat with
                 | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
                    string ">>"
                 | P_aux (P_id id,_)
-                   when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+                   when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) &&
                         not (is_enum (env_of e1) id) ->
                    separate space [string ">>= fun"; doc_id id; bigarrow]
                 | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
-                   when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+                   when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) &&
                         not (is_enum (env_of e1) id) ->
                    separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
                 | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
                 | P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id,_),_),_)),_)
                 | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_)
-                    when not (is_enum (env_of e1) id) ->
+                    when not (is_enum env1 id) ->
                       let full_typ = (expand_range_type typ) in
-                      let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with
-                        | ExGeneral, _ ->
+                      let binder = match classify_ex_type ctxt env1 (Env.expand_synonyms env1 full_typ) with
+                        | ExGeneral, _, _ ->
                            squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
-                        | (ExBool | ExNone), _ ->
+                        | ExNone, _, _ ->
                            parens (separate space [doc_id id; colon; doc_typ ctxt typ])
                       in separate space [string ">>= fun"; binder; bigarrow]
+                | P_aux (P_id id,_) ->
+                   let typ = typ_of e1 in
+                   let plain_binder = squote ^^ doc_pat ctxt true true (pat, typ_of e1) in
+                   let binder = match classify_ex_type ctxt env1 ~binding:id (Env.expand_synonyms env1 typ) with
+                     | ExGeneral, _, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') ->
+                         squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
+                     | ExNone, _, typ' -> begin
+                        match typ' with
+                        | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) ->
+                           squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
+                        | _ -> plain_binder
+                       end
+                     | _ -> plain_binder
+                   in separate space [string ">>= fun"; binder; bigarrow]
                 | _ ->
                    separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow]
               in
-              infix 0 1 middle (expY e1) (expN e2)
+              infix 0 1 middle (expY e1) (top_exp new_ctxt false e2)
             in
             if aexp_needed then parens (align epp) else epp
        end
@@ -1779,7 +1922,7 @@ let doc_exp, doc_let =
        in
        let valpp =
          let env = env_of e1 in
-         construct_dep_pairs env true e1 ret_typ
+         construct_dep_pairs env true e1 ret_typ ~rawbools:true
        in
        wrap_parens (align (separate space [string "returnm"; valpp]))
     | E_sizeof nexp ->
@@ -1830,13 +1973,13 @@ let doc_exp, doc_let =
     (* Prefer simple lets over patterns, because I've found Coq can struggle to
        work out return types otherwise *)
     | LB_val(P_aux (P_id id,_),e)
-      when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) &&
+      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) (typ_of e)) &&
            not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; coloneq])
               (top_exp ctxt false e)
     | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
-      when Util.is_none (is_auto_decomposed_exist (env_of e) typ) &&
+      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) typ) &&
            not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq])
@@ -1857,10 +2000,11 @@ let doc_exp, doc_let =
       else doc_id id in
     group (doc_op coloneq fname (top_exp ctxt true e))
 
-  and doc_case ctxt typ = function
+  and doc_case ctxt old_env typ = function
   | Pat_aux(Pat_exp(pat,e),_) ->
-    group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow])
-                  (group (top_exp ctxt false e)))
+     let new_ctxt = merge_new_tyvars ctxt old_env pat (env_of e) in
+     group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow])
+              (group (top_exp new_ctxt false e)))
   | Pat_aux(Pat_when(_,_,_),(l,_)) ->
     raise (Reporting.err_unreachable l __POS__
      "guarded pattern expression should have been rewritten before pretty-printing")
@@ -2118,7 +2262,7 @@ let pat_is_plain_binder env (P_aux (p,_)) =
 let demote_all_patterns env i (P_aux (p,p_annot) as pat,typ) =
   match pat_is_plain_binder env pat with
   | Some id ->
-     if Util.is_none (is_auto_decomposed_exist env typ)
+     if Util.is_none (is_auto_decomposed_exist empty_ctxt env typ)
      then (pat,typ), fun e -> e
      else
        (P_aux (P_id id, p_annot),typ),
@@ -2241,12 +2385,6 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff
     | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
   in
-  let build_ex, ret_typ = replace_atom_return_type ret_typ in
-  let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with
-    | ExGeneral, _ -> Some "build_ex"
-    | ExBool, _ -> Some "build_Bool"
-    | ExNone, _ -> build_ex
-  in
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
@@ -2268,15 +2406,23 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id
     | _ -> false, IdSet.empty
   in
-  let ctxt =
+  let ctxt0 =
     { early_ret = contains_early_return exp;
       kid_renames = mk_kid_renames ids_to_avoid kids_used;
       kid_id_renames = kid_to_arg_rename;
       bound_nvars = bound_kids;
-      build_at_return = if effectful eff then build_ex else None;
+      build_at_return = None; (* filled in below *)
       recursive_ids = recursive_ids;
       debug = List.mem (string_of_id id) (!opt_debug_on)
     } in
+  let build_ex, ret_typ = replace_atom_return_type ret_typ in
+  let build_ex = match classify_ex_type ctxt0 env (Env.expand_synonyms env (expand_range_type ret_typ)) with
+    | ExGeneral, _, _ -> Some "build_ex"
+    | ExNone, _, _ -> build_ex
+  in
+  let ctxt = { ctxt0 with
+      build_at_return = if effectful eff then build_ex else None;
+             } in
   let () =
     debug ctxt (lazy ("Function " ^ string_of_id id));
     debug ctxt (lazy (" return type " ^ string_of_typ ret_typ));
@@ -2299,19 +2445,21 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
       debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ))
     in
     match pat_is_plain_binder env pat with
-    | Some id ->
-       if Util.is_none (is_auto_decomposed_exist env exp_typ) then
-         parens (separate space [doc_id id; colon; doc_typ ctxt typ])
-       else begin
+    | Some id -> begin
+       match classify_ex_type ctxt env ~binding:id exp_typ with
+       | ExNone, _, typ' ->
+         parens (separate space [doc_id id; colon; doc_typ ctxt typ'])
+       | ExGeneral, _, _ ->
            let full_typ = (expand_range_type exp_typ) in
            match destruct_exist_plain (Env.expand_synonyms env full_typ) with
            | Some ([kopt], NC_aux (NC_true,_),
-                   Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                   Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool" as tyname),_),
                                      [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_))
                when Kid.compare (kopt_kid kopt) kid == 0 ->
-              parens (separate space [doc_id id; colon; string "Z"])
+              let coqty = if tyname = "atom" then "Z" else "bool" in
+              parens (separate space [doc_id id; colon; string coqty])
            | Some ([kopt], nc,
-                   Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                   Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool"),_),
                                      [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_))
                when Kid.compare (kopt_kid kopt) kid == 0 && not is_measured ->
               (used_a_pattern := true;
@@ -2596,6 +2744,9 @@ let rec doc_def unimplemented generic_eq_types def =
   | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point"
   | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings"
   | DEF_pragma _ -> empty
+  | DEF_measure (id,_,_) -> unreachable (id_loc id) __POS__
+                              ("Termination measure for " ^ string_of_id id ^
+                                 " should have been rewritten before backend")
 
 let find_exc_typ defs =
   let is_exc_typ_def = function
diff --git a/src/sail.ml b/src/sail.ml
index 0450c0ca..949663d4 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -145,6 +145,12 @@ let options = Arg.align ([
   ( "-c_prefix",
     Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
     "<prefix> prefix generated C functions" );
+  ( "-c_extra_params",
+    Arg.String (fun params -> C_backend.opt_extra_params := Some params),
+    "<parameters> generate C functions with additional parameters" );
+  ( "-c_extra_args",
+    Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
+    "<arguments> supply extra argument to every generated C function call" );
   ( "-elf",
     Arg.String (fun elf -> opt_process_elf := Some elf),
     " process an ELF file so that it can be executed by compiled C code");
diff --git a/src/type_check.ml b/src/type_check.ml
index 8de4a904..a2612794 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1304,6 +1304,15 @@ let bind_existential l name typ env =
   | Some (kids, nc, typ) -> typ, add_existential l kids nc env
   | None -> typ, env
 
+let bind_tuple_existentials l name (Typ_aux (aux, annot) as typ) env =
+  match aux with
+  | Typ_tup typs ->
+     let typs, env =
+       List.fold_right (fun typ (typs, env) -> let typ, env = bind_existential l name typ env in typ :: typs, env) typs ([], env)
+     in
+     Typ_aux (Typ_tup typs, annot), env
+  | _ -> typ, env
+
 let destruct_range env typ =
   let kopts, constr, (Typ_aux (typ_aux, _)) =
     Util.option_default ([], nc_true, typ) (destruct_exist (Env.expand_synonyms env typ))
@@ -1567,6 +1576,8 @@ let merge_uvars l unifiers1 unifiers2 =
   KBindings.merge (merge_unifiers l) unifiers1 unifiers2
 
 let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as typ2) =
+  typ_debug (lazy (Util.("Unify type " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2
+                   ^ " goals " ^ string_of_list ", " string_of_kid (KidSet.elements goals)));
   match aux1, aux2 with
   | Typ_internal_unknown, _ | _, Typ_internal_unknown
        when Env.allow_unknowns env ->
@@ -1577,7 +1588,14 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as
   | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]),
     Typ_app (atom, [A_aux (A_nexp m, _)])
        when string_of_id range = "range" && string_of_id atom = "atom" ->
-     merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
+     let n1, n2 = nexp_simp n1, nexp_simp n2 in
+     begin match n1, n2 with
+     | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) ->
+        if prove __POS__ env (nc_and (nc_lteq n1 m) (nc_lteq m n2)) then KBindings.empty
+        else unify_error l (string_of_typ typ1 ^ " is not contained within " ^ string_of_typ typ1)
+     | _, _ ->
+        merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
+     end
 
   | Typ_app (id1, args1), Typ_app (id2, args2) when List.length args1 = List.length args2 && Id.compare id1 id2 = 0 ->
      List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2)
@@ -1793,7 +1811,7 @@ and ambiguous_nexp_vars (Nexp_aux (aux, _)) =
 let destruct_atom_nexp env typ =
   match Env.expand_synonyms env typ with
   | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _)]), _)
-       when string_of_id f = "atom" -> Some n
+       when string_of_id f = "atom" || string_of_id f = "implicit" -> Some n
   | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _); A_aux (A_nexp m, _)]), _)
        when string_of_id f = "range" && nexp_identical n m -> Some n
   | _ -> None
@@ -2932,6 +2950,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
     try
       typ_debug (lazy ("Coercing unification: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ));
       let atyp, env = bind_existential l None (typ_of annotated_exp) env in
+      let atyp, env = bind_tuple_existentials l None atyp env in
       annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env
     with
     | Unification_error (_, m) when Env.allow_casts env ->
diff --git a/test/typecheck/pass/existential_ast.sail b/test/typecheck/pass/existential_ast.sail
new file mode 100644
index 00000000..37cf2378
--- /dev/null
+++ b/test/typecheck/pass/existential_ast.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect
new file mode 100644
index 00000000..f743abb6
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v1.sail]:46:7-21
+46 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v1.sail b/test/typecheck/pass/existential_ast/v1.sail
new file mode 100644
index 00000000..935313f7
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.sail
@@ -0,0 +1,47 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b01);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect
new file mode 100644
index 00000000..20738cd8
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v2.sail]:39:7-21
+39 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v2.sail b/test/typecheck/pass/existential_ast/v2.sail
new file mode 100644
index 00000000..fd272dbb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 30)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
new file mode 100644
index 00000000..1b6239bb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -0,0 +1,7 @@
+Type error:
+[existential_ast/v3.sail]:26:7-21
+26 |  Some(Ctor1(a, x, c))
+   |       ^------------^
+   | Could not resolve quantifiers for Ctor1
+   | * datasize('ex59#)
+   | 
diff --git a/test/typecheck/pass/existential_ast/v3.sail b/test/typecheck/pass/existential_ast/v3.sail
new file mode 100644
index 00000000..1bacbf80
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|16, 32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file