Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Propagate attributes from Pack Statements #165

Merged
merged 2 commits into from
Jun 23, 2023
Merged

Propagate attributes from Pack Statements #165

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e4bf5a9
Propagate attributes from `Pack` Statements
Gbury Jun 16, 2023
dc9bde4
Propagate annotations to typed statements
Gbury Jun 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions src/loop/parser.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -376,9 +376,13 @@ module Make(State : State.S) = struct

let expand st c =
let ret = match c with
| { S.descr = S.Pack l; _ } ->
| { S.descr = S.Pack l; attrs; _ } ->
let file = State.get State.logic_file st in
st, `Gen (merge, wrap_parser ~file (Gen.of_list l))
let g =
Gen.of_list l
|> Gen.map (S.add_attrs attrs)
in
st, `Gen (merge, wrap_parser ~file g)
(* TODO: filter the statements by passing some options *)
| { S.descr = S.Include file; _ } ->
let logic_file = State.get State.logic_file st in
Expand Down
141 changes: 75 additions & 66 deletions src/loop/typer.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1841,6 +1841,7 @@ module Make
id : Dolmen.Std.Id.t;
loc : Dolmen.Std.Loc.t;
contents : 'a;
attrs : Dolmen.Std.Term.t list;
}

type def = [
Expand Down Expand Up @@ -1908,7 +1909,8 @@ module Make

(* Simple constructor *)
(* let tr implicit contents = { implicit; contents; } *)
let simple id loc (contents: typechecked) = { id; loc; contents; }
let simple id loc attrs (contents: typechecked) =
{ id; loc; attrs; contents; }

let print_def fmt = function
| `Type_alias (id, c, vars, body) ->
Expand Down Expand Up @@ -2009,10 +2011,17 @@ module Make
| `Exit ->
Format.fprintf fmt "@[<hov 2>exit@]"

let print fmt ({ id; loc; contents; } : typechecked stmt) =
Format.fprintf fmt "@[<v 2>%a[%a]:@,%a@]"
let print_attr fmt t =
Format.fprintf fmt "{%a}@," Dolmen.Std.Term.print t

let print_attrs fmt attrs =
List.iter (print_attr fmt) attrs

let print fmt ({ id; loc; attrs; contents; } : typechecked stmt) =
Format.fprintf fmt "@[<v 2>%a[%a]:@,%a%a@]"
Dolmen.Std.Id.print id
Dolmen.Std.Loc.print_compact loc
print_attrs attrs
print_typechecked contents

(* Typechecking *)
Expand Down Expand Up @@ -2074,93 +2083,93 @@ module Make
let input = `Logic (State.get State.logic_file st) in
match normalize st c with
(* State&Assertion stack management *)
| { S.descr = S.Reset; _ } ->
let st = Typer.reset st ~loc:c.S.loc () in
st, simple (other_id c) c.S.loc `Reset
| { S.descr = S.Pop i; _ } ->
let st = Typer.pop st ~input ~loc:c.S.loc i in
st, (simple (other_id c) c.S.loc (`Pop i))
| { S.descr = S.Push i; _ } ->
let st = Typer.push st ~input ~loc:c.S.loc i in
st, (simple (other_id c) c.S.loc (`Push i))
| { S.descr = S.Reset_assertions; _ } ->
let st = Typer.reset_assertions st ~loc:c.S.loc () in
st, (simple (other_id c) c.S.loc `Reset_assertions)
| { S.descr = S.Reset; loc; attrs; _ } ->
let st = Typer.reset st ~loc () in
st, simple (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))
| { 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))
| { S.descr = S.Reset_assertions; loc; attrs; _ } ->
let st = Typer.reset_assertions st ~loc () in
st, (simple (other_id c) loc attrs `Reset_assertions)

(* Plain statements
TODO: allow the `plain` function to return a meaningful value *)
| { S.descr = S.Plain t; _ } ->
st, (simple (other_id c) c.S.loc (`Plain t))
| { S.descr = S.Plain t; loc; attrs; _ } ->
st, (simple (other_id c) loc attrs (`Plain t))

(* Hypotheses and goal statements *)
| { S.descr = S.Prove { hyps; goals }; _ } ->
let st, hyps = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs hyps in
let st, goals = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs goals in
st, (simple (prove_id c) c.S.loc (`Solve (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)))

(* Hypotheses & Goals *)
| { S.descr = S.Clause l; _ } ->
let st, res = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in
let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Clause res) in
| { 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
| { S.descr = S.Antecedent t; _ } ->
let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:false t in
let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Hyp ret) in
| { 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
| { S.descr = S.Consequent t; _ } ->
let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:true t in
let stmt : typechecked stmt = simple (goal_id c) c.S.loc (`Goal ret) in
| { 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

(* Other set_logics should check whether corresponding plugins are activated ? *)
| { S.descr = S.Set_logic s; _ } ->
let st, new_logic = Typer.set_logic st ~input ~loc:c.S.loc s in
st, (simple (other_id c) c.S.loc (`Set_logic (s, new_logic)))
| { 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)))

(* Set/Get info *)
| { S.descr = S.Get_info s; _ } ->
st, (simple (other_id c) c.S.loc (`Get_info s))
| { S.descr = S.Set_info t; _ } ->
st, (simple (other_id c) c.S.loc (`Set_info t))
| { S.descr = S.Get_info s; loc; attrs; _ } ->
st, (simple (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))

(* Set/Get options *)
| { S.descr = S.Get_option s; _ } ->
st, (simple (other_id c) c.S.loc (`Get_option s))
| { S.descr = S.Set_option t; _ } ->
st, (simple (other_id c) c.S.loc (`Set_option t))
| { S.descr = S.Get_option s; loc; attrs; _ } ->
st, (simple (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))

(* Declarations and definitions *)
| { S.descr = S.Defs d; _ } ->
let st, l = Typer.defs ~mode:`Create_id st ~input ~loc:c.S.loc ~attrs:c.S.attrs d in
let res : typechecked stmt = simple (def_id c) c.S.loc (`Defs l) in
| { 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; _ } ->
let st, l = Typer.decls st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in
let res : typechecked stmt = simple (decl_id c) c.S.loc (`Decls l) in
| { 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)

(* Smtlib's proof/model instructions *)
| { S.descr = S.Get_proof; _ } ->
st, (simple (other_id c) c.S.loc `Get_proof)
| { S.descr = S.Get_unsat_core; _ } ->
st, (simple (other_id c) c.S.loc `Get_unsat_core)
| { S.descr = S.Get_unsat_assumptions; _ } ->
st, (simple (other_id c) c.S.loc `Get_unsat_assumptions)
| { S.descr = S.Get_model; _ } ->
st, (simple (other_id c) c.S.loc `Get_model)
| { S.descr = S.Get_value l; _ } ->
let st, l = Typer.terms st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in
st, (simple (other_id c) c.S.loc (`Get_value l))
| { S.descr = S.Get_assignment; _ } ->
st, (simple (other_id c) c.S.loc `Get_assignment)
| { S.descr = S.Get_proof; loc; attrs; _ } ->
st, (simple (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)
| { S.descr = S.Get_unsat_assumptions; loc; attrs; _ } ->
st, (simple (other_id c) loc attrs `Get_unsat_assumptions)
| { S.descr = S.Get_model; loc; attrs; _ } ->
st, (simple (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))
| { S.descr = S.Get_assignment; loc; attrs; _ } ->
st, (simple (other_id c) loc attrs `Get_assignment)
(* Assertions *)
| { S.descr = S.Get_assertions; _ } ->
st, (simple (other_id c) c.S.loc `Get_assertions)
| { S.descr = S.Get_assertions; loc; attrs; _ } ->
st, (simple (other_id c) loc attrs `Get_assertions)
(* Misc *)
| { S.descr = S.Echo s; _ } ->
st, (simple (other_id c) c.S.loc (`Echo s))
| { S.descr = S.Exit; _ } ->
st, (simple (other_id c) c.S.loc `Exit)
| { S.descr = S.Echo s; loc; attrs; _ } ->
st, (simple (other_id c) loc attrs (`Echo s))
| { S.descr = S.Exit; loc; attrs; _ } ->
st, (simple (other_id c) loc attrs `Exit)

(* packs and includes *)
| { S.descr = S.Include _; _ } -> assert false
Expand Down
1 change: 1 addition & 0 deletions src/loop/typer_intf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,6 +186,7 @@ module type S = sig
id : Dolmen.Std.Id.t;
loc : Dolmen.Std.Loc.t;
contents : 'a;
attrs : Dolmen.Std.Term.t list;
}
(** Wrapper around statements. It records implicit type declarations. *)

Expand Down
3 changes: 3 additions & 0 deletions src/standard/statement.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -329,6 +329,9 @@ let annot = Term.apply
let mk ?id ?(loc=Loc.no_loc) ?(attrs=[]) descr =
{ id; descr; loc; attrs; }

let add_attrs attrs t =
{ t with attrs = attrs @ t.attrs; }

(* Pack *)
let pack ?id ?loc ?attrs l =
mk ?id ?loc ?attrs (Pack l)
Expand Down
3 changes: 3 additions & 0 deletions src/standard/statement.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,6 +171,9 @@ include Dolmen_intf.Stmt.Logic

(** {2 Additional functions} *)

val add_attrs : term list -> t -> t
(** Add some attributes to a statement. *)

val mk_decls :
?loc:location -> ?attrs:term list -> recursive:bool -> decl list -> t
(** Create a group of declarations *)
Expand Down