Merge branch 'new_system' into alias

modules/python.mlw

@@ -21,16 +21,12 @@ module Python
   type list 'a = Array.array 'a
 
   function ([]) (l: list 'a) (i: int) : 'a =
-    Array.get l i
+    Array.([]) l i
 
   function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a =
-    Array.set l i v
+    Array.([<-]) l i v
 
-  function len (l: list 'a) : int =
-    Array.length l
-
-  let len (l: list 'a) : int
-    ensures { result = len(l) }
+  let function len (l: list 'a) : int
   = Array.length l
 
   let ([]) (l: list 'a) (i: int) : 'a
@@ -77,15 +73,13 @@ module Python
   lemma mod_sign:
     forall x y:int. y <> 0 -> if y < 0 then mod x y <= 0 else mod x y >= 0
 
-  let (//) (x y: int) : int
+  val (//) (x y: int) : int
     requires { y <> 0 }
     ensures  { result = div x y }
-  = div x y
 
-  let (%) (x y: int) : int
+  val (%) (x y: int) : int
     requires { y <> 0 }
     ensures  { result = mod x y }
-  = mod x y
 
   (* random.randint *)
   val randint (l u: int) : int

plugins/python/py_ast.ml

@@ -24,7 +24,7 @@ type binop =
 
 type expr = {
   expr_desc: expr_desc;
-  expr_loc : Why3.Loc.position;
+  expr_loc : Loc.position;
 }
 
 and expr_desc =

plugins/python/py_main.ml

@@ -152,8 +152,8 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
       | Py_ast.Badd -> Eidapp (infix ~loc "+", [e1; e2])
       | Py_ast.Bsub -> Eidapp (infix ~loc "-", [e1; e2])
       | Py_ast.Bmul -> Eidapp (infix ~loc "*", [e1; e2])
-      | Py_ast.Bdiv -> Eidapp (Qident (mk_id ~loc "div"), [e1; e2])
-      | Py_ast.Bmod -> Eidapp (Qident (mk_id ~loc "mod"), [e1; e2])
+      | Py_ast.Bdiv -> Eidapp (infix ~loc "//", [e1; e2])
+      | Py_ast.Bmod -> Eidapp (infix ~loc "%", [e1; e2])
       | Py_ast.Beq  -> Eidapp (infix ~loc "=", [e1; e2])
       | Py_ast.Bneq -> Eidapp (infix ~loc "<>", [e1; e2])
       | Py_ast.Blt  -> Eidapp (infix ~loc "<", [e1; e2])
@@ -289,33 +289,32 @@ and block env ~loc = function
     let s = stmt env s in
     if sl = [] then s else mk_expr ~loc (Esequence (s, block env ~loc sl))
   | Ddef (id, idl, sp, bl) :: sl ->
-    let lam = def (id, idl, sp, bl) in
+    (* f(x1,...,xn): body ==>
+      let f x1 ... xn =
+        let x1 = ref x1 in ... let xn = ref xn in
+        try body with Return x -> x *)
+    let env' = List.fold_left add_var empty_env idl in
+    let body = block env' ~loc:id.id_loc bl in
+    let body = if not (has_returnl bl) then body else
+      let loc = id.id_loc in
+      mk_expr ~loc (Etry (body, return_handler ~loc)) in
+    let local bl id =
+      let loc = id.id_loc in
+      let ref = mk_ref ~loc (mk_var ~loc id) in
+      mk_expr ~loc (Elet (id, false, Expr.RKnone, ref, bl)) in
+    let body = List.fold_left local body idl in
+    let param id = id.id_loc, Some id, false, None in
+    let params = if idl = [] then no_params ~loc else List.map param idl in
     let s = block env ~loc sl in
-    if block_has_call id bl then mk_expr ~loc (Erec ([id, false, Expr.RKnone, assert false, assert false, assert false, assert false, assert false], s))
-    else mk_expr ~loc (Efun (assert false, None, assert false, assert false, s))
+    let e = if block_has_call id bl then
+      Erec ([id, false, Expr.RKnone, params, None, Ity.MaskVisible, sp, body], s)
+    else
+      let e = Efun (params, None, Ity.MaskVisible, sp, body) in
+      Elet (id, false, Expr.RKnone, mk_expr ~loc e, s) in
+    mk_expr ~loc e
   | (Dimport _ | Py_ast.Dlogic _) :: sl ->
     block env ~loc sl
 
-(* f(x1,...,xn): body
-
-   let f x1 ... xn =
-     let x1 = ref x1 in ... let xn = ref xn in
-     try body with Return x -> x *)
-and def (id, idl, sp, bl) =
-  let loc = id.id_loc in
-  let env = empty_env in
-  let env = List.fold_left add_var env idl in
-  let body = block env ~loc bl in
-  let body = if has_returnl bl then
-      mk_expr ~loc (Etry (body, return_handler ~loc)) else body in
-  let local bl id =
-    let loc = id.id_loc in
-    mk_expr ~loc (Elet (id, false, Expr.RKnone, mk_ref ~loc (mk_var ~loc id), bl)) in
-  let body = List.fold_left local body idl in
-  let param id = id.id_loc, Some id, false, None in
-  let params = if idl = [] then no_params ~loc else List.map param idl in
-  params, None, body, sp
-
 let fresh_type_var =
   let r = ref 0 in
   fun loc -> incr r;
@@ -324,22 +323,22 @@ let fresh_type_var =
 let logic_param id =
   id.id_loc, Some id, false, fresh_type_var id.id_loc
 
-let logic inc = function
+let logic = function
   | Py_ast.Dlogic (func, id, idl) ->
     let d = { ld_loc = id.id_loc;
               ld_ident = id;
               ld_params = List.map logic_param idl;
               ld_type = if func then Some (fresh_type_var id.id_loc) else None;
               ld_def = None } in
-    assert false
-    (*inc.new_decl id.id_loc (Dlogic [d])*)
+    Typing.add_decl id.id_loc (Dlogic [d])
   | _ -> ()
 
-let translate ~loc inc dl =
-  List.iter (logic inc) dl;
-  let fd = (no_params ~loc, None, block empty_env ~loc dl, empty_spec) in
-  let main = assert false (*Dfun (mk_id ~loc "main", Gnone, fd)*) in
-  assert false (*inc.new_pdecl loc main*)
+let translate ~loc dl =
+  List.iter logic dl;
+  let bl = block empty_env ~loc dl in
+  let fd = Efun (no_params ~loc, None, Ity.MaskVisible, empty_spec, bl) in
+  let main = Dlet (mk_id ~loc "main", false, Expr.RKnone, mk_expr ~loc fd) in
+  Typing.add_decl loc main
 
 let read_channel env path file c =
   let f = Py_lexer.parse file c in
@@ -348,28 +347,25 @@ let read_channel env path file c =
   let file = Filename.chop_extension file in
   let name = Strings.capitalize file in
   Debug.dprintf debug "building module %s.@." name;
-  let inc = Typing.open_file env path in
-  let loc = Why3.Loc.user_position file 0 0 0 in
-  assert false (*
-  inc.open_module (mk_id ~loc name);
+  Typing.open_file env path;
+  let loc = Loc.user_position file 0 0 0 in
+  Typing.open_module (mk_id ~loc name);
   let use_import (f, m) =
-    let q = Qdot (Qident (mk_id ~loc f), mk_id ~loc m) in
-    let use = {use_theory = q; use_import = Some (true, m) }, None in
-    inc.use_clone loc use in
+    let m = mk_id ~loc m in
+    Typing.open_scope loc m;
+    Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_id ~loc f), m)));
+    Typing.close_scope loc ~import:true in
   List.iter use_import
     ["int", "Int"; "ref", "Refint"; "python", "Python"];
-  translate ~loc inc f;
-  inc.close_module ();
-  let mm, _ as res = Mlw_typing.close_file () in
+  translate ~loc f;
+  Typing.close_module loc;
+  let mm = Typing.close_file () in
   if path = [] && Debug.test_flag debug then begin
     let add_m _ m modm = Ident.Mid.add m.mod_theory.Theory.th_name m modm in
-    let modm = Mstr.fold add_m mm Ident.Mid.empty in
-    let print_m _ m = Format.eprintf
-      "@[<hov 2>module %a@\n%a@]@\nend@\n@." Pretty.print_th m.mod_theory
-      (Pp.print_list Pp.newline2 Mlw_pretty.print_pdecl) m.mod_decls in
-    Ident.Mid.iter print_m modm
+    let print_m _ m = Pmodule.print_module Format.err_formatter m in
+    Ident.Mid.iter print_m (Mstr.fold add_m mm Ident.Mid.empty)
   end;
-  res *)
+  mm
 
 let () =
   Env.register_format mlw_language "python" ["py"] read_channel

plugins/python/py_parser.mly

@@ -14,7 +14,7 @@
   open Ptree
   open Py_ast
 
-  let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
+  let () = Exn_printer.register (fun fmt exn -> match exn with
     | Error -> Format.fprintf fmt "syntax error"
     | _ -> raise exn)
 
@@ -78,10 +78,10 @@
 %nonassoc IN
 %nonassoc DOT ELSE
 %right ARROW LRARROW
-%left OR
-%left AND
+%right OR
+%right AND
 %nonassoc NOT
-%left CMP
+%right CMP
 %left PLUS MINUS
 %left TIMES DIV MOD
 %nonassoc unary_minus prec_prefix_op
@@ -278,16 +278,18 @@ term: t = mk_term(term_) { t }
 term_:
 | term_arg_
     { match $1 with (* break the infix relation chain *)
-      | Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
+      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
+      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
+      | d -> d }
 | NOT term
     { Tnot $2 }
 | o = prefix_op ; t = term %prec prec_prefix_op
     { Tidapp (Qident o, [t]) }
 | l = term ; o = bin_op ; r = term
     { Tbinop (l, o, r) }
-| l = term ; o = infix_op ; r = term
+| l = term ; o = infix_op_1 ; r = term
     { Tinfix (l, o, r) }
-| l = term ; o = div_mod_op ; r = term
+| l = term ; o = infix_op_234 ; r = term
     { Tidapp (Qident o, [l; r]) }
 | IF term THEN term ELSE term
     { Tif ($2, $4, $6) }
@@ -326,12 +328,9 @@ term_sub_:
 | OR      { Dterm.DTor }
 | AND     { Dterm.DTand }
 
-%inline infix_op:
-| PLUS   { mk_id (infix "+") $startpos $endpos }
-| MINUS  { mk_id (infix "-") $startpos $endpos }
-| TIMES  { mk_id (infix "*") $startpos $endpos }
+%inline infix_op_1:
 | c=CMP  { let op = match c with
-          | Beq -> "="
+          | Beq  -> "="
           | Bneq -> "<>"
           | Blt  -> "<"
           | Ble  -> "<="
@@ -343,9 +342,12 @@ term_sub_:
 %inline prefix_op:
 | MINUS { mk_id (prefix "-")  $startpos $endpos }
 
-%inline div_mod_op:
-| DIV  { mk_id "div" $startpos $endpos }
-| MOD  { mk_id "mod" $startpos $endpos }
+%inline infix_op_234:
+| DIV    { mk_id "div" $startpos $endpos }
+| MOD    { mk_id "mod" $startpos $endpos }
+| PLUS   { mk_id (infix "+") $startpos $endpos }
+| MINUS  { mk_id (infix "-") $startpos $endpos }
+| TIMES  { mk_id (infix "*") $startpos $endpos }
 
 comma_list1(X):
 | separated_nonempty_list(COMMA, X) { $1 }

src/core/theory.ml

@@ -399,6 +399,8 @@ let add_symbol_pr uc pr = add_symbol add_pr pr.pr_name pr uc
 
 let create_decl d = mk_tdecl (Decl d)
 
+let print_id fmt id = Format.fprintf fmt "%s" id.id_string
+
 let warn_dubious_axiom uc k p syms =
   match k with
   | Plemma | Pgoal -> ()
@@ -412,7 +414,8 @@ let warn_dubious_axiom uc k p syms =
           | _ -> ())
         syms;
       Warning.emit ?loc:p.id_loc
-        "axiom %s does not contain any local abstract symbol" p.id_string
+        "@[axiom %s does not contain any local abstract symbol@ (contains: @[%a@])@]" p.id_string
+        (Pp.print_list Pp.comma print_id) (Sid.elements syms)
     with Exit -> ()
 
 let lab_w_non_conservative_extension_no =
@@ -421,7 +424,7 @@ let lab_w_non_conservative_extension_no =
 let should_be_conservative id =
   not (Slab.mem lab_w_non_conservative_extension_no id.id_label)
 
-let add_decl uc d =
+let add_decl ?(warn=true) uc d =
   let uc = add_tdecl uc (create_decl d) in
   match d.d_node with
   | Dtype ts  ->
@@ -449,19 +452,19 @@ let add_decl uc d =
         List.fold_left add uc la in
       List.fold_left add_ind uc dl
   | Dprop (k,pr,_) ->
-      if should_be_conservative uc.uc_name &&
+      if warn && should_be_conservative uc.uc_name &&
          should_be_conservative pr.pr_name
       then warn_dubious_axiom uc k pr.pr_name d.d_syms;
       add_symbol_pr uc pr
 
 (** Declaration constructors + add_decl *)
 
-let add_ty_decl uc ts = add_decl uc (create_ty_decl ts)
-let add_data_decl uc dl = add_decl uc (create_data_decl dl)
-let add_param_decl uc ls = add_decl uc (create_param_decl ls)
-let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
-let add_ind_decl uc s dl = add_decl uc (create_ind_decl s dl)
-let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
+let add_ty_decl uc ts = add_decl ~warn:false uc (create_ty_decl ts)
+let add_data_decl uc dl = add_decl ~warn:false uc (create_data_decl dl)
+let add_param_decl uc ls = add_decl ~warn:false uc (create_param_decl ls)
+let add_logic_decl uc dl = add_decl ~warn:false uc (create_logic_decl dl)
+let add_ind_decl uc s dl = add_decl ~warn:false uc (create_ind_decl s dl)
+let add_prop_decl ?warn uc k p f = add_decl ?warn uc (create_prop_decl k p f)
 
 (** Use *)
 
@@ -885,7 +888,7 @@ let add_decl_with_tuples uc d =
     | None -> s in
   let ixs = Sid.fold add ids Sint.empty in
   let add n uc = use_export uc (tuple_theory n) in
-  add_decl (Sint.fold add ixs uc) d
+  add_decl ~warn:false (Sint.fold add ixs uc) d
 
 (* Exception reporting *)
 

src/core/theory.mli

@@ -154,14 +154,14 @@ val restore_path : ident -> string list * string * string list
 
 val create_decl : decl -> tdecl
 
-val add_decl : theory_uc -> decl -> theory_uc
+val add_decl : ?warn:bool -> theory_uc -> decl -> theory_uc
 
 val add_ty_decl : theory_uc -> tysymbol -> theory_uc
 val add_data_decl : theory_uc -> data_decl list -> theory_uc
 val add_param_decl : theory_uc -> lsymbol -> theory_uc
 val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
 val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
-val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
+val add_prop_decl : ?warn:bool -> theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
 
 val lab_w_non_conservative_extension_no : Ident.label
 

src/mlw/pmodule.ml

@@ -286,9 +286,9 @@ let add_pdecl_no_logic uc d =
   | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
   | PDpure -> uc
 
-let add_pdecl_raw uc d =
+let add_pdecl_raw ?(warn=true) uc d =
   let uc = add_pdecl_no_logic uc d in
-  let th = List.fold_left add_decl uc.muc_theory d.pd_pure in
+  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
   { uc with muc_theory = th }
 
 (** {2 Builtin symbols} *)
@@ -329,7 +329,7 @@ let unit_module =
   let td = create_alias_decl (id_fresh "unit") [] ity_unit in
   let d,metas = create_type_decl [td] in
   assert (metas = []);
-  close_module (add_pdecl_raw uc d)
+  close_module (add_pdecl_raw ~warn:false uc d)
 
 let create_module env ?(path=[]) n =
   let m = empty_module env n path in
@@ -345,14 +345,14 @@ let add_use uc d = Sid.fold (fun id uc ->
   | Some n -> use_export uc (tuple_module n)
   | None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc
 
-let add_pdecl ~vc uc d =
+let add_pdecl ?(warn=true) ~vc uc d =
   let uc = add_use uc d in
   let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
   (* verification conditions must not add additional dependencies
      on built-in theories like TupleN or HighOrd. Also, we expect
      int.Int or any other library theory to be in the context:
      importing them automatically seems to be too invasive. *)
-  add_pdecl_raw (List.fold_left add_pdecl_raw uc dl) d
+  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
 
 (** {2 Cloning} *)
 
@@ -527,7 +527,7 @@ let clone_decl inst cl uc d = match d.d_node with
       uc
   | Dparam ls ->
       let d = create_param_decl (clone_ls cl ls) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
   | Dlogic ldl ->
       List.iter (fun (ls,_) ->
         if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
@@ -535,7 +535,7 @@ let clone_decl inst cl uc d = match d.d_node with
       let get_logic (_,ld) =
         Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
       let d = create_logic_decl (List.map get_logic ldl) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
   | Dind (s, idl) ->
       let lls = List.map (fun (ls,_) ->
         if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
@@ -547,7 +547,7 @@ let clone_decl inst cl uc d = match d.d_node with
         pr', clone_fmla cl f in
       let get_ind ls (_,la) = ls, List.map get_case la in
       let d = create_ind_decl s (List.map2 get_ind lls idl) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
   | Dprop (k,pr,f) ->
       let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
         | Pgoal, _ -> true, Pgoal
@@ -559,7 +559,7 @@ let clone_decl inst cl uc d = match d.d_node with
       let pr' = create_prsymbol (id_clone pr.pr_name) in
       cl.pr_table <- Mpr.add pr pr' cl.pr_table;
       let d = create_prop_decl k' pr' (clone_fmla cl f) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
 
 let cl_save_ls cl s s' =
   cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table
@@ -929,7 +929,7 @@ let add_vc uc (its, f) =
   let label = Slab.singleton (Ident.create_label ("expl:VC for " ^ nm)) in
   let pr = create_prsymbol (id_fresh ~label ?loc ("VC " ^ nm)) in
   let d = create_pure_decl (create_prop_decl Pgoal pr f) in
-  add_pdecl ~vc:false uc d
+  add_pdecl ~warn:false ~vc:false uc d
 
 let clone_pdecl inst cl uc d = match d.pd_node with
   | PDtype tdl ->
@@ -938,7 +938,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
         let d,metas = create_type_decl tdl in
       List.fold_left
         (fun uc (m,a) -> add_meta uc m a)
-        (add_pdecl ~vc:false uc d)
+        (add_pdecl ~warn:false ~vc:false uc d)
         metas
   | PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs ->
       (* refine only [val] symbols *)
@@ -967,7 +967,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       (* FIXME check effects of cexp/ld wrt rs *)
       (* FIXME add correspondance for "let lemma" to cl.pr_table *)
       let dl = Vc.vc uc.muc_env uc.muc_known (create_let_decl ld) in
-      List.fold_left add_pdecl_raw uc dl
+      List.fold_left (add_pdecl_raw ~warn:false) uc dl
   | PDlet ld ->
       begin match ld with
         | LDvar ({pv_vs=vs}, _) when Mvs.mem vs inst.mi_pv ->
@@ -990,7 +990,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       cl.rn_table <- Mreg.set_union cl.rn_table frz;
       let sm, ld = clone_let_defn cl (sm_of_cl cl) ld in
       cl.pv_table <- sm.sm_pv; cl.rs_table <- sm.sm_rs;
-      add_pdecl ~vc:false uc (create_let_decl ld)
+      add_pdecl ~warn:false ~vc:false uc (create_let_decl ld)
   | PDexn ({xs_name = id} as xs) when Mxs.mem xs inst.mi_xs ->
       let xs' = Mxs.find xs inst.mi_xs in
       begin try let ity = clone_ity cl xs.xs_ity in
@@ -1004,7 +1004,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       let ity = clone_ity cl xs.xs_ity in
       let xs' = create_xsymbol id ~mask:xs.xs_mask ity in
       cl.xs_table <- Mxs.add xs xs' cl.xs_table;
-      add_pdecl ~vc:false uc (create_exn_decl xs')
+      add_pdecl ~warn:false ~vc:false uc (create_exn_decl xs')
   | PDpure ->
       List.fold_left (clone_decl inst cl) uc d.pd_pure
 

src/mlw/pmodule.mli

@@ -117,7 +117,7 @@ val add_meta : pmodule_uc -> meta -> meta_arg list -> pmodule_uc
 
 (** {2 Program decls} *)
 
-val add_pdecl : vc:bool -> pmodule_uc -> pdecl -> pmodule_uc
+val add_pdecl : ?warn:bool -> vc:bool -> pmodule_uc -> pdecl -> pmodule_uc
 (** [add_pdecl ~vc m d] adds declaration [d] in module [m].
     If [vc] is [true], VC is computed and added to [m]. *)
 

tests/python/triangular.py

@@ -9,6 +9,7 @@ k = 0
 while k <= n:
     #@ invariant 0 <= k <= n+1
     #@ invariant s == (k - 1) * k // 2
+    #@ variant n - k
     s = s + k
     k = k + 1
 

theories/floating_point.why

@@ -104,7 +104,7 @@ theory GenFloat
 
   predicate no_overflow (m:mode) (x:real) = abs (round m x) <= max
 
-  axiom Bounded_real_no_overflow "W:non_conservative_extension:N":
+  axiom Bounded_real_no_overflow :
     forall m:mode, x:real. abs x <= max -> no_overflow m x
 
   axiom Round_monotonic :

theories/ieee_float.why

@@ -285,10 +285,10 @@ theory GenericFloat
 
   axiom eq_refl: forall x. is_finite x -> x .= x
 
-  axiom eq_sym "W:non_conservative_extension:N" :
+  axiom eq_sym :
     forall x y. x .= y -> y .= x
 
-  axiom eq_trans "W:non_conservative_extension:N":
+  axiom eq_trans :
     forall x y z. x .= y -> y .= z -> x .= z
 
   axiom eq_zero: zeroF .= (.- zeroF)