Support bitvector-size-parametric functions in Lem output

Translates atom('n) types into itself('n) types that won't be erased
Also exports more rewriting functions

7 files changed, 327 insertions, 32 deletions

diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index d4dca80c..8fb55137 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -3,6 +3,16 @@ open import Machine_word
 open import Sail_impl_base
 open import Sail_values
 
+(* Translating between a type level number (itself 'n) and an integer *)
+
+let size_itself_int x = integerFromNat (size_itself x)
+
+(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
+   the actual integer is ignored. *)
+
+val make_the_value : forall 'n. integer -> itself 'n
+let inline make_the_value x = the_value
+
 (*** Bit vector operations *)
 
 let bitvector_length bs = integerFromNat (word_length bs)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 61e352f5..b33d90f5 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -913,6 +913,7 @@ let initial_kind_env =
     ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})});
     ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) });
     ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} );
+    ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})});
   ]
 
 let typschm_of_string order str =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 2c3dda0e..53200b16 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -264,24 +264,24 @@ and contains_exist_arg (Typ_arg_aux (arg,_)) =
       -> false
   | Typ_arg_typ typ -> contains_exist typ
 
+let rec size_nvars_nexp (Nexp_aux (ne,_)) =
+  match ne with
+  | Nexp_var v -> [v]
+  | Nexp_id _
+  | Nexp_constant _
+    -> []
+  | Nexp_times (n1,n2)
+  | Nexp_sum (n1,n2)
+  | Nexp_minus (n1,n2)
+    -> size_nvars_nexp n1 @ size_nvars_nexp n2
+  | Nexp_exp n
+  | Nexp_neg n
+    -> size_nvars_nexp n
+
 (* Given a type for a constructor, work out which refinements we ought to produce *)
 (* TODO collision avoidance *)
 let split_src_type id ty (TypQ_aux (q,ql)) =
   let i = string_of_id id in
-  let rec size_nvars_nexp (Nexp_aux (ne,_)) =
-    match ne with
-    | Nexp_var v -> [v]
-    | Nexp_id _
-    | Nexp_constant _
-      -> []
-    | Nexp_times (n1,n2)
-    | Nexp_sum (n1,n2)
-    | Nexp_minus (n1,n2)
-      -> size_nvars_nexp n1 @ size_nvars_nexp n2
-    | Nexp_exp n
-    | Nexp_neg n
-      -> size_nvars_nexp n
-  in
   (* This was originally written for the general case, but I cut it down to the
      more manageable prenex-form below *)
   let rec size_nvars_ty (Typ_aux (ty,l) as typ) =
@@ -1438,13 +1438,266 @@ let split_defs splits defs =
       | DEF_reg_dec _
       | DEF_comm _
       | DEF_overload _
+      | DEF_fixity _
         -> [d]
       | DEF_fundef fd -> [DEF_fundef (map_fundef fd)]
       | DEF_val lb -> [DEF_val (map_letbind lb)]
       | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd)
-
     in
     Defs (List.concat (List.map map_def defs))
   in
   map_locs splits defs'
 
+
+
+(* The next section of code turns atom('n) types into itself('n) types, which
+   survive into the Lem output, so can be used to parametrise functions over
+   internal bitvector lengths (such as datasize and regsize in ARM specs *)
+
+module AtomToItself =
+struct
+
+let findi f =
+  let rec aux n = function
+    | [] -> None
+    | h::t -> match f h with Some x -> Some (n,x) | _ -> aux (n+1) t
+  in aux 0
+
+let mapat f is xs =
+  let rec aux n = function
+    | _, [] -> []
+    | (i,_)::is, h::t when i = n ->
+       let h' = f h in
+       let t' = aux (n+1) (is, t) in
+       h'::t'
+    | is, h::t ->
+       let t' = aux (n+1) (is, t) in
+       h::t'
+  in aux 0 (is, xs)
+
+let mapat_extra f is xs =
+  let rec aux n = function
+    | _, [] -> [], []
+    | (i,v)::is, h::t when i = n ->
+       let h',x = f v h in
+       let t',xs = aux (n+1) (is, t) in
+       h'::t',x::xs
+    | is, h::t ->
+       let t',xs = aux (n+1) (is, t) in
+       h::t',xs
+  in aux 0 (is, xs)
+
+let tyvars_bound_in_pat pat =
+  let open Rewriter in
+  fst (fold_pat
+         { (compute_pat_alg KidSet.empty KidSet.union) with
+           p_var = (fun ((s,pat),kid) -> KidSet.add kid s, P_var (pat,kid)) }
+         pat)
+let tyvars_bound_in_lb (LB_aux (LB_val (pat,_),_)) = tyvars_bound_in_pat pat
+
+let rec sizes_of_typ (Typ_aux (t,l)) =
+  match t with
+    Typ_wild
+  | Typ_id _
+  | Typ_var _
+    -> KidSet.empty
+  | Typ_fn _ -> raise (Reporting_basic.err_general l
+                         "Function type on expressinon")
+  | Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs)
+  | Typ_exist (kids,_,typ) ->
+     List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids
+  | Typ_app (Id_aux (Id "vector",_),
+             [_;Typ_arg_aux (Typ_arg_nexp size,_);
+              _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
+     KidSet.of_list (size_nvars_nexp size)
+  | Typ_app (_,tas) ->
+     kidset_bigunion (List.map sizes_of_typarg tas)
+and sizes_of_typarg (Typ_arg_aux (ta,_)) =
+  match ta with
+    Typ_arg_nexp _
+  | Typ_arg_order _
+    -> KidSet.empty
+  | Typ_arg_typ typ -> sizes_of_typ typ
+
+let sizes_of_annot = function
+  | _,None -> KidSet.empty
+  | _,Some (_,typ,_) -> sizes_of_typ typ
+
+let change_parameter_pat kid = function
+  | P_aux (P_id var, (l,_))
+  | P_aux (P_typ (_,P_aux (P_id var, (l,_))),_)
+    -> P_aux (P_id var, (l,None)), (var,kid)
+  | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l
+                                "Expected variable pattern")
+
+(* We add code to change the itself('n) parameter into the corresponding
+   integer. *)
+let add_var_rebind exp (var,kid) =
+  let l = Generated Unknown in
+  let annot = (l,None) in
+  E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,annot),
+                                E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot)),annot),exp),annot)
+
+(* atom('n) arguments to function calls need to be rewritten *)
+let replace_with_the_value (E_aux (_,(l,_)) as exp) =
+  let typ = Env.expand_synonyms (env_of exp) (typ_of exp) in
+  let typ, wrap = match typ with
+    | Typ_aux (Typ_exist (kids,nc,typ),l) -> typ, fun t -> Typ_aux (Typ_exist (kids,nc,t),l)
+    | _ -> typ, fun x -> x
+  in
+  let mk_exp nexp l l' =
+     E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
+                                      [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)),
+                    E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,None))),
+            (Generated l,None))
+  in
+  match typ with
+  | Typ_aux (Typ_app (Id_aux (Id "range",_),
+                      [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp nexp',_)]),_)
+    when nexp = nexp' ->
+     mk_exp nexp l l'
+  | _ -> raise (Reporting_basic.err_unreachable l
+                  "atom stopped being an atom?")
+
+let replace_type env typ =
+  let Typ_aux (t,l) = Env.expand_synonyms env typ in
+  match t with
+  | Typ_app (Id_aux (Id "range",_),
+             [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp _,_)]) ->
+     Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
+                       [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l)
+  | _ -> raise (Reporting_basic.err_unreachable l
+                  "atom stopped being an atom?")
+
+
+let rewrite_size_parameters env (Defs defs) =
+  let open Rewriter in
+  let size_vars exp =
+    fst (fold_exp
+           { (compute_exp_alg KidSet.empty KidSet.union) with
+             e_aux = (fun ((s,e),annot) -> KidSet.union s (sizes_of_annot annot), E_aux (e,annot));
+             e_let = (fun ((sl,lb),(s2,e2)) -> KidSet.union sl (KidSet.diff s2 (tyvars_bound_in_lb lb)), E_let (lb,e2));
+             pat_exp = (fun ((sp,pat),(s,e)) -> KidSet.diff s (tyvars_bound_in_pat pat), Pat_exp (pat,e))}
+           exp)
+  in
+  let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pat,exp),(l,_))) =
+    let sizes = size_vars exp in
+    (* TODO: what, if anything, should sequential be? *)
+    let visible_tyvars =
+      KidSet.union (Pretty_print_lem.lem_tyvars_of_typ false true (pat_typ_of pat))
+         (Pretty_print_lem.lem_tyvars_of_typ false true (typ_of exp))
+    in
+    let expose_tyvars = KidSet.diff sizes visible_tyvars in
+    let parameters = match pat with
+      | P_aux (P_tup ps,_) -> ps
+      | _ -> [pat]
+    in
+    let to_change = List.map
+      (fun kid ->
+        let check (P_aux (_,(_,Some (env,typ,_)))) =
+          match Env.expand_synonyms env typ with
+            Typ_aux (Typ_app(Id_aux (Id "range",_),
+                             [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_);
+                              Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_) ->
+              if Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 then Some kid else None
+          | _ -> None
+        in match findi check parameters with
+        | None -> raise (Reporting_basic.err_general l
+                           ("Unable to find an argument for " ^ string_of_kid kid))
+        | Some i -> i)
+      (KidSet.elements expose_tyvars)
+    in
+    let to_change = List.sort compare to_change in
+    match Bindings.find id fsizes with
+    | old -> if old = to_change then fsizes else
+        raise (Reporting_basic.err_general l
+                 ("Different size type variables in different clauses of " ^ string_of_id id))
+    | exception Not_found -> Bindings.add id to_change fsizes
+  in
+  let sizes_def fsizes = function
+    | DEF_fundef (FD_aux (FD_function (_,_,_,funcls),_)) ->
+       List.fold_left sizes_funcl fsizes funcls
+    | _ -> fsizes
+  in
+  let fn_sizes = List.fold_left sizes_def Bindings.empty defs in
+
+  let rewrite_e_app (id,args) =
+    match Bindings.find id fn_sizes with
+    | [] -> E_app (id,args)
+    | to_change ->
+       let args' = mapat replace_with_the_value to_change args in
+       E_app (id,args')
+    | exception Not_found -> E_app (id,args)
+  in
+  let rewrite_funcl (FCL_aux (FCL_Funcl (id,pat,body),(l,annot))) =
+    let pat,body =
+      (* Update pattern and add itself -> nat wrapper to body *)
+      match Bindings.find id fn_sizes with
+      | [] -> pat,body
+      | to_change ->
+         let pat, vars =
+           match pat with
+             P_aux (P_tup pats,(l,_)) ->
+               let pats, vars = mapat_extra change_parameter_pat to_change pats in
+               P_aux (P_tup pats,(l,None)), vars
+           | P_aux (_,(l,_)) ->
+              begin
+                match to_change with
+                | [0,kid] ->
+                   let pat, var = change_parameter_pat kid pat in
+                   pat, [var]
+                | _ ->
+                   raise (Reporting_basic.err_unreachable l
+                            "Expected multiple parameters at single parameter")
+              end
+         in
+         let body = List.fold_left add_var_rebind body vars in
+         pat,body
+      | exception Not_found -> pat,body
+    in
+    (* Update function applications *)
+    let body = fold_exp { id_exp_alg with e_app = rewrite_e_app } body in
+    FCL_aux (FCL_Funcl (id,pat,body),(l,None))
+  in
+  let rewrite_def = function
+    | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) ->
+       (* TODO rewrite tannopt? *)
+       DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None)))
+    | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec ->
+       begin
+         match Bindings.find id fn_sizes with
+         | [] -> spec
+         | to_change ->
+            let typschm = match typschm with
+              | TypSchm_aux (TypSchm_ts (tq,typ),l) ->
+                 let typ = match typ with
+                   | Typ_aux (Typ_fn (Typ_aux (Typ_tup ts,l),t2,eff),l2) ->
+                      Typ_aux (Typ_fn (Typ_aux (Typ_tup (mapat (replace_type env) to_change ts),l),t2,eff),l2)
+                   | _ -> replace_type env typ
+                 in TypSchm_aux (TypSchm_ts (tq,typ),l)
+            in
+            DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,None)))
+         | exception Not_found -> spec
+       end
+    | def -> def
+  in
+(*
+  Bindings.iter (fun id args ->
+    print_endline (string_of_id id ^ " needs " ^
+                     String.concat ", " (List.map string_of_int args))) fn_sizes
+*)
+  Defs (List.map rewrite_def defs)
+
+end
+
+let monomorphise mwords splits defs =
+  let defs = split_defs splits defs in
+  (* TODO: currently doing this because constant propagation leaves numeric literals as
+     int, try to avoid this later; also use final env for DEF_spec case above, because the
+     type checker doesn't store the env at that point :( *)
+  if mwords then
+    let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
+    let defs = AtomToItself.rewrite_size_parameters env defs in
+    defs
+  else
+    defs
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f4ff3a40..6efebbc7 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -427,7 +427,9 @@ let rec typeclass_nexps (Typ_aux(t,_)) = match t with
 | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
 | Typ_app (Id_aux (Id "vector",_),
            [_;Typ_arg_aux (Typ_arg_nexp size_nexp,_);
-            _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
+            _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
+| Typ_app (Id_aux (Id "itself",_),
+           [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) ->
    let size_nexp = simplify_nexp size_nexp in
    if is_nexp_constant size_nexp then NexpSet.empty else
    NexpSet.singleton (orig_nexp size_nexp)
@@ -494,13 +496,14 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
   | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
   | P_record (_,_) -> empty (* TODO *)
 
-let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
-  | Typ_tup ts -> List.exists contains_bitvector_typ ts
-  | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists contains_bitvector_typ_arg targs
-  | Typ_fn (t1,t2,_) -> contains_bitvector_typ t1 || contains_bitvector_typ t2
+let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
+  | Typ_tup ts -> List.exists typ_needs_printed ts
+  | Typ_app (Id_aux (Id "itself",_),_) -> true
+  | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs
+  | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2
   | _ -> false
-and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with
-  | Typ_arg_typ t -> contains_bitvector_typ t
+and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with
+  | Typ_arg_typ t -> typ_needs_printed t
   | _ -> false
 
 let contains_early_return exp =
@@ -697,7 +700,7 @@ let doc_exp_lem, doc_let_lem =
           let (taepp,aexp_needed) =
             let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
             let eff = effect_of full_exp in
-            if contains_bitvector_typ t && not (contains_t_pp_var t)
+            if typ_needs_printed t && not (contains_t_pp_var t)
             then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
             else (epp, aexp_needed) in
           if aexp_needed then parens (align taepp) else taepp*)
@@ -739,7 +742,7 @@ let doc_exp_lem, doc_let_lem =
              let (taepp,aexp_needed) =
                let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in
                let eff = effect_of full_exp in
-               if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t)
+               if typ_needs_printed (Env.base_typ_of (env_of full_exp) t)
                then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
                else (epp, aexp_needed) in
              liftR (if aexp_needed then parens (align taepp) else taepp)
@@ -797,7 +800,7 @@ let doc_exp_lem, doc_let_lem =
        let (epp,aexp_needed) =
          if has_effect eff BE_rreg then
            let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
-           if contains_bitvector_typ t && not (contains_t_pp_var t)
+           if typ_needs_printed t && not (contains_t_pp_var t)
            then (epp ^^ doc_tannot_lem sequential mwords true t, true)
            else (epp, aexp_needed)
          else
@@ -818,7 +821,7 @@ let doc_exp_lem, doc_let_lem =
            let eff = effect_of full_exp in
            let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
            let (ta,aexp_needed) =
-             if contains_bitvector_typ t
+             if typ_needs_printed t
              then (doc_tannot_lem sequential mwords (effectful eff) t, true)
              else (empty, aexp_needed) in
            let epp = field_f ^^ space ^^ (expY fexp) in
@@ -853,7 +856,7 @@ let doc_exp_lem, doc_let_lem =
                   | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield"
                   | _ -> "read_reg_field" in
                 let ta =
-                  if contains_bitvector_typ t && not (contains_t_pp_var t)
+                  if typ_needs_printed t && not (contains_t_pp_var t)
                   then doc_tannot_lem sequential mwords true t else empty in
                 let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
@@ -861,7 +864,7 @@ let doc_exp_lem, doc_let_lem =
                 let (call,ta) =
                   if has_effect eff BE_rreg then
                     let ta =
-                      if contains_bitvector_typ t && not (contains_t_pp_var t)
+                      if typ_needs_printed t && not (contains_t_pp_var t)
                       then doc_tannot_lem sequential mwords true t else empty in
                     ("read_two_regs", ta)
                   else
@@ -874,7 +877,7 @@ let doc_exp_lem, doc_let_lem =
                     separate space [string "read_reg_bit";string reg;doc_int start]
                   else
                     let ta =
-                      if contains_bitvector_typ t && not (contains_t_pp_var t)
+                      if typ_needs_printed t && not (contains_t_pp_var t)
                       then doc_tannot_lem sequential mwords true t else empty in
                     separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
@@ -886,7 +889,7 @@ let doc_exp_lem, doc_let_lem =
         | Base((_,t),External _,_,_,_,_) ->
            (* TODO: Does this case still exist with the new type checker? *)
            let epp = string "read_reg" ^^ space ^^ expY e in
-           if contains_bitvector_typ t && not (contains_t_pp_var t)
+           if typ_needs_printed t && not (contains_t_pp_var t)
            then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp
         | Base((_,t),_,_,_,_,_) ->
            (match typ with
@@ -1118,7 +1121,7 @@ let doc_exp_lem, doc_let_lem =
                 | _ ->
                    string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
            let (epp,aexp_needed) =
-             if contains_bitvector_typ t && not (contains_t_pp_var t)
+             if typ_needs_printed t && not (contains_t_pp_var t)
              then (parens epp ^^ doc_tannot_lem sequential mwords false t, true)
              else (epp, aexp_needed) in
            if aexp_needed then parens (align epp) else epp
diff --git a/src/process_file.ml b/src/process_file.ml
index 59518075..aea53ca7 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -121,7 +121,7 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E
 let opt_ddump_raw_mono_ast = ref false
 
 let monomorphise_ast locs ast =
-  let ast = Monomorphise.split_defs locs ast in
+  let ast = Monomorphise.monomorphise (!opt_lem_mwords) locs ast in
   let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in
   let ienv = Type_check.Env.no_casts Type_check.initial_env in
   Type_check.check ienv ast
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 3125c410..3f375e25 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -151,12 +151,24 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; pat_alg                  : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
  }
 
+(* fold over patterns *)
+val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat
+
 (* fold over expressions *)
 val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
 
 val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
+val id_exp_alg :
+  ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp,
+  'a fexp_aux,'a fexps,'a fexps_aux,
+  'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux,
+  'a letbind_aux,'a letbind,
+  'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg
+
+val compute_pat_alg : 'b -> ('b -> 'b -> 'b) ->
+  ('a,('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) pat_alg
 
 val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
   ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp),
diff --git a/src/type_check.ml b/src/type_check.ml
index 6c5205fe..6b7495c2 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -507,6 +507,7 @@ end = struct
     || Id.compare id (mk_id "real") = 0
     || Id.compare id (mk_id "list") = 0
     || Id.compare id (mk_id "string") = 0
+    || Id.compare id (mk_id "itself") = 0
 
   (* Check if a type, order, or n-expression is well-formed. Throws a
      type error if the type is badly formed. FIXME: Add arity to type
@@ -922,6 +923,21 @@ let initial_env =
   Env.empty
   |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args)))
 
+  (* Internal functions for Monomorphise.AtomToItself *)
+
+  |> Env.add_extern (mk_id "size_itself_int") "size_itself_int"
+  |> Env.add_val_spec (mk_id "size_itself_int")
+      (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
+                                  Parse_ast.Unknown)],Parse_ast.Unknown),
+       function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))])
+         (atom_typ (nvar (mk_kid "n"))) no_effect)
+  |> Env.add_extern (mk_id "make_the_value") "make_the_value"
+  |> Env.add_val_spec (mk_id "make_the_value")
+      (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
+                                  Parse_ast.Unknown)],Parse_ast.Unknown),
+       function_typ (atom_typ (nvar (mk_kid "n")))
+         (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) no_effect)
+
 let ex_counter = ref 0
 
 let fresh_existential ?name:(n="") () =