[wp] fix import for boolean and sum types

- also fix compilation of imported fun calls
- also fix Why3 path wrt to -wp-library

src/plugins/wp/ProverWhy3.ml

@@ -56,10 +56,11 @@ let get_why3_conf = Conf.memoize
     begin fun () ->
       let config = Why3Provers.config () in
       let main = Why3.Whyconf.get_main config in
-      let ld =
-        (WpContext.directory () :> string)::
-        ((Wp_parameters.Share.get_dir "why3") :> string)::
-        (Why3.Whyconf.loadpath main) in
+      let ctx = (WpContext.directory () :> string) in
+      let wp = ((Wp_parameters.Share.get_dir "why3") :> string) in
+      let user = (Wp_parameters.Library.get () :> string list) in
+      let why3 = Why3.Whyconf.loadpath main in
+      let ld = ctx :: wp :: (user @ why3) in
       { env = Why3.Env.create_env ld ; config = main }
     end
 
@@ -506,8 +507,9 @@ let rec of_term ~cnv expected t : Why3.Term.term =
       coerce ~cnv sort expected $
       t_app' ~cnv ~f:["map"] ~l:"Const" ~p:["const"] [of_term ~cnv vsort v] (of_tau ~cnv sort)
     (* Generic *)
-    | Fun (FUN({m_source=Wsymbol(f,l,p)}),ls), _, _ ->
-      t_app ~cnv ~f ~l ~p $ List.map (of_term' cnv) ls
+    | Fun (FUN({m_source=Wsymbol(f,l,p)}),ls), tau, expected ->
+      coerce ~cnv sort expected $
+      t_app' ~cnv ~f ~l ~p (List.map (of_term' cnv) ls) (of_tau ~cnv tau)
 
     | Fun (f,l), _, _ -> begin
         let t_app ls l r  =
@@ -520,12 +522,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
               Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s))
           in
           match find s, expected with
-          | ls, (Prop | Bool) ->
-            coerce ~cnv sort expected $
-            t_app ls l (of_tau ~cnv sort)
-          | ls, _ ->
-            coerce ~cnv sort expected $
-            t_app ls l (of_tau ~cnv sort)
+          | ls, _ -> coerce ~cnv sort expected $ t_app ls l (of_tau ~cnv sort)
           | exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
         in
         let apply_from_ns' s l =

src/plugins/wp/Why3Import.ml

@@ -84,6 +84,7 @@ type env = {
   tenv : C.logic_type_info W.Ty.Hts.t;
   lenv : C.logic_info W.Term.Hls.t;
   lils : W.Term.lsymbol Logic_info.Hashtbl.t;
+  lcts : W.Term.lsymbol Logic_ctor_info.Hashtbl.t;
   ltts : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
   menv : why3module Datatype.String.Hashtbl.t;
 }
@@ -97,9 +98,10 @@ let create wenv =
   let tenv  = W.Ty.Hts.create 0 in
   let lenv  = W.Term.Hls.create 0 in
   let lils  = Logic_info.Hashtbl.create 0 in
+  let lcts  = Logic_ctor_info.Hashtbl.create 0 in
   let ltts  = Logic_type_info.Hashtbl.create 0 in
   let menv  = Datatype.String.Hashtbl.create 0 in
-  { wenv; tenv; lenv; lils; ltts; menv }
+  { wenv; tenv; lenv; lils; lcts; ltts; menv }
 
 (* -------------------------------------------------------------------------- *)
 (* ---    Built-in                                                        --- *)
@@ -120,7 +122,6 @@ let add_builtins env =
   begin
     let ts_list = find_ts env ["list"] "List" ["list"] in
     let ts_set = find_ts env ["set"] "Set" ["set"] in
-    add_builtin env.tenv W.Ty.ts_bool Utf8_logic.boolean [];
     add_builtin env.tenv ts_list "\\list" ["A"];
     add_builtin env.tenv ts_set "set" ["A"];
   end
@@ -161,47 +162,55 @@ let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
        x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
     ) txs ([], W.Ty.Mtv.empty)
 
-let rec lt_of_ty (env : env) (menv) (tvs : tvars)  (ty: W.Ty.ty) : C.logic_type =
+let rec lt_of_ty env menv (tvs : tvars)  (ty: W.Ty.ty) : C.logic_type =
   match ty.ty_node with
   | Tyvar x -> W.Ty.Mtv.find x tvs
   | Tyapp(s,[]) when W.Ty.(ts_equal s ts_int) -> C.Linteger
   | Tyapp(s,[]) when W.Ty.(ts_equal s ts_real) -> C.Lreal
+  | Tyapp(s,[]) when W.Ty.(ts_equal s ts_bool) -> C.Lboolean
   | Tyapp(s,ts) ->
-    C.Ltype( lt_of_ts env menv s,  List.map (lt_of_ty env menv tvs ) ts)
+    C.Ltype(lt_of_ts env menv s [], List.map (lt_of_ty env menv tvs ) ts)
 
-and lt_of_ts (env : env) (menv : menv) (ts : W.Ty.tysymbol) : C.logic_type_info =
+and lt_of_ts env menv (ts : W.Ty.tysymbol) (cs: W.Decl.constructor list) : C.logic_type_info =
   try W.Ty.Hts.find env.tenv ts with Not_found ->
-    let (lt_params,tvars) = tvars_of_txs ts.ts_args in
-    let lt_def =
-      match ts.ts_def with
-      | NoDef | Range _ | Float _ -> None
-      | Alias ty -> Some (C.LTsyn (lt_of_ty env menv tvars ty))
-    in
-    let lti =
-      C.{
-        lt_name =  acsl_name ts.ts_name;
-        lt_params ; lt_def ;
-        lt_attr = [];
-      }
-    in W.Ty.Hts.add env.tenv ts lti ;
+    let lt_params,tvars = tvars_of_txs ts.ts_args in
+    let lt_name = acsl_name ts.ts_name in
+    let lti = C.{ lt_name ; lt_params ; lt_def = None ; lt_attr = []; } in
+    lti.lt_def <-
+      (match ts.ts_def with
+       | Range _ | Float _ -> None
+       | NoDef -> Some (C.LTsum (List.map (cli_of_constr env menv lti) cs))
+       | Alias ty -> Some (C.LTsyn (lt_of_ty env menv tvars ty))
+      );
+    W.Ty.Hts.add env.tenv ts lti ;
     menv.lti <- (lti, (convert_location ts.ts_name.id_loc) ) :: menv.lti;
     Logic_type_info.Hashtbl.add env.ltts lti ts;
     lti
 
+and cli_of_constr env menv ctor_type (ls, _: W.Decl.constructor) : C.logic_ctor_info =
+  let _,tvars =
+    tvars_of_txs @@ W.Ty.Stv.elements @@  W.Term.ls_ty_freevars ls in
+  let l_profile = List.mapi (lv_of_ty env menv tvars ) ls.ls_args in
+  let ctor_params = List.map ( fun (lv:C.logic_var) -> lv.lv_type) l_profile in
+  let ctor_name = acsl_name ls.ls_name in
+  let ctor = Cil_types.{ ctor_name ; ctor_type ; ctor_params } in
+  Logic_ctor_info.Hashtbl.add env.lcts ctor ls ;
+  ctor
+
 (* -------------------------------------------------------------------------- *)
 (* ---    Functions conversion                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
-let lv_of_ty (env:env) (menv : menv) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
+and lv_of_ty env menv (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
   Cil_const.make_logic_var_formal (Printf.sprintf "x%d" index)
   @@ (lt_of_ty env menv tvars ty)
 
-let lt_of_ty_opt (lt_opt) =
+and lt_of_ty_opt (lt_opt) =
   match lt_opt with
   | None -> C.Ctype (C.TVoid []) (* Same as logic_typing *)
   | Some tr -> tr
 
-let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol) : C.logic_info =
+let li_of_ls env menv (ls : W.Term.lsymbol) : C.logic_info =
   let l_tparams,tvars =
     tvars_of_txs @@ W.Ty.Stv.elements @@  W.Term.ls_ty_freevars ls in
   let l_type = Option.map (lt_of_ty  env menv tvars ) ls.ls_value in
@@ -219,32 +228,32 @@ let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol) : C.logic_info =
   menv.li <- (li, (convert_location ls.ls_name.id_loc) ):: menv.li;
   Logic_info.Hashtbl.add env.lils li ls; li
 
-let add_ts env menv (ts : W.Ty.tysymbol) =
-  L.debug ~dkey "Importing type %a" pp_id ts.ts_name ;
-  ignore @@ lt_of_ts env menv ts
+let add_ts env menv (ts : W.Ty.tysymbol) (cs: W.Decl.constructor list)=
+  L.debug ~dkey "Importing type %a: %s" pp_id ts.ts_name (acsl_name ts.ts_name);
+  ignore @@ lt_of_ts env menv ts cs
 let add_ls env menv (ls : W.Term.lsymbol) =
-  L.debug ~dkey "Importing logic %a" pp_id ls.ls_name ;
+  L.debug ~dkey "Importing logic %a: %s" pp_id ls.ls_name (acsl_name ls.ls_name);
   ignore @@ li_of_ls env menv ls
 
 (* -------------------------------------------------------------------------- *)
 (* ---    Theory                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let get_theory (env) (theory_name) (theory_path) =
+let get_theory env (theory_name) (theory_path) =
   try W.Env.read_theory env.wenv theory_path theory_name
   with W.Env.LibraryNotFound _ ->
     L.error "Library %s not found" theory_name; W.Theory.ignore_theory
 
-let parse_theory (env) (theory:W.Theory.theory) (menv) =
+let parse_theory env (theory:W.Theory.theory) (menv) =
   begin
     List.iter (fun (tdecl : T.tdecl) ->
         match tdecl.td_node with
         | Decl decl ->
           begin
             match decl.d_node with
-            | Dtype ts -> add_ts env menv ts
-            | Dparam ls ->add_ls env menv ls
-            | Ddata ds -> List.iter (fun (ts, _) -> add_ts env menv ts) ds
+            | Dtype ts -> add_ts env menv ts []
+            | Dparam ls -> add_ls env menv ls
+            | Ddata ds -> List.iter (fun (ts, cs) -> add_ts env menv ts cs) ds
             | Dlogic ds -> List.iter (fun (ls,_) -> add_ls env menv ls) ds
             | Dind (_,ds) -> List.iter (fun (ls,_) -> add_ls env menv ls) ds
             | Dprop _ -> ()
@@ -257,6 +266,7 @@ let kind_of_lt (lt : C.logic_type) : LB.kind =
   match lt with
   | C.Linteger -> LB.Z
   | C.Lreal -> LB.R
+  | C.Lboolean -> LB.B
   | _ -> LB.A
 
 let sort_of_lt (lt : C.logic_type) : Qed.Logic.sort =
@@ -271,25 +281,40 @@ let sort_of_result = function
 
 let register_builtin env m =
   begin
-    List.iter (fun (lti, _) ->
-        let ty = Logic_type_info.Hashtbl.find env.ltts lti in
-        let (package,theory,name) = T.restore_path ty.ts_name in
-        LB.add_builtin_type lti.lt_name @@
-        Lang.imported_t ~package ~theory ~name
-      ) m.types;
-    List.iter (fun (li, _) ->
-        let ls = Logic_info.Hashtbl.find env.lils li in
-        let (package,theory,name) = T.restore_path ls.ls_name in
-        let profile = List.map (fun lv -> lv.C.lv_type) li.l_profile in
-        let kinds = List.map kind_of_lt profile in
-        let params = List.map sort_of_lt profile in
-        let result = sort_of_result li.l_type in
-        LB.add_builtin li.l_var_info.lv_name kinds @@
-        Lang.imported_f ~package ~theory ~name ~params ~result  ()
-      ) m.logics;
+    let add_builtin (ls: W.Term.lsymbol) acsl_name profile result =
+      let (package, theory, name) = T.restore_path ls.ls_name in
+      let kinds = List.map kind_of_lt profile in
+      let params = List.map sort_of_lt profile in
+      LB.add_builtin acsl_name kinds @@
+      Lang.imported_f ~package ~theory ~name ~params ~result  ()
+    in
+    let add_builtin_li li =
+      let ls = Logic_info.Hashtbl.find env.lils li in
+      let profile = List.map (fun lv -> lv.C.lv_type) li.l_profile in
+      let result = sort_of_result li.l_type in
+      add_builtin ls li.l_var_info.lv_name profile result
+    in
+    let add_builtin_ctor ctor =
+      let ls = Logic_ctor_info.Hashtbl.find env.lcts ctor in
+      let profile = ctor.Cil_types.ctor_params in
+      let result = Qed.Logic.Sdata in
+      add_builtin ls ctor.ctor_name profile result
+    in
+    let add_builtin_t lti =
+      let ty = Logic_type_info.Hashtbl.find env.ltts lti in
+      let (package,theory,name) = T.restore_path ty.ts_name in
+      LB.add_builtin_type lti.lt_name @@
+      Lang.imported_t ~package ~theory ~name ;
+      begin match lti.lt_def with
+        | Some C.LTsum ctors -> List.iter add_builtin_ctor ctors
+        | _ -> ()
+      end
+    in
+    List.iter (fun (lti, _) -> add_builtin_t lti) m.types;
+    List.iter (fun (li, _) -> add_builtin_li li) m.logics;
   end
 
-let import_theory (env : env) thname =
+let import_theory env thname =
   try
     Datatype.String.Hashtbl.find env.menv thname
   with Not_found ->