whyml: program typing in progress

src/parser/typing.mli

@@ -80,6 +80,7 @@ val dpat_list :
   theory_uc -> denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
 
 val print_denv : Format.formatter -> denv -> unit
+val print_qualid: Format.formatter -> Ptree.qualid -> unit
 
 val split_qualid : Ptree.qualid -> string list * string
 val string_list_of_qualid : string list -> Ptree.qualid -> string list

src/whyml/mlw_dtree.ml

@@ -74,7 +74,7 @@ type dloop_annotation = {
 
 type dexpr = {
   dexpr_desc : dexpr_desc;
-  dexpr_type : Denv.dty;
+  dexpr_type : Mlw_dty.darrow;
   dexpr_lab  : Ident.label list;
   dexpr_loc  : loc;
 }
@@ -82,8 +82,8 @@ type dexpr = {
 and dexpr_desc =
   | DEconstant of constant
   | DElocal of string
-  | DEglobal of prgsymbol
-  | DElogic of Term.lsymbol
+  | DEglobal of prgsymbol * dexpr list
+  | DElogic of Term.lsymbol * dexpr list
   | DEapply of dexpr * dexpr
   | DEfun of dubinder list * dtriple
   | DElet of ident * dexpr * dexpr

src/whyml/mlw_dty.ml

@@ -28,37 +28,41 @@ open Ptree
 open Mlw_ty
 open Mlw_ty.T
 open Mlw_expr
+open Mlw_module
 
 type dity = dity_desc ref
 
 and dity_desc = {
+  uid : int;
   node: dity_node;
   ity : ity Lazy.t;
 }
 
 and dity_node =
-  | Duvar of string (* user type variable *)
+  | Duvar of Ptree.ident (* user type variable *)
   | Dvar
   | Dits of itysymbol * dity list
   | Dts  of tysymbol  * dity list
 
+let unique = let r = ref 0 in fun () -> incr r; !r
+
+let create n l = ref { uid = unique (); node = n; ity = l }
+
 let create_user_type_variable x =
   let id = id_user x.id x.id_loc in
-  ref { node = Duvar x.id; ity = lazy (ity_var (create_tvsymbol id)) }
+  create (Duvar x) (lazy (ity_var (create_tvsymbol id)))
 
 let create_type_variable () =
   let id = id_fresh "a" in
-  ref { node = Dvar; ity = lazy (ity_var (create_tvsymbol id)) }
+  create Dvar (lazy (ity_var (create_tvsymbol id)))
 
 let ity_of_dity d = Lazy.force !d.ity
 
 let its_app its dl =
-  ref { node = Dits (its, dl);
-        ity = lazy (ity_app_fresh its (List.map ity_of_dity dl)) }
+  create (Dits (its, dl)) (lazy (ity_app_fresh its (List.map ity_of_dity dl)))
 
 let ts_app ts dl =
-  ref { node = Dts (ts, dl);
-        ity = lazy (ity_pur ts (List.map ity_of_dity dl)) }
+  create (Dts (ts, dl)) (lazy (ity_pur ts (List.map ity_of_dity dl)))
 
 (* unification *)
 
@@ -67,7 +71,7 @@ let rec unify d1 d2 =
     begin match !d1.node, !d2.node with
     | Dvar, _ | _, Dvar ->
         ()
-    | Duvar s1, Duvar s2 when s1 = s2 ->
+    | Duvar s1, Duvar s2 when s1.id = s2.id ->
         ()
     | Dits (its1, dl1), Dits (its2, dl2) when its_equal its1 its2 ->
         if List.length dl1 <> List.length dl2 then raise Exit;
@@ -93,6 +97,8 @@ let find_type_variable htv tv =
     Htv.add htv tv dtv;
     dtv
 
+type darrow = dity list * dity
+
 let rec dity_of_ity htv ity = match ity.ity_node with
   | Ityvar tv -> find_type_variable htv tv
   | Itypur (ts, ityl) -> ts_app ts (List.map (dity_of_ity htv) ityl)
@@ -100,7 +106,11 @@ let rec dity_of_ity htv ity = match ity.ity_node with
 
 let dity_of_vtv htv v = dity_of_ity htv v.vtv_ity
 
-let specialize_psymbol ps =
+let specialize_vtvalue vtv =
+  let htv = Htv.create 17 in
+  [], dity_of_vtv htv vtv
+
+let specialize_vtarrow vta =
   let htv = Htv.create 17 in
   let rec decompose args a =
     let args = dity_of_vtv htv a.vta_arg :: args in
@@ -108,7 +118,7 @@ let specialize_psymbol ps =
     | VTvalue v -> List.rev args, dity_of_vtv htv v
     | VTarrow a1 -> decompose args a1
   in
-  decompose [] ps.ps_vta
+  decompose [] vta
 
 let specialize_plsymbol pls =
   let htv = Htv.create 17 in
@@ -124,3 +134,40 @@ let specialize_lsymbol ls =
   in
   List.map (dity_of_ty htv) ls.ls_args, ty
 
+let specialize_prgsymbol = function
+  | PV pv -> specialize_vtvalue pv.pv_vtv
+  | PA pa -> specialize_vtarrow pa.pa_vta
+  | PS ps -> specialize_vtarrow ps.ps_vta
+  | PL pl -> specialize_plsymbol pl
+
+let specialize_darrow (args, res) =
+  let htv = Hashtbl.create 17 in
+  let rec specialize_dity d =
+    try Hashtbl.find htv !d.uid
+    with Not_found ->
+      let d = match !d.node with
+        | Dvar -> create_type_variable ()
+        | Duvar s -> create_user_type_variable s
+        | Dits (its, dl) -> its_app its (List.map specialize_dity dl)
+        | Dts (ts, dl) -> ts_app ts (List.map specialize_dity dl)
+      in
+      Hashtbl.add htv !d.uid d;
+      d
+  in
+  List.map specialize_dity args, specialize_dity res
+
+let match_darrow ps da =
+  let rec match_arrow s vta (args, res) =
+    let s, args = match args with
+      | [] -> assert false
+      | arg :: args ->
+        let ity1 = vta.vta_arg.vtv_ity in
+        let ity2 = ity_of_dity arg in
+        ity_match s ity1 ity2, args
+    in
+    match vta.vta_result with
+      | VTvalue v -> assert (args = []); ity_match s v.vtv_ity (ity_of_dity res)
+      | VTarrow a -> match_arrow s a (args, res)
+  in
+  match_arrow ity_subst_empty ps.ps_vta da
+

src/whyml/mlw_dty.mli

@@ -27,6 +27,7 @@ open Term
 open Mlw_ty
 open Mlw_ty.T
 open Mlw_expr
+open Mlw_module
 
 type dity
 
@@ -41,6 +42,10 @@ val unify: dity -> dity -> unit
 val ity_of_dity: dity -> ity
   (** use with care, only once unification is done *)
 
-val specialize_lsymbol:  lsymbol  -> dity list * dity
-val specialize_psymbol:  psymbol  -> dity list * dity
-val specialize_plsymbol: plsymbol -> dity list * dity
+type darrow = dity list * dity
+
+val specialize_darrow: darrow -> darrow
+val specialize_lsymbol: lsymbol  -> darrow
+val specialize_prgsymbol: prgsymbol -> darrow
+
+val match_darrow: psymbol -> darrow -> ity_subst

src/whyml/mlw_typing.ml

@@ -33,6 +33,7 @@ open Mlw_ty.T
 open Mlw_expr
 open Mlw_decl
 open Mlw_module
+open Mlw_dty
 
 (** errors *)
 
@@ -90,25 +91,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
 
 (** Typing type expressions *)
 
-let ts_arrow =
-  let a = create_tvsymbol (Ident.id_fresh "a") in
-  let b = create_tvsymbol (Ident.id_fresh "b") in
-  Ty.create_tysymbol (Ident.id_fresh "arrow") [a; b] None
-
-let ts_region =
-  let a = create_tvsymbol (Ident.id_fresh "a") in
-  let b = create_tvsymbol (Ident.id_fresh "b") in
-  Ty.create_tysymbol (Ident.id_fresh "region") [a; b] None
-
-(* let rec ity_of_dty = function *)
-(*   | Tyvar { type_val = Some t } -> *)
-(*       ty_of_dty t *)
-(*   | Tyvar { type_val = None; user = false; type_var_loc = loc } -> *)
-(*       error ?loc (AnyMessage "undefined type variable") *)
-(*   | Tyvar { tvsymbol = tv } -> *)
-(*       ty_var tv *)
-(*   | Tyapp (s, tl) -> *)
-(*       ty_app s (List.map ty_of_dty tl) *)
+
 
 (** Typing program expressions *)
 
@@ -122,7 +105,7 @@ let rec extract_labels labs loc e = match e.Ptree.expr_desc with
 
 type denv = {
   uc     : module_uc;
-  locals : Denv.dty Mstr.t;
+  locals : (bool * darrow) Mstr.t;
   denv   : Typing.denv; (* for user type variables only *)
 }
 
@@ -131,6 +114,33 @@ let create_denv uc =
     locals = Mstr.empty;
     denv = Typing.create_denv (); }
 
+let unify_arg dity { dexpr_loc = loc; dexpr_type = (args, res) } =
+  if args <> [] then errorm ~loc "value expected";
+  unify dity res
+
+let unify_args ls args el =
+  try
+    List.iter2 unify_arg args el
+  with Invalid_argument _ ->
+    raise (Term.BadArity (ls, List.length args, List.length el))
+
+let unify_args_prg ~loc prg args el = match prg with
+  | PV { pv_vs = vs } ->
+      errorm ~loc "%s: not a function" vs.vs_name.id_string
+  | PL pl ->
+      unify_args pl.pl_ls args el; []
+  | PA { pa_name = id } | PS { ps_name = id } ->
+      let rec unify_list = function
+        | a :: args, e :: el -> unify_arg a e; unify_list (args, el)
+        | args, [] -> args
+        | [], _ :: _ -> errorm ~loc "too many arguments for %s" id.id_string
+      in
+      unify_list (args, el)
+
+let rec decompose_app args e = match e.Ptree.expr_desc with
+  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
+  | _ -> e, args
+
 let rec dexpr ~userloc denv e =
   let loc = e.Ptree.expr_loc in
   let labs, userloc, d = extract_labels [] userloc e in
@@ -141,11 +151,40 @@ let rec dexpr ~userloc denv e =
   in
   e
 
-and dexpr_desc ~userloc denv _loc = function
+and dexpr_desc ~userloc denv loc = function
   | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
       (* local variable *)
-      let tyv = Mstr.find x denv.locals in
-      DElocal x, tyv
+      let poly, da = Mstr.find x denv.locals in
+      let da = if poly then specialize_darrow da else da in
+      DElocal x, da
+  | Ptree.Eident p ->
+      let x = Typing.string_list_of_qualid [] p in
+      begin
+        try
+          let prg = ns_find_ps (get_namespace denv.uc) x in
+          DEglobal (prg, []), specialize_prgsymbol prg
+        with Not_found -> try
+          let ls = ns_find_ls (Theory.get_namespace (get_theory denv.uc)) x in
+          DElogic (ls, []), specialize_lsymbol ls
+        with Not_found ->
+          errorm ~loc "unbound symbol %a" Typing.print_qualid p
+      end
+  | Ptree.Eapply (e1, e2) ->
+      let e, el = decompose_app [e2] e1 in
+      let e = dexpr ~userloc denv e in
+      let el = List.map (dexpr ~userloc denv) el in
+      begin match e.dexpr_desc with
+        | DElogic (ls, _) ->
+            let args, res = e.dexpr_type in
+            unify_args ls args el;
+            DElogic (ls, el), ([], res)
+        | DEglobal (prg, _) ->
+            let args, res = e.dexpr_type in
+            let args = unify_args_prg ~loc prg args el in
+            DEglobal (prg, el), (args, res)
+        | _ ->
+          assert false (*TODO*)
+      end
   | _ ->
       ignore (userloc);
       assert false (*TODO*)
@@ -153,10 +192,7 @@ and dexpr_desc ~userloc denv _loc = function
 type local_var =
   | Lpvsymbol of pvsymbol
   | Lpasymbol of pasymbol
-  | Lpsymbol  of psymbol * Denv.type_var Mtv.t * Denv.type_var Mreg.t
-
-let region_table : region Htv.t =
-  Htv.create 17 (* FIXME: use Wtv instead *)
+  | Lpsymbol  of psymbol * darrow
 
 let rec expr locals de = match de.dexpr_desc with
   | DElocal x ->
@@ -164,10 +200,7 @@ let rec expr locals de = match de.dexpr_desc with
       begin match Mstr.find x locals with
       | Lpvsymbol pv -> e_value pv
       | Lpasymbol pa -> e_arrow pa
-      | Lpsymbol  (_ps, _, _) ->
-          (* let ity = ity_of_dty de.dexpr_dty in *)
-          (* e_inst ps *)
-          assert false (*TODO*)
+      | Lpsymbol (ps, da) -> e_inst ps (match_darrow ps da)
       end
   | _ ->
       assert false (*TODO*)