tuples: syntax and typing

parent 6d363790
......@@ -486,6 +486,9 @@ bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
# test targets
###############
test2: bin/why.byte $(TOOLS)
bin/why.byte tests/test-jcf.why
test: bin/why.byte $(TOOLS)
mkdir -p output_why3
bin/why.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
......
......@@ -513,6 +513,19 @@ let f_app p tl =
let f_app_unsafe = f_app
let fs_tuple n =
let tyl = ref [] in
for i = 1 to n do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
let ty = ty_tuple !tyl in
create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty
let fs_tuple = Util.memo fs_tuple
let t_tuple tl =
let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
t_app (fs_tuple (List.length tl)) tl ty
(* unsafe map with level *)
exception UnboundIndex
......
......@@ -285,6 +285,9 @@ val f_neq : term -> term -> fmla
val f_equ_simp : term -> term -> fmla
val f_neq_simp : term -> term -> fmla
val fs_tuple : int -> lsymbol
val t_tuple : term list -> term
(** Term library *)
(* generic term/fmla traversal *)
......
......@@ -131,7 +131,6 @@ let builtin_theory =
th_used = Mid.empty;
th_local = Sid.empty }
(** Constructors and utilities *)
type theory_uc = {
......@@ -562,3 +561,12 @@ let clone_export uc th inst =
let clone_theory add_tdecl acc th inst =
clone_theory (cl_init th inst) add_tdecl acc th inst
(* Tuple theories *)
let tuple_theory n =
let uc = create_theory (id_fresh ("Tuple" ^ string_of_int n)) in
let uc = add_ty_decl uc [ts_tuple n, Talgebraic [fs_tuple n]] in
close_theory uc
let tuple_theory = Util.memo tuple_theory
......@@ -64,6 +64,8 @@ and clone_map = Sid.t Mid.t
val builtin_theory : theory
val tuple_theory : int -> theory
(** Constructors and utilities *)
type theory_uc (* a theory under construction *)
......
......@@ -208,3 +208,13 @@ let ts_real = create_tysymbol (id_fresh "real") [] None
let ty_int = ty_app ts_int []
let ty_real = ty_app ts_real []
let ts_tuple n =
let vl = ref [] in
for i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None
let ts_tuple = Util.memo ts_tuple
let ty_tuple tyl =
ty_app (ts_tuple (List.length tyl)) tyl
......@@ -95,3 +95,5 @@ val ts_real : tysymbol
val ty_int : ty
val ty_real : ty
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
......@@ -129,10 +129,6 @@ let rec specialize ~loc env t = match t.ty_node with
| Ty.Tyapp (s, tl) ->
Tyapp (s, List.map (specialize ~loc env) tl)
let specialize_tysymbol ~loc s =
let env = Htv.create 17 in
List.map (find_type_var ~loc env) s.ts_args
let specialize_lsymbol ~loc s =
let tl = s.ls_args in
let t = s.ls_value in
......
......@@ -40,9 +40,6 @@ val ty_of_dty : dty -> ty
(** Specialization *)
val specialize_tysymbol :
loc:Ptree.loc -> tysymbol -> type_var list
val specialize_lsymbol :
loc:Ptree.loc -> lsymbol -> dty list * dty option
......
......@@ -192,6 +192,8 @@ rule token = parse
{ OP1 s }
| op_char_234* op_char_2 op_char_234* as s
{ OP2 s }
| "*"
{ STAR }
| op_char_34* op_char_3 op_char_34* as s
{ OP3 s }
| op_char_4+ as s
......
......@@ -68,7 +68,7 @@
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LRARROW
%token QUOTE
%token RIGHTPAR RIGHTSQ
%token RIGHTPAR RIGHTSQ STAR
%token UNDERSCORE
%token EOF
......@@ -89,7 +89,7 @@
%nonassoc NOT
%left EQUAL OP1
%left OP2
%left OP3
%left OP3 STAR
%left OP4
%nonassoc prefix_op
......@@ -154,6 +154,7 @@ lident_op:
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| STAR { "*" }
| OP4 { $1 }
| EQUAL { "=" }
;
......@@ -162,6 +163,7 @@ any_op:
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| STAR { "*" }
| OP4 { $1 }
;
......@@ -330,15 +332,26 @@ indcase:
| uident COLON lexpr { (loc (),$1,$3) }
;
primitive_type:
simple_primitive_type:
| type_var
{ PPTtyvar $1 }
| lqualid
{ PPTtyapp ([], $1) }
| primitive_type lqualid
| simple_primitive_type lqualid
{ PPTtyapp ([$1], $2) }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
{ PPTtyapp ($2 :: $4, $6) }
| LEFTPAR RIGHTPAR
{ PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
{ $2 }
;
primitive_type:
| simple_primitive_type
{ $1 }
| simple_primitive_type STAR list1_simple_primitive_type_sep_star
{ PPTtuple ($1 :: $3) }
;
list1_primitive_type_sep_comma:
......@@ -346,6 +359,11 @@ list1_primitive_type_sep_comma:
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;
list1_simple_primitive_type_sep_star:
| simple_primitive_type { [$1] }
| simple_primitive_type STAR list1_simple_primitive_type_sep_star { $1 :: $3 }
;
lexpr:
| lexpr ARROW lexpr
{ infix_pp $1 PPimplies $3 }
......@@ -369,6 +387,9 @@ lexpr:
| lexpr OP3 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
| lexpr STAR lexpr
{ let id = { id = infix "*"; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
| lexpr OP4 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
......@@ -395,15 +416,21 @@ lexpr:
{ mk_pp PPfalse }
| LEFTPAR lexpr RIGHTPAR
{ $2 }
| LEFTPAR RIGHTPAR
{ mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
{ mk_pp (PPtuple ($2 :: $4)) }
| STRING lexpr %prec prec_named
{ mk_pp (PPnamed ($1, $2)) }
| LET lident EQUAL lexpr IN lexpr
{ mk_pp (PPlet ($2, $4, $6)) }
| LET pattern EQUAL lexpr IN lexpr
{ match $2.pat_desc with
| PPpvar id -> mk_pp (PPlet (id, $4, $6))
| _ -> mk_pp (PPmatch ([$4], [[$2], $6])) }
| MATCH list1_lexpr_sep_comma WITH bar_ match_cases END
{ mk_pp (PPmatch ($2, $5)) }
| EPSILON lident COLON primitive_type DOT lexpr
{ mk_pp (PPeps ($2, $4, $6)) }
| lexpr COLON primitive_type
| lexpr COLON simple_primitive_type
{ mk_pp (PPcast ($1, $3)) }
;
......@@ -434,6 +461,9 @@ pattern:
| uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR { mk_pat (PPpapp ($1, $3)) }
| pattern AS lident { mk_pat (PPpas ($1,$3)) }
| LEFTPAR pattern RIGHTPAR { $2 }
| LEFTPAR RIGHTPAR { mk_pat (PPptuple []) }
| LEFTPAR pattern COMMA list1_pat_sep_comma RIGHTPAR
{ mk_pat (PPptuple ($2 :: $4)) }
;
triggers:
......
......@@ -44,6 +44,7 @@ type qualid =
type pty =
| PPTtyvar of ident
| PPTtyapp of pty list * qualid
| PPTtuple of pty list
type pattern =
{ pat_loc : loc; pat_desc : pat_desc }
......@@ -52,6 +53,7 @@ and pat_desc =
| PPpwild
| PPpvar of ident
| PPpapp of qualid * pattern list
| PPptuple of pattern list
| PPpas of pattern * ident
type uquant =
......@@ -76,6 +78,7 @@ and pp_desc =
| PPeps of ident * pty * lexpr
| PPmatch of lexpr list * (pattern list * lexpr) list
| PPcast of lexpr * pty
| PPtuple of lexpr list
(*s Declarations. *)
......@@ -97,7 +100,7 @@ type clone_subst =
| CSlsym of qualid * qualid
| CSlemma of qualid
| CSgoal of qualid
type param = ident option * pty
type type_def =
......
......@@ -176,7 +176,32 @@ let specialize_tysymbol loc p uc =
try ns_find_ts (get_namespace uc) sl
with Not_found -> error ~loc (UnboundType sl)
in
ts, specialize_tysymbol ~loc ts
ts, List.length ts.ts_args
(* lazy declaration of tuples *)
let tuples_needed = Hashtbl.create 17
let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n
let add_tuple_decls uc =
Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
tuples_needed uc
let with_tuples ?(reset=false) f uc x =
let uc = f (add_tuple_decls uc) x in
if reset then Hashtbl.clear tuples_needed;
uc
let add_ty_decl = with_tuples add_ty_decl
let add_ty_decls = with_tuples ~reset:true add_ty_decls
let add_logic_decl = with_tuples add_logic_decl
let add_logic_decls = with_tuples ~reset:true add_logic_decls
let add_ind_decl = with_tuples add_ind_decl
let add_ind_decls = with_tuples ~reset:true add_ind_decls
let rec type_inst s ty = match ty.ty_node with
| Ty.Tyvar n -> Mtv.find n s
......@@ -187,18 +212,21 @@ let rec dty env = function
Tyvar (find_user_type_var x env)
| PPTtyapp (p, x) ->
let loc = qloc x in
let ts, tv = specialize_tysymbol loc x env.uc in
let ts, a = specialize_tysymbol loc x env.uc in
let np = List.length p in
let a = List.length tv in
if np <> a then error ~loc (TypeArity (x, a, np));
let tyl = List.map (dty env) p in
match ts.ts_def with
begin match ts.ts_def with
| None ->
Tyapp (ts, tyl)
| Some ty ->
let add m v t = Mtv.add v t m in
let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
type_inst s ty
end
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
Tyapp (ts, List.map (dty env) tyl)
let find_ns find p ns =
let loc = qloc p in
......@@ -299,29 +327,38 @@ let check_pat_linearity pl =
let rec check p = match p.pat_desc with
| PPpwild -> ()
| PPpvar id -> add id
| PPpapp (_, pl) -> List.iter check pl
| PPpapp (_, pl) | PPptuple pl -> List.iter check pl
| PPpas (p, id) -> check p; add id
in
List.iter check pl
let fresh_type_var loc =
let tv = create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc ~user:false tv)
let rec dpat env pat =
let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
env, { dp_node = n; dp_ty = ty }
and dpat_node loc env = function
| PPpwild ->
let tv = create_tvsymbol (id_user "a" loc) in
let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
let ty = fresh_type_var loc in
env, Pwild, ty
| PPpvar {id=x} ->
let tv = create_tvsymbol (id_user "a" loc) in
let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
let ty = fresh_type_var loc in
let env = { env with dvars = Mstr.add x ty env.dvars } in
env, Pvar x, ty
| PPpapp (x, pl) ->
let s, tyl, ty = specialize_fsymbol x env.uc in
let env, pl = dpat_args s.ls_name loc env tyl pl in
env, Papp (s, pl), ty
| PPptuple pl ->
let n = List.length pl in
let s = fs_tuple n in
let tyl = List.map (fun _ -> fresh_type_var loc) pl in
let env, pl = dpat_args s.ls_name loc env tyl pl in
let ty = Tyapp (ts_tuple n, tyl) in
env, Papp (s, pl), ty
| PPpas (p, {id=x}) ->
let env, p = dpat env p in
let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
......@@ -376,6 +413,13 @@ and dterm_node loc env = function
let s, tyl, ty = specialize_fsymbol x env.uc in
let tl = dtype_args s.ls_name loc env tyl tl in
Tapp (s, tl), ty
| PPtuple tl ->
let n = List.length tl in
let s = fs_tuple n in
let tyl = List.map (fun _ -> fresh_type_var loc) tl in
let tl = dtype_args s.ls_name loc env tyl tl in
let ty = Tyapp (ts_tuple n, tyl) in
Tapp (s, tl), ty
| PPinfix (e1, x, e2) ->
let s, tyl, ty = specialize_fsymbol (Qident x) env.uc in
let tl = dtype_args s.ls_name loc env tyl [e1; e2] in
......@@ -393,10 +437,7 @@ and dterm_node loc env = function
| PPmatch (el, bl) ->
let tl = List.map (dterm env) el in
let tyl = List.map (fun t -> t.dt_ty) tl in
let tb = (* the type of all branches *)
let tv = create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc ~user:false tv)
in
let tb = fresh_type_var loc in (* the type of all branches *)
let branch (pl, e) =
let env, pl = dpat_list env tyl pl in
let loc = e.pp_loc in
......@@ -500,7 +541,7 @@ and dfmla env e = match e.pp_desc with
Fnamed (x, f1)
| PPvar x ->
Fvar (snd (find_prop x env.uc))
| PPeps _ | PPconst _ | PPcast _ ->
| PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
error ~loc:e.pp_loc PredicateExpected
and dpat_list env tyl pl =
......@@ -683,10 +724,14 @@ let add_types dl th =
| Qident _ | Qdot _ ->
find_tysymbol q th
in
try
begin try
ty_app ts (List.map apply tyl)
with Ty.BadTypeArity (tsal, tyll) ->
error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
end
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
ty_app ts (List.map apply tyl)
in
create_tysymbol id vl (Some (apply ty))
| TDabstract | TDalgebraic _ ->
......
......@@ -50,7 +50,7 @@ val specialize_fsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
val specialize_tysymbol :
Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol * Denv.type_var list
Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol * int
type denv
......
......@@ -73,8 +73,10 @@ let type_file file =
let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
let th = Env.find_theory env ["programs"] "Prelude" in
let uc = Theory.use_export uc th in
let _uc, _dl = Pgm_typing.file env uc p in
let uc, _dl = Pgm_typing.file env uc p in
if !type_only then raise Exit;
let th = Theory.close_theory uc in
printf "%a@." Pretty.print_theory th;
()
let handle_file file =
......
......@@ -107,3 +107,11 @@ struct
module W = Hashweak.Make(X)
end
(* memoization *)
let memo ?(size=17) f =
let h = Hashtbl.create size in
fun x -> try Hashtbl.find h x
with Not_found -> let y = f x in Hashtbl.add h x y; y
......@@ -94,3 +94,6 @@ sig
module W : Hashweak.S with type key = X.t
end
(* memoization *)
val memo : ?size:int -> ('a -> 'b) -> 'a -> 'b
......@@ -20,6 +20,22 @@ theory Test
goal G : (forall x:int.x=x) or
(forall x:int. x=x+1)
goal G2 : forall x:int. let x = 0 + 1 in x = 1
type t = int * real
logic c : t = (1, 3.14)
use import list.List
axiom A :
let x = 1 in
let (y,z) = c in
x = y
end
theory Test2
use import Test
logic d : t = (2, 6.3)
end
theory Test_simplify_array
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment