Merge remote-tracking branch 'origin/sail2' into asl_flow2

13 files changed, 180 insertions, 49 deletions

diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index de7588dc..33a665a0 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -64,10 +64,6 @@ let rec n_leading_spaces s =
          | _ -> 0
       end
     else
-      (* match len with
-   *     (\* | 0 -> 0 *\)
-   * (\* | 1 -> *\) 
-   * | len -> *)
            (* Isabelle generation for pattern matching on characters
               is currently broken, so use an if-expression *)
            if nth s 0 = #' '
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 30b8bc96..ae65f13d 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -726,6 +726,8 @@ let to_ast_def ctx def : unit def ctx_out =
   | P.DEF_scattered sdef ->
      let sdef, ctx = to_ast_scattered ctx sdef in
      DEF_scattered sdef, ctx
+  | P.DEF_measure (id, pat, exp) ->
+     DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp), ctx
 
 let rec remove_mutrec = function
   | [] -> []
diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index 3d238676..eadc85bf 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -155,6 +155,7 @@ type barrier_kind =
   | Barrier_RISCV_rw_r
   | Barrier_RISCV_r_w
   | Barrier_RISCV_w_r
+  | Barrier_RISCV_tso
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE
@@ -184,6 +185,7 @@ instance (Show barrier_kind)
     | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
     | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
     | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
+    | Barrier_RISCV_tso   -> "Barrier_RISCV_tso"
     | Barrier_RISCV_i     -> "Barrier_RISCV_i"
     | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
   end
@@ -300,7 +302,8 @@ instance (EnumerationType barrier_kind)
     | Barrier_RISCV_rw_r -> 19
     | Barrier_RISCV_r_w -> 20
     | Barrier_RISCV_w_r -> 21
-    | Barrier_RISCV_i -> 22
-    | Barrier_x86_MFENCE -> 23
+    | Barrier_RISCV_tso -> 22
+    | Barrier_RISCV_i -> 23
+    | Barrier_x86_MFENCE -> 24
   end
 end
diff --git a/src/lexer.mll b/src/lexer.mll
index 8df728e2..604931ac 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -180,6 +180,7 @@ let kw_table =
      ("nondet",                  (fun x -> Nondet));
      ("escape",                  (fun x -> Escape));
      ("configuration",           (fun _ -> Configuration));
+     ("termination_measure",     (fun _ -> TerminationMeasure));
    ]
 
 
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index cbd2a8c5..2e78b825 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -506,6 +506,7 @@ def =  (* Top-level definition *)
  | DEF_spec of val_spec (* top-level type constraint *)
  | DEF_default of default_typing_spec (* default kind and type assumptions *)
  | DEF_scattered of scattered_def (* scattered definition *)
+ | DEF_measure of id * pat * exp (* separate termination measure declaration *)
  | DEF_reg_dec of dec_spec (* register declaration *)
  | DEF_pragma of string * string * l
  | DEF_internal_mutrec of fundef list
diff --git a/src/parser.mly b/src/parser.mly
index 68720048..7540d1f4 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -182,7 +182,7 @@ let rec desugar_rchain chain s e =
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
-%token Repeat Until While Do Mutual Var Ref Configuration
+%token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure
 
 %nonassoc Then
 %nonassoc Else
@@ -1430,6 +1430,8 @@ def:
     { DEF_internal_mutrec $3 }
   | Pragma
     { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) }
+  | TerminationMeasure id pat Eq exp
+    { DEF_measure ($2, $3, $5) }
 
 defs_list:
   | def
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5a122557..802957c6 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -65,6 +65,20 @@ let opt_debug_on : string list ref = ref []
  * PPrint-based sail-to-coq pprinter
 ****************************************************************************)
 
+(* Data representation:
+ *
+ * In pure computations we keep values with top level existential types
+ * (including ranges and nats) separate from the proofs of the accompanying
+ * constraints, which keeps the terms shorter and more manageable.
+ * Existentials embedded in types (e.g., in tuples or datatypes) are dependent
+ * pairs.
+ *
+ * Monadic values always includes the proof in a dependent pair because the
+ * constraint solving tactic won't see the term that defined the value, and
+ * must rely entirely on the type (like the Sail type checker).
+ *)
+
+
 type context = {
   early_ret : bool;
   kid_renames : kid KBindings.t; (* Plain tyvar -> tyvar renames *)
@@ -225,9 +239,9 @@ let doc_nexp ctx ?(skip_vars=KidSet.empty) nexp =
   and app (Nexp_aux (n,l) as nexp) =
     match n with
     | Nexp_app (Id_aux (Id "div",_), [n1;n2])
-        -> separate space [string "Z.quot"; atomic n1; atomic n2]
+        -> separate space [string "ZEuclid.div"; atomic n1; atomic n2]
     | Nexp_app (Id_aux (Id "mod",_), [n1;n2])
-        -> separate space [string "Z.rem"; atomic n1; atomic n2]
+        -> separate space [string "ZEuclid.modulo"; atomic n1; atomic n2]
     | Nexp_app (Id_aux (Id "abs_atom",_), [n1])
         -> separate space [string "Z.abs"; atomic n1]
     | _ -> atomic nexp
@@ -571,8 +585,9 @@ let doc_lit (L_aux(lit,l)) =
   | L_false -> utf8string "false"
   | L_true  -> utf8string "true"
   | L_num i ->
-     let ipp = Big_int.to_string i in
-     utf8string ipp
+     let s = Big_int.to_string i in
+     let ipp = utf8string s in
+     if Big_int.less i Big_int.zero then parens ipp else ipp
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
@@ -761,9 +776,9 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
           | _ -> raise (Reporting.err_unreachable l __POS__ "tuple pattern doesn't have tuple type")
         in
         (match pats, typs with
-        | [p], [typ'] -> doc_pat ctxt apat_needed exists_as_pairs (p, typ')
+        | [p], [typ'] -> doc_pat ctxt apat_needed true (p, typ')
         | [_], _ -> raise (Reporting.err_unreachable l __POS__ "tuple pattern length does not match tuple type length")
-        | _ -> parens (separate_map comma_sp (doc_pat ctxt false exists_as_pairs) (List.combine pats typs)))
+        | _ -> parens (separate_map comma_sp (doc_pat ctxt false true) (List.combine pats typs)))
      | P_list pats ->
         let el_typ = match typ with
           | Typ_aux (Typ_app (f, [A_aux (A_typ el_typ,_)]),_)
@@ -1182,13 +1197,39 @@ let doc_exp, doc_let =
             else if IdSet.mem f ctxt.recursive_ids
             then doc_id f, false, false, true
             else doc_id f, false, false, false in
-          let (tqs,fn_ty) = Env.get_val_spec_orig f env in
+          let (tqs,fn_ty) = Env.get_val_spec f env in
+          (* Calculate the renaming *)
+          let tqs_map = List.fold_left
+                          (fun m k ->
+                            let kid = kopt_kid k in
+                            KBindings.add (orig_kid kid) kid m)
+                          KBindings.empty (quant_kopts tqs) in
           let arg_typs, ret_typ, eff = match fn_ty with
             | Typ_aux (Typ_fn (arg_typs,ret_typ,eff),_) -> arg_typs, ret_typ, eff
             | _ -> raise (Reporting.err_unreachable l __POS__ "Function not a function type")
           in
           let inst =
-            match instantiation_of_without_type full_exp with
+            (* We attempt to get an instantiation of the function signature's
+               type variables which agrees with Coq by
+               1. using dummy variables with the expected type of each argument
+                  (avoiding the inferred type, which might have (e.g.) stripped
+                  out an existential quantifier)
+               2. calculating the instantiation without using the expected
+                  return type, so that we can work out if we need a cast around
+                  the function call. *)
+            let dummy_args =
+              Util.list_mapi (fun i exp -> mk_id ("#coq#arg" ^ string_of_int i),
+                                           general_typ_of exp) args
+            in
+            let dummy_exp = mk_exp (E_app (f, List.map (fun (id,_) -> mk_exp (E_id id)) dummy_args)) in
+            let dummy_env = List.fold_left (fun env (id,typ) -> Env.add_local id (Immutable,typ) env) env dummy_args in
+            let inst_exp =
+              try infer_exp dummy_env dummy_exp
+              with ex ->
+                debug ctxt (lazy (" cannot infer dummy application " ^ Printexc.to_string ex));
+                full_exp
+            in
+            match instantiation_of_without_type inst_exp with
             | x -> x
             (* Not all function applications can be inferred, so try falling back to the
                type inferred when we know the target type.
@@ -1196,7 +1237,8 @@ let doc_exp, doc_let =
                to cast. *)
             | exception _ -> instantiation_of full_exp
           in
-          let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+          let inst = KBindings.fold (fun k u m -> KBindings.add (KBindings.find (orig_kid k) tqs_map) u m) inst KBindings.empty in
+          let () = debug ctxt (lazy (" instantiations: " ^ String.concat ", " (List.map (fun (kid,tyarg) -> string_of_kid kid ^ " => " ^ string_of_typ_arg tyarg) (KBindings.bindings inst)))) in
 
           (* Insert existential packing of arguments where necessary *)
           let doc_arg want_parens arg typ_from_fn =
@@ -1221,14 +1263,29 @@ let doc_exp, doc_let =
                  not (similar_nexps ctxt env n1 n2)
               | _ -> false
             in
-            let want_parens1 = want_parens || autocast in
-            let arg_pp =
-              construct_dep_pairs env want_parens1 arg typ_from_fn
+            (* If the argument is an integer that can be inferred from the
+               context in a different form, let Coq fill it in.  E.g.,
+               when "64" is really "8 * width".  Avoid cases where the
+               type checker has introduced a phantom type variable while
+               calculating the instantiations. *)
+            let vars_in_env n =
+              let ekids = Env.get_typ_vars env in
+              KidSet.for_all (fun kid -> KBindings.mem kid ekids) (nexp_frees n)
             in
-            if autocast && false
-            then let arg_pp = string "autocast" ^^ space ^^ arg_pp in
-                 if want_parens then parens arg_pp else arg_pp
-            else arg_pp
+            match typ_of_arg, typ_from_fn with
+            | Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n1,_)]),_),
+              Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n2,_)]),_)
+                 when vars_in_env n2 && not (similar_nexps ctxt env n1 n2) ->
+               underscore
+            | _ ->
+               let want_parens1 = want_parens || autocast in
+               let arg_pp =
+                 construct_dep_pairs env want_parens1 arg typ_from_fn
+               in
+               if autocast && false
+               then let arg_pp = string "autocast" ^^ space ^^ arg_pp in
+                    if want_parens then parens arg_pp else arg_pp
+               else arg_pp
           in
           let epp =
             if is_ctor
@@ -1240,7 +1297,7 @@ let doc_exp, doc_let =
                                  [parens (string "_limit_reduces _acc")]
                 else match f with
                      | Id_aux (Id x,_) when is_prefix "#rec#" x ->
-                        main_call @ [parens (string "Zwf_well_founded _ _")]
+                        main_call @ [parens (string "Zwf_guarded _")]
                      | _ ->  main_call
               in hang 2 (flow (break 1) all) in
 
@@ -1383,7 +1440,11 @@ let doc_exp, doc_let =
          if effects then
            if inner_ex then
              if cast_ex
-             then string "derive_m" ^^ space ^^ epp
+             (* If the types are the same use the cast as a hint to Coq,
+                otherwise derive the new type from the old one. *)
+             then if alpha_equivalent env inner_typ cast_typ
+                  then epp
+                  else string "derive_m" ^^ space ^^ epp
              else string "projT1_m" ^^ space ^^ epp
            else if cast_ex
            then string "build_ex_m" ^^ space ^^ epp
@@ -1409,7 +1470,7 @@ let doc_exp, doc_let =
        in
        if aexp_needed then parens epp else epp
     | E_tuple exps ->
-       parens (align (group (separate_map (comma ^^ break 1) expN exps)))
+       construct_dep_pairs (env_of_annot (l,annot)) true full_exp (general_typ_of full_exp)
     | E_record fexps ->
        let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 0a1b38f9..1b91bb5d 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1270,10 +1270,6 @@ let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) arg_typs =
   | _, _ ->
      [pat], identity
 
-let doc_rec_lem force_rec (Rec_aux(r,_)) = match r with
-  | Rec_nonrec when not force_rec -> space
-  | _ -> space ^^ string "rec" ^^ space
-
 let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
   | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem typ)
   | Typ_annot_opt_none -> empty
@@ -1327,9 +1323,19 @@ let doc_mutrec_lem = function
 let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
-  | FCL_aux (FCL_Funcl(id,_),annot) :: _
-    when not (Env.is_extern id (env_of_annot annot) "lem") ->
-    string "let" ^^ (doc_rec_lem (List.length fcls > 1) r) ^^ (doc_fundef_rhs_lem fd)
+  | FCL_aux (FCL_Funcl(id, pexp),annot) :: _
+     when not (Env.is_extern id (env_of_annot annot) "lem") ->
+    (* Output "rec" modifier if function calls itself.  Mutually recursive
+       functions are handled separately by doc_mutrec_lem. *)
+    let is_funcl_rec =
+      fold_pexp
+        { (pure_exp_alg false (||)) with
+          e_app = (fun (id', args) -> List.fold_left (||) (Id.compare id id' = 0) args);
+          e_app_infix = (fun (l, id', r) -> l || (Id.compare id id' = 0) || r) }
+        pexp
+    in
+    let doc_rec = if is_funcl_rec then [string "rec"] else [] in
+    separate space ([string "let"] @ doc_rec @ [doc_fundef_rhs_lem fd])
   | _ -> empty
 
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index becdccc0..5430b284 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -669,6 +669,9 @@ let rec doc_def def = group (match def with
      ^^ hardline ^^ string "}"
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> doc_scattered sdef
+  | DEF_measure (id,pat,exp) ->
+     string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^
+       space ^^ equals ^/^ doc_exp exp
   | DEF_pragma (pragma, arg, l) ->
      string ("$" ^ pragma ^ " " ^ arg)
   | DEF_fixity (prec, n, id) ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 03c0e074..81fa7c29 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -363,15 +363,13 @@ let rewrite_def rewriters d = match d with
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
   | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l)
-  | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter")
+  | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
+  | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp)
 
 let rewrite_defs_base rewriters (Defs defs) =
-  let rec rewrite = function
+  let rec rewrite ds = match ds with
     | [] -> []
-    | d :: ds ->
-       let d = rewriters.rewrite_def rewriters d in
-       d :: rewrite ds
-  in
+    | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in
   Defs (rewrite defs)
 
 let rewrite_defs_base_progress prefix rewriters (Defs defs) =
diff --git a/src/rewrites.ml b/src/rewrites.ml
index be02a63f..1ca39998 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4802,6 +4802,35 @@ let minimise_recursive_functions (Defs defs) =
     | d -> d
   in Defs (List.map rewrite_def defs)
 
+let move_termination_measures (Defs defs) =
+  let scan_for id defs =
+    let rec aux = function
+      | [] -> None
+      | (DEF_measure (id',pat,exp))::t ->
+         if Id.compare id id' == 0 then Some (pat,exp) else aux t
+      | (DEF_fundef (FD_aux (FD_function (_,_,_,FCL_aux (FCL_Funcl (id',_),_)::_),_)))::_
+      | (DEF_spec (VS_aux (VS_val_spec (_,id',_,_),_))::_)
+        when Id.compare id id' == 0 -> None
+      | _::t -> aux t
+    in aux defs
+  in
+  let rec aux acc = function
+    | [] -> List.rev acc
+    | (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann))) as d)::t -> begin
+       let id = match fs with
+         | [] -> assert false (* TODO *)
+         | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id
+       in
+       match scan_for id t with
+       | None -> aux (d::acc) t
+       | Some (pat,exp) ->
+          let r = Rec_aux (Rec_measure (pat,exp), Generated l) in
+          aux (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann)))::acc) t
+      end
+    | (DEF_measure _)::t -> aux acc t
+    | h::t -> aux (h::acc) t
+  in Defs (aux [] defs)
+
 (* Make recursive functions with a measure use the measure as an
    explicit recursion limit, enforced by an assertion. *)
 let rewrite_explicit_measure (Defs defs) =
@@ -4845,8 +4874,8 @@ let rewrite_explicit_measure (Defs defs) =
     | exception Not_found -> [vs]
   in
   (* Add extra argument and assertion to each funcl, and rewrite recursive calls *)
-  let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),ann) as fcl) =
-    let loc = Parse_ast.Generated (fst ann) in
+  let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann) as fcl) =
+    let loc = Parse_ast.Generated (fst fcl_ann) in
     let P_aux (pat,pann),guard,body,ann = destruct_pexp pexp in
     let extra_pat = P_aux (P_id limit,(loc,empty_tannot)) in
     let pat = match pat with
@@ -4878,7 +4907,7 @@ let rewrite_explicit_measure (Defs defs) =
         } body
     in
     let body = E_aux (E_block [assert_exp; body],(loc,empty_tannot)) in
-    FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),ann)
+    FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),fcl_ann)
   in
   let rewrite_function (FD_aux (FD_function (r,t,e,fcls),ann) as fd) =
     let loc = Parse_ast.Generated (fst ann) in
@@ -4920,6 +4949,7 @@ let rewrite_explicit_measure (Defs defs) =
              | [wpat] -> wpat
              | _ -> P_aux (P_tup wpats,(loc,empty_tannot))
            in
+           let measure_exp = E_aux (E_cast (int_typ, measure_exp),(loc,empty_tannot)) in
            let wbody = E_aux (E_app (rec_id id,wexps@[measure_exp]),(loc,empty_tannot)) in
            let wrapper =
              FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (wpat,wbody),(loc,empty_tannot))),(loc,empty_tannot))
@@ -5068,10 +5098,15 @@ let rewrite_defs_coq = [
   ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   (* ("constraint", rewrite_constraint); *)
   (* ("remove_assert", rewrite_defs_remove_assert); *)
+  ("move_termination_measures", move_termination_measures);
   ("top_sort_defs", top_sort_defs);
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
+  (* merge funcls before adding the measure argument so that it doesn't
+     disappear into an internal pattern match *)
+  ("merge function clauses", merge_funcls);
+  ("recheck_defs_without_effects", recheck_defs_without_effects);
   ("make_cases_exhaustive", MakeExhaustive.rewrite);
   ("rewrite_explicit_measure", rewrite_explicit_measure);
   ("recheck_defs_without_effects", recheck_defs_without_effects);
@@ -5082,7 +5117,6 @@ let rewrite_defs_coq = [
   ("internal_lets", rewrite_defs_internal_lets);
   ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
   ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns);
-  ("merge function clauses", merge_funcls);
   ("recheck_defs", recheck_defs)
   ]
 
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index e57b1988..634b34b6 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -352,9 +352,10 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_)
     | [] -> failwith "fv_of_fun fell off the end looking for the function name"
     | FCL_aux(FCL_Funcl(id,_),_)::_ -> string_of_id id in
   let base_bounds = match rec_opt with
-    (* Current Sail does not have syntax for declaring functions as recursive,
+    (* Current Sail does not require syntax for declaring functions as recursive,
        and type checker does not check whether functions are recursive, so
-       just always add a self-dependency of functions on themselves
+       just always add a self-dependency of functions on themselves, as well as
+       adding dependencies from any specified termination measure further below
     | Rec_aux(Ast.Rec_rec,_) -> init_env fun_name
     | _ -> mt*)
     | _ -> init_env fun_name in
@@ -365,6 +366,13 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_)
       bound, fv_of_typ consider_var bound mt typ
     | Typ_annot_opt_aux(Typ_annot_opt_none, _) ->
       base_bounds, mt in
+  let ns_measure = match rec_opt with
+    | Rec_aux(Rec_measure (pat,exp),_) ->
+       let pat_bs,pat_ns = pat_bindings consider_var base_bounds mt pat in
+       let _, exp_ns,_ = fv_of_exp consider_var pat_bs pat_ns Nameset.empty exp in
+       exp_ns
+    | _ -> mt
+  in
   let ns = List.fold_right (fun (FCL_aux(FCL_Funcl(_,pexp),_)) ns ->
     match pexp with
     | Pat_aux(Pat_exp (pat,exp),_) ->
@@ -379,7 +387,7 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_)
   ) funcls mt in
   let ns_vs = init_env ("val:" ^ (string_of_id (id_of_fundef fd))) in
   (* let _ = Printf.eprintf "Function %s uses %s\n" fun_name (set_to_string (Nameset.union ns ns_r)) in *)
-  init_env fun_name, Nameset.union ns_vs (Nameset.union ns ns_r)
+  init_env fun_name, Nameset.union ns_vs (Nameset.union ns (Nameset.union ns_r ns_measure))
 
 let fv_of_vspec consider_var (VS_aux(vspec,_)) = match vspec with
   | VS_val_spec(ts,id,_,_) ->
@@ -494,6 +502,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
   | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
   | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
   | DEF_pragma _ -> mt,mt
+  | DEF_measure _ -> mt,mt (* currently removed beforehand *)
 
 let group_defs consider_scatter_as_one (Ast.Defs defs) =
   List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs
diff --git a/src/type_check.ml b/src/type_check.ml
index 7746ffee..9ece1e25 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4307,6 +4307,22 @@ let check_tannotopt env typq ret_typ = function
      then ()
      else typ_error env l (string_of_bind (typq, ret_typ) ^ " and " ^ string_of_bind (annot_typq, annot_ret_typ) ^ " do not match between function and val spec")
 
+let check_termination_measure env arg_typs pat exp =
+  let typ = match arg_typs with [x] -> x | _ -> Typ_aux (Typ_tup arg_typs,Unknown) in
+  let tpat, env = bind_pat_no_guard env (strip_pat pat) typ in
+  let texp = check_exp env (strip_exp exp) int_typ in
+  tpat, texp
+
+let check_termination_measure_decl env (id, pat, exp) =
+  let quant, typ = Env.get_val_spec id env in
+  let arg_typs, l = match typ with
+    | Typ_aux (Typ_fn (arg_typs, _ ,_),l) -> arg_typs,l
+    | _ -> typ_error env (id_loc id) "Function val spec is not a function type"
+  in
+  let env = add_typquant l quant env in
+  let tpat, texp = check_termination_measure env arg_typs pat exp in
+  DEF_measure (id, tpat, texp)
+
 let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux) =
   let id =
     match (List.fold_right
@@ -4339,9 +4355,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
     | Rec_aux (Rec_nonrec, l) -> Rec_aux (Rec_nonrec, l)
     | Rec_aux (Rec_rec, l) -> Rec_aux (Rec_rec, l)
     | Rec_aux (Rec_measure (measure_p, measure_e), l) ->
-       let typ = match vtyp_args with [x] -> x | _ -> Typ_aux (Typ_tup vtyp_args,Unknown) in
-       let tpat, env = bind_pat_no_guard funcl_env (strip_pat measure_p) typ in
-       let texp = check_exp env (strip_exp measure_e) int_typ in
+       let tpat, texp = check_termination_measure funcl_env vtyp_args measure_p measure_e in
        Rec_aux (Rec_measure (tpat, texp), l)
   in
   let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
@@ -4579,6 +4593,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
   | DEF_scattered sdef -> check_scattered env sdef
+  | DEF_measure (id, pat, exp) -> [check_termination_measure_decl env (id, pat, exp)], env
 
 and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t =
   fun n total env defs ->