un peu de typage des programmes

src/parser/typing.ml

@@ -52,7 +52,6 @@ type error =
   | UnboundTypeVar of string
   | UnboundType of string list
   | UnboundSymbol of string list
-  | AnyMessage of string
 
 exception Error of error
 
@@ -68,7 +67,7 @@ let errorm ?loc f =
        Format.pp_print_flush fmt ();
        let s = Buffer.contents buf in
        Buffer.clear buf;
-       error ?loc (AnyMessage s))
+       error ?loc (Message s))
     fmt f
 
 let rec print_qualid fmt = function
@@ -118,8 +117,6 @@ let report fmt = function
        fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
   | UnboundSymbol sl ->
        fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
-  | AnyMessage s ->
-      fprintf fmt "%s" s
 
 (** Environments *)
 

src/parser/typing.mli

@@ -42,3 +42,8 @@ exception Error of error
 
 val report : Format.formatter -> error -> unit
 
+(** export for program typing *)
+
+val specialize_fsymbol : 
+  Ptree.qualid -> Theory.theory_uc -> Term.lsymbol * Denv.dty list * Denv.dty
+

src/programs/pgm_main.ml

@@ -49,6 +49,8 @@ let rec report fmt = function
       fprintf fmt "syntax error"
   | Typing.Error e ->
       Typing.report fmt e
+  | Pgm_typing.Error e ->
+      Pgm_typing.report fmt e
   | e ->
       fprintf fmt "anomaly: %s" (Printexc.to_string e)
 

src/programs/pgm_parser.mly

@@ -28,8 +28,8 @@
   let loc_i i = (rhs_start_pos i, rhs_end_pos i)
   let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
 
-  let mk_expr d = { expr_loc = loc (); expr_info = (); expr_desc = d }
-  let mk_expr_i i d = { expr_loc = loc_i i; expr_info = (); expr_desc = d }
+  let mk_expr d = { expr_loc = loc (); expr_desc = d }
+  let mk_expr_i i d = { expr_loc = loc_i i; expr_desc = d }
  
   (* FIXME: factorize with parser/parser.mly *)
   let infix s = "infix " ^ s
@@ -45,11 +45,11 @@
 	Eapply (f, a)
     | a :: l -> 
 	let loc = join f.expr_loc a.expr_loc in 
-	mk_apply { expr_loc = loc; expr_info = (); expr_desc = Eapply (f, a) } l
+	mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
 
   let mk_apply_id id = 
     let e = 
-      { expr_desc = Eident (Qident id); expr_info = (); expr_loc = id.id_loc } 
+      { expr_desc = Eident (Qident id); expr_loc = id.id_loc } 
     in
     mk_apply e
       
@@ -239,7 +239,7 @@ expr:
 simple_expr:
 | constant
     { mk_expr (Econstant $1) }
-| BANG expr
+| BANG simple_expr
     { mk_prefix "!" $2 }
 | lqualid 
     { mk_expr (Eident $1) }

src/programs/pgm_ptree.mli

@@ -34,29 +34,28 @@ type loop_annotation = {
   loop_variant   : lexpr option;
 }
 
-type 'info expr = {
-  expr_desc : 'info expr_desc;
+type expr = {
+  expr_desc : expr_desc;
   expr_loc  : loc;
-  expr_info : 'info;
 }
 
-and 'info expr_desc =
+and expr_desc =
   | Econstant of constant
   | Eident of qualid
-  | Eapply of 'info expr * 'info expr
-  | Esequence of 'info expr * 'info expr
-  | Eif of 'info expr * 'info expr * 'info expr
+  | Eapply of expr * expr
+  | Esequence of expr * expr
+  | Eif of expr * expr * expr
   | Eskip 
   | Eassert of assertion_kind * lexpr
-  | Elazy_and of 'info expr * 'info expr
-  | Elazy_or of 'info expr * 'info expr
-  | Elet of ident * 'info expr * 'info expr
-  | Eghost of 'info expr
-  | Elabel of ident * 'info expr
-  | Ewhile of 'info expr * loop_annotation * 'info expr
+  | Elazy_and of expr * expr
+  | Elazy_or of expr * expr
+  | Elet of ident * expr * expr
+  | Eghost of expr
+  | Elabel of ident * expr
+  | Ewhile of expr * loop_annotation * expr
 
 type decl =
-  | Dcode  of ident * unit expr
+  | Dcode  of ident * expr
   | Dlogic of Ptree.decl list
 
 type file = decl list

src/programs/pgm_ttree.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+type loc = Loc.position
+
+type ident = Ptree.ident
+
+type qualid = Ptree.qualid
+
+type constant = Term.constant
+
+type assertion_kind = Pgm_ptree.assertion_kind
+
+type lexpr = Ptree.lexpr
+
+type loop_annotation = Pgm_ptree.loop_annotation
+
+type expr = {
+  expr_desc : expr_desc;
+  expr_type : Denv.dty;
+  expr_loc  : loc;
+}
+
+and expr_desc =
+  | Econstant of constant
+  | Elocal of string
+  | Eglobal of Term.lsymbol
+  | Eapply of expr * expr
+  | Esequence of expr * expr
+  | Eif of expr * expr * expr
+  | Eskip 
+  | Eassert of assertion_kind * lexpr
+  | Elazy_and of expr * expr
+  | Elazy_or of expr * expr
+  | Elet of ident * expr * expr
+  | Eghost of expr
+  | Elabel of ident * expr
+  | Ewhile of expr * loop_annotation * expr
+

src/programs/pgm_typing.ml

@@ -17,22 +17,89 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Format
+open Util
+open Term
 open Theory
-open Pgm_ptree
+open Denv
+open Ptree
+open Pgm_ttree
 
-type env = {
-  env_uc : theory_uc;
+type error =
+  | Message of string
+
+exception Error of error
+
+let error ?loc e = match loc with
+  | None -> raise (Error e)
+  | Some loc -> raise (Loc.Located (loc, Error e))
+
+let errorm ?loc f =
+  let buf = Buffer.create 512 in
+  let fmt = Format.formatter_of_buffer buf in
+  Format.kfprintf
+    (fun _ ->
+       Format.pp_print_flush fmt ();
+       let s = Buffer.contents buf in
+       Buffer.clear buf;
+       error ?loc (Message s))
+    fmt f
+
+let report fmt = function
+  | Message s ->
+      fprintf fmt "%s" s
+
+(*** from Typing *************************************************************)
+type denv = {
+  uc : theory_uc; (* the theory under construction *)
+  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
+  dvars : dty Mstr.t; (* local variables, to be bound later *)
+  ts_arrow : Ty.tysymbol;
+}
+
+let create_denv uc = {
+  uc = uc;
+  utyvars = Hashtbl.create 17;
+  dvars = Mstr.empty;
+  ts_arrow = ns_find_ts (get_namespace uc) ["Prelude"; "arrow"];
 }
+(*****************************************************************************)
 
-let create_env uc = assert false (*TODO*)
+let currying env tyl ty =
+  let make_arrow_type ty1 ty2 = Tyapp (env.ts_arrow, [ty1; ty2]) in
+  List.fold_right make_arrow_type tyl ty
 
 let rec expr env e = 
-  let d, ty = expr_desc env e.expr_loc e.expr_desc in
-  { expr_desc = d; expr_info = ty; expr_loc = e.expr_loc }
+  let d, ty = expr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
+  { expr_desc = d; expr_type = ty; expr_loc = e.Pgm_ptree.expr_loc }
 
 and expr_desc env loc = function
-_ -> assert false (*TODO*)
-(*   | Econstant of constant *)
+  | Pgm_ptree.Econstant (ConstInt _ as c) ->
+      Econstant c, Tyapp (Ty.ts_int, [])
+  | Pgm_ptree.Econstant (ConstReal _ as c) ->
+      Econstant c, Tyapp (Ty.ts_real, [])
+  | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.dvars ->
+      (* local variable *)
+      let ty = Mstr.find x env.dvars in
+      Elocal x, ty
+  | Pgm_ptree.Eident p ->
+      let s, tyl, ty = Typing.specialize_fsymbol p env.uc in
+      Eglobal s, currying env tyl ty
+  | Pgm_ptree.Eapply (e1, e2) ->
+      let e1 = expr env e1 in
+      let e2 = expr env e2 in
+      begin match e1.expr_type with
+	| Tyapp (ts, [ty2; ty]) when ts == env.ts_arrow ->
+	    if not (Denv.unify ty2 e2.expr_type) then
+	      errorm ~loc:e2.expr_loc 
+		"this expression has type %a, but is expected to have type %a"
+		print_dty e2.expr_type print_dty ty2;
+	    Eapply (e1, e2), ty
+	| _ ->
+	    errorm ~loc:e1.expr_loc "this expression is not a function"
+      end
+  | _ -> 
+      assert false (*TODO*)
 (*   | Eident of qualid *)
 (*   | Eapply of 'info expr * 'info expr *)
 (*   | Esequence of 'info expr * 'info expr *)
@@ -47,7 +114,7 @@ _ -> assert false (*TODO*)
 (*   | Ewhile of 'info expr * loop_annotation * 'info expr *)
 
 let code uc id e =
-  let env = create_env uc in
+  let env = create_denv uc in
   ignore (expr env e)
 
 (*

src/programs/test.mlw

@@ -2,22 +2,21 @@
 (* test file for ML-why *)
 
 { 
-use import prelude.Programs
-use import prelude.Int
-logic f(int) : int 
-logic g(x : int) : int = f(x+1)
+  use import programs.Prelude
+  use import int.Int
+  type foo
+  logic foo : foo
+  logic f(int) : int 
+  logic g(x : int) : int = f(x+1)
 }
 
 let p = 
-  let x = ref 0 in 
-  L:
-  assert { !x = 0 };
-  x := 1;
-  assert { at(!x, L) = 0 };
-  !x
+   !(ref 1)
+   +  
+   2
 
 { 
-axiom A : forall x:int. f(x) = g(x-1)
+  axiom A : forall x:int. f(x) = g(x-1)
 }
 
 

theories/programs.why

+
+theory Prelude
+  type ('a, 'b) arrow
+
+  type  'a ref
+  logic ref ('a)     : 'a ref
+  logic (!_)('a ref) : 'a
+
+  type  label
+  logic at  ('a, label) : 'a
+  logic old ('a)        : 'a
+end
\ No newline at end of file