typage des triggers

Makefile.in

@@ -112,8 +112,8 @@ PARSER_CMO := parser.cmo lexer.cmo typing.cmo
 
 PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 
-TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo \
-	inlining.cmo
+TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo 
+#	inlining.cmo
 
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 

bench/typing/good/algebraic1.why

+theory TreeForest
+  type 'a list = Nil | Cons('a, 'a list)
+  type 'a tree = Leaf('a) | Node('a forest)
+  type 'a forest = 'a tree list
+end

lib/prelude/prelude.why

@@ -17,16 +17,16 @@ theory Int
   logic neg(int) : int
   
   (* ring structure *)
-  axiom Add_assoc: forall x,y,z:int. x+(y+z) = (x+y)+z
-  axiom Add_comm: forall x,y:int. x+y = y+x
+  axiom Add_assoc:    forall x,y,z:int. x+(y+z) = (x+y)+z
+  axiom Add_comm:     forall x,y:int. x+y = y+x
   axiom Zero_neutral: forall x:int. x+0 = x
-  axiom Neg: forall x:int. x+neg(x) = 0
-  axiom Mul_assoc: forall x,y,z:int. x*(y*z) = (x*y)*z
-  axiom Mul_distr: forall  x,y,z:int. x*(y+z) = x*y + x*z
+  axiom Neg:          forall x:int. x+neg(x) = 0
+  axiom Mul_assoc:    forall x,y,z:int. x*(y*z) = (x*y)*z
+  axiom Mul_distr:    forall x,y,z:int. x*(y+z) = x*y + x*z
 
   (* int is a unitary, communtative ring *)
-  axiom Mul_comm: forall x,y:int. x*y = y*x
-  axiom Unitary: forall x:int. 1*x = x
+  axiom Mul_comm:     forall x,y:int. x*y = y*x
+  axiom One_neutral:  forall x:int. 1*x = x
 
 end
 
@@ -37,44 +37,38 @@ theory Real
   logic (>) (real, real)
   logic (>=)(real, real)
   
-  logic ( + ) (real, real) : real
-  logic ( - ) (real, real) : real
-  logic ( * ) (real, real) : real
-  logic ( / ) (real, real) : real
+  logic (+) (real, real) : real
+  logic (-) (real, real) : real
+  logic (*) (real, real) : real
+  logic (/) (real, real) : real
 
   logic neg(real) : real
   logic inv(real) : real
 
   (* field structure *)
-  axiom Add_assoc: forall x,y,z:real. x+(y+z) = (x+y)+z
-  axiom Add_comm: forall x,y:real. x+y = y+x
-  axiom Mul_comm: forall x,y:real. x*y = y*x
+  axiom Add_assoc:    forall x,y,z:real. x+(y+z) = (x+y)+z
+  axiom Add_comm:     forall x,y:real. x+y = y+x
+  axiom Mul_comm:     forall x,y:real. x*y = y*x
   axiom Zero_neutral: forall x:real. x+0. = x
-  axiom Neg: forall x:real. x+neg(x) = 0.
-  axiom Mul_assoc: forall x,y,z:real. x*(y*z) = (x*y)*z
-  axiom Mul_distr: forall  x,y,z:real. x*(y+z) = x*y + x*z
-  axiom Unitary: forall x:real. 1.*x = x
-  axiom Inv: forall x:real. x*inv(x) = 1.
+  axiom Neg:          forall x:real. x+neg(x) = 0.
+  axiom Mul_assoc:    forall x,y,z:real. x*(y*z) = (x*y)*z
+  axiom Mul_distr:    forall x,y,z:real. x*(y+z) = x*y + x*z
+  axiom One_neutral:  forall x:real. 1.*x = x
+  axiom Inv:          forall x:real. x*inv(x) = 1.
 
 end
 
 theory Bool
 
-  (*type t = | True | False*)
+  type bool = True | False
 
 end
 
 theory List
 
-  (* type 'a list = Nil | Cons ('a, 'a list) *)
+  type 'a list = Nil | Cons('a, 'a list)
 
-  type 'a list
-
-  logic nil : 'a list
-
-  logic cons('a, 'a list) : 'a list
-
-  logic is_nil('a list)
+  logic is_nil(x : 'a list) = x = Nil
 
 end
 
@@ -103,13 +97,13 @@ theory Set
 
   type 'a t 
 
-  logic mem ('a, 'a t)
+  logic mem('a, 'a t)
 
   logic empty : 'a t
 
   axiom Empty_def1 : forall x : 'a. not mem(x, empty)
 
-  logic add ('a, 'a t) : 'a t
+  logic add('a, 'a t) : 'a t
 
   axiom Add_def1 : 
     forall x, y : 'a. forall s : 'a t.
@@ -121,8 +115,22 @@ theory Set
     forall s1, s2 : 'a t. forall x : 'a.
     mem(x, union(s1, s2)) <-> (mem(x, s1) or mem(x, s2))
 
+  logic inter('a t, 'a t) : 'a t
+
+  axiom Inter_def1 : 
+    forall s1, s2 : 'a t. forall x : 'a.
+    mem(x, inter(s1, s2)) <-> (mem(x, s1) and mem(x, s2))
+
+  logic diff('a t, 'a t) : 'a t
+
+  axiom Diff_def1 : 
+    forall s1, s2 : 'a t. forall x : 'a.
+    mem(x, diff(s1, s2)) <-> (mem(x, s1) and not mem(x, s2))
+
   logic equal(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) <-> mem(x, s2)
 
+  logic subset(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) -> mem(x, s2)
+
 end
 
 

src/main.ml

@@ -74,10 +74,10 @@ let transform l =
       List.map (fun t -> Transform.apply 
                      Simplify_recursive_definition.t_use t) l
     else l in
-    let l = if !inlining 
-    then 
-      List.map (fun t -> Transform.apply Inlining.t_use t) l
-    else l in
+(*     let l = if !inlining  *)
+(*     then  *)
+(*       List.map (fun t -> Transform.apply Inlining.t_use t) l *)
+(*     else l in *)
     if !print_stdout then 
       List.iter (Pretty.print_decl_or_use_list Format.std_formatter) l
 

src/parser/lexer.mll

@@ -48,7 +48,6 @@
 	"assert", ASSERT;
 	"axiom", AXIOM;
 	"begin", BEGIN;
-        "bool", BOOL;
         "check", CHECK;
 	"clone", CLONE;
 	"do", DO;

src/parser/parser.mly

@@ -97,7 +97,7 @@
 %token <string> STRING
 %token ABSURD AMPAMP AND ARRAY ARROW AS ASSERT AT AXIOM 
 %token BANG BAR BARBAR BEGIN 
-%token BIGARROW BOOL CHECK CLONE COLON COLONEQUAL COMMA DO 
+%token BIGARROW CHECK CLONE COLON COLONEQUAL COMMA DO 
 %token DONE DOT ELSE END EOF EQUAL
 %token EXCEPTION EXISTS EXPORT EXTERNAL FALSE FOR FORALL FPI 
 %token FUN FUNCTION GOAL
@@ -353,10 +353,6 @@ primitive_type:
    { PPTtyapp ([$1], $2) }
 | LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
    { PPTtyapp ($2 :: $4, $6) }
-/*
-| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
-   { match $2 with [p] -> p | _ -> raise Parse_error }
-*/
 ;
 
 list1_primitive_type_sep_comma:
@@ -398,14 +394,15 @@ lexpr:
    { mk_pp (PPapp ($1, $3)) }
 | IF lexpr THEN lexpr ELSE lexpr %prec prec_if 
    { mk_pp (PPif ($2, $4, $6)) }
-| FORALL list1_lident_sep_comma COLON primitive_type triggers 
-  DOT lexpr %prec prec_forall
-   { let rec mk = function
+| FORALL list1_lident_sep_comma COLON primitive_type triggers DOT lexpr 
+  %prec prec_forall
+   { mk_pp (PPforall ($2, $4, $5, $7))
+     (*let rec mk = function
        | [] -> assert false
        | [id] -> mk_pp (PPforall (id, $4, $5, $7))
        | id :: l -> mk_pp (PPforall (id, $4, [], mk l))
      in
-     mk $2 }
+     mk $2 *) }
 | EXISTS lident COLON primitive_type DOT lexpr %prec prec_exists
    { mk_pp (PPexists ($2, $4, $6)) }
 | INTEGER
@@ -468,14 +465,6 @@ list1_type_var_sep_comma:
 | type_var COMMA list1_type_var_sep_comma { $1 :: $3 }
 ;
 
-/***
-qualid_ident:
-| IDENT          { $1, None }
-| IDENT AT       { $1, Some "" }
-| IDENT AT IDENT { $1, Some $3 }
-;
-***/
-
 ident_or_string:
 | ident  { $1.id }
 | STRING { $1 }
@@ -527,6 +516,12 @@ subst:
 
 /******* programs **************************************************
 
+qualid_ident:
+| IDENT          { $1, None }
+| IDENT AT       { $1, Some "" }
+| IDENT AT IDENT { $1, Some $3 }
+;
+
 list0_ident_sep_comma:
 | /* epsilon * /         { [] }
 | list1_ident_sep_comma { $1 }

src/parser/ptree.mli

@@ -54,7 +54,7 @@ and pp_desc =
   | PPinfix of lexpr * pp_infix * lexpr
   | PPprefix of pp_prefix * lexpr
   | PPif of lexpr * lexpr * lexpr
-  | PPforall of ident * pty * lexpr list list * lexpr
+  | PPforall of ident list * pty * lexpr list list * lexpr
   | PPexists of ident * pty * lexpr
   | PPnamed of string * lexpr
   | PPlet of ident* lexpr * lexpr

src/parser/typing.ml

@@ -372,7 +372,7 @@ and dterm_node =
 
 and dfmla = 
   | Fapp of psymbol * dterm list
-  | Fquant of quant * string * dty * dfmla
+  | Fquant of quant * string list * dty * dtrigger list list * dfmla
   | Fbinop of binop * dfmla * dfmla
   | Fnot of dfmla
   | Ftrue
@@ -381,6 +381,10 @@ and dfmla =
 (*   | Flet of dterm * string * dfmla *)
 (*   | Fcase of dterm * (pattern * dfmla) list *)
 
+and dtrigger =
+  | TRterm of dterm
+  | TRfmla of dfmla
+
 let binop = function
   | PPand -> Fand
   | PPor -> For
@@ -433,14 +437,27 @@ and dfmla env e = match e.pp_desc with
       Fbinop (binop op, dfmla env a, dfmla env b)
   | PPif (a, b, c) ->
       Fif (dfmla env a, dfmla env b, dfmla env c)  
-  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
+  | PPforall (idl, ty, trl, a) ->
       let ty = dty env ty in
-      let env = { env with dvars = M.add x ty env.dvars } in
-      Fquant (Fforall, x, ty, dfmla env a)
-  | PPexists ({id=x}, ty, a) -> (* TODO: triggers *)
+      let env, idl = 
+	map_fold_left
+	  (fun env {id=x} -> { env with dvars = M.add x ty env.dvars }, x)
+	  env idl
+      in
+      let trigger e = (* FIXME? *)
+	try 
+	  TRterm (dterm env e) 
+	with 
+	  | Error (TermExpected | UnboundSymbol _) 
+	  | Loc.Located (_, Error (TermExpected | UnboundSymbol _)) -> 
+	      TRfmla (dfmla env e) 
+      in
+      let trl = List.map (List.map trigger) trl in
+      Fquant (Fforall, idl, ty, trl, dfmla env a)
+  | PPexists ({id=x}, ty, a) -> (* TODO: triggers? *)
       let ty = dty env ty in
       let env = { env with dvars = M.add x ty env.dvars } in
-      Fquant (Fexists, x, ty, dfmla env a)
+      Fquant (Fexists, [x], ty, [], dfmla env a)
   | PPapp (x, tl) ->
       let s = find_psymbol x env.th in
       let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
@@ -497,11 +514,16 @@ and fmla env = function
       f_binary op (fmla env f1) (fmla env f2)
   | Fif (f1, f2, f3) ->
       f_if (fmla env f1) (fmla env f2) (fmla env f3)
-  | Fquant (q, x, t, f1) ->
+  | Fquant (q, xl, ty, trl, f1) ->
       (* TODO: shouldn't we localize this ident? *)
-      let v = create_vsymbol (id_fresh x) (ty_of_dty t) in
-      let env = M.add x v env in
-      f_quant q [v] [] (fmla env f1)
+      let ty = ty_of_dty ty in
+      let env, vl = 
+	map_fold_left 
+	  (fun env x -> 
+	     let v = create_vsymbol (id_fresh x) ty in M.add x v env, v) 
+	  env xl 
+      in
+      f_quant q vl [] (fmla env f1)
   | Fapp (s, tl) ->
       f_app s (List.map (term env) tl)
 

src/test.why

@@ -2,15 +2,8 @@
 (* test file *)
 
 theory A
-  type t
-  logic c : t
-end
-
-theory B
-  use A as C
-  clone import A
-  logic f(C.t) : t
-  axiom Ax : forall x:t. x = C.c
+  use import prelude.Int
+  axiom A : forall x:int [x+x,x=0]. x+x = x -> x = 0
 end
 
 theory TreeForest