Avoid nested explicit type annotations

Isabelle does not like nested annotations like "((exp :: typ) :: typ)".

4 files changed, 27 insertions, 19 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 730cf4a8..38862382 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -449,8 +449,8 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
   | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
      (* Isabelle does not seem to like type-annotated tuple patterns;
         it gives a syntax error. Avoid this by annotating the tuple elements instead *)
-     let doc_elem typ (P_aux (_, annot) as pat) =
-       doc_pat_lem ctxt true (P_aux (P_typ (typ, pat), annot)) in
+     let doc_elem typ pat =
+       doc_pat_lem ctxt true (add_p_typ typ pat) in
      parens (separate comma_sp (List.map2 doc_elem typs pats))
   | P_typ(typ,p) ->
     let doc_p = doc_pat_lem ctxt true p in
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 539ba0c8..519828b7 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -82,6 +82,29 @@ let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
 
 let simple_annot l typ = (gen_loc l, Some (initial_env, typ, no_effect))
 
+
+let lookup_generated_kid env kid =
+  let match_kid_nc kid = function
+    | NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _)
+      when Kid.compare kid kid2 = 0 && not (is_kid_generated kid1) -> kid1
+    | _ -> kid
+  in
+  List.fold_left match_kid_nc kid (Env.get_constraints env)
+
+let rec remove_p_typ = function
+  | P_aux (P_typ (typ, pat), _) -> remove_p_typ pat
+  | pat -> pat
+
+let add_p_typ typ (P_aux (paux, annot) as pat) =
+  let env = pat_env_of pat in
+  let generated_kids typ = KidSet.filter is_kid_generated (tyvars_of_typ typ) in
+  let subst_kid kid typ = typ_subst_kid kid (lookup_generated_kid env kid) typ in
+  let typ' = KidSet.fold subst_kid (generated_kids typ) typ in
+  if KidSet.is_empty (generated_kids typ') then
+    P_aux (P_typ (typ', remove_p_typ pat), annot)
+  else pat
+
+
 let rec small (E_aux (exp,_)) = match exp with
   | E_id _
   | E_lit _ -> true
diff --git a/src/rewriter.mli b/src/rewriter.mli
index b830bdeb..08241a4b 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -204,6 +204,8 @@ val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
 
 val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot
 
+val add_p_typ : typ -> tannot pat -> tannot pat
+
 val union_eff_exps : (tannot exp) list -> effect
 
 val fix_eff_exp : tannot exp -> tannot exp
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e3f9a93e..9cba6b39 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -103,23 +103,6 @@ let effectful_effs = function
        | _ -> true
       ) effs
 
-
-let lookup_generated_kid env kid =
-  let match_kid_nc kid = function
-    | NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _)
-      when Kid.compare kid kid2 = 0 && not (is_kid_generated kid1) -> kid1
-    | _ -> kid
-  in
-  List.fold_left match_kid_nc kid (Env.get_constraints env)
-
-let add_p_typ typ (P_aux (paux, annot) as pat) =
-  let env = pat_env_of pat in
-  let generated_kids typ = KidSet.filter is_kid_generated (tyvars_of_typ typ) in
-  let subst_kid kid typ = typ_subst_kid kid (lookup_generated_kid env kid) typ in
-  let typ' = KidSet.fold subst_kid (generated_kids typ) typ in
-  if KidSet.is_empty (generated_kids typ') then P_aux (P_typ (typ', pat), annot) else pat
-
-
 let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
 let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))