diff --git a/bench/typing/bad/cast1.why b/bench/typing/bad/cast1.why new file mode 100644 index 0000000000000000000000000000000000000000..4875b929f1384760d0b42e53631791a6a5c11145 --- /dev/null +++ b/bench/typing/bad/cast1.why @@ -0,0 +1,3 @@ +theory Test + axiom A : forall x:int. (x : real) = x +end diff --git a/bench/typing/bad/linearity1.why b/bench/typing/bad/linearity1.why new file mode 100644 index 0000000000000000000000000000000000000000..a45bf180ff81f90e33978a9211dcb95d4d8dedc7 --- /dev/null +++ b/bench/typing/bad/linearity1.why @@ -0,0 +1,3 @@ +theory Test + axiom A : forall x,x:int. x=x +end diff --git a/src/parser/parser.mly b/src/parser/parser.mly index dcba8f8421c9d9537f8a22f4d1651fff56e1d083..2ac2c874643666a0b81c95e4d147a7e15e672994 100644 --- a/src/parser/parser.mly +++ b/src/parser/parser.mly @@ -439,12 +439,14 @@ lexpr: { mk_pp PPfalse } | LEFTPAR lexpr RIGHTPAR { $2 } -| ident_or_string COLON lexpr %prec prec_named - { mk_pp (PPnamed ($1, $3)) } +| STRING lexpr %prec prec_named + { mk_pp (PPnamed ($1, $2)) } | LET lident EQUAL lexpr IN lexpr { mk_pp (PPlet ($2, $4, $6)) } | MATCH lexpr WITH bar_ match_cases END { mk_pp (PPmatch ($2, $5)) } +| lexpr COLON primitive_type + { mk_pp (PPcast ($1, $3)) } ; list1_uquant_sep_comma: @@ -503,11 +505,6 @@ list1_type_var_sep_comma: | type_var COMMA list1_type_var_sep_comma { $1 :: $3 } ; -ident_or_string: -| ident { $1.id } -| STRING { $1 } -; - bar_: | /* epsilon */ { () } | BAR { () } diff --git a/src/parser/ptree.mli b/src/parser/ptree.mli index 39e7856504cb073afc8c4f9734bf200df4d349a8..f9f6ebabc1e4b57c092138768a91594d40905d3a 100644 --- a/src/parser/ptree.mli +++ b/src/parser/ptree.mli @@ -73,6 +73,7 @@ and pp_desc = | PPnamed of string * lexpr | PPlet of ident * lexpr * lexpr | PPmatch of lexpr * (pattern * lexpr) list + | PPcast of lexpr * pty (*s Declarations. *) diff --git a/src/parser/typing.ml b/src/parser/typing.ml index d45a0f90b34e6e88356912733f90a74b61e53381..fa4aba60a31d9c071d29608431b59e9f7a1061f4 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -38,8 +38,6 @@ type error = | PredicateExpected | TermExpected | UnboundSymbol of string - | TermExpectedType of (formatter -> unit) * (formatter -> unit) - (* actual / expected *) | BadNumberOfArguments of Ident.ident * int * int | ClashTheory of string | ClashNamespace of string @@ -98,9 +96,6 @@ let report fmt = function | BadNumberOfArguments (s, n, m) -> fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n; fprintf fmt "but is expecting %d arguments@]" m - | TermExpectedType (ty1, ty2) -> - fprintf fmt "@[This term has type "; ty1 fmt; - fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]" | ClashTheory s -> fprintf fmt "clash with previous theory %s" s | ClashNamespace s -> @@ -179,6 +174,11 @@ let rec print_dty fmt = function fprintf fmt "(%a) %s" (print_list comma print_dty) l s.ts_name.id_short +let term_expected_type ~loc ty1 ty2 = + errorm ~loc + "@[This term has type %a@ but is expected to have type@ %a@]" + print_dty ty1 print_dty ty2 + let create_type_var = let t = ref 0 in fun ?loc ~user tv -> @@ -505,6 +505,12 @@ and dterm_node loc env = function | PPnamed (x, e1) -> let e1 = dterm env e1 in Tnamed (x, e1), e1.dt_ty + | PPcast (e1, ty) -> + let loc = e1.pp_loc in + let e1 = dterm env e1 in + let ty = dty env ty in + if not (unify e1.dt_ty ty) then term_expected_type ~loc e1.dt_ty ty; + e1.dt_node, ty | PPquant _ | PPif _ | PPprefix _ | PPinfix _ | PPfalse | PPtrue -> error ~loc TermExpected @@ -568,7 +574,7 @@ and dfmla env e = match e.pp_desc with Fnamed (x, f1) | PPvar _ -> assert false (* TODO *) - | PPconst _ -> + | PPconst _ | PPcast _ -> error ~loc:e.pp_loc PredicateExpected and dtype_args s loc env el tl = @@ -580,9 +586,7 @@ and dtype_args s loc env el tl = | a :: al, t :: bl -> let loc = t.pp_loc in let t = dterm env t in - if not (unify a t.dt_ty) then - error ~loc (TermExpectedType ((fun f -> print_dty f t.dt_ty), - (fun f -> print_dty f a))); + if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a; t :: check_arg (al, bl) | _ -> assert false @@ -853,9 +857,7 @@ let add_logics loc dl th = in let env = env_of_vsymbol_list vl in try Some (make_fs_defn fs vl (term env t)) - with _ -> error ~loc (TermExpectedType - ((fun f -> print_dty f t.dt_ty), - (fun f -> print_dty f (dty denv ty)))) + with _ -> term_expected_type ~loc t.dt_ty (dty denv ty) in Lfunction (fs, defn) in diff --git a/src/test.why b/src/test.why index 67a6949db96eb992df4266472a287c7a80db3453..f4870eb939b0aff7c9b815d058f40dff64023d77 100644 --- a/src/test.why +++ b/src/test.why @@ -4,7 +4,7 @@ theory A use import prelude.Int logic p(int, int) - axiom A : forall x,y:int, z,t:real. x=x + axiom A : forall x:int. x = x end theory TreeForest