From 6c9a93a033acd5511639294c6f48cb27d9ccaa21 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 2 Nov 2023 14:37:02 +0100 Subject: [PATCH 1/5] Add implicit decls/defs --- doc/tuto.md | 4 +- doc/type.md | 4 +- src/bin/main.ml | 15 +- src/loop/typer.ml | 281 ++++++++++++------ src/loop/typer_intf.ml | 47 +-- src/model/loop.ml | 50 ++-- src/typecheck/core.ml | 53 +++- src/typecheck/core.mli | 1 + src/typecheck/intf.ml | 44 ++- src/typecheck/misc.ml | 7 + src/typecheck/misc.mli | 3 + src/typecheck/thf.ml | 151 +++++++--- tests/typing/errors/smt2_named/dune | 36 +++ tests/typing/errors/smt2_named/flags.dune | 0 .../errors/smt2_named/open_named.expected | 4 + .../typing/errors/smt2_named/open_named.smt2 | 9 + tests/typing/pass/smtlib/v2.6/named/dune | 32 ++ .../smtlib/v2.6/named/multiple_uses.expected | 0 .../pass/smtlib/v2.6/named/multiple_uses.smt2 | 5 + 19 files changed, 544 insertions(+), 202 deletions(-) create mode 100644 tests/typing/errors/smt2_named/dune create mode 100644 tests/typing/errors/smt2_named/flags.dune create mode 100644 tests/typing/errors/smt2_named/open_named.expected create mode 100644 tests/typing/errors/smt2_named/open_named.smt2 create mode 100644 tests/typing/pass/smtlib/v2.6/named/multiple_uses.expected create mode 100644 tests/typing/pass/smtlib/v2.6/named/multiple_uses.smt2 diff --git a/doc/tuto.md b/doc/tuto.md index ceb3ee513..310fd55bd 100644 --- a/doc/tuto.md +++ b/doc/tuto.md @@ -69,8 +69,8 @@ let test file = (* We can loop over the parsed statements to generated the typed statements *) let final_state, rev_typed_stmts = List.fold_left (fun (state, acc) parsed_stmt -> - let state, typed_stmt = Typer.check state parsed_stmt in - (state, typed_stmt :: acc) + let state, typed_stmts = Typer.check state parsed_stmt in + (state, List.rev_append typed_stmts acc) ) (state, []) parsed_statements in let typed_stmts = List.rev rev_typed_stmts in diff --git a/doc/type.md b/doc/type.md index 41bfca309..02c718254 100644 --- a/doc/type.md +++ b/doc/type.md @@ -42,8 +42,8 @@ let state = let () = let final_state, rev_typed_stmts = List.fold_left (fun (state, acc) parsed_stmt -> - let state, typed_stmt = Typer.check state parsed_stmt in - (state, typed_stmt :: acc) + let state, typed_stmts = Typer.check state parsed_stmt in + (state, List.rev_append typed_stmts acc) ) (state, []) parsed in let typed_stmts = List.rev rev_typed_stmts in diff --git a/src/bin/main.ml b/src/bin/main.ml index ae332cf5b..51eb745d8 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -12,12 +12,15 @@ let debug_parsed_pipe st c = Dolmen.Std.Statement.print c; st, c -let debug_typed_pipe st stmt = - if Loop.State.get Loop.State.debug st then - Format.eprintf "[logic][typed][%a] @[%a@]@\n@." - Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc - Loop.Typer_Pipe.print stmt; - st, stmt +let debug_typed_pipe st stmts = + if Loop.State.get Loop.State.debug st then begin + List.iter (fun stmt -> + Format.eprintf "[logic][typed][%a] @[%a@]@\n" + Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc + Loop.Typer_Pipe.print stmt) stmts; + Format.eprintf "@."; + end; + st, stmts (* Run dolmen (regular use) *) diff --git a/src/loop/typer.ml b/src/loop/typer.ml index 72702d956..f209d4b0c 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -996,6 +996,23 @@ let incorrect_sexpression = ) ~name:"Incorrect S-expression" () +let non_closed_named_term = + Report.Error.mk ~code ~mnemonic:"non-cloed-named-term" + ~message:(fun fmt (ty_vars, t_vars) -> + let pp_sep fmt () = Format.fprintf fmt ",@ " in + Format.fprintf fmt "%a:@ %a%a%a" + Format.pp_print_text + "Named terms must be closed, but the following variables \ + are free" + (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.Var.print) ty_vars + (match ty_vars with + | [] -> (fun _ _ -> ()) + | _ :: _ -> pp_sep + ) () + (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Term.Var.print) t_vars + ) + ~name:"Non-closed Named Term" () + let unknown_error = Report.Error.mk ~code:Code.bug ~mnemonic:"unknown-typing-error" ~message:(fun fmt cstr_name -> @@ -1320,9 +1337,11 @@ module Typer(State : State.S) = struct error ~input ~loc st invalid_string_char c | Smtlib2_String.Invalid_escape_sequence (s, i) -> error ~input ~loc st invalid_string_escape_sequence (s, i) - (* Bad sexpr *) + (* Smtlib2 core errors *) | Smtlib2_Core.Incorrect_sexpression msg -> error ~input ~loc st incorrect_sexpression msg + | Smtlib2_Core.Non_closed_named_term (ty_vars, t_vars) -> + error ~input ~loc st non_closed_named_term (ty_vars, t_vars) (* Uncaught exception during type-checking *) | T.Uncaught_exn ((Alarm.Out_of_time | Alarm.Out_of_space | @@ -1748,9 +1767,38 @@ module Typer(State : State.S) = struct let st = warn ~input ~loc st set_logic_not_supported () in st, Dolmen_type.Logic.Auto - (* Declarations *) + (* Some types *) (* ************************************************************************ *) + type decl = [ + | `Term_decl of Dolmen_std.Expr.ty Dolmen_std.Expr.id + | `Type_decl of + Dolmen_std.Expr.type_fun Dolmen_std.Expr.id * + Dolmen_std.Expr.ty_def option + ] + + type def = [ + | `Instanceof of + Dolmen_std.Id.t * Dolmen_std.Expr.ty Dolmen_std.Expr.id * + Dolmen_std.Expr.ty list * + Dolmen_std.Expr.type_ Dolmen_std.Expr.id list * + Dolmen_std.Expr.ty Dolmen_std.Expr.id list * Dolmen_std.Expr.term + | `Term_def of + Dolmen_std.Id.t * Dolmen_std.Expr.ty Dolmen_std.Expr.id * + Dolmen_std.Expr.type_ Dolmen_std.Expr.id list * + Dolmen_std.Expr.ty Dolmen_std.Expr.id list * Dolmen_std.Expr.term + | `Type_alias of + Dolmen_std.Id.t * Dolmen_std.Expr.type_fun Dolmen_std.Expr.id * + Dolmen_std.Expr.type_ Dolmen_std.Expr.id list * Dolmen_std.Expr.ty + ] + + type 'a ret = { + implicit_decls : decl list; + implicit_defs : def list; + ret : 'a; + } + + (* Declarations helpers *) let allow_function_decl (st : State.t) = match (State.get ty_state st).logic with | Smtlib2 logic -> logic.features.free_functions @@ -1784,53 +1832,96 @@ module Typer(State : State.S) = struct if is_function && not (allow_function_decl st) then T._error env (Decl d) Illegal_decl - let check_decls st env l decls = - List.iter2 (check_decl st env) l decls + let tr_decl st env parsed_decl typed_decl = + let () = check_decl st env parsed_decl typed_decl in + typed_decl + + (* definitions helpers *) + let tr_def ~implicit ~recursive typed_def = + match typed_def with + | `Type_alias (id, c, vars, body) -> + if not recursive && not implicit then begin + Dolmen.Std.Expr.Ty.alias_to c vars body; + `Type_alias (id, c, vars, body) + end else + assert false (* TODO: proper exception *) + | `Term_def (id, f, vars, params, body) -> + `Term_def (id, f, vars, params, body) + | `Instanceof (id, f, ty_args, vars, params, body) -> + `Instanceof (id, f, ty_args, vars, params, body) + + let empty_ret ret = + { implicit_decls = []; + implicit_defs = []; + ret; } + + let mk_ret ~f (ret : _ T.ret) = + let implicit_decls = ret.implicit_decls in + let implicit_defs = + List.map (tr_def ~implicit:true ~recursive:false) ret.implicit_defs + in + let ret = f ret.result in + { implicit_decls; implicit_defs; ret; } + + let merge_rets l = + let implicit_decls = + Dolmen_std.Misc.list_concat_map (fun r -> r.implicit_decls) l + in + let implicit_defs = + Dolmen_std.Misc.list_concat_map (fun r -> r.implicit_defs) l + in + let ret = List.map (fun r -> r.ret) l in + { implicit_decls; implicit_defs; ret; } + + (* Declarations *) + (* ************************************************************************ *) - let decls (st : State.t) ~input ?loc ?attrs d = + let decls (st : State.t) ~input ?loc ?attrs d : state * decl list ret = typing_wrap ?attrs ?loc ~input st ~f:(fun env -> - let decls = T.decls env ?attrs d in - let () = check_decls st env d.contents decls in - decls + let ret_decls = T.decls env ?attrs d in + mk_ret ret_decls ~f:(List.map2 (tr_decl st env) d.contents) ) - (* Definitions *) (* ************************************************************************ *) - let defs ~mode st ~input ?loc ?attrs d = + let defs ~mode st ~input ?loc ?attrs d : state * def list ret = typing_wrap ?attrs ?loc ~input st ~f:(fun env -> - let l = T.defs ~mode env ?attrs d in - List.map (fun typed -> - match typed with - | `Type_alias (id, c, vars, body) -> - if not d.recursive then Dolmen.Std.Expr.Ty.alias_to c vars body; - `Type_alias (id, c, vars, body) - | `Term_def (id, f, vars, params, body) -> - `Term_def (id, f, vars, params, body) - | `Instanceof (id, f, ty_args, vars, params, body) -> - `Instanceof (id, f, ty_args, vars, params, body) - ) l + let ret_defs = T.defs ~mode env ?attrs d in + mk_ret ret_defs ~f:(List.map (tr_def ~implicit:false ~recursive:d.recursive)) ) (* Wrappers around the Type-checking module *) (* ************************************************************************ *) - let terms st ~input ?loc ?attrs = function - | [] -> st, [] - | l -> + let terms st ~input ?loc ?attrs l : state * _ ret = + match l with + | [] -> st, empty_ret [] + | _ -> typing_wrap ?attrs ?loc ~input st - ~f:(fun env -> List.map (T.parse_term env) l) + ~f:(fun env -> + let ret_l = List.map (T.term env) l in + let rets = List.map (mk_ret ~f:(fun t -> t)) ret_l in + merge_rets rets + ) - let formula st ~input ?loc ?attrs ~goal:_ (t : Dolmen.Std.Term.t) = + let formula st ~input ?loc ?attrs ~goal:_ t : state * _ ret = typing_wrap ?attrs ?loc ~input st - ~f:(fun env -> T.parse env t) - - let formulas st ~input ?loc ?attrs = function - | [] -> st, [] - | l -> + ~f:(fun env -> + let ret_f = T.formula env t in + mk_ret ret_f ~f:(fun f -> f) + ) + + let formulas st ~input ?loc ?attrs l : state * _ ret = + match l with + | [] -> st, empty_ret [] + | _ -> typing_wrap ?attrs ?loc ~input st - ~f:(fun env -> List.map (T.parse env) l) + ~f:(fun env -> + let ret_l = List.map (T.formula env) l in + let rets = List.map (mk_ret ~f:(fun t -> t)) ret_l in + merge_rets rets + ) end @@ -1884,10 +1975,11 @@ module Make (* Used for representing typed statements *) type +'a stmt = { - id : Dolmen.Std.Id.t; - loc : Dolmen.Std.Loc.t; + id : Dolmen.Std.Id.t; + loc : Dolmen.Std.Loc.t; contents : 'a; - attrs : Dolmen.Std.Term.t list; + attrs : Dolmen.Std.Term.t list; + implicit : bool; } type def = [ @@ -1954,9 +2046,8 @@ module Make type typechecked = [ defs | decls | assume | solve | get_info | set_info | stack_control | exit ] (* Simple constructor *) - (* let tr implicit contents = { implicit; contents; } *) - let simple id loc attrs (contents: typechecked) = - { id; loc; attrs; contents; } + let mk_stmt ?(implicit=false) id loc attrs (contents: typechecked) = + { id; loc; attrs; contents; implicit; } let print_def fmt = function | `Type_alias (id, c, vars, body) -> @@ -2064,7 +2155,7 @@ module Make let print_attrs fmt attrs = List.iter (print_attr fmt) attrs - let print fmt ({ id; loc; attrs; contents; } : typechecked stmt) = + let print fmt ({ id; loc; attrs; contents; implicit = _; } : typechecked stmt) = Format.fprintf fmt "@[%a[%a]:@,%a%a@]" Dolmen.Std.Id.print id Dolmen.Std.Loc.print_compact loc @@ -2074,14 +2165,19 @@ module Make (* Typechecking *) (* ************************************************************************ *) - let stmt_id ref_name = + let new_stmt_id ref_name = let counter = ref 0 in + (fun () -> + let () = incr counter in + let name = Format.sprintf "%s_%d" ref_name !counter in + Dolmen.Std.Id.mk Dolmen.Std.Id.decl name + ) + + let stmt_id ref_name = + let new_id = new_stmt_id ref_name in (fun c -> match c.Dolmen.Std.Statement.id with - | None -> - let () = incr counter in - let name = Format.sprintf "%s_%d" ref_name !counter in - Dolmen.Std.Id.mk Dolmen.Std.Id.decl name + | None -> new_id () | Some id -> id) let def_id = stmt_id "def" @@ -2091,6 +2187,22 @@ module Make let prove_id = stmt_id "prove" let other_id = stmt_id "other" + let implicit_decl_name = new_stmt_id "implicit_decl" + let implicit_def_name = new_stmt_id "implicit_def" + + let implicits loc attrs ({ implicit_decls; implicit_defs; ret = _; } : _ Typer.ret) = + let decls = + List.map (fun d -> + mk_stmt ~implicit:true (implicit_decl_name ()) loc attrs (`Decls [d]) + ) implicit_decls + in + let defs = + List.map (fun d -> + mk_stmt ~implicit:true (implicit_def_name ()) loc attrs (`Defs [d]) + ) implicit_defs + in + decls @ defs + let fv_list l = let l' = List.map Dolmen.Std.Term.fv l in List.sort_uniq Dolmen.Std.Id.compare (List.flatten l') @@ -2132,91 +2244,94 @@ module Make (* State&Assertion stack management *) | { S.descr = S.Reset; loc; attrs; _ } -> let st = Typer.reset st ~loc () in - st, simple (other_id c) loc attrs `Reset + st, [mk_stmt (other_id c) loc attrs `Reset] | { S.descr = S.Pop i; loc; attrs; _ } -> let st = Typer.pop st ~input ~loc i in - st, (simple (other_id c) loc attrs (`Pop i)) + st, [mk_stmt (other_id c) loc attrs (`Pop i)] | { S.descr = S.Push i; loc; attrs; _ } -> let st = Typer.push st ~input ~loc i in - st, (simple (other_id c) loc attrs (`Push i)) + st, [mk_stmt (other_id c) loc attrs (`Push i)] | { S.descr = S.Reset_assertions; loc; attrs; _ } -> let st = Typer.reset_assertions st ~loc () in - st, (simple (other_id c) loc attrs `Reset_assertions) + st, [mk_stmt (other_id c) loc attrs `Reset_assertions] (* Plain statements TODO: allow the `plain` function to return a meaningful value *) | { S.descr = S.Other { name; args; }; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs (`Other (name, args))) + st, [mk_stmt (other_id c) loc attrs (`Other (name, args))] - (* Hypotheses and goal statements *) + (* Prove statements (with local hyps/goals) *) | { S.descr = S.Prove { hyps; goals }; loc; attrs; _ } -> - let st, hyps = Typer.formulas st ~input ~loc ~attrs hyps in - let st, goals = Typer.formulas st ~input ~loc ~attrs goals in - st, (simple (prove_id c) loc attrs(`Solve (hyps, goals))) + let st, h_ret = Typer.formulas st ~input ~loc ~attrs hyps in + let st, g_ret = Typer.formulas st ~input ~loc ~attrs goals in + let prove = mk_stmt (prove_id c) loc attrs (`Solve (h_ret.ret, g_ret.ret)) in + st, (implicits loc attrs h_ret @ + implicits loc attrs g_ret @ + [prove]) (* Hypotheses & Goals *) | { S.descr = S.Clause l; loc; attrs; _ } -> let st, res = Typer.formulas st ~input ~loc ~attrs l in - let stmt : typechecked stmt = simple (hyp_id c) loc attrs (`Clause res) in - st, stmt + let clause : typechecked stmt = mk_stmt (hyp_id c) loc attrs (`Clause res.ret) in + st, (implicits loc attrs res @ [clause]) | { S.descr = S.Antecedent t; loc; attrs; _ } -> - let st, ret = Typer.formula st ~input ~loc ~attrs ~goal:false t in - let stmt : typechecked stmt = simple (hyp_id c) loc attrs (`Hyp ret) in - st, stmt + let st, f = Typer.formula st ~input ~loc ~attrs ~goal:false t in + let hyp : typechecked stmt = mk_stmt (hyp_id c) loc attrs (`Hyp f.ret) in + st, (implicits loc attrs f @ [hyp]) | { S.descr = S.Consequent t; loc; attrs; _ } -> - let st, ret = Typer.formula st ~input ~loc ~attrs ~goal:true t in - let stmt : typechecked stmt = simple (goal_id c) loc attrs (`Goal ret) in - st, stmt + let st, f = Typer.formula st ~input ~loc ~attrs ~goal:true t in + let goal : typechecked stmt = mk_stmt (goal_id c) loc attrs (`Goal f.ret) in + st, (implicits loc attrs f @ [goal]) (* Other set_logics should check whether corresponding plugins are activated ? *) | { S.descr = S.Set_logic s; loc; attrs; _ } -> let st, new_logic = Typer.set_logic st ~input ~loc s in - st, (simple (other_id c) loc attrs (`Set_logic (s, new_logic))) + st, [mk_stmt (other_id c) loc attrs (`Set_logic (s, new_logic))] (* Set/Get info *) | { S.descr = S.Get_info s; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs (`Get_info s)) + st, [mk_stmt (other_id c) loc attrs (`Get_info s)] | { S.descr = S.Set_info t; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs (`Set_info t)) + st, [mk_stmt (other_id c) loc attrs (`Set_info t)] (* Set/Get options *) | { S.descr = S.Get_option s; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs (`Get_option s)) + st, [mk_stmt (other_id c) loc attrs (`Get_option s)] | { S.descr = S.Set_option t; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs (`Set_option t)) + st, [mk_stmt (other_id c) loc attrs (`Set_option t)] (* Declarations and definitions *) - | { S.descr = S.Defs d; loc; attrs; _ } -> - let st, l = Typer.defs ~mode:`Create_id st ~input ~loc ~attrs d in - let res : typechecked stmt = simple (def_id c) loc attrs (`Defs l) in - st, (res) | { S.descr = S.Decls l; loc; attrs; _ } -> - let st, l = Typer.decls st ~input ~loc ~attrs l in - let res : typechecked stmt = simple (decl_id c) loc attrs (`Decls l) in - st, (res) + let st, res = Typer.decls st ~input ~loc ~attrs l in + let decls : typechecked stmt = mk_stmt (decl_id c) loc attrs (`Decls res.ret) in + st, (implicits loc attrs res @ [decls]) + | { S.descr = S.Defs d; loc; attrs; _ } -> + let st, res = Typer.defs ~mode:`Create_id st ~input ~loc ~attrs d in + let defs : typechecked stmt = mk_stmt (def_id c) loc attrs (`Defs res.ret) in + st, (implicits loc attrs res @ [defs]) (* Smtlib's proof/model instructions *) | { S.descr = S.Get_proof; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Get_proof) + st, [mk_stmt (other_id c) loc attrs `Get_proof] | { S.descr = S.Get_unsat_core; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Get_unsat_core) + st, [mk_stmt (other_id c) loc attrs `Get_unsat_core] | { S.descr = S.Get_unsat_assumptions; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Get_unsat_assumptions) + st, [mk_stmt (other_id c) loc attrs `Get_unsat_assumptions] | { S.descr = S.Get_model; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Get_model) + st, [mk_stmt (other_id c) loc attrs `Get_model] | { S.descr = S.Get_value l; loc; attrs; _ } -> - let st, l = Typer.terms st ~input ~loc ~attrs l in - st, (simple (other_id c) loc attrs (`Get_value l)) + let st, res = Typer.terms st ~input ~loc ~attrs l in + st, (implicits loc attrs res @ [mk_stmt (other_id c) loc attrs (`Get_value res.ret)]) | { S.descr = S.Get_assignment; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Get_assignment) + st, [mk_stmt (other_id c) loc attrs `Get_assignment] (* Assertions *) | { S.descr = S.Get_assertions; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Get_assertions) + st, [mk_stmt (other_id c) loc attrs `Get_assertions] (* Misc *) | { S.descr = S.Echo s; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs (`Echo s)) + st, [mk_stmt (other_id c) loc attrs (`Echo s)] | { S.descr = S.Exit; loc; attrs; _ } -> - st, (simple (other_id c) loc attrs `Exit) + st, [mk_stmt (other_id c) loc attrs `Exit] (* packs and includes *) | { S.descr = S.Include _; _ } -> assert false diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml index 1f36c714e..abbbdcb75 100644 --- a/src/loop/typer_intf.ml +++ b/src/loop/typer_intf.ml @@ -36,6 +36,23 @@ module type Typer = sig | `Response of Response.language ] + type decl = [ + | `Type_decl of ty_cst * ty_def option + | `Term_decl of term_cst + ] + + type def = [ + | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty + | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term + | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term + ] + + type 'a ret = { + implicit_decls : decl list; + implicit_defs : def list; + ret : 'a; + } + val reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state @@ -52,38 +69,31 @@ module type Typer = sig state -> input:input -> ?loc:Dolmen.Std.Loc.t -> string -> state * Dolmen_type.Logic.t + val decls : + state -> input:input -> ?loc:Dolmen.Std.Loc.t -> + ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> + state * decl list ret + val defs : mode:[`Create_id | `Use_declared_id] -> state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.defs -> - state * [ - | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty - | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term - | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term - ] list - - val decls : - state -> input:input -> ?loc:Dolmen.Std.Loc.t -> - ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> - state * [ - | `Type_decl of ty_cst * ty_def option - | `Term_decl of term_cst - ] list + state * def list ret val terms : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> - state * term list + state * term list ret val formula : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> - state * formula + state * formula ret val formulas : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> - state * formula list + state * formula list ret val typing_wrap : ?attrs:Dolmen.Std.Term.t list -> @@ -187,6 +197,7 @@ module type S = sig loc : Dolmen.Std.Loc.t; contents : 'a; attrs : Dolmen.Std.Term.t list; + implicit : bool; } (** Wrapper around statements. It records implicit type declarations. *) @@ -268,11 +279,11 @@ module type S = sig val print : Format.formatter -> typechecked stmt -> unit (** Printing funciton for typechecked statements. *) - val check : state -> Dolmen.Std.Statement.t -> state * typechecked stmt + val check : state -> Dolmen.Std.Statement.t -> state * typechecked stmt list (** Typechecks a statement. *) val typecheck : state -> Dolmen.Std.Statement.t -> - state * [ `Continue of typechecked stmt | `Done of unit ] + state * [ `Continue of typechecked stmt list | `Done of unit ] (** Typechecks a statement. *) end diff --git a/src/model/loop.ml b/src/model/loop.ml index 31ad3e932..384905936 100644 --- a/src/model/loop.ml +++ b/src/model/loop.ml @@ -387,9 +387,13 @@ module Make if State.get State.debug st then Format.eprintf "[model][parsed] @[%a@]@." Dolmen.Std.Statement.(print_group print_def) parsed_defs; - let st, defs = + (* We explicitly ignore the implicit decls, as they happen regularly + because of abstract symbols. *) + let st, ({ implicit_decls = _; implicit_defs; ret = defs } : _ Typer.ret) = Typer.defs ~mode:`Use_declared_id st ~input ?attrs parsed_defs in + (* TODO: proper error for implicit defs *) + assert (implicit_defs = []); (* Record inferred abstract values *) let model = List.fold_left (fun model c -> @@ -697,31 +701,33 @@ module Make (* Pipe/toplevel function *) (* ************************************************************************ *) - let check st (c : Typer_Pipe.typechecked Typer_Pipe.stmt) = + let check st l = let st = if not (State.get check_model st) then st else begin - let file = State.get State.logic_file st in - let loc = Dolmen.Std.Loc.{ file = file.loc; loc = c.loc; } in - match c.contents with - | #Typer_Pipe.exit - | #Typer_Pipe.decls - | #Typer_Pipe.get_info - | #Typer_Pipe.set_info -> st - | #Typer_Pipe.stack_control -> - State.error ~file ~loc st assertion_stack_not_supported () - | `Defs defs -> - check_defs ~file ~loc st defs - | `Hyp contents -> - check_hyps ~file ~loc st contents - | `Goal contents -> - check_goal ~file ~loc st contents - | `Clause contents -> - check_clause ~file ~loc st contents - | `Solve (hyps, goals) -> - check_solve ~file ~loc st hyps goals + List.fold_left (fun st (c : Typer_Pipe.typechecked Typer_Pipe.stmt) -> + let file = State.get State.logic_file st in + let loc = Dolmen.Std.Loc.{ file = file.loc; loc = c.loc; } in + match c.contents with + | #Typer_Pipe.exit + | #Typer_Pipe.decls + | #Typer_Pipe.get_info + | #Typer_Pipe.set_info -> st + | #Typer_Pipe.stack_control -> + State.error ~file ~loc st assertion_stack_not_supported () + | `Defs defs -> + check_defs ~file ~loc st defs + | `Hyp contents -> + check_hyps ~file ~loc st contents + | `Goal contents -> + check_goal ~file ~loc st contents + | `Clause contents -> + check_clause ~file ~loc st contents + | `Solve (hyps, goals) -> + check_solve ~file ~loc st hyps goals + ) st l end in - st, c + st, l end diff --git a/src/typecheck/core.ml b/src/typecheck/core.ml index a16b85bcc..6b573376c 100644 --- a/src/typecheck/core.ml +++ b/src/typecheck/core.ml @@ -501,6 +501,7 @@ module Smtlib2 = struct type _ Type.err += | Incorrect_sexpression : Dolmen.Intf.Msg.t -> Dolmen.Std.Term.t Type.err + | Non_closed_named_term : Type.Ty.Var.t list * Type.T.Var.t list -> Dolmen.Std.Term.t Type.err let inferred_model_constants = Dolmen.Std.Tag.create () @@ -514,14 +515,9 @@ module Smtlib2 = struct Type.set_global_custom_state state inferred_model_constants (c :: l) let parse_name env = function - | ({ Ast.term = Ast.Symbol s; _ } as ast) - | ({ Ast.term = Ast.App ({ Ast.term = Ast.Symbol s; _ }, []); _ } as ast) -> - begin match Dolmen.Std.Id.name s with - | Simple s -> s - | _ -> Type._error env (Ast ast) (Type.Expected ("simple name", None)) - end - | ast -> - Type._error env (Ast ast) (Type.Expected ("symbol", None)) + | { Ast.term = Ast.Symbol s; _ } + | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s; _ }, []); _ } -> s + | ast -> Type._error env (Ast ast) (Type.Expected ("symbol", None)) let extract_sexpr_list_from_sexpr env = function | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Sexpr; _ }, l); _} -> l @@ -598,10 +594,43 @@ module Smtlib2 = struct (* Named formulas *) | Type.Id { name = Simple ":named"; ns = Attr } -> - Type.builtin_tags (Base.make_op1 (module Type) env s (fun _ t -> - let name = parse_name env t in - [Type.Set (Tag.named, name)] - )) + begin match version with + | `Response _ -> + (* ":named" attributes in models do not make sense. + TODO: maybe a proper error here would be better ? *) + `Not_found + | `Script _ -> + Type.builtin_tags (Base.make_op1 (module Type) env s (fun _ named -> + [Type.Hook (fun res_ast res -> + match (res : Type.res) with + | Term t -> + (* Check that the named term is closed *) + begin match Type.T.fv t with + | [], [] -> () + | ty_vars, t_vars -> + Type._error env (Type.Ast res_ast) + (Non_closed_named_term (ty_vars, t_vars)) + end; + let ty = Type.T.ty t in + let id = parse_name env named in + let path = Type.cst_path env id.name in + let f = Type.T.Const.mk path ty in + (* Ids in attributes are created with namespace Attr, but named ids + are meant to be also used in terms, so we need to tweak the + namespace before declaring the binding. *) + let bound_id = { id with ns = Term } in + Type.decl_term_const env (Type.Ast res_ast) bound_id f + (Type.Implicit_in_term (Type.file env, res_ast)); + Type.register_implicit env + (`Term_def (bound_id, f, [], [], t)); + Type.T.Const.set_tag f Tag.named ""; + Type.Term (Type.T.apply_cst f [] []) + | _ -> + assert false + ) + ] + )) + end (* Trigger annotations *) | Type.Id { name = Simple ":pattern"; ns = Attr } -> diff --git a/src/typecheck/core.mli b/src/typecheck/core.mli index 6264284e4..1f65d5f32 100644 --- a/src/typecheck/core.mli +++ b/src/typecheck/core.mli @@ -79,6 +79,7 @@ module Smtlib2 : sig type _ Type.err += | Incorrect_sexpression : Dolmen.Intf.Msg.t -> Dolmen.Std.Term.t Type.err + | Non_closed_named_term : Type.Ty.Var.t list * Type.T.Var.t list -> Dolmen.Std.Term.t Type.err val inferred_model_constants : Type.T.Const.t list Dolmen.Std.Tag.t diff --git a/src/typecheck/intf.ml b/src/typecheck/intf.ml index 7bc5c1fc5..2f100d664 100644 --- a/src/typecheck/intf.ml +++ b/src/typecheck/intf.ml @@ -128,9 +128,10 @@ module type Formulas = sig type tag = | Set : 'a ast_tag * 'a -> tag | Add : 'a list ast_tag * 'a -> tag + | Hook : (Dolmen.Std.Term.t -> res -> res) -> tag (** Existencial wrapper around tags *) - type res = + and res = | Ttype | Ty of ty | Term of term @@ -228,7 +229,6 @@ module type Formulas = sig type not_found = [ `Not_found ] (** Not bound bindings *) - type var_kind = [ | `Let_bound | `Quantified @@ -242,6 +242,18 @@ module type Formulas = sig | Builtin of Dolmen.Std.Term.builtin (**) (** Wrapper around potential function symbols from the Dolmen AST. *) + type decl = [ + | `Type_decl of ty_cst * ty_def option + | `Term_decl of term_cst + ] + + type def = [ + | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty + | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term + | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term + ] + + type implicit = [ decl | def ] (** {2 Errors and warnings} *) @@ -495,6 +507,9 @@ module type Formulas = sig val _error : env -> 'a fragment -> 'a err -> _ (** Raise an error *) + val file : env -> Dolmen.Std.Loc.file + (** Return the current file for th eenv. *) + val suggest : limit:int -> env -> Dolmen.Std.Id.t -> Dolmen.Std.Id.t list (** From a dolmen identifier, return a list of existing bound identifiers in the env that are up to [~limit] in terms of distance of edition. *) @@ -584,7 +599,8 @@ module type Formulas = sig (** Declare a new term constant in the global environment used by the given environment *) - + val register_implicit : env -> implicit -> unit + (** Register a new implicit declaration/definition *) (** {2 Custom global state} *) @@ -653,25 +669,25 @@ module type Formulas = sig (** {2 High-level functions} *) + type 'a ret = { + implicit_decls : decl list; + implicit_defs : def list; + result : 'a; + } + val decls : env -> ?attrs:Dolmen.Std.Term.t list -> - Dolmen.Std.Statement.decls -> [ - | `Type_decl of ty_cst * ty_def option - | `Term_decl of term_cst - ] list + Dolmen.Std.Statement.decls -> decl list ret (** Parse a list of potentially mutually recursive declarations. *) val defs : ?mode:[`Create_id | `Use_declared_id] -> env -> ?attrs:Dolmen.Std.Term.t list -> - Dolmen.Std.Statement.defs -> [ - | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty - | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term - | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term - ] list + Dolmen.Std.Statement.defs -> def list ret (** Parse a definition *) - val parse : term typer - (** Parse a formula *) + val term : env -> Dolmen.Std.Term.t -> term ret + val formula : env -> Dolmen.Std.Term.t -> term ret + (** Top-level functions to typecheck terms and formulas. *) end diff --git a/src/typecheck/misc.ml b/src/typecheck/misc.ml index a3798d028..3eca3e440 100644 --- a/src/typecheck/misc.ml +++ b/src/typecheck/misc.ml @@ -61,6 +61,13 @@ module Lists = struct aux f accu (x :: l_accu) l in aux f accu [] l + let split3 l = + let rec aux l1 l2 l3 = function + | [] -> List.rev l1, List.rev l2, List.rev l3 + | (a, b, c) :: r -> aux (a :: l1) (b :: l2) (c :: l3) r + in + aux [] [] [] l + end (* String manipulation *) diff --git a/src/typecheck/misc.mli b/src/typecheck/misc.mli index d770824f5..665fc075b 100644 --- a/src/typecheck/misc.mli +++ b/src/typecheck/misc.mli @@ -47,6 +47,9 @@ module Lists : sig val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list (** Same as {!List.fold_left_map} (which is onlt available for ocaml >= 4.11). *) + val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list + (** Similar to [List.split] but for triplets. *) + end (** String helper *) diff --git a/src/typecheck/thf.ml b/src/typecheck/thf.ml index 884f10875..a015c926f 100644 --- a/src/typecheck/thf.ml +++ b/src/typecheck/thf.ml @@ -106,15 +106,15 @@ module Make type tag = | Set : 'a Tag.t * 'a -> tag | Add : 'a list Tag.t * 'a -> tag + | Hook : (Ast.t -> res -> res) -> tag (* Result of parsing an expression *) - type res = + and res = | Ttype | Ty of Ty.t | Term of T.t | Tags of tag list - (* Wrapper around potential function symbols in Dolmen *) type symbol = Intf.symbol = | Id of Id.t @@ -266,7 +266,6 @@ module Make | `Builtin of builtin_res ] - type var_kind = [ | `Let_bound | `Quantified @@ -275,6 +274,23 @@ module Make ] (** The type of kinds of variables *) + type decl = [ + | `Type_decl of Ty.Const.t * Ty.def option + | `Term_decl of T.Const.t + ] + (** The type of info for top-level declarations *) + + type def = [ + | `Type_alias of Dolmen.Std.Id.t * Ty.Const.t * Ty.Var.t list * Ty.t + | `Term_def of Dolmen.Std.Id.t * T.Const.t * Ty.Var.t list * T.Var.t list * T.t + | `Instanceof of Dolmen.Std.Id.t * T.Const.t * Ty.t list * Ty.Var.t list * T.Var.t list * T.t + ] + (** The type of info for top-level definitions *) + + type implicit = [ decl | def ] + (** Convenient alias for implicit declarations/definitions. *) + + (* Maps & Hashtbls *) (* ************************************************************************ *) @@ -417,10 +433,12 @@ module Make mutable field_locs : reason V.t; (* stores reasons for typing record fields *) + mutable implicits : implicit list; + (** Stores the ids that have been implicitly declared/defined *) + mutable custom : Hmap.map; (* heterogeneous map for theories to store custom information, all the while being kept in sync with changes in the global state. *) - } (* The local environments used for type-checking. *) @@ -527,6 +545,8 @@ module Make let _error env fragment e = raise (Typing_error (Error (env, fragment, e))) + let file env = env.file + let loc env loc : Loc.full = { file = env.file; loc; } @@ -790,6 +810,7 @@ module Make dstrs_locs = S.empty; field_locs = V.empty; custom = Hmap.empty; + implicits = []; } let copy_state st = { @@ -800,6 +821,7 @@ module Make cstrs_locs = st.cstrs_locs; dstrs_locs = st.dstrs_locs; field_locs = st.field_locs; + implicits = st.implicits; } (* Var/Const creation *) @@ -830,6 +852,9 @@ module Make let mk_term_cst env name ty = T.Const.mk (cst_path env name) ty + let register_implicit env (implicit : implicit) = + env.st.implicits <- implicit :: env.st.implicits + (* Const declarations *) let add_global env fragment id reason (v : cst) = @@ -1524,11 +1549,12 @@ module Make | ast -> _error env (Ast ast) Unhandled_ast and apply_attr env res ast l = - let () = List.iter (function - | Set (tag, v) -> set_tag env ast tag v res - | Add (tag, v) -> add_tag env ast tag v res - ) (parse_attrs env [] l) in - res + List.fold_left (fun res tag -> + match (tag : tag) with + | Set (tag, v) -> set_tag env ast tag v res; res + | Add (tag, v) -> add_tag env ast tag v res; res + | Hook f -> f ast res + ) res (parse_attrs env [] l) and parse_attr env ast = match parse_expr (expect_anything env) ast with @@ -2068,6 +2094,7 @@ module Make let n = List.length args in let f = mk_ty_cst env (Id.name s) n in decl_ty_const env (Ast ast) s f (Inferred (env.file, s_ast)); + register_implicit env (`Type_decl (f, None)); sym_infer.sym_hook (`Ty_cst f); parse_app_ty_cst env ast f args end @@ -2090,6 +2117,7 @@ module Make sym.inferred_ty <- f_ty; let f = mk_term_cst env (Id.name s) f_ty in decl_term_const env (Ast ast) s f (Inferred (env.file, s_ast)); + register_implicit env (`Term_decl f); sym_infer.sym_hook (`Term_cst f); f | _ -> assert false @@ -2170,6 +2198,27 @@ module Make let ty = parse_ty env t in ty, None + (* Helpers for toplevel exposed functions *) + (* ************************************************************************ *) + + type 'a ret = { + implicit_decls : decl list; + implicit_defs : def list; + result : 'a; + } + + let mk_ret env result = + let implicits = env.st.implicits in + env.st.implicits <- []; + let implicit_decls, implicit_defs = + List.fold_left (fun (decls, defs) implicit -> + match (implicit : implicit) with + | #decl as d -> d :: decls, defs + | #def as d -> decls, d :: defs + ) ([], []) implicits + in + { implicit_decls; implicit_defs; result; } + (* Typechecking mutually recursive datatypes *) (* ************************************************************************ *) @@ -2300,6 +2349,7 @@ module Make List.iter (function | Set (tag, v) -> Ty.Const.set_tag c tag v | Add (tag, v) -> Ty.Const.add_tag c tag v + | Hook _ -> assert false (* TODO; proper error *) ) tags; env, (id, `Type_decl c) | `Fun_ty (vars, args, ret) -> @@ -2309,6 +2359,7 @@ module Make List.iter (function | Set (tag, v) -> T.Const.set_tag f tag v | Add (tag, v) -> T.Const.add_tag f tag v + | Hook _ -> assert false (* TODO: proper error *) ) tags; env, (id, `Term_decl f) end @@ -2320,6 +2371,7 @@ module Make List.iter (function | Set (tag, v) -> Ty.Const.set_tag c tag v | Add (tag, v) -> Ty.Const.add_tag c tag v + | Hook _ -> assert false (* TODO: proper error *) ) tags; env, (id, `Type_decl c) @@ -2328,40 +2380,43 @@ module Make | `Type_decl c -> decl_ty_const env (Decl t) id c (Declared (env.file, t)) | `Term_decl f -> decl_term_const env (Decl t) id f (Declared (env.file, t)) - let decls env ?(attrs=[]) (d: Stmt.decl Stmt.group) = + let decls env ?(attrs=[]) (d: Stmt.decl Stmt.group) : decl list ret = let tags = List.flatten @@ List.map (fun ast -> - let l = parse_attr env ast in - check_no_free_wildcards env ast; - l + let l = parse_attr env ast in + check_no_free_wildcards env ast; + l ) attrs in - if d.recursive then begin - (* Check well-foundedness *) - check_well_founded env d d.contents; - (* First pre-parse all definitions and generate the typed symbols for them *) - let env, parsed = Misc.Lists.fold_left_map (parse_decl tags) env d.contents in - (* Then, since the decls are recursive, register in the global env the type - const for each decl before fully parsing and defining them. *) - let () = List.iter2 (record_decl env) parsed d.contents in - (* Then parse the complete type definition and define them. - TODO: parse (and thus define them with T) in the topological order - defined by the well-founded check ? *) - let defs = List.map2 (define_decl env) parsed d.contents in - (* Return the defined types *) - defs - end else begin - List.map (fun t -> - (* First pre-parse all definitions and generate the typed symbols for them *) - let env, parsed = parse_decl tags env t in - (* Then parse the complete type definition and define them. *) - let def = define_decl env parsed t in - (* Finally record them in the state *) - let () = record_decl env parsed t in - (* return *) - def - ) d.contents - end + let decls = + if d.recursive then begin + (* Check well-foundedness *) + check_well_founded env d d.contents; + (* First pre-parse all definitions and generate the typed symbols for them *) + let env, parsed = Misc.Lists.fold_left_map (parse_decl tags) env d.contents in + (* Then, since the decls are recursive, register in the global env the type + const for each decl before fully parsing and defining them. *) + let () = List.iter2 (record_decl env) parsed d.contents in + (* Then parse the complete type definition and define them. + TODO: parse (and thus define them with T) in the topological order + defined by the well-founded check ? *) + let defs = List.map2 (define_decl env) parsed d.contents in + (* Return the defined types *) + defs + end else begin + List.map (fun t -> + (* First pre-parse all definitions and generate the typed symbols for them *) + let env, parsed = parse_decl tags env t in + (* Then parse the complete type definition and define them. *) + let def = define_decl env parsed t in + (* Finally record them in the state *) + let () = record_decl env parsed t in + (* return *) + def + ) d.contents + end + in + mk_ret env decls (* Definitions *) (* ************************************************************************ *) @@ -2416,6 +2471,7 @@ module Make List.iter (function | Set (tag, v) -> Ty.Const.set_tag c tag v | Add (tag, v) -> Ty.Const.add_tag c tag v + | Hook _ -> assert false (* TODO: proper error *) ) tags; if defs.Stmt.recursive then _error env (Defs defs) (Type_def_rec d) @@ -2429,6 +2485,7 @@ module Make List.iter (function | Set (tag, v) -> T.Const.set_tag f tag v | Add (tag, v) -> T.Const.add_tag f tag v + | Hook _ -> assert false (* TODO: proper error *) ) tags; decl_term_const env (Def d) d.id f (Defined (env.file, d)); `Term (d.id, f) @@ -2521,8 +2578,9 @@ module Make | `Ty _, `Term _ | (`Term _ | `Instanceof _), `Ty _ -> assert false - let defs ?(mode=`Create_id) env ?(attrs=[]) (d : Stmt.defs) = + let defs ?(mode=`Create_id) env ?(attrs=[]) (d : Stmt.defs) : def list ret = let tags = parse_attrs env [] attrs in + let defs = if d.recursive then begin let envs = List.map (fun _ -> split_env_for_def env) d.contents in let sigs = List.map2 parse_def_sig envs d.contents in @@ -2540,13 +2598,20 @@ module Make finalize_def id ssig def ) d.contents end + in + mk_ret env defs (* High-level parsing function *) (* ************************************************************************ *) - let parse env ast = + let term env ast : _ ret = + let res = parse_term env ast in + let env, res = finalize_wildcards_prop (`Term ast) env ast res in + mk_ret env res + + let formula env ast : _ ret = let res = parse_prop env ast in - let _env, res = finalize_wildcards_prop (`Term ast) env ast res in - res + let env, res = finalize_wildcards_prop (`Term ast) env ast res in + mk_ret env res end diff --git a/tests/typing/errors/smt2_named/dune b/tests/typing/errors/smt2_named/dune new file mode 100644 index 000000000..457a9dbbd --- /dev/null +++ b/tests/typing/errors/smt2_named/dune @@ -0,0 +1,36 @@ +; File auto-generated by gentests.ml + +; Auto-generated part begin +; Test for open_named.smt2 +; Incremental test + +(rule + (target open_named.incremental) + (deps (:input open_named.smt2)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff open_named.expected open_named.incremental))) + +; Full mode test + +(rule + (target open_named.full) + (deps (:input open_named.smt2)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff open_named.expected open_named.full))) + + +; Auto-generated part end diff --git a/tests/typing/errors/smt2_named/flags.dune b/tests/typing/errors/smt2_named/flags.dune new file mode 100644 index 000000000..e69de29bb diff --git a/tests/typing/errors/smt2_named/open_named.expected b/tests/typing/errors/smt2_named/open_named.expected new file mode 100644 index 000000000..bc1a3308a --- /dev/null +++ b/tests/typing/errors/smt2_named/open_named.expected @@ -0,0 +1,4 @@ +File "tests/typing/errors/smt2_named/open_named.smt2", line 6, character 7-30: +6 | (= (! (+ x y z) :named t ) t) + ^^^^^^^^^^^^^^^^^^^^^^^ +Error Named terms must be closed, but the following variables are free: z diff --git a/tests/typing/errors/smt2_named/open_named.smt2 b/tests/typing/errors/smt2_named/open_named.smt2 new file mode 100644 index 000000000..6ade2cc22 --- /dev/null +++ b/tests/typing/errors/smt2_named/open_named.smt2 @@ -0,0 +1,9 @@ +(set-logic UFNIA) +(declare-const x Int) +(declare-const y Int) +(assert + (forall ((z Int)) + (= (! (+ x y z) :named t ) t) + ) +) +(exit) diff --git a/tests/typing/pass/smtlib/v2.6/named/dune b/tests/typing/pass/smtlib/v2.6/named/dune index f557c29d2..d5282e781 100644 --- a/tests/typing/pass/smtlib/v2.6/named/dune +++ b/tests/typing/pass/smtlib/v2.6/named/dune @@ -1,6 +1,38 @@ ; File auto-generated by gentests.ml ; Auto-generated part begin +; Test for multiple_uses.smt2 +; Incremental test + +(rule + (target multiple_uses.incremental) + (deps (:input multiple_uses.smt2)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff multiple_uses.expected multiple_uses.incremental))) + +; Full mode test + +(rule + (target multiple_uses.full) + (deps (:input multiple_uses.smt2)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff multiple_uses.expected multiple_uses.full))) + + ; Test for test-named.smt2 ; Incremental test diff --git a/tests/typing/pass/smtlib/v2.6/named/multiple_uses.expected b/tests/typing/pass/smtlib/v2.6/named/multiple_uses.expected new file mode 100644 index 000000000..e69de29bb diff --git a/tests/typing/pass/smtlib/v2.6/named/multiple_uses.smt2 b/tests/typing/pass/smtlib/v2.6/named/multiple_uses.smt2 new file mode 100644 index 000000000..4de538a21 --- /dev/null +++ b/tests/typing/pass/smtlib/v2.6/named/multiple_uses.smt2 @@ -0,0 +1,5 @@ +(set-logic UFNIA) +(declare-const x Int) +(declare-const y Int) +(assert (= (! (+ x y) :named t ) t)) +(exit) From 885238cb097e19a6ec0c77bedad8b9d827c4c1c3 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 16 Nov 2023 17:57:54 +0100 Subject: [PATCH 2/5] changes + some error handling --- CHANGES.md | 4 +++ src/loop/parser.ml | 1 - src/loop/report.ml | 2 +- src/loop/typer.ml | 8 +++++- src/typecheck/intf.ml | 4 +++ src/typecheck/thf.ml | 64 ++++++++++++++++++++++++------------------- 6 files changed, 52 insertions(+), 31 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 2ee2a3f89..706842da6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -26,6 +26,10 @@ next non linearity and other arithmetic restrictions (PR#184) - More information for reserved Id, resulting in more precise errors when smt2 scripts use reserved ids (PR#193) +- Expose implicit declarations/definitions that happen during + typechecking (PR#199) +- Treat smtlib `:named` annotations as implicit definitions as + required by the spec (PR#199) ### Loop diff --git a/src/loop/parser.ml b/src/loop/parser.ml index af5a86e90..15af9780b 100644 --- a/src/loop/parser.ml +++ b/src/loop/parser.ml @@ -110,7 +110,6 @@ module Make(State : State.S) = struct (* Helper functions *) (* ************************************************************************ *) - let gen_of_llist l = let l = ref l in (fun () -> match Lazy.force !l with diff --git a/src/loop/report.ml b/src/loop/report.ml index fa62c9412..e1f614b14 100644 --- a/src/loop/report.ml +++ b/src/loop/report.ml @@ -170,7 +170,7 @@ module Error = struct let internal_error = mk ~code:Code.bug ~mnemonic:"internal-error" ~message:(fun fmt t -> - Format.fprintf fmt "%t" t) + Format.fprintf fmt "@[%t@ Please report upstream, ^^@]" t) ~name:"Internal Error" () let uncaught_exn = diff --git a/src/loop/typer.ml b/src/loop/typer.ml index f209d4b0c..05dcceb26 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -1284,6 +1284,12 @@ module Typer(State : State.S) = struct error ~input ~loc st incoherent_type_redefinition (id, cst, reason, n) | T.Incoherent_term_redefinition (id, cst, reason, ty) -> error ~input ~loc st incoherent_term_redefinition (id, cst, reason, ty) + | T.Inferred_builtin b -> + error ~input ~loc st Report.Error.internal_error + (Format.dprintf "Inferred_builtin %a" Dolmen.Std.Term.print_builtin b) + | T.Forbidden_hook -> + error ~input ~loc st Report.Error.internal_error + (Format.dprintf "Forbidden Hook") | T.Unhandled_ast -> error ~input ~loc st unhandled_ast (env, fragment) (* Alt-Ergo Functional Array errors *) @@ -1488,7 +1494,7 @@ module Typer(State : State.S) = struct (* Zipperposition Format - no inference of constants - - only the base builtin + - base + arith builtins *) | `Logic Zf -> let poly = T.Flexible in diff --git a/src/typecheck/intf.ml b/src/typecheck/intf.ml index 2f100d664..eb4cf8adf 100644 --- a/src/typecheck/intf.ml +++ b/src/typecheck/intf.ml @@ -418,6 +418,10 @@ module type Formulas = sig | Incoherent_term_redefinition : Dolmen.Std.Id.t * term_cst * reason * ty -> Dolmen.Std.Statement.def err (** *) + | Inferred_builtin : Dolmen.Std.Term.builtin -> Dolmen.Std.Term.t err + (** *) + | Forbidden_hook : Dolmen.Std.Term.t err + (** *) | Uncaught_exn : exn * Printexc.raw_backtrace -> Dolmen.Std.Term.t err (** *) | Unhandled_ast : Dolmen.Std.Term.t err diff --git a/src/typecheck/thf.ml b/src/typecheck/thf.ml index a015c926f..6d92ffcae 100644 --- a/src/typecheck/thf.ml +++ b/src/typecheck/thf.ml @@ -404,6 +404,8 @@ module Make Id.t * Ty.Const.t * reason * int -> Stmt.def err | Incoherent_term_redefinition : Id.t * T.Const.t * reason * Ty.t -> Stmt.def err + | Inferred_builtin : Ast.builtin -> Ast.t err + | Forbidden_hook : Ast.t err | Uncaught_exn : exn * Printexc.raw_backtrace -> Ast.t err | Unhandled_ast : Ast.t err @@ -568,7 +570,7 @@ module Make let rec find_pattern_ast pat asts parsed = match asts, parsed with - | [], _ | _, [] -> assert false + | [], _ | _, [] -> assert false (* internal invariant *) | (ast, _) :: r, (t, _) :: r' -> if pat == t then ast else find_pattern_ast pat r r' @@ -756,6 +758,12 @@ module Make _error env (Def def) (Incoherent_term_redefinition (def.id, cst, reason, ty)) + let _inferred_builtin env ast b = + _error env (Ast ast) (Inferred_builtin b) + + let _forbidden_hook env ast = + _error env (Ast ast) Forbidden_hook + let _wrap_exn env ast = function | Ty.Prenex_polymorphism ty -> _non_prenex_polymorphism env ast ty @@ -834,6 +842,7 @@ module Make let cst_path _env name = match (name : Dolmen.Std.Name.t) with + (* TODO; proper error *) | Indexed _ -> assert false | Simple name -> Dolmen.Std.Path.global name @@ -1157,6 +1166,9 @@ module Make (* variables should not be declare-able nor builtin *) | Builtin | Reserved _ | Declared _ | Defined _ | Implicit_in_def _ | Implicit_in_decl _ | Implicit_in_term _ -> + (* this should never happen, and we could simply do nothing in this case; + the assert is there to see if it can happen and what kind of situation + would trigger that. *) assert false let find_term_var_reason env v = @@ -1171,6 +1183,9 @@ module Make and we do not use any term wildcards. *) | Builtin | Reserved _ | Declared _ | Defined _ | Implicit_in_def _ | Implicit_in_decl _ | Implicit_in_term _ -> + (* this should never happen, and we could simply do nothing in this case; + the assert is there to see if it can happen and what kind of situation + would trigger that. *) assert false @@ -1549,7 +1564,7 @@ module Make | ast -> _error env (Ast ast) Unhandled_ast and apply_attr env res ast l = - List.fold_left (fun res tag -> + List.fold_left (fun res (_ast, tag) -> match (tag : tag) with | Set (tag, v) -> set_tag env ast tag v res; res | Add (tag, v) -> add_tag env ast tag v res; res @@ -1558,7 +1573,7 @@ module Make and parse_attr env ast = match parse_expr (expect_anything env) ast with - | Tags l -> l + | Tags l -> List.map (fun tag -> ast, tag) l | res -> _expected env "tag" ast (Some res) and parse_attrs env acc = function @@ -1979,7 +1994,9 @@ module Make and parse_app_builtin env ast b args = match env.builtins env (Builtin b) with | `Not_found -> _unknown_builtin env ast b - | #builtin_res as b_res -> builtin_apply_builtin env ast b b_res args + | #builtin_infer -> _inferred_builtin env ast b + | #builtin_reserved -> _unknown_builtin env ast b + | #builtin_common as b -> builtin_apply_common env b ast args and builtin_apply_common env b ast args = match (b : builtin_common) with @@ -1988,15 +2005,6 @@ module Make | `Term (_meta, f) -> Term (_wrap2 env ast f ast args) | `Tags (_meta, f) -> Tags (_wrap2 env ast f ast args) - and builtin_apply_builtin env ast b b_res args : res = - match (b_res : builtin_res) with - | #builtin_common as b -> builtin_apply_common env b ast args - | `Reserved ((`Solver _ | `Model _)) -> _unknown_builtin env ast b - | `Infer _ -> - (* TODO: proper erorr. - We do not have a map from builtins symbols to typed expressions. *) - assert false - and parse_builtin env ast b = parse_app_builtin env ast b [] @@ -2347,9 +2355,9 @@ module Make check_no_free_wildcards env ast; let c = mk_ty_cst env (Id.name id) n in List.iter (function - | Set (tag, v) -> Ty.Const.set_tag c tag v - | Add (tag, v) -> Ty.Const.add_tag c tag v - | Hook _ -> assert false (* TODO; proper error *) + | _, Set (tag, v) -> Ty.Const.set_tag c tag v + | _, Add (tag, v) -> Ty.Const.add_tag c tag v + | ast, Hook _ -> _forbidden_hook env ast ) tags; env, (id, `Type_decl c) | `Fun_ty (vars, args, ret) -> @@ -2357,9 +2365,9 @@ module Make let env, ty = finalize_wildcards_ty (`Decl t) env ast ty in let f = mk_term_cst env (Id.name id) ty in List.iter (function - | Set (tag, v) -> T.Const.set_tag f tag v - | Add (tag, v) -> T.Const.add_tag f tag v - | Hook _ -> assert false (* TODO: proper error *) + | _, Set (tag, v) -> T.Const.set_tag f tag v + | _, Add (tag, v) -> T.Const.add_tag f tag v + | ast, Hook _ -> _forbidden_hook env ast ) tags; env, (id, `Term_decl f) end @@ -2369,9 +2377,9 @@ module Make let n = List.length vars in let c = mk_ty_cst env (Id.name id) n in List.iter (function - | Set (tag, v) -> Ty.Const.set_tag c tag v - | Add (tag, v) -> Ty.Const.add_tag c tag v - | Hook _ -> assert false (* TODO: proper error *) + | _, Set (tag, v) -> Ty.Const.set_tag c tag v + | _, Add (tag, v) -> Ty.Const.add_tag c tag v + | ast, Hook _ -> _forbidden_hook env ast ) tags; env, (id, `Type_decl c) @@ -2469,9 +2477,9 @@ module Make assert (params = []); let c = mk_ty_cst env (Id.name d.id) (List.length vars) in List.iter (function - | Set (tag, v) -> Ty.Const.set_tag c tag v - | Add (tag, v) -> Ty.Const.add_tag c tag v - | Hook _ -> assert false (* TODO: proper error *) + | _, Set (tag, v) -> Ty.Const.set_tag c tag v + | _, Add (tag, v) -> Ty.Const.add_tag c tag v + | ast, Hook _ -> _forbidden_hook env ast ) tags; if defs.Stmt.recursive then _error env (Defs defs) (Type_def_rec d) @@ -2483,9 +2491,9 @@ module Make let ty = if freshen then Ty.freshen ty else ty in let f = mk_term_cst env (Id.name d.id) ty in List.iter (function - | Set (tag, v) -> T.Const.set_tag f tag v - | Add (tag, v) -> T.Const.add_tag f tag v - | Hook _ -> assert false (* TODO: proper error *) + | _, Set (tag, v) -> T.Const.set_tag f tag v + | _, Add (tag, v) -> T.Const.add_tag f tag v + | ast, Hook _ -> _forbidden_hook env ast ) tags; decl_term_const env (Def d) d.id f (Defined (env.file, d)); `Term (d.id, f) From 2116d4adb8dc352a59a12575f00ea1ea5fa585f0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 17 Nov 2023 15:12:26 +0100 Subject: [PATCH 3/5] fix typo MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com> --- src/loop/typer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/loop/typer.ml b/src/loop/typer.ml index 05dcceb26..fb3bdd8af 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -997,7 +997,7 @@ let incorrect_sexpression = ~name:"Incorrect S-expression" () let non_closed_named_term = - Report.Error.mk ~code ~mnemonic:"non-cloed-named-term" + Report.Error.mk ~code ~mnemonic:"non-closed-named-term" ~message:(fun fmt (ty_vars, t_vars) -> let pp_sep fmt () = Format.fprintf fmt ",@ " in Format.fprintf fmt "%a:@ %a%a%a" From b2f7cd3f98e692a10d12f3b942b2e8cac50782cf Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 17 Nov 2023 15:22:08 +0100 Subject: [PATCH 4/5] review --- src/loop/typer_intf.ml | 8 +++++++- src/typecheck/core.ml | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml index abbbdcb75..5eb5402bb 100644 --- a/src/loop/typer_intf.ml +++ b/src/loop/typer_intf.ml @@ -280,7 +280,13 @@ module type S = sig (** Printing funciton for typechecked statements. *) val check : state -> Dolmen.Std.Statement.t -> state * typechecked stmt list - (** Typechecks a statement. *) + (** Typechecks a statement. This returns a list because some languages have implicit + declarations and definitions: for intance, tptp has symbol inferrence (which result + in implicit declarations), and smtlib has `:named` annotation (which result in implicit + definitions). The list is returned in dependency order: implicits declarations/definitions + are first in the list, and they should be in an order such that only later statements + can depend on earlier statements. + *) val typecheck : state -> Dolmen.Std.Statement.t -> state * [ `Continue of typechecked stmt list | `Done of unit ] diff --git a/src/typecheck/core.ml b/src/typecheck/core.ml index 6b573376c..90f71c567 100644 --- a/src/typecheck/core.ml +++ b/src/typecheck/core.ml @@ -615,6 +615,7 @@ module Smtlib2 = struct let id = parse_name env named in let path = Type.cst_path env id.name in let f = Type.T.Const.mk path ty in + Type.T.Const.set_tag f Tag.named ""; (* Ids in attributes are created with namespace Attr, but named ids are meant to be also used in terms, so we need to tweak the namespace before declaring the binding. *) @@ -623,7 +624,6 @@ module Smtlib2 = struct (Type.Implicit_in_term (Type.file env, res_ast)); Type.register_implicit env (`Term_def (bound_id, f, [], [], t)); - Type.T.Const.set_tag f Tag.named ""; Type.Term (Type.T.apply_cst f [] []) | _ -> assert false From a759773265e67f5365f9078eb8502ff99f3d0e07 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 17 Nov 2023 16:39:30 +0100 Subject: [PATCH 5/5] change some assert false into proper errors --- src/loop/typer.ml | 47 ++++++++++++++++++++++++++++--------------- src/typecheck/core.ml | 2 +- src/typecheck/intf.ml | 6 +++--- src/typecheck/thf.ml | 20 +++++++++--------- 4 files changed, 45 insertions(+), 30 deletions(-) diff --git a/src/loop/typer.ml b/src/loop/typer.ml index fb3bdd8af..bb5757269 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -960,6 +960,12 @@ let illegal_decl = Format.fprintf fmt "Illegal declaration.") ~name:"Illegal declaration in a file" () +let illegal_def = + Report.Error.mk ~code ~mnemonic:"illegal-def" + ~message:(fun fmt () -> + Format.fprintf fmt "Illegal definition.") + ~name:"Illegal definition" () + let invalid_push = Report.Error.mk ~code ~mnemonic:"invalid-push" ~message:(fun fmt () -> @@ -1136,6 +1142,7 @@ module Typer(State : State.S) = struct | Bad_tptp_kind : string option -> Dolmen.Std.Loc.t T.err | Missing_smtlib_logic : Dolmen.Std.Loc.t T.err | Illegal_decl : Dolmen.Std.Statement.decl T.err + | Illegal_def : Dolmen.Std.Loc.t T.err | Invalid_push_n : Dolmen.Std.Loc.t T.err | Invalid_pop_n : Dolmen.Std.Loc.t T.err | Pop_with_empty_stack : Dolmen.Std.Loc.t T.err @@ -1364,6 +1371,8 @@ module Typer(State : State.S) = struct (* Illegal declarations *) | Illegal_decl -> error ~input ~loc st illegal_decl () + | Illegal_def -> + error ~input ~loc st illegal_def () (* Push/Pop errors *) | Invalid_push_n -> error ~input ~loc st invalid_push () @@ -1432,8 +1441,14 @@ module Typer(State : State.S) = struct (* Match the language to determine bultins and other options *) let lang = match lang_of_input input with - | `Missing -> assert false | #lang as lang -> lang + | `Missing -> + let st = + error st ~input ~loc:{ file; loc; } Report.Error.internal_error + (Format.dprintf "Missing input language \ + (should have been set during parsing)") + in + raise (State.Error st) in let additional_builtins = State.get additional_builtins st st lang in match lang with @@ -1694,7 +1709,6 @@ module Typer(State : State.S) = struct stack = []; } st - let rec push st ~input ?(loc=Dolmen.Std.Loc.no_loc) = function | 0 -> st | i -> @@ -1842,18 +1856,19 @@ module Typer(State : State.S) = struct let () = check_decl st env parsed_decl typed_decl in typed_decl - (* definitions helpers *) - let tr_def ~implicit ~recursive typed_def = + (* Definitions helpers, this function should only be called in the context + of a typing_wrap function. *) + let tr_def env ~implicit ~recursive typed_def = match typed_def with - | `Type_alias (id, c, vars, body) -> + | `Type_alias (loc, id, c, vars, body) -> if not recursive && not implicit then begin Dolmen.Std.Expr.Ty.alias_to c vars body; `Type_alias (id, c, vars, body) end else - assert false (* TODO: proper exception *) - | `Term_def (id, f, vars, params, body) -> + T._error env (Located loc) Illegal_def + | `Term_def (_loc, id, f, vars, params, body) -> `Term_def (id, f, vars, params, body) - | `Instanceof (id, f, ty_args, vars, params, body) -> + | `Instanceof (_loc, id, f, ty_args, vars, params, body) -> `Instanceof (id, f, ty_args, vars, params, body) let empty_ret ret = @@ -1861,10 +1876,10 @@ module Typer(State : State.S) = struct implicit_defs = []; ret; } - let mk_ret ~f (ret : _ T.ret) = + let mk_ret env ~f (ret : _ T.ret) = let implicit_decls = ret.implicit_decls in let implicit_defs = - List.map (tr_def ~implicit:true ~recursive:false) ret.implicit_defs + List.map (tr_def env ~implicit:true ~recursive:false) ret.implicit_defs in let ret = f ret.result in { implicit_decls; implicit_defs; ret; } @@ -1885,7 +1900,7 @@ module Typer(State : State.S) = struct let decls (st : State.t) ~input ?loc ?attrs d : state * decl list ret = typing_wrap ?attrs ?loc ~input st ~f:(fun env -> let ret_decls = T.decls env ?attrs d in - mk_ret ret_decls ~f:(List.map2 (tr_decl st env) d.contents) + mk_ret env ret_decls ~f:(List.map2 (tr_decl st env) d.contents) ) (* Definitions *) @@ -1894,7 +1909,7 @@ module Typer(State : State.S) = struct let defs ~mode st ~input ?loc ?attrs d : state * def list ret = typing_wrap ?attrs ?loc ~input st ~f:(fun env -> let ret_defs = T.defs ~mode env ?attrs d in - mk_ret ret_defs ~f:(List.map (tr_def ~implicit:false ~recursive:d.recursive)) + mk_ret env ret_defs ~f:(List.map (tr_def env ~implicit:false ~recursive:d.recursive)) ) (* Wrappers around the Type-checking module *) @@ -1907,7 +1922,7 @@ module Typer(State : State.S) = struct typing_wrap ?attrs ?loc ~input st ~f:(fun env -> let ret_l = List.map (T.term env) l in - let rets = List.map (mk_ret ~f:(fun t -> t)) ret_l in + let rets = List.map (mk_ret env ~f:(fun t -> t)) ret_l in merge_rets rets ) @@ -1915,7 +1930,7 @@ module Typer(State : State.S) = struct typing_wrap ?attrs ?loc ~input st ~f:(fun env -> let ret_f = T.formula env t in - mk_ret ret_f ~f:(fun f -> f) + mk_ret env ret_f ~f:(fun f -> f) ) let formulas st ~input ?loc ?attrs l : state * _ ret = @@ -1925,7 +1940,7 @@ module Typer(State : State.S) = struct typing_wrap ?attrs ?loc ~input st ~f:(fun env -> let ret_l = List.map (T.formula env) l in - let rets = List.map (mk_ret ~f:(fun t -> t)) ret_l in + let rets = List.map (mk_ret env ~f:(fun t -> t)) ret_l in merge_rets rets ) @@ -2233,7 +2248,7 @@ module Make | free_vars -> let loc = c.S.loc in let f = match l with - | [] -> assert false + | [] -> Dolmen.Std.Term.false_ ~loc () | [p] -> p | _ -> Dolmen.Std.Term.apply ~loc (Dolmen.Std.Term.or_t ~loc ()) l in diff --git a/src/typecheck/core.ml b/src/typecheck/core.ml index 90f71c567..92a70691a 100644 --- a/src/typecheck/core.ml +++ b/src/typecheck/core.ml @@ -623,7 +623,7 @@ module Smtlib2 = struct Type.decl_term_const env (Type.Ast res_ast) bound_id f (Type.Implicit_in_term (Type.file env, res_ast)); Type.register_implicit env - (`Term_def (bound_id, f, [], [], t)); + (`Term_def (res_ast.loc, bound_id, f, [], [], t)); Type.Term (Type.T.apply_cst f [] []) | _ -> assert false diff --git a/src/typecheck/intf.ml b/src/typecheck/intf.ml index eb4cf8adf..3dbfa1777 100644 --- a/src/typecheck/intf.ml +++ b/src/typecheck/intf.ml @@ -248,9 +248,9 @@ module type Formulas = sig ] type def = [ - | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty - | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term - | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term + | `Type_alias of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * ty_cst * ty_var list * ty + | `Term_def of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term + | `Instanceof of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term ] type implicit = [ decl | def ] diff --git a/src/typecheck/thf.ml b/src/typecheck/thf.ml index 6d92ffcae..1d63884e9 100644 --- a/src/typecheck/thf.ml +++ b/src/typecheck/thf.ml @@ -281,9 +281,9 @@ module Make (** The type of info for top-level declarations *) type def = [ - | `Type_alias of Dolmen.Std.Id.t * Ty.Const.t * Ty.Var.t list * Ty.t - | `Term_def of Dolmen.Std.Id.t * T.Const.t * Ty.Var.t list * T.Var.t list * T.t - | `Instanceof of Dolmen.Std.Id.t * T.Const.t * Ty.t list * Ty.Var.t list * T.Var.t list * T.t + | `Type_alias of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * Ty.Const.t * Ty.Var.t list * Ty.t + | `Term_def of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * T.Const.t * Ty.Var.t list * T.Var.t list * T.t + | `Instanceof of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * T.Const.t * Ty.t list * Ty.Var.t list * T.Var.t list * T.t ] (** The type of info for top-level definitions *) @@ -2551,10 +2551,10 @@ module Make _id_def_conflict env d.loc d.id (with_reason (find_reason env bound) bound) - let id_for_def ~freshen ~mode ~defs tags ssig d = + let id_for_def ~freshen ~mode ~defs tags ssig (d : Stmt.def) = match mode with - | `Create_id -> create_id_for_def ~freshen ~defs tags ssig d - | `Use_declared_id -> lookup_id_for_def tags ssig d + | `Create_id -> d.loc, create_id_for_def ~freshen ~defs tags ssig d + | `Use_declared_id -> d.loc, lookup_id_for_def tags ssig d let parse_def (env, _vars, _params, ssig) (d : Stmt.def) = match ssig, parse_expr env d.body with @@ -2565,23 +2565,23 @@ module Make _expected env "term or a type" d.body (Some ret) | _ -> assert false - let finalize_def id (env, vars, params, _ssig) (ast, ret) = + let finalize_def (loc, id) (env, vars, params, _ssig) (ast, ret) = check_no_free_wildcards env ast; match id, ret with (* type alias *) | `Ty (id, c), `Ty body -> assert (params = []); List.iter (check_used_ty_var ~kind:`Type_alias_param env) vars; - `Type_alias (id, c, vars, body) + `Type_alias (loc, id, c, vars, body) (* function definition *) | `Term (id, f), `Term body -> List.iter (check_used_ty_var ~kind:`Function_param env) vars; List.iter (check_used_term_var ~kind:`Function_param env) params; - `Term_def (id, f, vars, params, body) + `Term_def (loc, id, f, vars, params, body) | `Instanceof (id, f, ty_args), `Term body -> List.iter (check_used_ty_var ~kind:`Function_param env) vars; List.iter (check_used_term_var ~kind:`Function_param env) params; - `Instanceof (id, f, ty_args, vars, params, body) + `Instanceof (loc, id, f, ty_args, vars, params, body) (* error cases *) | `Ty _, `Term _ | (`Term _ | `Instanceof _), `Ty _ -> assert false