@@ -390,6 +390,41 @@ and translate_pair exp =
390
390
391
391
let mk desc = { desc; ty = () ; bv = StringSet. empty; fail = false }
392
392
393
+ let deconstruct_pat env pat =
394
+ let rec deconstruct_pat_aux acc indexes = function
395
+ | { ppat_desc = Ppat_constraint (pat , ty ) } ->
396
+ let acc, _ = deconstruct_pat_aux acc indexes pat in
397
+ acc, translate_type env ty
398
+
399
+ | { ppat_desc = Ppat_var { txt = var ; loc } } ->
400
+ (var, loc_of_loc loc, indexes) :: acc, Tunit (* Dummy type value *)
401
+
402
+ | { ppat_desc = Ppat_any ; ppat_loc } ->
403
+ (" _" , loc_of_loc ppat_loc, indexes) :: acc, Tunit (* Dummy type value *)
404
+
405
+ | { ppat_desc = Ppat_tuple pats } ->
406
+ let _, acc, tys =
407
+ List. fold_left (fun (i , acc , tys ) pat ->
408
+ let acc, ty = deconstruct_pat_aux acc (i :: indexes) pat in
409
+ i + 1 , acc, ty :: tys
410
+ ) (0 , acc, [] ) pats
411
+ in
412
+ acc, Ttuple (List. rev tys)
413
+
414
+ | { ppat_loc } ->
415
+ error_loc ppat_loc " cannot deconstruct this pattern"
416
+ in
417
+ deconstruct_pat_aux [] [] pat
418
+
419
+ let access_of_deconstruct var_name loc indexes =
420
+ let a = mk (Var (var_name, loc, [] )) in
421
+ List. fold_right (fun i a ->
422
+ mk (Apply (Prim_tuple_get , loc, [
423
+ a;
424
+ mk (Const (Tnat , CNat (LiquidPrinter. integer_of_int i)))
425
+ ]))
426
+ ) indexes a
427
+
393
428
let rec translate_code env exp =
394
429
let desc =
395
430
match exp with
@@ -463,16 +498,27 @@ let rec translate_code env exp =
463
498
translate_code env arg_exp,
464
499
translate_code env body)
465
500
466
- | { pexp_desc = Pexp_let (Nonrecursive ,
467
- [
468
- {
469
- pvb_pat = { ppat_desc =
470
- Ppat_var { txt = var; loc } };
471
- pvb_expr = var_exp;
472
- }
473
- ], body) } ->
474
- Let (var, loc_of_loc loc,
475
- translate_code env var_exp, translate_code env body)
501
+ | { pexp_desc = Pexp_let (Nonrecursive , [ {
502
+ pvb_pat = pat;
503
+ pvb_expr = var_exp;
504
+ } ], body); pexp_loc } ->
505
+
506
+ let vars_infos, _ = deconstruct_pat env pat in
507
+ let exp, body = translate_code env var_exp, translate_code env body in
508
+ begin match vars_infos with
509
+ | [] -> assert false
510
+ | [v, loc, []] -> Let (v, loc, exp, body)
511
+ | _ ->
512
+ let var_name =
513
+ String. concat " _" (List. rev_map (fun (v ,_ ,_ ) -> v) vars_infos) in
514
+ let lets_body =
515
+ List. fold_left (fun e (v , loc , indexes ) ->
516
+ let access = access_of_deconstruct var_name loc indexes in
517
+ mk (Let (v, loc, access, e))
518
+ ) body vars_infos
519
+ in
520
+ Let (var_name, loc_of_loc pexp_loc, exp, lets_body)
521
+ end
476
522
477
523
| { pexp_desc = Pexp_sequence (exp1 , exp2 ) } ->
478
524
Seq (translate_code env exp1, translate_code env exp2)
@@ -529,21 +575,28 @@ let rec translate_code env exp =
529
575
MatchVariant (e, loc_of_loc pexp_loc, args)
530
576
end
531
577
532
- | { pexp_desc =
533
- Pexp_fun (
534
- Nolabel , None ,
535
- { ppat_desc =
536
- Ppat_constraint (
537
- { ppat_desc =
538
- Ppat_var { txt = arg_name } },
539
- arg_type)
540
- },
541
- body_exp) } ->
578
+ | { pexp_desc = Pexp_fun (Nolabel, None, pat , body_exp ) } ->
542
579
let body_exp = translate_code env body_exp in
543
- let arg_type = translate_type env arg_type in
544
- Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc,
545
- body_exp,
546
- Tunit ) (* not yet inferred *)
580
+ let vars_infos, arg_type = deconstruct_pat env pat in
581
+ begin match vars_infos with
582
+ | [] -> assert false
583
+ | [arg_name, loc, []] ->
584
+ Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc,
585
+ body_exp,
586
+ Tunit ) (* not yet inferred *)
587
+ | _ ->
588
+ let arg_name =
589
+ String. concat " _" (List. rev_map (fun (v ,_ ,_ ) -> v) vars_infos) in
590
+ let lets_body =
591
+ List. fold_left (fun e (v , loc , indexes ) ->
592
+ let access = access_of_deconstruct arg_name loc indexes in
593
+ mk (Let (v, loc, access, e))
594
+ ) body_exp vars_infos
595
+ in
596
+ Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc,
597
+ lets_body,
598
+ Tunit ) (* not yet inferred *)
599
+ end
547
600
548
601
| { pexp_desc = Pexp_record (lab_x_exp_list , None) } ->
549
602
let lab_x_exp_list =
0 commit comments