Code extraction: better printing of record creation.

Theory seq.OfList: refactoring

src/mlw/ocaml_printer.ml

@@ -277,7 +277,8 @@ module Print = struct
         fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
           (print_list comma (print_expr info)) tl
       | pjl, tl ->
-        fprintf fmt "@[<hov 2>{ %a }@]"
+        let equal fmt () = fprintf fmt " = " in
+        fprintf fmt "@[<hov 2>{ @[%a@] }@]"
           (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
       end
     | _, None, [] ->
@@ -347,7 +348,7 @@ module Print = struct
       fprintf fmt (protect_on paren "%a")
         (print_apply info (Hrs.find_def ht_rs rs rs)) pvl end
     | Ematch (e, pl) ->
-      fprintf fmt (protect_on paren "begin match @[%a@] with@\n@[%a@] end")
+      fprintf fmt (protect_on paren "begin match @[%a@] with@\n@[%a@]@\nend")
         (print_expr info) e (print_list newline (print_branch info)) pl
     | Eassign al ->
       let assign fmt (rho, rs, pv) =
@@ -408,7 +409,7 @@ module Print = struct
     (* | Ecast _ -> (\* TODO *\) assert false *)
 
   and print_branch info fmt (p, e) =
-    fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]"
+    fprintf fmt "@[<hov 2>| %a ->@ @[%a@]@]"
       (print_pat info) p (print_expr info) e
 
   and print_raise ~paren info xs fmt e_opt =

theories/seq.why

@@ -173,34 +173,41 @@ end
 theory OfList
   use import int.Int
   use import option.Option
-  use import Seq
   use import list.List
   use import list.Length as L
   use import list.Nth
+  use import Seq
   use import list.Append
 
-  function of_list (l: list 'a) : seq 'a = match l with
+  let rec function of_list (l: list 'a) : seq 'a = match l with
     | Nil -> empty
     | Cons x r -> cons x (of_list r)
     end
-  meta coercion function of_list
 
   lemma length_of_list:
-    forall l: list 'a. length l = L.length l
+    forall l: list 'a. length (of_list l) = L.length l
+
+  predicate point_wise (s: seq 'a) (l: list 'a) =
+    forall i. 0 <= i < L.length l -> Some (get s i) = nth i l
 
   lemma elts_seq_of_list: forall l: list 'a.
-    forall i. 0 <= i < length l -> Some (get l i) = nth i l
+    point_wise (of_list l) l
+
+  lemma is_of_list: forall l: list 'a, s: seq 'a.
+    L.length l = length s -> point_wise s l -> s == of_list l
 
   let rec lemma of_list_app (l1 l2: list 'a)
-    ensures { l1 ++ l2 == Seq.(++) l1 l2 }
+    ensures { of_list (l1 ++ l2) == Seq.(++) (of_list l1) (of_list l2) }
     variant { l1 }
   = match l1 with
     | Nil -> ()
     | Cons _ r -> of_list_app r l2
     end
 
-  lemma of_list_app_length:
-    forall l1 l2: list 'a. length (l1 ++ l2) = length l1 + length l2
+  lemma of_list_app_length: forall l1"induction" l2: list 'a.
+    length (of_list (l1 ++ l2)) = L.length l1 + L.length l2
+
+  meta coercion function of_list
 
 end