From dfd6d278deb29e5fd39e3246a52bb0999451a47c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 19 Dec 2017 11:28:48 +0000
Subject: Fix a bug in untupling function arguments for Lem

Was missing the case where the tuple of arguments is bound against a single
variable using P_id (not P_as).  Now replaces that with the expected number of
argument variables, and rebinds the single variable in the body, as for the
other cases.
---
 src/pretty_print_lem.ml | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index b0b76ac1..96f312fb 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1222,30 +1222,25 @@ let args_of_typ l env typ =
 
 let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) =
   let env = env_of_annot annot in
-  let id = (fun body -> body) in
-  match paux with
-  | P_tup [] ->
+  let (Typ_aux (taux, _)) = typ_of_annot annot in
+  let identity = (fun body -> body) in
+  match paux, taux with
+  | P_tup [], _ ->
      let annot = (l, Some (Env.empty, unit_typ, no_effect)) in
-     [P_aux (P_lit (mk_lit L_unit), annot)], id
-  | P_tup pats -> pats, id
-  | P_wild ->
-     begin
-       match pat_typ_of pat with
-       | Typ_aux (Typ_tup typs, _) ->
-          let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in
-          List.map wild typs, id
-       | _ -> [pat], id
-     end
-  | P_lit _ | P_id _ | P_var _ | P_app _ | P_record _
-  | P_vector _ | P_vector_concat _ | P_list _ | P_cons _ ->
-     [pat], id
-  | P_typ (_, pat) -> untuple_args_pat pat
-  | P_as _ ->
+     [P_aux (P_lit (mk_lit L_unit), annot)], identity
+  | P_tup pats, _ -> pats, identity
+  | P_wild, Typ_tup typs ->
+     let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in
+     List.map wild typs, identity
+  | P_typ (_, pat), _ -> untuple_args_pat pat
+  | P_as _, Typ_tup _ | P_id _, Typ_tup _ ->
      let argpats, argexps = args_of_typ l env (pat_typ_of pat) in
      let argexp = E_aux (E_tuple argexps, annot) in
      let bindargs (E_aux (_, bannot) as body) =
        E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
      argpats, bindargs
+  | _, _ ->
+     [pat], identity
 
 let doc_rec_lem (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> space
-- 
cgit v1.2.3