Skip to content

Commit

Permalink
Propagate annotations to typed statements
Browse files Browse the repository at this point in the history
  • Loading branch information
@Gbury
Gbury committed Jun 23, 2023
1 parent 95f6df0 commit 002fedd
Show file tree
Hide file tree
Showing 2 changed files with 76 additions and 66 deletions.
141 changes: 75 additions & 66 deletions src/loop/typer.ml
View file
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
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

0 comments on commit 002fedd

Please sign in to comment.