Code extraction: assertions and absurd

src/mlw/compile.ml

@@ -49,9 +49,13 @@
     - est-ce qu'il y a des utilisations particulières du champ
       [itd_fields], vis-à-vis du champ [itd_constructors] ?
 
-    - comme l'AST [expr] est déjà en forme normale-A, est-ce que je
-      peux utiliser des applications de la forme [Eapp ident * ident list] ?
+    - comme l'AST [expr] est déjà en forme normale-A, est-ce que ça
+      fait du sense pour vous d'utiliser des applications de la forme
+      [Eapp of ident * ident list] ?
+ *)
 
+(*
+  TODO: réfléchir sur l'affectation parallèle
 *)
 
 
@@ -91,7 +95,7 @@ module ML = struct
     | Xsyntax of string
     | Xexit             (* Pervasives.Exit *)
 
-  type ity = I of Ity.ity | C of Ity.cty (* TODO: keep like this? *)
+  type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
 
   type expr = {
     e_node   : expr_node;
@@ -144,6 +148,11 @@ module ML = struct
 
   let tunit = Ttuple []
 
+  let enope = Eblock []
+
+  let mk_unit =
+    mk_expr enope (I Ity.ity_unit) Ity.eff_empty
+
 end
 
 (** Translation from Mlw to ML *)
@@ -214,24 +223,30 @@ module Translate = struct
     List.map pvty
 
   (* expressions *)
-  let rec expr e =
+  let rec expr ({e_effect = eff } as e) =
+    assert (not eff.eff_ghost);
     match e.e_node with
+    | Econst c ->
+       let c = match c with Number.ConstInt c -> c | _ -> assert false in
+       ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff
     | Evar pvs ->
        let pv_id = pv_name pvs in
-       ML.mk_expr (ML.Eident pv_id) (ML.I e.e_ity) e.e_effect
+       ML.mk_expr (ML.Eident pv_id) (ML.I e.e_ity) eff
     | Elet (LDvar (pvs, e1), e2) ->
        let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in
-       ML.mk_expr ml_let (ML.I e.e_ity) e.e_effect
+       ML.mk_expr ml_let (ML.I e.e_ity) eff
     | Eexec ({c_node = Capp (rs, pvl)}, _) ->
        let rs_id = rs.rs_name in
        let pv_id = List.map pv_name pvl in
-       ML.mk_expr (ML.Eapp (rs_id, pv_id)) (ML.I e.e_ity) e.e_effect
+       ML.mk_expr (ML.Eapp (rs_id, pv_id)) (ML.I e.e_ity) eff
     | Eabsurd ->
-       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) e.e_effect
+       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
     | Ecase (e1, pl) ->
        let e1 = expr e1 in
        let pl = List.map ebranch pl in
-       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) e.e_effect
+       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
+    | Eassert _ ->
+       ML.mk_unit
     | _ -> (* TODO *) assert false
 
   and ebranch ({pp_pat = p}, e) =

src/mlw/ocaml_printer.ml

@@ -122,7 +122,30 @@ module Print = struct
        in
        fprintf fmt "{ %a }" (print_list semi print_field) fl
 
+  let print_const fmt c =
+    let n = Number.compute_int c in
+    let m = BigInt.to_int n in
+    fprintf fmt "%d" m
+
+  (** Expressions *)
+
+  let extract_op {id_string = s} =
+    try Some (Strings.remove_prefix "infix " s) with Not_found ->
+    try Some (Strings.remove_prefix "prefix " s) with Not_found ->
+    None
+
+  let print_apply fmt s vl =
+    match extract_op s, vl with
+    | Some o, [t1; t2] ->
+       fprintf fmt "@[<hov 1>%a %s %a@]"
+         print_ident t1 o print_ident t2
+    | _, tl ->
+       fprintf fmt "@[<hov 2>%a %a@]"
+         print_ident s (print_list space print_ident) tl
+
   let rec print_enode fmt = function
+    | Econst c ->
+       fprintf fmt "%a" print_const c
     | Eident id ->
        print_ident fmt id
     | Elet (id, e1, e2) ->
@@ -130,12 +153,13 @@ module Print = struct
          print_ident id print_expr e1 print_expr e2
     | Eabsurd ->
        fprintf fmt "assert false (* absurd *)"
-    | Eapp (e, el) ->
-       fprintf fmt "@[<hov 2>%a %a@]"
-         print_ident e (print_list space print_ident) el
+    | Eapp (s, vl) ->
+       print_apply fmt s vl
     | Ematch (e, pl) ->
        fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
          print_expr e (print_list newline print_branch) pl
+    | Eblock [] ->
+       fprintf fmt "()"
     | _ -> (* TODO *) assert false
 
   and print_branch fmt (p, e) =
@@ -154,8 +178,7 @@ module Print = struct
       | l ->
          fprintf fmt "@[<hov 4>| %a of %a@]"
                  print_ident id (* FIXME: print_uident *)
-                 (print_list star (print_ty ~paren:false)) l
-    in
+                 (print_list star (print_ty ~paren:false)) l in
     let print_field fmt (is_mutable, id, ty) =
       fprintf fmt "%s%a: %a;"
               (if is_mutable then "mutable " else "")
@@ -170,8 +193,7 @@ module Print = struct
       | Drecord fl ->
          fprintf fmt " = {@\n%a@\n}" (print_list newline print_field) fl
       | Dalias ty ->
-         fprintf fmt " =@ %a" (print_ty ~paren:false) ty
-    in
+         fprintf fmt " =@ %a" (print_ty ~paren:false) ty in
     fprintf fmt "@[<hov 2>%s %a%a%a@]"
             (if true then "type" else "and") (* FIXME: mutual recursive types *)
             print_tv_args args

src/whyml/mlw_ocaml.ml

@@ -513,7 +513,7 @@ module Translate = struct
       | Elet ({ let_sym = LetV pv }, e2) when ity_equal pv.pv_ity ity_mark ->
           expr info e2
       | Elet ({ let_sym = LetV pv; let_expr = e1 }, e2) when is_underscore pv ->
-          ML.eseq (expr info e1) (expr info e2)
+         ML.eseq (expr info e1) (expr info e2)
       | Elet ({ let_sym = lv ; let_expr = e1 }, e2) ->
           ML.Elet (lv_name lv, expr info e1, expr info e2)
       | Eif (e0, e1, e2) ->

tests/test_extraction_mario.mlw

@@ -31,28 +31,30 @@ module M
     ghost mutable v : seq 'a;
   }
 
+  let update (c: cursor int) : unit
+  = let t = ghost c.v <- empty in t; ()
+
   exception Empty (list int, int)
   exception Out_of_bounds int
 
-  let rec length (x: int) (l: list 'a) : int
+  let rec length (l: list 'a) : int
     variant  { l }
   = match l with
-    | Nil -> x
-    | Cons _ r -> length x r
+    | Nil -> 0
+    | Cons _ r -> 1 + length r
     end
 
   let t (x:int) : int
     requires { false }
   = absurd
 
-  let rec ff (x: int) : int
-    diverges
-  = ff x
+  let a () : unit
+  = assert { true }
 
 end
 
 (*
  * Local Variables:
- * compile-command: "../bin/why3extract -D ../drivers/c.drv -o extract test_extraction_mario.mlw"
+ * compile-command: "make -C .. -j3; ../bin/why3extract -D ../drivers/c.drv -o extract test_extraction_mario.mlw"
  * End:
  *)
\ No newline at end of file