From 460e93f8fbbb41ffb52ebb94ee99363daed042c0 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Sat, 19 Oct 2013 21:31:42 +0200 Subject: [PATCH] switch Typing to the new Dterm-based API Also: - Make [Highord.pred 'a] an alias for [Highord.func 'a bool], rename [Highorg.(@!)] to [(@)], remove [Highorg.(@?)], remove the quantifiers [\!] and [\?] and only leave [\] which is the only true lambda now; - Allow mixing bool and Prop in logic, Dterm will introduce coercions where necessary (trying to minimize the number of if-then-else in the term context). --- Makefile.in | 2 +- drivers/ocaml.drv | 3 +- src/core/dterm.ml | 246 ++++++---- src/core/dterm.mli | 26 +- src/core/term.ml | 15 +- src/core/term.mli | 11 +- src/core/theory.ml | 2 +- src/core/ty.ml | 6 +- src/core/ty.mli | 2 +- src/parser/denv.ml | 318 ------------ src/parser/denv.mli | 84 ---- src/parser/lexer.mll | 4 - src/parser/parser.mly | 211 ++++---- src/parser/ptree.ml | 6 +- src/parser/typing.ml | 1008 +++++++++++++-------------------------- src/parser/typing.mli | 3 +- src/whyml/mlw_typing.ml | 84 ++-- 17 files changed, 684 insertions(+), 1347 deletions(-) delete mode 100644 src/parser/denv.ml delete mode 100644 src/parser/denv.mli diff --git a/Makefile.in b/Makefile.in index 269380ee6..ac2358063 100644 --- a/Makefile.in +++ b/Makefile.in @@ -113,7 +113,7 @@ LIB_UTIL = config util opt lists strings extmap extset exthtbl weakhtbl \ LIB_CORE = ident ty term pattern decl theory \ task pretty dterm env trans printer -LIB_PARSER = ptree denv glob parser typing lexer +LIB_PARSER = ptree glob parser typing lexer LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \ whyconf autodetection diff --git a/drivers/ocaml.drv b/drivers/ocaml.drv index 126a04ad0..4dd9ab84a 100644 --- a/drivers/ocaml.drv +++ b/drivers/ocaml.drv @@ -8,8 +8,7 @@ end theory HighOrd syntax type func "((%1) -> (%2))" syntax type pred "((%1) -> bool)" - syntax function (@!) "((%1) (%2))" - syntax predicate (@?) "((%1) (%2))" + syntax function (@) "((%1) (%2))" end theory option.Option diff --git a/src/core/dterm.ml b/src/core/dterm.ml index 7a2fd08d5..99ef400ec 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -30,12 +30,17 @@ let dty_fresh = let i = ref 0 in fun () -> Dvar (ref (Dind (incr i; !i))) let dty_of_ty ty = Duty ty let rec ty_of_dty ~strict = function - | Dvar { contents = Dval dty } -> ty_of_dty ~strict dty + | Dvar { contents = Dval (Duty ty) } -> + ty + | Dvar ({ contents = Dval dty } as r) -> + let ty = ty_of_dty ~strict dty in + r := Dval (Duty ty); ty | Dvar r -> - if strict then Loc.errorm "undefined type variable"; - let ty = ty_var (create_tvsymbol (id_fresh "xi")) in - r := Dval (Duty ty); ty - | Dapp (ts,dl) -> ty_app ts (List.map (ty_of_dty ~strict) dl) + if strict then Loc.errorm "undefined type variable"; + let ty = ty_var (create_tvsymbol (id_fresh "xi")) in + r := Dval (Duty ty); ty + | Dapp (ts,dl) -> + ty_app ts (List.map (ty_of_dty ~strict) dl) | Duty ty -> ty let rec occur_check i = function @@ -65,12 +70,9 @@ let rec dty_unify dty1 dty2 = match dty1,dty2 with List.iter2 dty_unify dl1 dl2 | _ -> raise Exit -(* -exception DTypeMismatch of dty * dty - -let dty_unify dty1 dty2 = - try dty_unify dty1 dty2 with Exit -> raise (DTypeMismatch (dty1,dty2)) -*) +let dty_int = Duty ty_int +let dty_real = Duty ty_real +let dty_bool = Duty ty_bool let rec print_dty ht inn fmt = function | Dvar { contents = Dval dty } -> @@ -147,13 +149,12 @@ and dpattern_node = type dterm = { dt_node : dterm_node; dt_dty : dty option; - dt_label : Slab.t; dt_loc : Loc.position option; - dt_uloc : Loc.position option; } and dterm_node = - | DTvar of string + | DTvar of string * dty + | DTgvar of vsymbol | DTconst of Number.constant | DTapp of lsymbol * dterm list | DTif of dterm * dterm * dterm @@ -165,54 +166,62 @@ and dterm_node = | DTnot of dterm | DTtrue | DTfalse + | DTcast of dterm * ty + | DTuloc of dterm * Loc.position + | DTlabel of dterm * Slab.t (** Environment *) -type denv = dty Mstr.t +type denv = dterm_node Mstr.t exception TermExpected exception FmlaExpected exception DuplicateVar of string exception UnboundVar of string -let denv_get_var ?loc denv n = - let dty = Mstr.find_exn (UnboundVar n) n denv in - { dt_node = DTvar n; - dt_dty = Some dty; - dt_label = Slab.empty; - dt_loc = loc; - dt_uloc = None } +let denv_get denv n = Mstr.find_exn (UnboundVar n) n denv + +let denv_get_opt denv n = Mstr.find_opt n denv let dty_of_dterm dt = match dt.dt_dty with | None -> Loc.error ?loc:dt.dt_loc TermExpected | Some dty -> dty +let denv_empty = Mstr.empty + let denv_add_var denv id dty = - Mstr.add (preid_name id) dty denv + let n = preid_name id in + Mstr.add n (DTvar (n, dty)) denv let denv_add_let denv dt id = - Mstr.add (preid_name id) (dty_of_dterm dt) denv + let n = preid_name id in + Mstr.add n (DTvar (n, dty_of_dterm dt)) denv let denv_add_quant denv vl = let add acc (id,dty) = let n = preid_name id in - Mstr.add_new (DuplicateVar n) n dty acc in + Mstr.add_new (DuplicateVar n) n (DTvar (n, dty)) acc in let s = List.fold_left add Mstr.empty vl in Mstr.set_union s denv let denv_add_pat denv dp = let rec get dp = match dp.dp_node with | DPwild -> Mstr.empty - | DPvar id -> Mstr.singleton (preid_name id) dp.dp_dty + | DPvar id -> + let n = preid_name id in + Mstr.singleton n (DTvar (n, dp.dp_dty)) | DPapp (_,dpl) -> let join n _ _ = raise (DuplicateVar n) in let add acc dp = Mstr.union join acc (get dp) in List.fold_left add Mstr.empty dpl | DPor (dp1,dp2) -> - let join _ dty1 dty2 = dty_unify dty1 dty2; Some dty1 in + let join _ dtn1 dtn2 = match dtn1, dtn2 with + | DTvar (_,dty1), DTvar (_,dty2) -> dty_unify dty1 dty2; Some dtn1 + | _ -> assert false in Mstr.union join (get dp1) (get dp2) | DPas (dp,id) -> let n = preid_name id in - Mstr.add_new (DuplicateVar n) n dp.dp_dty (get dp) in + Mstr.add_new (DuplicateVar n) n (DTvar (n, dp.dp_dty)) (get dp) + in Mstr.set_union (get dp) denv (** Unification tools *) @@ -233,13 +242,17 @@ let darg_expected_type ?loc dt_dty dty = let dterm_expected_type dt dty = match dt.dt_dty with | Some dt_dty -> darg_expected_type ?loc:dt.dt_loc dt_dty dty - | None -> Loc.error ?loc:dt.dt_loc TermExpected + | None -> begin try dty_unify dty_bool dty with Exit -> + Loc.error ?loc:dt.dt_loc TermExpected end -let dfmla_expected_type dt dty = match dt.dt_dty, dty with - | Some dt_dty, Some dty -> darg_expected_type ?loc:dt.dt_loc dt_dty dty - | Some _, None -> Loc.error ?loc:dt.dt_loc FmlaExpected - | None, Some _ -> Loc.error ?loc:dt.dt_loc TermExpected - | None, None -> () +let dfmla_expected_type dt = match dt.dt_dty with + | Some dt_dty -> begin try dty_unify dt_dty dty_bool with Exit -> + Loc.error ?loc:dt.dt_loc FmlaExpected end + | None -> () + +let dexpr_expected_type dt dty = match dty with + | Some dty -> dterm_expected_type dt dty + | None -> dfmla_expected_type dt (** Constructors *) @@ -261,17 +274,22 @@ let dpattern ?loc node = let dterm ?loc node = let get_dty = function - | DTvar _ -> Loc.errorm "Invalid argument, use Dterm.denv_get_var" - | DTconst (Number.ConstInt _) -> Some (dty_of_ty ty_int) - | DTconst (Number.ConstReal _) -> Some (dty_of_ty ty_real) + | DTvar (_,dty) -> + Some dty + | DTgvar vs -> + Some (dty_of_ty vs.vs_ty) + | DTconst (Number.ConstInt _) -> + Some dty_int + | DTconst (Number.ConstReal _) -> + Some dty_real | DTapp (ls,dtl) -> let dtyl, dty = specialize_ls ls in dty_unify_app ls dterm_expected_type dtl dtyl; dty | DTif (df,dt1,dt2) -> - dfmla_expected_type df None; - dfmla_expected_type dt2 dt1.dt_dty; - dt1.dt_dty + dfmla_expected_type df; + dexpr_expected_type dt2 dt1.dt_dty; + if dt2.dt_dty = None then None else dt1.dt_dty | DTlet (dt,_,df) -> ignore (dty_of_dterm dt); df.dt_dty @@ -281,41 +299,38 @@ let dterm ?loc node = dterm_expected_type dt dp1.dp_dty; let check (dp,df) = dpat_expected_type dp dp1.dp_dty; - dfmla_expected_type df df1.dt_dty in + dexpr_expected_type df df1.dt_dty in List.iter check bl; - df1.dt_dty + let is_fmla (_,df) = df.dt_dty = None in + if List.exists is_fmla bl then None else df1.dt_dty | DTeps (_,dty,df) -> - dfmla_expected_type df None; + dfmla_expected_type df; Some dty | DTquant (_,_,_,df) -> - dfmla_expected_type df None; + dfmla_expected_type df; None | DTbinop (_,df1,df2) -> - dfmla_expected_type df1 None; - dfmla_expected_type df2 None; + dfmla_expected_type df1; + dfmla_expected_type df2; None | DTnot df -> - dfmla_expected_type df None; + dfmla_expected_type df; None | DTtrue | DTfalse -> - None - in + (* we put here [Some dty_bool] instead of [None] because we can + always replace [true] by [True] and [false] by [False], so that + there is no need to count these constructs as "formulas" which + require explicit if-then-else conversion to bool *) + Some dty_bool + | DTcast (dt,ty) -> + let dty = dty_of_ty ty in + dterm_expected_type dt dty; + Some dty + | DTuloc (dt,_) + | DTlabel (dt,_) -> + dt.dt_dty in let dty = Loc.try1 ?loc get_dty node in - { dt_node = node; dt_dty = dty; - dt_label = Slab.empty; - dt_loc = loc; dt_uloc = None } - -let dterm_type_cast dt ty = - dterm_expected_type dt (dty_of_ty ty); dt - -let dterm_add_label dt lab = - { dt with dt_label = Slab.add lab dt.dt_label } - -let dterm_set_labels dt slab = - { dt with dt_label = slab } - -let dterm_set_uloc dt loc = - { dt with dt_uloc = Some loc } + { dt_node = node; dt_dty = dty; dt_loc = loc } (** Final stage *) @@ -363,55 +378,108 @@ let check_exists_implies q f = match q, f.t_node with "form \"exists x. P -> Q\" is likely an error (use \"not P \\/ Q\" if not)" | _ -> () -let term ~strict ~keep_loc env dt = - let rec get uloc env dt = - let uloc = if dt.dt_uloc = None then uloc else dt.dt_uloc in - let t = Loc.try4 ?loc:dt.dt_loc try_get uloc env dt.dt_dty dt.dt_node in - let loc = if keep_loc then dt.dt_loc else None in - let loc = if uloc = None then loc else uloc in - if loc = None && Slab.is_empty dt.dt_label - then t else t_label ?loc dt.dt_label t - and try_get uloc env dty = function - | DTvar n -> +let term ~strict ~keep_loc env prop dt = + let t_label loc labs t = + if loc = None && Slab.is_empty labs + then t else t_label ?loc labs t in + + let rec strip uloc labs dt = match dt.dt_node with + | DTcast (dt,_) -> strip uloc labs dt + | DTuloc (dt,loc) -> strip (Some loc) labs dt + | DTlabel (dt,s) -> strip uloc (Slab.union labs s) dt + | _ -> uloc, labs, dt in + + let rec get uloc env prop dt = + let uloc, labs, dt = strip uloc Slab.empty dt in + let tloc = if keep_loc then dt.dt_loc else None in + let tloc = if uloc <> None then uloc else tloc in + let t = t_label tloc labs (Loc.try5 ?loc:dt.dt_loc + try_get uloc env prop dt.dt_dty dt.dt_node) in + match t.t_ty with + | Some _ when prop -> t_label tloc Slab.empty + (Loc.try2 ?loc:dt.dt_loc t_equ t t_bool_true) + | None when not prop -> t_label tloc Slab.empty + (t_if t t_bool_true t_bool_false) + | _ -> t + + and try_get uloc env prop dty = function + | DTvar (n,_) -> t_var (Mstr.find_exn (UnboundVar n) n env) + | DTgvar vs -> + t_var vs | DTconst c -> t_const c + | DTapp (ls,[]) when ls_equal ls fs_bool_true -> + if prop then t_true else t_bool_true + | DTapp (ls,[]) when ls_equal ls fs_bool_false -> + if prop then t_false else t_bool_false + | DTapp (ls,[dt1;dt2]) when ls_equal ls ps_equ -> + (* avoid putting formulas into a term context *) + if dt1.dt_dty = None || dt2.dt_dty = None + then t_iff (get uloc env true dt1) (get uloc env true dt2) + else t_equ (get uloc env false dt1) (get uloc env false dt2) | DTapp (ls,dtl) -> - t_app ls (List.map (get uloc env) dtl) (Opt.map (ty_of_dty ~strict) dty) - | DTif (df,dt1,dt2) -> - t_if (get uloc env df) (get uloc env dt1) (get uloc env dt2) + t_app ls (List.map (get uloc env false) dtl) + (Opt.map (ty_of_dty ~strict) dty) | DTlet (dt,id,df) -> - let t = get uloc env dt in + let prop = prop || dty = None in + let t = get uloc env false dt in let v = create_vsymbol id (t_type t) in let env = Mstr.add (preid_name id) v env in - let f = get uloc env df in + let f = get uloc env prop df in check_used_var f.t_vars v; t_let_close v t f + | DTif (df,dt1,dt2) -> + let prop = prop || dty = None in + t_if (get uloc env true df) + (get uloc env prop dt1) (get uloc env prop dt2) | DTcase (dt,bl) -> + let prop = prop || dty = None in let branch (dp,df) = let env, p = pattern ~strict env dp in - let f = get uloc env df in + let f = get uloc env prop df in Svs.iter (check_used_var f.t_vars) p.pat_vars; t_close_branch p f in - t_case (get uloc env dt) (List.map branch bl) + t_case (get uloc env false dt) (List.map branch bl) | DTeps (id,dty,df) -> let v = create_vsymbol id (ty_of_dty ~strict dty) in let env = Mstr.add (preid_name id) v env in - let f = get uloc env df in + let f = get uloc env true df in check_used_var f.t_vars v; t_eps_close v f | DTquant (q,vl,dll,df) -> let env, vl = quant_vars ~strict env vl in - let trl = List.map (List.map (get uloc env)) dll in - let f = get uloc env df in + let tr_get dt = get uloc env (dt.dt_dty = None) dt in + let trl = List.map (List.map tr_get) dll in + let f = get uloc env true df in List.iter (check_used_var f.t_vars) vl; check_exists_implies q f; t_quant_close q vl trl f | DTbinop (op,df1,df2) -> - t_binary op (get uloc env df1) (get uloc env df2) + t_binary op (get uloc env true df1) (get uloc env true df2) | DTnot df -> - t_not (get uloc env df) - | DTtrue -> t_true - | DTfalse -> t_false + t_not (get uloc env true df) + | DTtrue -> + if prop then t_true else t_bool_true + | DTfalse -> + if prop then t_false else t_bool_false + | DTcast _ | DTuloc _ | DTlabel _ -> + assert false (* already stripped *) in - get None env dt + get None env prop dt + +let fmla ~strict ~keep_loc env dt = term ~strict ~keep_loc env true dt +let term ~strict ~keep_loc env dt = term ~strict ~keep_loc env false dt + +(** Exception printer *) + +let () = Exn_printer.register (fun fmt e -> match e with + | TermExpected -> + Format.fprintf fmt "syntax error: term expected" + | FmlaExpected -> + Format.fprintf fmt "syntax error: formula expected" + | DuplicateVar s -> + Format.fprintf fmt "duplicate variable %s" s + | UnboundVar s -> + Format.fprintf fmt "unbound variable %s" s + | _ -> raise e) diff --git a/src/core/dterm.mli b/src/core/dterm.mli index 36065d339..6bdb9730e 100644 --- a/src/core/dterm.mli +++ b/src/core/dterm.mli @@ -40,13 +40,12 @@ and dpattern_node = type dterm = private { dt_node : dterm_node; dt_dty : dty option; - dt_label : Slab.t; dt_loc : Loc.position option; - dt_uloc : Loc.position option; } and dterm_node = - | DTvar of string + | DTvar of string * dty + | DTgvar of vsymbol | DTconst of Number.constant | DTapp of lsymbol * dterm list | DTif of dterm * dterm * dterm @@ -58,6 +57,9 @@ and dterm_node = | DTnot of dterm | DTtrue | DTfalse + | DTcast of dterm * ty + | DTuloc of dterm * Loc.position + | DTlabel of dterm * Slab.t (** Environment *) @@ -66,7 +68,9 @@ exception FmlaExpected exception DuplicateVar of string exception UnboundVar of string -type denv (** bound variables *) +type denv = dterm_node Mstr.t (** bound variables *) + +val denv_empty : denv (** Mstr.empty *) val denv_add_var : denv -> preid -> dty -> denv @@ -76,7 +80,9 @@ val denv_add_quant : denv -> (preid * dty) list -> denv val denv_add_pat : denv -> dpattern -> denv -val denv_get_var : ?loc:Loc.position -> denv -> string -> dterm +val denv_get : denv -> string -> dterm_node (** raises UnboundVar *) + +val denv_get_opt : denv -> string -> dterm_node option (** Constructors *) @@ -84,15 +90,7 @@ val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern val dterm : ?loc:Loc.position -> dterm_node -> dterm -val dterm_type_cast : dterm -> ty -> dterm - -val dterm_add_label : dterm -> label -> dterm - -val dterm_set_labels : dterm -> Slab.t -> dterm - -val dterm_set_uloc : dterm -> Loc.position -> dterm - (** Final stage *) val term : strict:bool -> keep_loc:bool -> vsymbol Mstr.t -> dterm -> term - +val fmla : strict:bool -> keep_loc:bool -> vsymbol Mstr.t -> dterm -> term diff --git a/src/core/term.ml b/src/core/term.ml index c8c0893d9..78fd0f709 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -829,20 +829,13 @@ let t_tuple tl = let fs_func_app = let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in let ty_b = ty_var (create_tvsymbol (id_fresh "b")) in - create_fsymbol (id_fresh "infix @!") [ty_func ty_a ty_b; ty_a] ty_b - -let ps_pred_app = - let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in - create_psymbol (id_fresh "infix @?") [ty_pred ty_a; ty_a] + create_fsymbol (id_fresh "infix @") [ty_func ty_a ty_b; ty_a] ty_b let t_func_app fn t = t_app_infer fs_func_app [fn; t] -let t_pred_app pr t = ps_app ps_pred_app [pr; t] - -let t_func_app_l = List.fold_left t_func_app +let t_pred_app pr t = t_equ (t_func_app pr t) t_bool_true -let t_pred_app_l pr tl = match List.rev tl with - | t::tl -> t_pred_app (t_func_app_l pr (List.rev tl)) t - | _ -> Pervasives.invalid_arg "t_pred_app_l" +let t_func_app_l fn tl = List.fold_left t_func_app fn tl +let t_pred_app_l pr tl = t_equ (t_func_app_l pr tl) t_bool_true (** Term library *) diff --git a/src/core/term.mli b/src/core/term.mli index a70bedcc4..d23892eee 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -297,14 +297,13 @@ val t_tuple : term list -> term val is_fs_tuple : lsymbol -> bool val is_fs_tuple_id : ident -> int option -val fs_func_app : lsymbol (* value-typed higher-order application *) -val ps_pred_app : lsymbol (* prop-typed higher-order application *) +val fs_func_app : lsymbol (* higher-order application symbol *) -val t_func_app : term -> term -> term -val t_pred_app : term -> term -> term +val t_func_app : term -> term -> term (* value-typed application *) +val t_pred_app : term -> term -> term (* prop-typed application *) -val t_func_app_l : term -> term list -> term -val t_pred_app_l : term -> term list -> term +val t_func_app_l : term -> term list -> term (* value-typed application *) +val t_pred_app_l : term -> term list -> term (* prop-typed application *) (** {2 Term library} *) diff --git a/src/core/theory.ml b/src/core/theory.ml index ea32399a2..b46bc631f 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -836,10 +836,10 @@ let bool_theory = let highord_theory = let uc = empty_theory (id_fresh "HighOrd") ["why3"] in + let uc = use_export uc bool_theory in let uc = add_ty_decl uc ts_func in let uc = add_ty_decl uc ts_pred in let uc = add_param_decl uc fs_func_app in - let uc = add_param_decl uc ps_pred_app in close_theory uc let tuple_theory = Hint.memo 17 (fun n -> diff --git a/src/core/ty.ml b/src/core/ty.ml index c9a7c066a..bc8ce6897 100644 --- a/src/core/ty.ml +++ b/src/core/ty.ml @@ -220,11 +220,13 @@ let ts_func = let tv_b = create_tvsymbol (id_fresh "b") in create_tysymbol (id_fresh "func") [tv_a;tv_b] None +let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b] + let ts_pred = let tv_a = create_tvsymbol (id_fresh "a") in - create_tysymbol (id_fresh "pred") [tv_a] None + let def = Some (ty_func (ty_var tv_a) ty_bool) in + create_tysymbol (id_fresh "pred") [tv_a] def -let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b] let ty_pred ty_a = ty_app ts_pred [ty_a] let ts_tuple_ids = Hid.create 17 diff --git a/src/core/ty.mli b/src/core/ty.mli index ba7b6878d..e59334b6f 100644 --- a/src/core/ty.mli +++ b/src/core/ty.mli @@ -115,7 +115,7 @@ val ts_func : tysymbol val ts_pred : tysymbol val ty_func : ty -> ty -> ty -val ty_pred : ty -> ty +val ty_pred : ty -> ty (* ty_pred 'a == ty_func 'a bool *) val ts_tuple : int -> tysymbol val ty_tuple : ty list -> ty diff --git a/src/parser/denv.ml b/src/parser/denv.ml deleted file mode 100644 index 232d5647d..000000000 --- a/src/parser/denv.ml +++ /dev/null @@ -1,318 +0,0 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) -(* *) -(* This software is distributed under the terms of the GNU Lesser *) -(* General Public License version 2.1, with the special exception *) -(* on linking described in file LICENSE. *) -(* *) -(********************************************************************) - -open Format -open Pp -open Stdlib -open Ident -open Ptree -open Ty -open Term - -(** types with destructive type variables *) - -type dty_view = - | Tyvar of type_var - | Tyuvar of tvsymbol - | Tyapp of tysymbol * dty_view list - -and type_var = { - tag : int; - tvsymbol : tvsymbol; - mutable type_val : dty_view option; - type_var_loc : loc option; -} - -let tyuvar tv = Tyuvar tv - -let rec type_inst s ty = match ty.ty_node with - | Ty.Tyvar n -> Mtv.find n s - | Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl) - -let tyapp ts tyl = match ts.ts_def with - | None -> - Tyapp (ts, tyl) - | Some ty -> - let add m v t = Mtv.add v t m in - try - let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in - type_inst s ty - with Invalid_argument _ -> - Loc.errorm "this type expects %d parameters" (List.length ts.ts_args) - -type dty = dty_view - -let rec print_dty fmt = function - | Tyvar { type_val = Some t } -> - print_dty fmt t - | Tyvar { type_val = None; tvsymbol = tv } - | Tyuvar tv -> - Pretty.print_tv fmt tv - | Tyapp (s, []) -> - fprintf fmt "%s" s.ts_name.id_string - | Tyapp (s, [t]) -> - fprintf fmt "%s %a" s.ts_name.id_string print_dty t - | Tyapp (s, l) -> - fprintf fmt "%s %a" s.ts_name.id_string (print_list space print_dty) l - -let create_ty_decl_var = - let t = ref 0 in - fun ?loc tv -> - incr t; - { tag = !t; tvsymbol = tv; type_val = None; type_var_loc = loc } - -let fresh_type_var loc = - let tv = create_tvsymbol (id_user "a" loc) in - Tyvar (create_ty_decl_var ~loc tv) - -let rec occurs v = function - | Tyvar { type_val = Some t } -> occurs v t - | Tyvar { tag = t; type_val = None } -> v.tag = t - | Tyuvar _ -> false - | Tyapp (_, l) -> List.exists (occurs v) l - -(* destructive type unification *) -let rec unify t1 t2 = match t1, t2 with - | Tyvar { type_val = Some t1 }, _ -> - unify t1 t2 - | _, Tyvar { type_val = Some t2 } -> - unify t1 t2 - | Tyvar v1, Tyvar v2 when v1.tag = v2.tag -> - true - (* instantiable variables *) - | Tyvar v, t | t, Tyvar v -> - not (occurs v t) && (v.type_val <- Some t; true) - (* recursive types *) - | Tyapp (s1, l1), Tyapp (s2, l2) -> - ts_equal s1 s2 && List.length l1 = List.length l2 && - List.for_all2 unify l1 l2 - | Tyapp _, _ | _, Tyapp _ -> - false - (* other cases *) - | Tyuvar tv1, Tyuvar tv2 -> - tv_equal tv1 tv2 - -(* intermediate types -> types *) -let rec ty_of_dty = function - | Tyvar { type_val = Some t } -> - ty_of_dty t - | Tyvar { type_val = None; type_var_loc = loc } -> - Loc.errorm ?loc "undefined type variable" - | Tyuvar tv -> - ty_var tv - | Tyapp (s, tl) -> - ty_app s (List.map ty_of_dty tl) - -let rec dty_of_ty ty = match ty.ty_node with - | Ty.Tyvar tv -> Tyuvar tv - | Ty.Tyapp (ts,tl) -> Tyapp (ts, List.map dty_of_ty tl) - -type ident = Ptree.ident - -type dpattern = { dp_node : dpattern_node; dp_ty : dty } - -and dpattern_node = - | Pwild - | Pvar of ident - | Papp of lsymbol * dpattern list - | Por of dpattern * dpattern - | Pas of dpattern * ident - -let create_user_id { id = x ; id_lab = ll ; id_loc = loc } = - let get_labels (ll,p) = function - | Lstr l -> Slab.add l ll, p - | Lpos p -> ll, Some p - in - let label,p = List.fold_left get_labels (Slab.empty,None) ll in - id_user ~label x (Opt.get_def loc p) - -let create_user_vs id ty = create_vsymbol (create_user_id id) ty - -let rec pattern_env env p = match p.dp_node with - | Pwild -> env - | Papp (_, pl) -> List.fold_left pattern_env env pl - | Por (p, _) -> pattern_env env p - | Pvar id -> - let vs = create_user_vs id (ty_of_dty p.dp_ty) in - Mstr.add id.id vs env - | Pas (p, id) -> - let vs = create_user_vs id (ty_of_dty p.dp_ty) in - pattern_env (Mstr.add id.id vs env) p - -let get_pat_var env p x = try Mstr.find x env with Not_found -> - raise (Term.UncoveredVar (create_vsymbol (id_fresh x) (ty_of_dty p.dp_ty))) - -let rec pattern_pat env p = match p.dp_node with - | Pwild -> pat_wild (ty_of_dty p.dp_ty) - | Pvar x -> pat_var (get_pat_var env p x.id) - | Pas (p, x) -> pat_as (pattern_pat env p) (get_pat_var env p x.id) - | Por (p, q) -> pat_or (pattern_pat env p) (pattern_pat env q) - | Papp (s, pl) -> - pat_app s (List.map (pattern_pat env) pl) (ty_of_dty p.dp_ty) - -let pattern env p = let env = pattern_env env p in env, pattern_pat env p - -type dterm = { dt_node : dterm_node; dt_ty : dty } - -and dterm_node = - | Tvar of string - | Tgvar of vsymbol - | Tconst of constant - | Tapp of lsymbol * dterm list - | Tif of dfmla * dterm * dterm - | Tlet of dterm * ident * dterm - | Tmatch of dterm * (dpattern * dterm) list - | Tnamed of label * dterm - | Teps of ident * dty * dfmla - -and dfmla = - | Fapp of lsymbol * dterm list - | Fquant of quant * (ident * dty) list * dtrigger list list * dfmla - | Fbinop of binop * dfmla * dfmla - | Fnot of dfmla - | Ftrue - | Ffalse - | Fif of dfmla * dfmla * dfmla - | Flet of dterm * ident * dfmla - | Fmatch of dterm * (dpattern * dfmla) list - | Fnamed of label * dfmla - | Fvar of term - -and dtrigger = - | TRterm of dterm - | TRfmla of dfmla - -let allowed_unused s = String.length s > 0 && s.[0] = '_' - -let check_used_var vars v = - if not (Mvs.mem v vars) then - let s = v.vs_name.id_string in - if not (allowed_unused s) then - Warning.emit ?loc:v.vs_name.Ident.id_loc "unused variable %s" s - -let check_used_vars vars = - List.iter (check_used_var vars) - -let check_exists_implies q f = - match q,f.t_node with - | Texists, Tbinop(Timplies, _,_) -> - Warning.emit ?loc:f.t_loc "form \"exists, P -> Q\" is likely an error (use \"not P \\/ Q\" if not)" - | _ -> () - -let rec term env t = match t.dt_node with - | Tvar x -> - assert (Mstr.mem x env); - t_var (Mstr.find x env) - | Tgvar vs -> - t_var vs - | Tconst c -> - t_const c - | Tapp (s, tl) -> - fs_app s (List.map (term env) tl) (ty_of_dty t.dt_ty) - | Tif (f, t1, t2) -> - t_if (fmla env f) (term env t1) (term env t2) - | Tlet (e1, id, e2) -> - let e1 = term env e1 in - let v = create_user_vs id (t_type e1) in - let env = Mstr.add id.id v env in - let e2 = term env e2 in - check_used_var e2.t_vars v; - t_let_close v e1 e2 - | Tmatch (t1, bl) -> - let branch (p,e) = - let env, p = pattern env p in t_close_branch p (term env e) - in - t_case (term env t1) (List.map branch bl) - | Tnamed _ -> - let rec collect p ll e = match e.dt_node with - | Tnamed (Lstr l, e) -> collect p (Slab.add l ll) e - | Tnamed (Lpos p, e) -> collect (Some p) ll e - | _ -> t_label ?loc:p ll (term env e) - in - collect None Slab.empty t - | Teps (id, ty, e1) -> - let v = create_user_vs id (ty_of_dty ty) in - let env = Mstr.add id.id v env in - let e1 = fmla env e1 in - t_eps_close v e1 - -and fmla env = function - | Ftrue -> - t_true - | Ffalse -> - t_false - | Fnot f -> - t_not (fmla env f) - | Fbinop (op, f1, f2) -> - t_binary op (fmla env f1) (fmla env f2) - | Fif (f1, f2, f3) -> - t_if (fmla env f1) (fmla env f2) (fmla env f3) - | Fquant (q, uqu, trl, f1) -> - let uquant env (id,ty) = - let v = create_user_vs id (ty_of_dty ty) in - Mstr.add id.id v env, v - in - let env, vl = Lists.map_fold_left uquant env uqu in - let trigger = function - | TRterm t -> term env t - | TRfmla f -> fmla env f - in - let trl = List.map (List.map trigger) trl in - let f = fmla env f1 in - check_used_vars f.Term.t_vars vl; - check_exists_implies q f; - t_quant_close q vl trl f - | Fapp (s, tl) -> - ps_app s (List.map (term env) tl) - | Flet (e1, id, f2) -> - let e1 = term env e1 in - let v = create_user_vs id (t_type e1) in - let env = Mstr.add id.id v env in - let f2 = fmla env f2 in - check_used_var f2.t_vars v; - t_let_close v e1 f2 - | Fmatch (t, bl) -> - let branch (p,e) = - let env, p = pattern env p in t_close_branch p (fmla env e) - in - t_case (term env t) (List.map branch bl) - | (Fnamed _) as f -> - let rec collect p ll = function - | Fnamed (Lstr l, e) -> collect p (Slab.add l ll) e - | Fnamed (Lpos p, e) -> collect (Some p) ll e - | e -> t_label ?loc:p ll (fmla env e) - in - collect None Slab.empty f - | Fvar f -> - f - -(* Specialize *) - -let find_type_var ~loc env tv = - try - Htv.find env tv - with Not_found -> - let v = create_ty_decl_var ~loc tv in - Htv.add env tv v; - v - -let rec specialize_ty ~loc env t = match t.ty_node with - | Ty.Tyvar tv -> - Tyvar (find_type_var ~loc env tv) - | Ty.Tyapp (s, tl) -> - Tyapp (s, List.map (specialize_ty ~loc env) tl) - -let specialize_lsymbol ~loc s = - let tl = s.ls_args in - let t = s.ls_value in - let env = Htv.create 17 in - List.map (specialize_ty ~loc env) tl, Opt.map (specialize_ty ~loc env) t - diff --git a/src/parser/denv.mli b/src/parser/denv.mli deleted file mode 100644 index 5b4fff35c..000000000 --- a/src/parser/denv.mli +++ /dev/null @@ -1,84 +0,0 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) -(* *) -(* This software is distributed under the terms of the GNU Lesser *) -(* General Public License version 2.1, with the special exception *) -(* on linking described in file LICENSE. *) -(* *) -(********************************************************************) - -open Stdlib -open Ty -open Term -open Theory - -(** Destructive unification *) - -type dty - -val tyuvar : tvsymbol -> dty -val tyapp : tysymbol -> dty list -> dty - -val fresh_type_var : Ptree.loc -> dty - -val unify : dty -> dty -> bool - -val print_dty : Format.formatter -> dty -> unit - -val ty_of_dty : dty -> ty -val dty_of_ty : ty -> dty - -type ident = Ptree.ident - -val create_user_id : Ptree.ident -> Ident.preid - -type dpattern = { dp_node : dpattern_node; dp_ty : dty } - -and dpattern_node = - | Pwild - | Pvar of ident - | Papp of lsymbol * dpattern list - | Por of dpattern * dpattern - | Pas of dpattern * ident - -val pattern : vsymbol Mstr.t -> dpattern -> vsymbol Mstr.t * pattern - -type dterm = { dt_node : dterm_node; dt_ty : dty } - -and dterm_node = - | Tvar of string - | Tgvar of vsymbol - | Tconst of Number.constant - | Tapp of lsymbol * dterm list - | Tif of dfmla * dterm * dterm - | Tlet of dterm * ident * dterm - | Tmatch of dterm * (dpattern * dterm) list - | Tnamed of Ptree.label * dterm - | Teps of ident * dty * dfmla - -and dfmla = - | Fapp of lsymbol * dterm list - | Fquant of quant * (ident * dty) list * dtrigger list list * dfmla - | Fbinop of binop * dfmla * dfmla - | Fnot of dfmla - | Ftrue - | Ffalse - | Fif of dfmla * dfmla * dfmla - | Flet of dterm * ident * dfmla - | Fmatch of dterm * (dpattern * dfmla) list - | Fnamed of Ptree.label * dfmla - | Fvar of term - -and dtrigger = - | TRterm of dterm - | TRfmla of dfmla - -val term : vsymbol Mstr.t -> dterm -> term - -val fmla : vsymbol Mstr.t -> dfmla -> term - -(** Specialization *) - -val specialize_lsymbol : loc:Ptree.loc -> lsymbol -> dty list * dty option diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll index ccea6c5a5..c15628e61 100644 --- a/src/parser/lexer.mll +++ b/src/parser/lexer.mll @@ -240,10 +240,6 @@ rule token = parse { OR } | "\\" { LAMBDA } - | "\\?" - { PRED } - | "\\!" - { FUNC } | "." { DOT } | "|" diff --git a/src/parser/parser.mly b/src/parser/parser.mly index 9cce37ac1..0e3b3d239 100644 --- a/src/parser/parser.mly +++ b/src/parser/parser.mly @@ -37,13 +37,6 @@ end let floc_ij i j = Loc.extract (loc_ij i j) *) - let pty_of_id i = PPTtyapp (Qident i, []) - - let params_of_binders bl = List.map (function - | l, None, _, None -> Loc.errorm ~loc:l "cannot determine the type" - | l, Some i, gh, None -> l, None, gh, pty_of_id i - | l, i, gh, Some t -> l, i, gh, t) bl - let quvars_of_lidents ty ll = List.map (function | l, None -> Loc.errorm ~loc:l "anonymous binders are not allowed here" | _, Some i -> i, ty) ll @@ -69,6 +62,10 @@ end let add_lab id l = { id with id_lab = l } + let rec mk_l_apply f a = + let loc = Loc.join f.pp_loc a.pp_loc in + { pp_loc = loc; pp_desc = PPhoapp (f,a) } + let mk_l_prefix op e1 = let id = mk_id (prefix op) (floc_i 1) in mk_pp (PPapp (Qident id, [e1])) @@ -207,9 +204,9 @@ end %token AND ARROW %token BAR %token COLON COMMA -%token DOT EQUAL FUNC LAMBDA LTGT +%token DOT EQUAL LAMBDA LTGT %token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ -%token LARROW LRARROW OR PRED +%token LARROW LRARROW OR %token RIGHTPAR RIGHTSQ %token UNDERSCORE @@ -568,13 +565,9 @@ indcase: /* Type expressions */ primitive_type: -| primitive_type_arg { $1 } -| lqualid primitive_type_args { PPTtyapp ($1, $2) } -; - -primitive_type_non_lident: -| primitive_type_arg_non_lident { $1 } -| uqualid DOT lident primitive_type_args { PPTtyapp (Qdot ($1, $3), $4) } +| primitive_type_arg { $1 } +| lqualid primitive_type_args { PPTtyapp ($1, $2) } +| primitive_type ARROW primitive_type { PPTarrow ($1, $3) } ; primitive_type_args: @@ -582,19 +575,9 @@ primitive_type_args: | primitive_type_arg primitive_type_args { $1 :: $2 } ; -primitive_type_args_non_lident: -| primitive_type_arg_non_lident { [$1] } -| primitive_type_arg_non_lident primitive_type_args { $1 :: $2 } -; - primitive_type_arg: -| lident { PPTtyapp (Qident $1, []) } -| primitive_type_arg_non_lident { $1 } -; - -primitive_type_arg_non_lident: -| uqualid DOT lident - { PPTtyapp (Qdot ($1, $3), []) } +| lqualid + { PPTtyapp ($1, []) } | quote_lident { PPTtyvar ($1, false) } | opaque_quote_lident @@ -604,7 +587,7 @@ primitive_type_arg_non_lident: | LEFTPAR RIGHTPAR { PPTtuple [] } | LEFTPAR primitive_type RIGHTPAR - { $2 } + { PPTparen $2 } ; list1_primitive_type_sep_comma: @@ -645,6 +628,8 @@ lexpr: { mk_l_prefix $1 $2 } | qualid list1_lexpr_arg { mk_pp (PPapp ($1, $2)) } +| lexpr_arg_noid list1_lexpr_arg + { List.fold_left mk_l_apply $1 $2 } | IF lexpr THEN lexpr ELSE lexpr { mk_pp (PPif ($2, $4, $6)) } | quant list1_quant_vars triggers DOT lexpr @@ -662,10 +647,6 @@ lexpr: { mk_pp (PPmatch ($2, $5)) } | MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) } -/* -| EPSILON lident labels COLON primitive_type DOT lexpr - { mk_pp (PPeps ((add_lab $2 $3, Some $5), $7)) } -*/ | lexpr COLON primitive_type { mk_pp (PPcast ($1, $3)) } | lexpr_arg @@ -695,6 +676,10 @@ constant: lexpr_arg: | qualid { mk_pp (PPvar $1) } +| lexpr_arg_noid { $1 } +; + +lexpr_arg_noid: | constant { mk_pp (PPconst $1) } | TRUE { mk_pp PPtrue } | FALSE { mk_pp PPfalse } @@ -732,8 +717,6 @@ quant: | FORALL { PPforall } | EXISTS { PPexists } | LAMBDA { PPlambda } -| FUNC { PPfunc } -| PRED { PPpred } ; /* Triggers */ @@ -820,7 +803,8 @@ list0_param: ; list1_param: -| list1_binder { params_of_binders $1 } +| param { $1 } +| param list1_param { $1 @ $2 } ; list1_binder: @@ -828,75 +812,97 @@ list1_binder: | binder list1_binder { $1 @ $2 } ; +/* [param] and [binder] below must have the same grammar and + raise [Parse_error] in the same cases. Interpretaion of + single-standing untyped [Qident]'s is different: [param] + treats them as type expressions, [binder], as parameter + names, whose type must be inferred. */ + +param: +| anon_binder + { Loc.errorm ~loc:(floc ()) + "cannot determine the type of the parameter" } +| primitive_type_arg + { [floc (), None, false, $1] } +| LEFTPAR GHOST primitive_type RIGHTPAR + { [floc (), None, true, $3] } +| primitive_type_arg label labels + { match $1 with + | PPTtyapp (Qident _, []) -> Loc.errorm ~loc:(floc ()) + "cannot determine the type of the parameter" + | _ -> Loc.error ~loc:(floc_i 2) Parsing.Parse_error } +| LEFTPAR binder_vars_rest RIGHTPAR + { match $2 with [l,_] -> Loc.errorm ~loc:l + "cannot determine the type of the parameter" + | _ -> Loc.error ~loc:(floc_i 3) Parsing.Parse_error } +| LEFTPAR GHOST binder_vars_rest RIGHTPAR + { match $3 with [l,_] -> Loc.errorm ~loc:l + "cannot determine the type of the parameter" + | _ -> Loc.error ~loc:(floc_i 4) Parsing.Parse_error } +| LEFTPAR binder_vars COLON primitive_type RIGHTPAR + { List.map (fun (l,i) -> l, i, false, $4) $2 } +| LEFTPAR GHOST binder_vars COLON primitive_type RIGHTPAR + { List.map (fun (l,i) -> l, i, true, $5) $3 } +; + binder: -| quote_lident - { [floc (), None, false, Some (PPTtyvar ($1, false))] } -| opaque_quote_lident - { [floc (), None, false, Some (PPTtyvar ($1, true))] } -| lqualid_qualified - { [floc (), None, false, Some (PPTtyapp ($1, []))] } -| lident labels - { [floc (), Some (add_lab $1 $2), false, None] } -| UNDERSCORE - { Loc.errorm ~loc:(floc ()) "untyped anonymous parameters are not allowed" } -| LEFTPAR RIGHTPAR - { [floc (), None, false, Some (PPTtuple [])] } -| LEFTPAR binder_in RIGHTPAR - { $2 } -| LEFTPAR GHOST binder_in RIGHTPAR - { List.map (fun (l,i,_,t) -> (l,i,true,t)) $3 } -| LEFTPAR binder_type COMMA list1_primitive_type_sep_comma RIGHTPAR - { [floc (), None, false, Some (PPTtuple ($2::$4))] } -; - -binder_in: -| lident labels - { [floc (), Some (add_lab $1 $2), false, None] } -| UNDERSCORE - { Loc.errorm ~loc:(floc ()) "untyped anonymous parameters are not allowed" } -| binder_type_rest - { [floc (), None, false, Some $1] } -| binder_vars COLON primitive_type - { List.map (fun (l,v) -> l, v, false, Some $3) $1 } -; - -binder_type: -| lident { PPTtyapp (Qident $1, []) } -| binder_type_rest { $1 } -; - -binder_type_rest: -| lident list1_lident - { PPTtyapp (Qident $1, List.map pty_of_id $2) } -| lident list0_lident primitive_type_args_non_lident - { PPTtyapp (Qident $1, List.map pty_of_id $2 @ $3) } -| primitive_type_non_lident - { $1 } +| anon_binder + { Loc.errorm ~loc:(floc ()) + "cannot determine the type of the parameter" } +| primitive_type_arg + { match $1 with + | PPTtyapp (Qident id, []) + | PPTparen (PPTtyapp (Qident id, [])) -> + [floc (), Some id, false, None] + | _ -> [floc (), None, false, Some $1] } +| LEFTPAR GHOST primitive_type RIGHTPAR + { match $3 with + | PPTtyapp (Qident id, []) -> + [floc (), Some id, true, None] + | _ -> [floc (), None, true, Some $3] } +| primitive_type_arg label labels + { match $1 with + | PPTtyapp (Qident id, []) -> + [floc (), Some (add_lab id ($2::$3)), false, None] + | _ -> Loc.error ~loc:(floc_i 2) Parsing.Parse_error } +| LEFTPAR binder_vars_rest RIGHTPAR + { match $2 with [l,i] -> [l, i, false, None] + | _ -> Loc.error ~loc:(floc_i 3) Parsing.Parse_error } +| LEFTPAR GHOST binder_vars_rest RIGHTPAR + { match $3 with [l,i] -> [l, i, true, None] + | _ -> Loc.error ~loc:(floc_i 4) Parsing.Parse_error } +| LEFTPAR binder_vars COLON primitive_type RIGHTPAR + { List.map (fun (l,i) -> l, i, false, Some $4) $2 } +| LEFTPAR GHOST binder_vars COLON primitive_type RIGHTPAR + { List.map (fun (l,i) -> l, i, true, Some $5) $3 } ; binder_vars: -| list1_lident - { List.map (fun id -> id.id_loc, Some id) $1 } -| list1_lident UNDERSCORE list0_lident_labels - { List.map (fun id -> id.id_loc, Some id) $1 @ (floc_i 2, None) :: $3 } -| lident list1_lident label labels list0_lident_labels - { let l = match List.rev ($1 :: $2) with - | i :: l -> add_lab i ($3 :: $4) :: l - | [] -> assert false in - List.fold_left (fun acc id -> (id.id_loc, Some id) :: acc) $5 l } -| lident label labels list0_lident_labels - { ($1.id_loc, Some (add_lab $1 ($2 :: $3))) :: $4 } -| UNDERSCORE list0_lident_labels - { (floc_i 1, None) :: $2 } -; - -list0_lident: -| /* epsilon */ { [] } -| list1_lident { $1 } +| binder_vars_head { List.rev $1 } +| binder_vars_rest { $1 } +; + +binder_vars_rest: +| binder_vars_head label labels list0_lident_labels + { List.rev_append (match $1 with + | (l, Some id) :: bl -> + (Loc.join l (floc_i 3), Some (add_lab id ($2::$3))) :: bl + | _ -> assert false) $4 } +| binder_vars_head anon_binder list0_lident_labels + { List.rev_append $1 ($2 :: $3) } +| anon_binder list0_lident_labels + { $1 :: $2 } ; -list1_lident: -| lident list0_lident { $1 :: $2 } +binder_vars_head: +| primitive_type { + let of_id id = id.id_loc, Some id in + let push acc = function + | PPTtyapp (Qident id, []) -> of_id id :: acc + | _ -> Loc.error ~loc:(floc ()) Parsing.Parse_error in + match $1 with + | PPTtyapp (Qident id, l) -> List.fold_left push [of_id id] l + | _ -> Loc.error ~loc:(floc ()) Parsing.Parse_error } ; list1_quant_vars: @@ -920,6 +926,9 @@ list1_lident_labels: lident_labels: | lident labels { floc (), Some (add_lab $1 $2) } +| anon_binder { $1 } + +anon_binder: | UNDERSCORE { floc (), None } ; @@ -1013,10 +1022,6 @@ lqualid_copy: | uqualid DOT lident { Qdot ($1, $3) } ; -lqualid_qualified: -| uqualid DOT lident { Qdot ($1, $3) } -; - uqualid: | uident { Qident $1 } | uqualid DOT uident { Qdot ($1, $3) } diff --git a/src/parser/ptree.ml b/src/parser/ptree.ml index 14f6e8b58..52b582445 100644 --- a/src/parser/ptree.ml +++ b/src/parser/ptree.ml @@ -24,7 +24,7 @@ type label = | Lpos of Loc.position type pp_quant = - | PPforall | PPexists | PPlambda | PPfunc | PPpred + | PPforall | PPexists | PPlambda type pp_binop = | PPand | PPor | PPimplies | PPiff @@ -44,6 +44,8 @@ type pty = | PPTtyvar of ident * opacity | PPTtyapp of qualid * pty list | PPTtuple of pty list + | PPTarrow of pty * pty + | PPTparen of pty type ghost = bool type top_ghost = Gnone | Gghost | Glemma @@ -70,6 +72,7 @@ type lexpr = and pp_desc = | PPvar of qualid | PPapp of qualid * lexpr list + | PPhoapp of lexpr * lexpr | PPtrue | PPfalse | PPconst of constant @@ -81,7 +84,6 @@ and pp_desc = | PPquant of pp_quant * quvar list * lexpr list list * lexpr | PPnamed of label * lexpr | PPlet of ident * lexpr * lexpr - | PPeps of quvar * lexpr | PPmatch of lexpr * (pattern * lexpr) list | PPcast of lexpr * pty | PPtuple of lexpr list diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 5b14c522f..c86cd9f59 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -17,191 +17,92 @@ open Ty open Term open Decl open Theory +open Dterm open Env -open Denv -(** errors *) - -exception DuplicateVar of string -exception DuplicateTypeVar of string -exception PredicateExpected -exception TermExpected -exception FSymExpected of lsymbol -exception PSymExpected of lsymbol -exception ClashTheory of string -(* dead code -exception UnboundTheory of qualid -*) -exception UnboundTypeVar of string -(* dead code -exception UnboundType of string list -*) -exception UnboundSymbol of qualid - -let error = Loc.error - -let errorm = Loc.errorm - -let rec print_qualid fmt = function - | Qident s -> fprintf fmt "%s" s.id - | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id - -let () = Exn_printer.register (fun fmt e -> match e with - | DuplicateTypeVar s -> - fprintf fmt "Duplicate type parameter %s" s - | DuplicateVar s -> - fprintf fmt "Duplicate variable %s" s - | PredicateExpected -> - fprintf fmt "syntax error: predicate expected" - | TermExpected -> - fprintf fmt "syntax error: term expected" - | FSymExpected ls -> - fprintf fmt "%a is not a function symbol" Pretty.print_ls ls - | PSymExpected ls -> - fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls - | ClashTheory s -> - fprintf fmt "Clash with previous theory %s" s -(* dead code - | UnboundTheory q -> - fprintf fmt "unbound theory %a" print_qualid q -*) - | UnboundTypeVar s -> - fprintf fmt "unbound type variable '%s" s -(* dead code - | UnboundType sl -> - fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl -*) - | UnboundSymbol q -> - fprintf fmt "Unbound symbol '%a'" print_qualid q - | _ -> raise e) +(** debug flags *) let debug_parse_only = Debug.register_flag "parse_only" ~desc:"Stop@ after@ parsing." + let debug_type_only = Debug.register_flag "type_only" ~desc:"Stop@ after@ type-checking." -(** Environments *) - -(** typing using destructive type variables - - parsed trees intermediate trees typed trees - (Ptree) (D below) (Term) - ----------------------------------------------------------- - ppure_type ---dty---> dty ---ty---> ty - lexpr --dterm--> dterm --term--> term - lexpr --dfmla--> dfmla --fmla--> fmla - -*) - -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 unify_raise ~loc ty1 ty2 = - if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2 - -(** Destructive typing environment, that is - environment + local variables. - It is only local to this module and created with [create_denv] below. *) - -let create_user_tv = - let hs = Hstr.create 17 in - fun s -> try Hstr.find hs s with Not_found -> - let tv = create_tvsymbol (id_fresh s) in - Hstr.add hs s tv; - tv - -(* TODO: shouldn't we localize this ident? *) -let create_user_type_var x = - tyuvar (create_user_tv x) - -type denv = { - dvars : dty Mstr.t; (* local variables, to be bound later *) - gvars : qualid -> vsymbol option; (* global variables, for programs *) -} +(** errors *) -let denv_empty = { dvars = Mstr.empty; gvars = Util.const None } -let denv_empty_with_globals gv = { dvars = Mstr.empty; gvars = gv } +exception UnboundTypeVar of string +exception DuplicateTypeVar of string +exception ClashTheory of string -(* dead code -let mem_var x denv = Mstr.mem x denv.dvars -let find_var x denv = Mstr.find x denv.dvars -*) -let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars } +(** lazy declaration of tuples *) -(* dead code -let print_denv fmt denv = - Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars -*) +let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts) +let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl) +let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls) +let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl) +let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl) +let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f) -(* parsed types -> intermediate types *) +(** symbol lookup *) let rec qloc = function | Qident x -> x.id_loc | Qdot (m, x) -> Loc.join (qloc m) x.id_loc -let rec string_list_of_qualid acc = function - | Qident id -> id.id :: acc - | Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p +let string_list_of_qualid q = + let rec sloq acc = function + | Qdot (p, id) -> sloq (id.id :: acc) p + | Qident id -> id.id :: acc in + sloq [] q -(* lazy declaration of tuples *) - -let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts) -let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl) -let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls) -let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl) -let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl) -let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f) - -let find_ns get_id find p ns = - let loc = qloc p in - let sl = string_list_of_qualid [] p in - try - let r = find ns sl in - if Debug.test_flag Glob.flag then Glob.use loc (get_id r); - r - with Not_found -> error ~loc (UnboundSymbol p) +let rec print_qualid fmt = function + | Qident s -> fprintf fmt "%s" s.id + | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id -let get_id_prop p = p.pr_name -let find_prop_ns = find_ns get_id_prop ns_find_pr -let find_prop p uc = find_prop_ns p (get_namespace uc) +exception UnboundSymbol of qualid -let get_id_ts ts = ts.ts_name -let find_tysymbol_ns = find_ns get_id_ts ns_find_ts -let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc) +let find_ns get_id find q ns = + let sl = string_list_of_qualid q in + let r = try find ns sl with Not_found -> + Loc.error ~loc:(qloc q) (UnboundSymbol q) in + if Debug.test_flag Glob.flag then Glob.use (qloc q) (get_id r); + r -let get_id_ls ls = ls.ls_name -let find_lsymbol_ns = find_ns get_id_ls ns_find_ls -let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc) +let find_prop_ns q ns = find_ns (fun pr -> pr.pr_name) ns_find_pr q ns +let find_tysymbol_ns q ns = find_ns (fun ts -> ts.ts_name) ns_find_ts q ns +let find_lsymbol_ns q ns = find_ns (fun ls -> ls.ls_name) ns_find_ls q ns let find_fsymbol_ns q ns = let ls = find_lsymbol_ns q ns in - if ls.ls_value = None then error ~loc:(qloc q) (FSymExpected ls) else ls + if ls.ls_value <> None then ls else + Loc.error ~loc:(qloc q) (FunctionSymbolExpected ls) let find_psymbol_ns q ns = let ls = find_lsymbol_ns q ns in - if ls.ls_value <> None then error ~loc:(qloc q) (PSymExpected ls) else ls + if ls.ls_value = None then ls else + Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls) -let find_fsymbol q uc = find_fsymbol_ns q (get_namespace uc) -let find_psymbol q uc = find_psymbol_ns q (get_namespace uc) +let find_prop q uc = find_prop_ns q (get_namespace uc) +let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc) +let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc) +let find_fsymbol q uc = find_fsymbol_ns q (get_namespace uc) +let find_psymbol q uc = find_psymbol_ns q (get_namespace uc) + +let find_namespace_ns q ns = + find_ns (fun _ -> Glob.dummy_id) ns_find_ns q ns -let get_dummy_id _ = Glob.dummy_id -let find_namespace_ns = find_ns get_dummy_id ns_find_ns (* dead code let find_namespace q uc = find_namespace_ns q (get_namespace uc) *) -let rec dty uc = function - | PPTtyvar ({id=x}, _) -> - create_user_type_var x - | PPTtyapp (x, p) -> - let ts = find_tysymbol x uc in - let tyl = List.map (dty uc) p in - Loc.try2 ~loc:(qloc x) tyapp ts tyl - | PPTtuple tyl -> - let ts = ts_tuple (List.length tyl) in - tyapp ts (List.map (dty uc) tyl) +(** Parsing types *) + +let create_user_tv = + let hs = Hstr.create 17 in + fun s -> try Hstr.find hs s with Not_found -> + let tv = create_tvsymbol (id_fresh s) in + Hstr.add hs s tv; + tv let rec ty_of_pty uc = function | PPTtyvar ({id=x}, _) -> @@ -213,476 +114,228 @@ let rec ty_of_pty uc = function | PPTtuple tyl -> let ts = ts_tuple (List.length tyl) in ty_app ts (List.map (ty_of_pty uc) tyl) - -let rec opaque_tvs acc = function - | Ptree.PPTtyvar (id, true) -> Stv.add (create_user_tv id.id) acc - | Ptree.PPTtyvar (_, false) -> acc - | Ptree.PPTtyapp (_, pl) - | Ptree.PPTtuple pl -> List.fold_left opaque_tvs acc pl + | PPTarrow (ty1, ty2) -> + ty_func (ty_of_pty uc ty1) (ty_of_pty uc ty2) + | PPTparen ty -> + ty_of_pty uc ty let opaque_tvs args value = + let rec opaque_tvs acc = function + | PPTtyvar (id, true) -> Stv.add (create_user_tv id.id) acc + | PPTtyvar (_, false) -> acc + | PPTtyapp (_, pl) + | PPTtuple pl -> List.fold_left opaque_tvs acc pl + | PPTarrow (ty1, ty2) -> opaque_tvs (opaque_tvs acc ty1) ty2 + | PPTparen ty -> opaque_tvs acc ty in let acc = Opt.fold opaque_tvs Stv.empty value in List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) acc args -let specialize_lsymbol p uc = - let s = find_lsymbol p uc in - let tl,ty = specialize_lsymbol ~loc:(qloc p) s in - s,tl,ty - -let specialize_fsymbol p uc = - let s,tl,ty = specialize_lsymbol p uc in - match ty with - | None -> let loc = qloc p in error ~loc TermExpected - | Some ty -> s, tl, ty - -let specialize_psymbol p uc = - let s,tl,ty = specialize_lsymbol p uc in - match ty with - | None -> s, tl - | Some _ -> let loc = qloc p in error ~loc PredicateExpected - -let is_psymbol p uc = - let s = find_lsymbol p uc in - s.ls_value = None - -(** Typing types *) - -let split_qualid = function - | Qident id -> [], id.id - | Qdot (p, id) -> string_list_of_qualid [] p, id.id - -(** Typing terms and formulas *) +(** typing using destructive type variables -let binop = function - | PPand -> Tand - | PPor -> Tor - | PPimplies -> Timplies - | PPiff -> Tiff + parsed trees intermediate trees typed trees + (Ptree) (Dterm) (Term) + ----------------------------------------------------------- + ppure_type ---dty---> dty ---ty---> ty + lexpr --dterm--> dterm --term--> term +*) -let check_pat_linearity p = - let s = ref Sstr.empty in - let add { id = id; id_loc = loc } = - s := Loc.try3 ~loc Sstr.add_new (DuplicateVar id) id !s +(** Typing patterns, terms, and formulas *) + +let create_user_id { id = x ; id_lab = ll ; id_loc = loc } = + let get_labels (ll,p) = function + | Lstr l -> Slab.add l ll, p + | Lpos p -> ll, Some p in + let label,p = List.fold_left get_labels (Slab.empty,None) ll in + id_user ~label x (Opt.get_def loc p) + +let parse_record ~loc uc get_val fl = + let fl = List.map (fun (q,e) -> find_lsymbol q uc, e) fl in + let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in + let get_val pj = get_val cs pj (Mls.find_opt pj flm) in + cs, List.map get_val pjl + +let dpattern uc pat = + let rec ppat { pat_desc = desc; pat_loc = loc } = + dpattern ~loc (match desc with + | PPpwild -> DPwild + | PPpvar x -> DPvar (create_user_id x) + | PPpapp (x,pl) -> DPapp (find_lsymbol x uc, List.map ppat pl) + | PPptuple pl -> DPapp (fs_tuple (List.length pl), List.map ppat pl) + | PPprec fl -> + let get_val _ _ = function + Some p -> ppat p | None -> dpattern DPwild in + let cs,fl = parse_record ~loc uc get_val fl in + DPapp (cs,fl) + | PPpas (p, x) -> DPas (ppat p, create_user_id x) + | PPpor (p, q) -> DPor (ppat p, ppat q)) in - let rec check p = match p.pat_desc with - | PPpwild -> () - | PPpvar id -> add id - | PPpapp (_, pl) | PPptuple pl -> List.iter check pl - | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl - | PPpas (p, id) -> check p; add id - | PPpor (p, _) -> check p + ppat pat + +let quant_var uc (x,ty) = + create_user_id x, match ty with + | Some ty -> dty_of_ty (ty_of_pty uc ty) + | None -> dty_fresh () + +let chainable_op uc op = + (* non-bool -> non-bool -> bool *) + op.id = "infix =" || op.id = "infix <>" || + match find_lsymbol (Qident op) uc with + | { ls_args = [ty1;ty2]; ls_value = ty } -> + Opt.fold (fun _ ty -> ty_equal ty ty_bool) true ty + && not (ty_equal ty1 ty_bool) + && not (ty_equal ty2 ty_bool) + | _ -> false + +let dterm uc gvars denv pp = + let rec pterm denv { pp_desc = desc; pp_loc = loc } = + let highord_app e1 e2 = + DTapp (fs_func_app, [dterm ~loc e1; pterm denv e2]) in + let highord_app e1 el = List.fold_left highord_app e1 el in + let qualid_app x el = match gvars x with + | Some vs -> + highord_app (DTgvar vs) el + | None -> + let ls = find_lsymbol x uc in + let rec take al l el = match l, el with + | (_::l), (e::el) -> take (pterm denv e :: al) l el + | _, _ -> List.rev al, el in + let al, el = take [] ls.ls_args el in + highord_app (DTapp (ls,al)) el + in + let qualid_app x el = match x with + | Qident {id = n} -> + (match denv_get_opt denv n with + | Some dt -> highord_app dt el + | None -> qualid_app x el) + | _ -> qualid_app x el + in + dterm ~loc (match desc with + | PPvar x -> + qualid_app x [] + | PPapp (x, tl) -> + qualid_app x tl + | PPhoapp (e1, e2) -> + DTapp (fs_func_app, [pterm denv e1; pterm denv e2]) + | PPtuple tl -> + let tl = List.map (pterm denv) tl in + DTapp (fs_tuple (List.length tl), tl) + | PPinfix (e12, op2, e3) + | PPinnfix (e12, op2, e3) -> + let make_app de1 op de2 = if op.id = "infix <>" then + let op = { op with id = "infix =" } in + let ls = find_lsymbol (Qident op) uc in + DTnot (dterm ~loc (DTapp (ls, [de1;de2]))) + else + DTapp (find_lsymbol (Qident op) uc, [de1;de2]) + in + let rec make_chain de1 = function + | [op,de2] -> + make_app de1 op de2 + | (op,de2) :: ch -> + let de12 = dterm ~loc (make_app de1 op de2) in + let de23 = dterm ~loc (make_chain de2 ch) in + DTbinop (Tand, de12, de23) + | [] -> assert false in + let rec get_chain e12 acc = match e12.pp_desc with + | PPinfix (e1, op1, e2) when chainable_op uc op1 -> + get_chain e1 ((op1, pterm denv e2) :: acc) + | _ -> e12, acc in + let ch = [op2, pterm denv e3] in + let e1, ch = if chainable_op uc op2 + then get_chain e12 ch else e12, ch in + make_chain (pterm denv e1) ch + | PPconst c -> + DTconst c + | PPlet (x, e1, e2) -> + let id = create_user_id x in + let e1 = pterm denv e1 in + let denv = denv_add_let denv e1 id in + let e2 = pterm denv e2 in + DTlet (e1, id, e2) + | PPmatch (e1, bl) -> + let e1 = pterm denv e1 in + let branch (p, e) = + let p = dpattern uc p in + let denv = denv_add_pat denv p in + p, pterm denv e in + DTcase (e1, List.map branch bl) + | PPif (e1, e2, e3) -> + let e1 = pterm denv e1 in + let e2 = pterm denv e2 in + let e3 = pterm denv e3 in + DTif (e1, e2, e3) + | PPtrue -> + DTtrue + | PPfalse -> + DTfalse + | PPunop (PPnot, e1) -> + DTnot (pterm denv e1) + | PPbinop (e1, op, e2) -> + let e1 = pterm denv e1 in + let e2 = pterm denv e2 in + let op = match op with + | PPand -> Tand + | PPor -> Tor + | PPimplies -> Timplies + | PPiff -> Tiff in + DTbinop (op, e1, e2) + | PPquant (q, uqu, trl, e1) -> + let qvl = List.map (quant_var uc) uqu in + let denv = denv_add_quant denv qvl in + let trl = List.map (List.map (pterm denv)) trl in + let e1 = pterm denv e1 in + begin match q with + | PPforall -> DTquant (Tforall, qvl, trl, e1) + | PPexists -> DTquant (Texists, qvl, trl, e1) + | PPlambda -> + let id = id_user "fc" loc and dty = dty_fresh () in + let add acc ({id = x}, _) = + let arg = dterm ~loc (denv_get denv x) in + DTapp (fs_func_app, [dterm ~loc acc; arg]) in + let app = List.fold_left add (DTvar ("fc",dty)) uqu in + let f = DTapp (ps_equ, [dterm ~loc app; e1]) in + let f = DTquant (Tforall, qvl, trl, dterm ~loc f) in + DTeps (id, dty, dterm ~loc f) + end + | PPrecord fl -> + let get_val cs pj = function + | Some e -> pterm denv e + | None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in + let cs, fl = parse_record ~loc uc get_val fl in + DTapp (cs, fl) + | PPupdate (e1, fl) -> + let e1 = pterm denv e1 in + let get_val _ pj = function + | Some e -> pterm denv e + | None -> dterm ~loc (DTapp (pj,[e1])) in + let cs, fl = parse_record ~loc uc get_val fl in + DTapp (cs, fl) + | PPnamed (Lpos uloc, e1) -> + DTuloc (pterm denv e1, uloc) + | PPnamed (Lstr lab, e1) -> + DTlabel (pterm denv e1, Slab.singleton lab) + | PPcast (e1, ty) -> + DTcast (pterm denv e1, ty_of_pty uc ty)) in - check p - -let rec dpat uc env pat = - let env, n, ty = dpat_node pat.pat_loc uc env pat.pat_desc in - env, { dp_node = n; dp_ty = ty } + pterm denv pp -and dpat_node loc uc env = function - | PPpwild -> - let ty = fresh_type_var loc in - env, Pwild, ty - | PPpvar x -> - let ty = fresh_type_var loc in - let env = add_var x.id ty env in - env, Pvar x, ty - | PPpapp (x, pl) -> - let s, tyl, ty = specialize_fsymbol x uc in - let env, pl = dpat_args s loc uc env tyl pl in - env, Papp (s, pl), ty - | PPprec fl -> - let renv = ref env in - let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in - let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in - let tyl,ty = Denv.specialize_lsymbol ~loc cs in - let get_val pj ty = match Mls.find_opt pj flm with - | Some e -> - let loc = e.pat_loc in - let env,e = dpat uc !renv e in - unify_raise ~loc e.dp_ty ty; - renv := env; - e - | None -> - { dp_node = Pwild; dp_ty = ty } - in - let al = List.map2 get_val pjl tyl in - !renv, Papp (cs, al), Opt.get 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 loc uc env tyl pl in - let ty = tyapp (ts_tuple n) tyl in - env, Papp (s, pl), ty - | PPpas (p, x) -> - let env, p = dpat uc env p in - let env = add_var x.id p.dp_ty env in - env, Pas (p,x), p.dp_ty - | PPpor (p, q) -> - let env, p = dpat uc env p in - let env, q = dpat uc env q in - unify_raise ~loc p.dp_ty q.dp_ty; - env, Por (p,q), p.dp_ty +let type_term uc gfn t = + let t = dterm uc gfn denv_empty t in + Dterm.term ~strict:true ~keep_loc:true Mstr.empty t -and dpat_args ls loc uc env el pl = - let n = List.length el and m = List.length pl in - if n <> m then error ~loc (BadArity (ls,m)); - let rec check_arg env = function - | [], [] -> - env, [] - | a :: al, p :: pl -> - let loc = p.pat_loc in - let env, p = dpat uc env p in - unify_raise ~loc p.dp_ty a; - let env, pl = check_arg env (al, pl) in - env, p :: pl - | _ -> - assert false - in - check_arg env (el, pl) +let type_fmla uc gfn f = + let f = dterm uc gfn denv_empty f in + Dterm.fmla ~strict:true ~keep_loc:true Mstr.empty f -let rec trigger_not_a_term_exn = function - | TermExpected -> true - | Loc.Located (_, exn) -> trigger_not_a_term_exn exn - | _ -> false +(** Typing declarations *) -let param_tys uc pl = - let s = ref Sstr.empty in - let ty_of_param (loc,id,gh,ty) = - if gh then Loc.errorm ~loc "ghost parameters are not allowed here"; - Opt.iter (fun { id = id; id_loc = loc } -> - s := Loc.try3 ~loc Sstr.add_new (DuplicateVar id) id !s) id; - ty_of_dty (dty uc ty) in +let tyl_of_params uc pl = + let ty_of_param (loc,_,gh,ty) = + if gh then Loc.errorm ~loc + "ghost parameters are not allowed in pure declarations"; + ty_of_pty uc ty in List.map ty_of_param pl -let quant_var uc env (id,ty) = - let ty = match ty with - | None -> Denv.fresh_type_var id.id_loc - | Some ty -> dty uc ty in - add_var id.id ty env, (id,ty) - -let quant_vars uc env qvl = - let s = ref Sstr.empty in - let add env (({ id = id; id_loc = loc }, _) as qv) = - s := Loc.try3 ~loc Sstr.add_new (DuplicateVar id) id !s; - quant_var uc env qv in - Lists.map_fold_left add env qvl - -let check_highord uc env x tl = match x with - | Qident { id = x } when Mstr.mem x env.dvars -> true - | _ -> env.gvars x <> None || - List.length tl > List.length ((find_lsymbol x uc).ls_args) - -let apply_highord loc x tl = match List.rev tl with - | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a] - | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a] - | [] -> assert false - -let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } = - let n, ty = dterm_node ~localize loc uc env t in - let t = { dt_node = n; dt_ty = ty } in - let rec down loc e = match e.dt_node with - | Tnamed (Lstr _, e) -> down loc e - | Tnamed (Lpos _, _) -> t - | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty } - in - match localize with - | Some (Some loc) -> down loc t - | Some None -> down loc t - | None -> t - -and dterm_node ~localize loc uc env = function - | PPvar (Qident {id=x}) when Mstr.mem x env.dvars -> - (* local variable *) - let ty = Mstr.find x env.dvars in - Tvar x, ty - | PPvar x when env.gvars x <> None -> - let vs = Opt.get (env.gvars x) in - Tgvar vs, dty_of_ty vs.vs_ty - | PPvar x -> - (* 0-arity symbol (constant) *) - let s, tyl, ty = specialize_fsymbol x uc in - if tyl <> [] then error ~loc (BadArity (s,0)); - Tapp (s, []), ty - | PPapp (x, tl) when check_highord uc env x tl -> - let tl = apply_highord loc x tl in - let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in - let tl = dtype_args ~localize fs_func_app loc uc env atyl tl in - Tapp (fs_func_app, tl), Opt.get aty - | PPapp (x, tl) -> - let s, tyl, ty = specialize_fsymbol x uc in - let tl = dtype_args ~localize s loc uc 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 ~localize s loc uc env tyl tl in - let ty = tyapp (ts_tuple n) tyl in - Tapp (s, tl), ty - | PPinfix (e1, x, e2) - | PPinnfix (e1, x, e2) -> - if x.id = "infix <>" then error ~loc TermExpected; - let s, tyl, ty = specialize_fsymbol (Qident x) uc in - let tl = dtype_args ~localize s loc uc env tyl [e1; e2] in - Tapp (s, tl), ty - | PPconst (Number.ConstInt _ as c) -> - Tconst c, tyapp Ty.ts_int [] - | PPconst (Number.ConstReal _ as c) -> - Tconst c, tyapp Ty.ts_real [] - | PPlet (x, e1, e2) -> - let e1 = dterm ~localize uc env e1 in - let ty = e1.dt_ty in - let env = add_var x.id ty env in - let e2 = dterm ~localize uc env e2 in - Tlet (e1, x, e2), e2.dt_ty - | PPmatch (e1, bl) -> - let t1 = dterm ~localize uc env e1 in - let ty1 = t1.dt_ty in - let tb = fresh_type_var loc in (* the type of all branches *) - let branch (p, e) = - let env, p = dpat_list uc env ty1 p in - let loc = e.pp_loc in - let e = dterm ~localize uc env e in - unify_raise ~loc e.dt_ty tb; - p, e - in - let bl = List.map branch bl in - Tmatch (t1, bl), tb - | PPnamed (x, e1) -> - let localize = match x with - | Lpos l -> Some (Some l) - | Lstr _ -> localize - in - let e1 = dterm ~localize uc env e1 in - Tnamed (x, e1), e1.dt_ty - | PPcast (e1, ty) -> - let loc = e1.pp_loc in - let e1 = dterm ~localize uc env e1 in - let ty = dty uc ty in - unify_raise ~loc e1.dt_ty ty; - e1.dt_node, ty - | PPif (e1, e2, e3) -> - let loc = e3.pp_loc in - let e2 = dterm ~localize uc env e2 in - let e3 = dterm ~localize uc env e3 in - unify_raise ~loc e3.dt_ty e2.dt_ty; - Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty - | PPeps (b, e1) -> - let env, (x, ty) = quant_var uc env b in - let e1 = dfmla ~localize uc env e1 in - Teps (x, ty, e1), ty - | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) -> - let env, uqu = quant_vars uc env uqu in - let trigger e = - try - TRterm (dterm ~localize uc env e) - with exn when trigger_not_a_term_exn exn -> - TRfmla (dfmla ~localize uc env e) - in - let trl = List.map (List.map trigger) trl in - let e = match q with - | PPfunc -> TRterm (dterm ~localize uc env a) - | PPpred -> TRfmla (dfmla ~localize uc env a) - | PPlambda -> trigger a - | _ -> assert false - in - let id, ty, f = match e with - | TRterm t -> - let id = { id = "fc"; id_lab = []; id_loc = loc } in - let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) -> - let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty) - uqu ([],t.dt_ty) - in - let h = { dt_node = Tvar id.id ; dt_ty = ty } in - let h = List.fold_left2 (fun h (uid,uty) ty -> - let u = { dt_node = Tvar uid.id ; dt_ty = uty } in - { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty }) - h uqu tyl - in - id, ty, Fapp (ps_equ, [h;t]) - | TRfmla f -> - let id = { id = "pc"; id_lab = []; id_loc = loc } in - let (uid,uty),uqu = match List.rev uqu with - | uq :: uqu -> uq, List.rev uqu - | [] -> assert false - in - let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) -> - let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty) - uqu ([], tyapp ts_pred [uty]) - in - let h = { dt_node = Tvar id.id ; dt_ty = ty } in - let h = List.fold_left2 (fun h (uid,uty) ty -> - let u = { dt_node = Tvar uid.id ; dt_ty = uty } in - { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty }) - h uqu tyl - in - let u = { dt_node = Tvar uid.id ; dt_ty = uty } in - id, ty, Fbinop (Tiff, Fapp (ps_pred_app, [h;u]), f) - in - Teps (id, ty, Fquant (Tforall, uqu, trl, f)), ty - | PPrecord fl -> - let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in - let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in - let tyl,ty = Denv.specialize_lsymbol ~loc cs in - let get_val pj ty = match Mls.find_opt pj flm with - | Some e -> - let loc = e.pp_loc in - let e = dterm ~localize uc env e in - unify_raise ~loc e.dt_ty ty; - e - | None -> error ~loc (RecordFieldMissing (cs,pj)) - in - let al = List.map2 get_val pjl tyl in - Tapp (cs,al), Opt.get ty - | PPupdate (e,fl) -> - let e = dterm ~localize uc env e in - let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in - let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in - let tyl,ty = Denv.specialize_lsymbol ~loc cs in - let get_val pj ty = match Mls.find_opt pj flm with - | Some e -> - let loc = e.pp_loc in - let e = dterm ~localize uc env e in - unify_raise ~loc e.dt_ty ty; - e - | None -> - let ptyl,pty = Denv.specialize_lsymbol ~loc pj in - unify_raise ~loc (Opt.get pty) ty; - unify_raise ~loc (List.hd ptyl) e.dt_ty; - (* FIXME? if e is a complex expression, use let *) - { dt_node = Tapp (pj,[e]) ; dt_ty = ty } - in - let al = List.map2 get_val pjl tyl in - Tapp (cs,al), Opt.get ty - | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue -> - error ~loc TermExpected - -and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } = - let f = dfmla_node ~localize loc uc env f in - let rec down loc e = match e with - | Fnamed (Lstr _, e) -> down loc e - | Fnamed (Lpos _, _) -> f - | _ -> Fnamed (Lpos loc, f) - in - match localize with - | Some (Some loc) -> down loc f - | Some None -> down loc f - | None -> f - -and dfmla_node ~localize loc uc env = function - | PPtrue -> - Ftrue - | PPfalse -> - Ffalse - | PPunop (PPnot, a) -> - Fnot (dfmla ~localize uc env a) - | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) -> - Fbinop (binop op, dfmla ~localize uc env a, dfmla ~localize uc env b) - | PPif (a, b, c) -> - Fif (dfmla ~localize uc env a, - dfmla ~localize uc env b, dfmla ~localize uc env c) - | PPquant (q, uqu, trl, a) -> - let env, uqu = quant_vars uc env uqu in - let trigger e = - try - TRterm (dterm ~localize uc env e) - with exn when trigger_not_a_term_exn exn -> - TRfmla (dfmla ~localize uc env e) - in - let trl = List.map (List.map trigger) trl in - let q = match q with - | PPforall -> Tforall - | PPexists -> Texists - | _ -> error ~loc PredicateExpected - in - Fquant (q, uqu, trl, dfmla ~localize uc env a) - | PPapp (x, tl) when check_highord uc env x tl -> - let tl = apply_highord loc x tl in - let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in - let tl = dtype_args ~localize ps_pred_app loc uc env atyl tl in - Fapp (ps_pred_app, tl) - | PPapp (x, tl) -> - let s, tyl = specialize_psymbol x uc in - let tl = dtype_args ~localize s loc uc env tyl tl in - Fapp (s, tl) - | PPinfix (e12, op2, e3) - | PPinnfix (e12, op2, e3) -> - begin match e12.pp_desc with - | PPinfix (_, op1, e2) - when op1.id = "infix <>" || is_psymbol (Qident op1) uc -> - let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in - Fbinop (Tand, dfmla ~localize uc env e12, - dfmla ~localize uc env e23) - | _ when op2.id = "infix <>" -> - let op2 = { op2 with id = "infix =" } in - let e0 = { pp_desc = PPinfix (e12, op2, e3); pp_loc = loc } in - Fnot (dfmla ~localize uc env e0) - | _ -> - let s, tyl = specialize_psymbol (Qident op2) uc in - let tl = dtype_args ~localize s loc uc env tyl [e12;e3] in - Fapp (s, tl) - end - | PPlet (x, e1, e2) -> - let e1 = dterm ~localize uc env e1 in - let ty = e1.dt_ty in - let env = add_var x.id ty env in - let e2 = dfmla ~localize uc env e2 in - Flet (e1, x, e2) - | PPmatch (e1, bl) -> - let t1 = dterm ~localize uc env e1 in - let ty1 = t1.dt_ty in - let branch (p, e) = - let env, p = dpat_list uc env ty1 p in - p, dfmla ~localize uc env e - in - Fmatch (t1, List.map branch bl) - | PPnamed (x, f1) -> - let localize = match x with - | Lpos l -> Some (Some l) - | Lstr _ -> localize - in - let f1 = dfmla ~localize uc env f1 in - Fnamed (x, f1) -(* - | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] -> - let pr = find_prop x uc in - Fvar (Decl.find_prop (Theory.get_known uc) pr) -*) - | PPvar x -> - let s, tyl = specialize_psymbol x uc in - let tl = dtype_args ~localize s loc uc env tyl [] in - Fapp (s, tl) - | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ | PPupdate _ -> - error ~loc PredicateExpected - -and dpat_list uc env ty p = - check_pat_linearity p; - let loc = p.pat_loc in - let env, p = dpat uc env p in - unify_raise ~loc p.dp_ty ty; - env, p - -and dtype_args ~localize ls loc uc env el tl = - let n = List.length el and m = List.length tl in - if n <> m then error ~loc (BadArity (ls,m)); - let rec check_arg = function - | [], [] -> - [] - | a :: al, t :: bl -> - let loc = t.pp_loc in - let t = dterm ~localize uc env t in - unify_raise ~loc t.dt_ty a; - t :: check_arg (al, bl) - | _ -> - assert false - in - check_arg (el, tl) - -(** Typing declarations, that is building environments. *) - -open Ptree - let add_types dl th = let def = List.fold_left (fun def d -> @@ -695,14 +348,14 @@ let add_types dl th = let d = Mstr.find x def in try match Hstr.find tysymbols x with - | None -> errorm ~loc:d.td_loc "Cyclic type definition" + | None -> Loc.errorm ~loc:d.td_loc "Cyclic type definition" | Some ts -> ts with Not_found -> Hstr.add tysymbols x None; let vars = Hstr.create 17 in let vl = List.map (fun id -> if Hstr.mem vars id.id then - error ~loc:id.id_loc (DuplicateTypeVar id.id); + Loc.error ~loc:id.id_loc (DuplicateTypeVar id.id); let i = create_user_tv id.id in Hstr.add vars id.id i; i) d.td_params @@ -713,8 +366,8 @@ let add_types dl th = let rec apply = function | PPTtyvar (v, _) -> begin - try ty_var (Hstr.find vars v.id) - with Not_found -> error ~loc:v.id_loc (UnboundTypeVar v.id) + try ty_var (Hstr.find vars v.id) with Not_found -> + Loc.error ~loc:v.id_loc (UnboundTypeVar v.id) end | PPTtyapp (q, tyl) -> let ts = match q with @@ -727,6 +380,10 @@ let add_types dl th = | PPTtuple tyl -> let ts = ts_tuple (List.length tyl) in ty_app ts (List.map apply tyl) + | PPTarrow (ty1, ty2) -> + ty_func (apply ty1) (apply ty2) + | PPTparen ty -> + apply ty in create_tysymbol id vl (Some (apply ty)) | TDabstract | TDalgebraic _ -> @@ -746,7 +403,8 @@ let add_types dl th = let th = List.fold_left add_ty_decl th abstr in let th = List.fold_left add_ty_decl th alias in th - with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (ClashSymbol s) + with ClashSymbol s -> + Loc.error ~loc:(Mstr.find s def).td_loc (ClashSymbol s) in let csymbols = Hstr.create 17 in let decl d (abstr,algeb,alias) = @@ -780,7 +438,7 @@ let add_types dl th = Some pj in let constructor (loc, id, pl) = - let tyl = param_tys th' pl in + let tyl = tyl_of_params th' pl in let pjl = List.map2 projection pl tyl in Hstr.replace csymbols id.id loc; create_fsymbol ~opaque ~constr (create_user_id id) tyl ty, pjl @@ -797,27 +455,27 @@ let add_types dl th = th with | ClashSymbol s -> - error ~loc:(Hstr.find csymbols s) (ClashSymbol s) + Loc.error ~loc:(Hstr.find csymbols s) (ClashSymbol s) | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) -> - error ~loc:(Hstr.find csymbols s) (RecordFieldMissing (cs,ls)) + Loc.error ~loc:(Hstr.find csymbols s) (RecordFieldMissing (cs,ls)) | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) -> - error ~loc:(Hstr.find csymbols s) (DuplicateRecordField (cs,ls)) + Loc.error ~loc:(Hstr.find csymbols s) (DuplicateRecordField (cs,ls)) let prepare_typedef td = if td.td_model then - errorm ~loc:td.td_loc "model types are not allowed in pure theories"; + Loc.errorm ~loc:td.td_loc "model types are not allowed in pure theories"; if td.td_vis <> Public then - errorm ~loc:td.td_loc "pure types cannot be abstract or private"; + Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private"; if td.td_inv <> [] then - errorm ~loc:td.td_loc "pure types cannot have invariants"; + Loc.errorm ~loc:td.td_loc "pure types cannot have invariants"; match td.td_def with | TDabstract | TDalgebraic _ | TDalias _ -> td | TDrecord fl -> let field { f_loc = loc; f_ident = id; f_pty = ty; f_mutable = mut; f_ghost = gh } = - if mut then errorm ~loc "a logic record field cannot be mutable"; - if gh then errorm ~loc "a logic record field cannot be ghost"; + if mut then Loc.errorm ~loc "a logic record field cannot be mutable"; + if gh then Loc.errorm ~loc "a logic record field cannot be ghost"; loc, Some id, false, ty in (* constructor for type t is "mk t" (and not String.capitalize t) *) @@ -827,20 +485,14 @@ let prepare_typedef td = let add_types dl th = add_types (List.map prepare_typedef dl) th -let env_of_vsymbol_list vl = - List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl - let add_logics dl th = let lsymbols = Hstr.create 17 in - let denvs = Hstr.create 17 in (* 1. create all symbols and make an environment with these symbols *) let create_symbol th d = let id = d.ld_ident.id in - let denv = denv_empty in - Hstr.add denvs id denv; let v = create_user_id d.ld_ident in - let pl = param_tys th d.ld_params in - let ty = Opt.map (fun t -> ty_of_dty (dty th t)) d.ld_type in + let pl = tyl_of_params th d.ld_params in + let ty = Opt.map (ty_of_pty th) d.ld_type in let opaque = opaque_tvs d.ld_params d.ld_type in let ls = create_lsymbol ~opaque v pl ty in Hstr.add lsymbols id ls; @@ -850,29 +502,28 @@ let add_logics dl th = (* 2. then type-check all definitions *) let type_decl d (abst,defn) = let id = d.ld_ident.id in - let dadd_var denv (_,x,_,ty) = match x with - | Some id -> add_var id.id (dty th' ty) denv - | None -> denv - in - let denv = Hstr.find denvs id in - let denv = List.fold_left dadd_var denv d.ld_params in + let ls = Hstr.find lsymbols id in let create_var (loc,x,_,_) ty = let id = match x with | Some id -> create_user_id id | None -> id_user "_" loc in create_vsymbol id ty in - let ls = Hstr.find lsymbols id in let vl = List.map2 create_var d.ld_params ls.ls_args in - let env = env_of_vsymbol_list vl in + let add_var mvs (_,x,_,_) vs = match x with + | Some {id = id} -> Mstr.add_new (DuplicateVar id) id (DTgvar vs) mvs + | None -> mvs in + let denv = List.fold_left2 add_var denv_empty d.ld_params vl in match d.ld_def, d.ld_type with | None, _ -> ls :: abst, defn | Some e, None -> (* predicate *) - let f = dfmla th' denv e in - abst, (ls, vl, fmla env f) :: defn + let f = dterm th' (fun _ -> None) denv e in + let f = fmla ~strict:true ~keep_loc:true Mstr.empty f in + abst, (ls, vl, f) :: defn | Some e, Some ty -> (* function *) - let t = dterm th' denv e in - unify_raise ~loc:e.pp_loc t.dt_ty (dty th' ty); - abst, (ls, vl, term env t) :: defn + let e = { e with pp_desc = PPcast (e, ty) } in + let t = dterm th' (fun _ -> None) denv e in + let t = term ~strict:true ~keep_loc:true Mstr.empty t in + abst, (ls, vl, t) :: defn in let abst,defn = List.fold_right type_decl dl ([],[]) in (* 3. detect opacity *) @@ -911,16 +562,6 @@ let add_logics dl th = let th = if defn = [] then th else add_logic_decl th (ldefns defn) in th -let type_term uc gfn t = - let denv = denv_empty_with_globals gfn in - let t = dterm ~localize:(Some None) uc denv t in - term Mstr.empty t - -let type_fmla uc gfn f = - let denv = denv_empty_with_globals gfn in - let f = dfmla ~localize:(Some None) uc denv f in - fmla Mstr.empty f - let add_prop k loc s f th = let pr = create_prsymbol (create_user_id s) in let f = type_fmla th (fun _ -> None) f in @@ -934,7 +575,7 @@ let add_inductives s dl th = let create_symbol th d = let id = d.in_ident.id in let v = create_user_id d.in_ident in - let pl = param_tys th d.in_params in + let pl = tyl_of_params th d.in_params in let opaque = opaque_tvs d.in_params None in let ps = create_psymbol ~opaque v pl in Hstr.add psymbols id ps; @@ -956,11 +597,11 @@ let add_inductives s dl th = try add_ind_decl th s (List.map type_decl dl) with | ClashSymbol s -> - error ~loc:(Hstr.find propsyms s) (ClashSymbol s) + Loc.error ~loc:(Hstr.find propsyms s) (ClashSymbol s) | InvalidIndDecl (ls,pr) -> - error ~loc:(loc_of_id pr.pr_name) (InvalidIndDecl (ls,pr)) + Loc.error ~loc:(loc_of_id pr.pr_name) (InvalidIndDecl (ls,pr)) | NonPositiveIndDecl (ls,pr,s) -> - error ~loc:(loc_of_id pr.pr_name) (NonPositiveIndDecl (ls,pr,s)) + Loc.error ~loc:(loc_of_id pr.pr_name) (NonPositiveIndDecl (ls,pr,s)) (* parse declarations *) @@ -969,14 +610,12 @@ let prop_kind = function | Kgoal -> Pgoal | Klemma -> Plemma -let find_theory env lenv q id = match q with - | [] -> - (* local theory *) +let find_theory env lenv q = match q with + | Qident { id = id } -> (* local theory *) begin try Mstr.find id lenv with Not_found -> read_lib_theory env [] id end - | _ :: _ -> - (* theory in file f *) - read_lib_theory env q id + | Qdot (p, { id = id }) -> (* theory in file f *) + read_lib_theory env (string_list_of_qualid p) id let rec clone_ns kn sl path ns2 ns1 s = let qualid fmt path = Pp.print_list @@ -1033,15 +672,15 @@ let rec clone_ns kn sl path ns2 ns1 s = { s with inst_ts = inst_ts; inst_ls = inst_ls } let add_decl loc th = function - | TypeDecl dl -> + | Ptree.TypeDecl dl -> add_types dl th - | LogicDecl dl -> + | Ptree.LogicDecl dl -> add_logics dl th - | IndDecl (s, dl) -> + | Ptree.IndDecl (s, dl) -> add_inductives s dl th - | PropDecl (k, s, f) -> + | Ptree.PropDecl (k, s, f) -> add_prop (prop_kind k) loc s f th - | Meta (id, al) -> + | Ptree.Meta (id, al) -> let convert = function | PMAty (PPTtyapp (q,[])) -> MAts (find_tysymbol q th) @@ -1070,7 +709,7 @@ let type_inst th t s = let ts1 = find_tysymbol_ns p t.th_export in let ts2 = find_tysymbol q th in if Mts.mem ts1 s.inst_ts - then error ~loc (ClashSymbol ts1.ts_name.id_string); + then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string); { s with inst_ts = Mts.add ts1 ts2 s.inst_ts } | CStsym (loc,p,tvl,pty) -> let ts1 = find_tysymbol_ns p t.th_export in @@ -1079,29 +718,29 @@ let type_inst th t s = let def = Some (ty_of_pty th pty) in let ts2 = Loc.try3 ~loc create_tysymbol id tvl def in if Mts.mem ts1 s.inst_ts - then error ~loc (ClashSymbol ts1.ts_name.id_string); + then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string); { s with inst_ts = Mts.add ts1 ts2 s.inst_ts } | CSfsym (loc,p,q) -> let ls1 = find_fsymbol_ns p t.th_export in let ls2 = find_fsymbol q th in if Mls.mem ls1 s.inst_ls - then error ~loc (ClashSymbol ls1.ls_name.id_string); + then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string); { s with inst_ls = Mls.add ls1 ls2 s.inst_ls } | CSpsym (loc,p,q) -> let ls1 = find_psymbol_ns p t.th_export in let ls2 = find_psymbol q th in if Mls.mem ls1 s.inst_ls - then error ~loc (ClashSymbol ls1.ls_name.id_string); + then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string); { s with inst_ls = Mls.add ls1 ls2 s.inst_ls } | CSlemma (loc,p) -> let pr = find_prop_ns p t.th_export in if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal - then error ~loc (ClashSymbol pr.pr_name.id_string); + then Loc.error ~loc (ClashSymbol pr.pr_name.id_string); { s with inst_lemma = Spr.add pr s.inst_lemma } | CSgoal (loc,p) -> let pr = find_prop_ns p t.th_export in if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal - then error ~loc (ClashSymbol pr.pr_name.id_string); + then Loc.error ~loc (ClashSymbol pr.pr_name.id_string); { s with inst_goal = Spr.add pr s.inst_goal } in List.fold_left add_inst empty_inst s @@ -1109,10 +748,8 @@ let type_inst th t s = let add_use_clone env lenv th loc (use, subst) = if Debug.test_flag debug_parse_only then th else let use_or_clone th = - let q, id = split_qualid use.use_theory in - let t = find_theory env lenv q id in - if Debug.test_flag Glob.flag then - Glob.use (match use.use_theory with Qident x | Qdot (_,x) -> x.id_loc) t.th_name; + let t = find_theory env lenv use.use_theory in + if Debug.test_flag Glob.flag then Glob.use (qloc use.use_theory) t.th_name; match subst with | None -> use_export th t | Some s -> @@ -1135,7 +772,7 @@ let close_theory lenv th = let th = close_theory th in let id = th.th_name.id_string in let loc = th.th_name.Ident.id_loc in - if Mstr.mem id lenv then error ?loc (ClashTheory id); + if Mstr.mem id lenv then Loc.error ?loc (ClashTheory id); Mstr.add id th lenv let close_namespace loc import th = @@ -1149,7 +786,7 @@ let open_file, close_file = let open_file env path = Stack.push Mstr.empty lenv; let open_theory id = - Stack.push (Theory.create_theory ~path (Denv.create_user_id id)) uc in + Stack.push (Theory.create_theory ~path (create_user_id id)) uc in let close_theory () = Stack.push (close_theory (Stack.pop lenv) (Stack.pop uc)) lenv in let open_namespace name = @@ -1174,6 +811,19 @@ let open_file, close_file = let close_file () = Stack.pop lenv in open_file, close_file +(** Exception printing *) + +let () = Exn_printer.register (fun fmt e -> match e with + | UnboundSymbol q -> + fprintf fmt "unbound symbol '%a'" print_qualid q + | UnboundTypeVar s -> + fprintf fmt "unbound type variable '%s" s + | DuplicateTypeVar s -> + fprintf fmt "duplicate type parameter '%s" s + | ClashTheory s -> + fprintf fmt "clash with previous theory %s" s + | _ -> raise e) + (* Local Variables: compile-command: "unset LANG; make -C ../.." diff --git a/src/parser/typing.mli b/src/parser/typing.mli index 23b32a2c8..7d8430cf3 100644 --- a/src/parser/typing.mli +++ b/src/parser/typing.mli @@ -40,9 +40,10 @@ val close_file : unit -> theory Mstr.t (***************************************************************************) val create_user_tv : string -> tvsymbol +val create_user_id : Ptree.ident -> Ident.preid +val string_list_of_qualid : Ptree.qualid -> string list val print_qualid : Format.formatter -> Ptree.qualid -> unit -val split_qualid : Ptree.qualid -> string list * string val qloc : Ptree.qualid -> Loc.position val find_ns : diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml index 8a4b27d98..6f0909449 100644 --- a/src/whyml/mlw_typing.ml +++ b/src/whyml/mlw_typing.ml @@ -143,6 +143,10 @@ let rec dity_of_pty denv = function | Ptree.PPTtuple pl -> let dl = List.map (dity_of_pty denv) pl in ts_app (ts_tuple (List.length pl)) dl + | Ptree.PPTarrow (ty1, ty2) -> + ts_app ts_func [dity_of_pty denv ty1; dity_of_pty denv ty2] + | Ptree.PPTparen ty -> + dity_of_pty denv ty let opaque_binders acc args = List.fold_left (fun acc (_,_,dty) -> opaque_tvs acc dty) acc args @@ -187,12 +191,16 @@ let pass_opacity (e,_) bl = match find_top_pty e with | Some pty -> let ht = Hstr.create 3 in let rec fill = function + | Ptree.PPTparen ty -> fill ty + | Ptree.PPTarrow (ty1, ty2) -> fill ty1; fill ty2 | Ptree.PPTtyapp (_, pl) | Ptree.PPTtuple pl -> List.iter fill pl | Ptree.PPTtyvar (id, true) -> Hstr.replace ht id.id () | Ptree.PPTtyvar _ -> () in fill pty; if Hstr.length ht = 0 then bl else let rec pass = function + | Ptree.PPTparen ty -> pass ty + | Ptree.PPTarrow (ty1, ty2) -> Ptree.PPTarrow (pass ty1, pass ty2) | Ptree.PPTtyvar (id,op) -> Ptree.PPTtyvar (id, op || Hstr.mem ht id.id) | Ptree.PPTtyapp (p, pl) -> Ptree.PPTtyapp (p, List.map pass pl) | Ptree.PPTtuple pl -> Ptree.PPTtuple (List.map pass pl) in @@ -338,7 +346,7 @@ let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with | Ptree.PPpwild -> PPwild, denv | Ptree.PPpvar id -> - PPvar (Denv.create_user_id id), add_var id dity denv + PPvar (Typing.create_user_id id), add_var id dity denv | Ptree.PPpapp (q,ppl) -> let sym, dvty = specialize_qualid denv.uc q in dpat_app denv loc (mk_dexpr sym dvty loc Slab.empty) ppl dity @@ -364,7 +372,7 @@ let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with PPor (pp1, pp2), denv | Ptree.PPpas (pp, id) -> let pp, denv = dpattern denv pp dity in - PPas (pp, Denv.create_user_id id), add_var id dity denv + PPas (pp, Typing.create_user_id id), add_var id dity denv and dpat_app denv gloc ({ de_loc = loc } as de) ppl dity = let ls = match de.de_desc with @@ -529,9 +537,9 @@ and de_desc denv loc = function | Ptree.Einfix (e1, op1, e2) when chainable_op denv op1 -> get_chain e1 ((op1, dexpr denv e2) :: acc) | _ -> e12, acc in + let ch = [op2, dexpr denv e3] in let e1, ch = if chainable_op denv op2 - then get_chain e12 [op2, dexpr denv e3] - else e12, [op2, dexpr denv e3] in + then get_chain e12 ch else e12, ch in make_chain "q1 " "q2 " (dexpr denv e1) ch | Ptree.Elet (id, gh, e1, e2) -> let e1 = dexpr denv e1 in @@ -893,7 +901,7 @@ let add_local x lv lenv = match lv with let binders bl = let binder (id, ghost, dity) = - create_pvsymbol (Denv.create_user_id id) ~ghost (ity_of_dity dity) in + create_pvsymbol (Typing.create_user_id id) ~ghost (ity_of_dity dity) in List.map binder bl let add_binders lenv pvl = @@ -1194,7 +1202,7 @@ and expr_desc lenv loc de = match de.de_desc with | DElet (x, gh, de1, de2) -> let e1 = e_ghostify gh (expr lenv de1) in let mk_expr e1 = - let def1 = create_let_defn (Denv.create_user_id x) e1 in + let def1 = create_let_defn (Typing.create_user_id x) e1 in let lenv = add_local x.id def1.let_sym lenv in let e2 = expr lenv de2 in let e2_unit = match e2.e_vty with @@ -1314,7 +1322,7 @@ and expr_desc lenv loc de = match de.de_desc with in e_try e1 (List.rev_map mk_branch xsl) | DEmark (x, de1) -> - let ld = create_let_defn (Denv.create_user_id x) e_now in + let ld = create_let_defn (Typing.create_user_id x) e_now in let lenv = add_local x.id ld.let_sym lenv in e_let ld (expr lenv de1) | DEany dtyc -> @@ -1329,7 +1337,7 @@ and expr_desc lenv loc de = match de.de_desc with | DEfor (x,defrom,dir,deto,inv,de1) -> let efrom = expr lenv defrom in let eto = expr lenv deto in - let pv = create_pvsymbol (Denv.create_user_id x) ity_int in + let pv = create_pvsymbol (Typing.create_user_id x) ity_int in let lenv = add_local x.id (LetV pv) lenv in let inv = create_pre lenv inv in let e1 = expr lenv de1 in @@ -1344,7 +1352,7 @@ and expr_rec lenv dfdl = if fst de.de_type <> [] then errorm ~loc:de.de_loc "The body of a recursive function must be a first-order value"; let aty = vty_arrow pvl (VTvalue (ity_of_dity (snd de.de_type))) in - let ps = create_psymbol (Denv.create_user_id id) ~ghost:gh aty in + let ps = create_psymbol (Typing.create_user_id id) ~ghost:gh aty in add_local id.id (LetA ps) lenv, (ps, gh, pvl, tr) in let lenv, fdl = Lists.map_fold_left step1 lenv dfdl in let step2 (ps, gh, pvl, tr) = ps, expr_lam lenv gh pvl tr in @@ -1388,7 +1396,7 @@ and expr_fun lenv x gh bl (de, dsp as tr) = let spec = { lam.l_spec with c_post = post } in { lam with l_spec = spec } in let lam = lambda_invariant lenv lam in - let fd = create_fun_defn (Denv.create_user_id x) lam in + let fd = create_fun_defn (Typing.create_user_id x) lam in Loc.try4 ~loc:de.de_loc check_lambda_effect lenv fd bl dsp; Loc.try2 ~loc:x.id_loc check_user_ps false fd.fun_ps; fd @@ -1464,6 +1472,8 @@ let add_types ~wp uc tdl = | _ -> seen in let rec check seen = function | PPTtyvar _ -> seen + | PPTparen ty -> check seen ty + | PPTarrow (ty1,ty2) -> check (check seen ty1) ty2 | PPTtyapp (q,tyl) -> List.fold_left check (ts_seen seen q) tyl | PPTtuple tyl -> List.fold_left check seen tyl in let seen = match d.td_def with @@ -1487,6 +1497,8 @@ let add_types ~wp uc tdl = in let rec check = function | PPTtyvar _ -> false + | PPTparen ty -> check ty + | PPTarrow (ty1,ty2) -> check ty1 || check ty2 | PPTtyapp (q,tyl) -> ts_imp q || List.exists check tyl | PPTtuple tyl -> List.exists check tyl in Hstr.replace impures x false; @@ -1524,6 +1536,8 @@ let add_types ~wp uc tdl = in let rec check = function | PPTtyvar _ -> false + | PPTparen ty -> check ty + | PPTarrow (ty1,ty2) -> check ty1 || check ty2 | PPTtyapp (q,tyl) -> ts_mut q || List.exists check tyl | PPTtuple tyl -> List.exists check tyl in Hstr.replace mutables x false; @@ -1565,7 +1579,7 @@ let add_types ~wp uc tdl = Mstr.add_new e id.id tv acc in let vars = List.fold_left add_tv Mstr.empty d.td_params in let vl = List.map (fun id -> Mstr.find id.id vars) d.td_params in - let id = Denv.create_user_id d.td_ident in + let id = Typing.create_user_id d.td_ident in let abst = d.td_vis = Abstract in let priv = d.td_vis = Private in Hstr.add tysymbols x None; @@ -1586,6 +1600,10 @@ let add_types ~wp uc tdl = | PPTtuple tyl -> let ts = ts_tuple (List.length tyl) in ity_pur ts (List.map parse tyl) + | PPTarrow (ty1,ty2) -> + ity_pur ts_func [parse ty1; parse ty2] + | PPTparen ty -> + parse ty in let ts = match d.td_def with | TDalias ty when Hstr.find impures x -> @@ -1619,16 +1637,16 @@ let add_types ~wp uc tdl = if gh <> fd.fd_ghost then Loc.errorm ~loc "this field must be ghost in every constructor"; ignore (Loc.try3 ~loc ity_match sbs fd.fd_ity ity); - (regs, inv), (Some (Denv.create_user_id id), fd) + (regs, inv), (Some (Typing.create_user_id id), fd) with Not_found -> Hstr.replace projs x fd; if not gh then nogh := ity_nonghost_reg !nogh ity; let regs = Sreg.union regs ity.ity_vars.vars_reg in - (regs, inv), (Some (Denv.create_user_id id), fd) + (regs, inv), (Some (Typing.create_user_id id), fd) in let mk_constr s (_loc,cid,pjl) = let s,pjl = Lists.map_fold_left mk_proj s pjl in - s, (Denv.create_user_id cid, pjl) + s, (Typing.create_user_id cid, pjl) in let init = (Sreg.empty, d.td_inv <> []) in let (regs,inv),def = Lists.map_fold_left mk_constr init csl in @@ -1641,7 +1659,7 @@ let add_types ~wp uc tdl = let mk_field (regs,inv) f = let ity = parse f.f_pty in let inv = inv || ity_has_inv ity in - let fid = Denv.create_user_id f.f_ident in + let fid = Typing.create_user_id f.f_ident in let regs,mut = if f.f_mutable then let r = create_region fid ity in Sreg.add r regs, Some r @@ -1657,7 +1675,7 @@ let add_types ~wp uc tdl = let ghost_reg = Sreg.diff regs !nogh in let rl = Sreg.elements regs in let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in - Hstr.replace predefs x [Denv.create_user_id cid, pjl]; + Hstr.replace predefs x [Typing.create_user_id cid, pjl]; PT (create_itysymbol id ~abst ~priv ~inv ~ghost_reg vl rl None) | TDalgebraic _ | TDrecord _ when Hstr.find impures x -> PT (create_itysymbol id ~abst ~priv ~inv:false vl [] None) @@ -1696,6 +1714,10 @@ let add_types ~wp uc tdl = | PPTtuple tyl -> let ts = ts_tuple (List.length tyl) in ity_pur ts (List.map parse tyl) + | PPTarrow (ty1,ty2) -> + ity_pur ts_func [parse ty1; parse ty2] + | PPTparen ty -> + parse ty in match d.td_def with | TDabstract -> @@ -1717,20 +1739,20 @@ let add_types ~wp uc tdl = if gh <> fd.fd_ghost then Loc.errorm ~loc "this field must be ghost in every constructor"; Loc.try2 ~loc ity_equal_check fd.fd_ity ity; - Some (Denv.create_user_id id), fd + Some (Typing.create_user_id id), fd with Not_found -> Hstr.replace projs x fd; - Some (Denv.create_user_id id), fd + Some (Typing.create_user_id id), fd in let mk_constr (_loc,cid,pjl) = - Denv.create_user_id cid, List.map mk_proj pjl in + Typing.create_user_id cid, List.map mk_proj pjl in abstr, (ts, List.map mk_constr csl) :: algeb, alias | TDrecord fl -> let mk_field f = - let fid = Denv.create_user_id f.f_ident in + let fid = Typing.create_user_id f.f_ident in Some fid, mk_field (parse f.f_pty) f.f_ghost None in let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in - let csl = [Denv.create_user_id cid, List.map mk_field fl] in + let csl = [Typing.create_user_id cid, List.map mk_field fl] in abstr, (ts, csl) :: algeb, alias in let abstr,algeb,alias = List.fold_right def_visit tdl ([],[],[]) in @@ -1914,7 +1936,7 @@ let add_pdecl ~wp loc uc = function let e = e_ghostify gh (expr (create_lenv uc) e) in if not gh && e.e_ghost then errorm ~loc "%s must be a ghost variable" id.id; - let def = create_let_defn (Denv.create_user_id id) e in + let def = create_let_defn (Typing.create_user_id id) e in create_let_decl def in add_pdecl_with_tuples ~wp uc pd | Dletrec fdl -> @@ -1925,7 +1947,7 @@ let add_pdecl ~wp loc uc = function add_pdecl_with_tuples ~wp uc pd | Dexn (id, pty) -> let ity = ity_of_dity (dity_of_pty (create_denv uc) pty) in - let xs = create_xsymbol (Denv.create_user_id id) ity in + let xs = create_xsymbol (Typing.create_user_id id) ity in let pd = create_exn_decl xs in add_pdecl_with_tuples ~wp uc pd | Dparam (id, gh, tyv) -> @@ -1934,9 +1956,9 @@ let add_pdecl ~wp loc uc = function let tyv = type_v (create_lenv uc) Spv.empty vars_empty Stv.empty tyv in let lv = match tyv with | VTvalue v -> - LetV (create_pvsymbol (Denv.create_user_id id) ~ghost:gh v) + LetV (create_pvsymbol (Typing.create_user_id id) ~ghost:gh v) | VTarrow a -> - LetA (create_psymbol (Denv.create_user_id id) ~ghost:gh a) in + LetA (create_psymbol (Typing.create_user_id id) ~ghost:gh a) in let pd = create_val_decl lv in add_pdecl_with_tuples ~wp uc pd @@ -1945,7 +1967,9 @@ let add_pdecl ~wp loc uc d = Loc.try3 ~loc (add_pdecl ~wp) loc uc d let use_clone_pure lib mth uc loc (use,inst) = - let path, s = Typing.split_qualid use.use_theory in + let path, s = match use.use_theory with + | Qdot (p,id) -> Typing.string_list_of_qualid p, id.id + | Qident id -> [], id.id in let th = find_theory loc lib mth path s in (* open namespace, if any *) let uc = match use.use_import with @@ -1967,7 +1991,9 @@ let use_clone_pure lib mth uc loc use = Loc.try5 ~loc use_clone_pure lib mth uc loc use let use_clone lib mmd mth uc loc (use,inst) = - let path, s = Typing.split_qualid use.use_theory in + let path, s = match use.use_theory with + | Qdot (p,id) -> Typing.string_list_of_qualid p, id.id + | Qident id -> [], id.id in let mth = find_module loc lib mmd mth path s in (* open namespace, if any *) let uc = match use.use_import with @@ -2020,9 +2046,9 @@ let open_file, close_file = let wp = path = [] && Debug.test_noflag Typing.debug_type_only in Stack.push (Mstr.empty,Mstr.empty) lenv; let open_theory id = Stack.push false inm; - Stack.push (Theory.create_theory ~path (Denv.create_user_id id)) tuc in + Stack.push (Theory.create_theory ~path (Typing.create_user_id id)) tuc in let open_module id = Stack.push true inm; - Stack.push (create_module env ~path (Denv.create_user_id id)) muc in + Stack.push (create_module env ~path (Typing.create_user_id id)) muc in let close_theory () = ignore (Stack.pop inm); Stack.push (close_theory (Stack.pop lenv) (Stack.pop tuc)) lenv in let close_module () = ignore (Stack.pop inm); -- GitLab