Adapt Coq and termination measure support to typechecker changes

Also output termination measures in Sail printer

4 files changed, 27 insertions, 18 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 053020db..18e288dd 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -692,7 +692,7 @@ let is_ctor env id = match Env.lookup_id id env with
 
 let is_auto_decomposed_exist env typ =
   let typ = expand_range_type typ in
-  match destruct_exist (Env.expand_synonyms env typ) with
+  match destruct_exist_plain (Env.expand_synonyms env typ) with
   | Some (_, _, typ') -> Some typ'
   | _ -> None
 
@@ -935,7 +935,7 @@ let doc_exp, doc_let =
         debug ctxt (lazy (" at type " ^ string_of_typ typ))
       in
       let typ = expand_range_type typ in
-      match destruct_exist typ with
+      match destruct_exist_plain typ with
       | None -> epp
       | Some _ ->
          let epp = string "build_ex" ^/^ epp in
@@ -951,12 +951,12 @@ let doc_exp, doc_let =
         | _ ->
            let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in
            let build_ex, out_typ =
-             match destruct_exist typ' with
+             match destruct_exist_plain typ' with
              | Some (_,_,t) -> true, t
              | None -> false, typ'
            in
            let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in
-           let in_typ = match destruct_exist in_typ with Some (_,_,t) -> t | None -> in_typ in
+           let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in
            let autocast =
              (* Avoid using helper functions which simplify the nexps *)
              is_bitvector_typ in_typ && is_bitvector_typ out_typ &&
@@ -1569,7 +1569,7 @@ let doc_exp, doc_let =
                 | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_)
                     when not (is_enum (env_of e1) id) ->
                       let full_typ = (expand_range_type typ) in
-                      let binder = match destruct_exist (Env.expand_synonyms (env_of e1) full_typ) with
+                      let binder = match destruct_exist_plain (Env.expand_synonyms (env_of e1) full_typ) with
                         | Some _ ->
                            squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
                         | _ ->
@@ -2039,7 +2039,7 @@ let doc_funcl rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | _ -> 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 destruct_exist (Env.expand_synonyms env (expand_range_type ret_typ)) with
+  let build_ex = match destruct_exist_plain (Env.expand_synonyms env (expand_range_type ret_typ)) with
     | Some _ -> true
     | _ -> build_ex
   in
@@ -2097,7 +2097,7 @@ let doc_funcl rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
          parens (separate space [doc_id id; colon; doc_typ ctxt typ])
        else begin
            let full_typ = (expand_range_type exp_typ) in
-           match destruct_exist (Env.expand_synonyms env full_typ) with
+           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",_),
                                      [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_))
@@ -2131,7 +2131,7 @@ let doc_funcl rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
          Util.map_filter (fun (pat,typ) ->
              match pat_is_plain_binder env pat with
              | Some id -> begin
-                 match destruct_exist (Env.expand_synonyms env (expand_range_type typ)) with
+                 match destruct_exist_plain (Env.expand_synonyms env (expand_range_type typ)) with
                  | Some (_, NC_aux (NC_true,_), _) -> None
                  | Some ([KOpt_aux (KOpt_kind (_, kid), _)], nc,
                          Typ_aux (Typ_app (Id_aux (Id "atom",_),
@@ -2143,7 +2143,7 @@ let doc_funcl rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
              | None -> None) pats
        in
        string "Fixpoint",
-       [parens (string "_acc : Acc (Zwf 0) _rec_limit")],
+       [parens (string "_acc : Acc (Zwf 0) _reclimit")],
        [string "{struct _acc}"],
        fixupspp
     | Rec_aux (r,_) ->
@@ -2343,7 +2343,7 @@ let doc_val pat exp =
     | None -> typpp, exp
     | Some typ ->
        let typ = expand_range_type (Env.expand_synonyms env typ) in
-       match destruct_exist typ with
+       match destruct_exist_plain typ with
        | None -> typpp, exp
        | Some _ ->
           empty, match exp with
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index c4b9bdd3..345312f7 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -509,14 +509,21 @@ let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) =
 
 let doc_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord]
 
+let doc_rec (Rec_aux (r,_)) =
+  match r with
+  | Rec_nonrec
+  | Rec_rec -> empty
+  | Rec_measure (pat,exp) -> braces (doc_pat pat ^^ string " => " ^^ doc_exp exp) ^^ space
+
 let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), annot)) =
   docstring annot
   ^^ match funcls with
      | [] -> failwith "Empty function list"
      | _ ->
+        let rec_pp = doc_rec r in
         let sep = hardline ^^ string "and" ^^ space in
         let clauses = separate_map sep doc_funcl funcls in
-        string "function" ^^ space ^^ clauses
+        string "function" ^^ space ^^ rec_pp ^^ clauses
 
 let rec doc_mpat (MP_aux (mp_aux, _) as mpat) =
   match mp_aux with
diff --git a/src/type_check.ml b/src/type_check.ml
index 8b6a9c45..53d87a05 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -221,7 +221,7 @@ let fresh_existential ?name:(n="") k =
   let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter ^ "#" ^ n), Parse_ast.Unknown) in
   incr ex_counter; mk_kopt k fresh
 
-let destruct_exist' typ =
+let destruct_exist_plain typ =
   match typ with
   | Typ_aux (Typ_exist (kopts, nc, typ), _) ->
      let fresh_kopts =
@@ -243,7 +243,7 @@ let destruct_exist' typ =
    - atom('n) => [], true, 'n
 **)
 let destruct_numeric typ =
-  match destruct_exist' typ, typ with
+  match destruct_exist_plain typ, typ with
   | Some (kids, nc, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _)), _ when string_of_id id = "atom" ->
      Some (List.map kopt_kid kids, nc, nexp)
   | None, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _) when string_of_id id = "atom" ->
@@ -262,7 +262,7 @@ let destruct_numeric typ =
 let destruct_exist typ =
   match destruct_numeric typ with
   | Some (kids, nc, nexp) -> Some (List.map (mk_kopt K_int) kids, nc, atom_typ nexp)
-  | None -> destruct_exist' typ
+  | None -> destruct_exist_plain typ
 
 let adding = Util.("Adding " |> darkgray |> clear)
 
@@ -1736,7 +1736,7 @@ let rec subtyp l env typ1 typ2 =
      if prove env nc2 then ()
      else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
   | _, _ ->
-  match destruct_exist' typ1, destruct_exist (canonicalize env typ2) with
+  match destruct_exist_plain typ1, destruct_exist (canonicalize env typ2) with
   | Some (kopts, nc, typ1), _ ->
      let env = add_existential l kopts nc env in subtyp l env typ1 typ2
   | None, Some (kopts, nc, typ2) ->
@@ -4184,17 +4184,17 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
   in
   check_tannotopt env quant vtyp_ret tannotopt;
   typ_debug (lazy ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)));
+  let funcl_env = add_typquant l quant env in
   let recopt =
     match recopt with
     | 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 env (strip_pat measure_p) typ 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
        Rec_aux (Rec_measure (tpat, texp), l)
   in
-  let funcl_env = add_typquant l quant env in
   let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
   let eff = List.fold_left union_effects no_effect (List.map funcl_effect funcls) in
   let vs_def, env, declared_eff =
diff --git a/src/type_check.mli b/src/type_check.mli
index 04ff48f7..81682606 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -210,7 +210,9 @@ val add_typquant : Ast.l -> typquant -> Env.t -> Env.t
 
 (** Safely destructure an existential type. Returns None if the type
    is not existential. This function will pick a fresh name for the
-   existential to ensure that no name-clashes occur. *)
+   existential to ensure that no name-clashes occur. The "plain"
+   version does not treat numeric types as existentials. *)
+val destruct_exist_plain : typ -> (kinded_id list * n_constraint * typ) option
 val destruct_exist : typ -> (kinded_id list * n_constraint * typ) option
 
 val add_existential : Ast.l -> kinded_id list -> n_constraint -> Env.t -> Env.t