Commit 7bd13b2f authored by Andrei Paskevich's avatar Andrei Paskevich

Expr: restore_ps from logical symbols

parent ed5ae9e3
......@@ -41,12 +41,18 @@ let ps_equal : psymbol -> psymbol -> bool = (==)
let ps_hash ps = id_hash ps.ps_name
let ps_compare ps1 ps2 = id_compare ps1.ps_name ps2.ps_name
let mk_ps id cty gh lg = {
ps_name = id;
ps_cty = cty;
ps_ghost = gh;
ps_logic = lg;
}
let mk_ps, restore_ps =
let ls_to_ps = Wls.create 17 in
(fun id cty gh lg ->
let ps = {
ps_name = id;
ps_cty = cty;
ps_ghost = gh;
ps_logic = lg;
} in
Wls.set ls_to_ps ls ps;
ps),
(fun ls -> Wls.find ls_to_ps ls)
type ps_kind =
| PKnone (* non-pure symbol *)
......
......@@ -53,3 +53,6 @@ val create_psymbol : preid -> ?ghost:bool -> ?kind:ps_kind -> cty -> psymbol
but regions are instantiable. If [?kind] is [PKpred] the result
type must be [ity_bool]. If [?kind] is [PKlemma] and the result
type is not [ity_unit], an existential premise is generated. *)
val restore_ps : lsymbol -> psymbol
(** raises [Not_found] if the argument is not a [ps_logic] *)
......@@ -437,7 +437,7 @@ let create_itysymbol_unsafe, restore_its =
} in
Wts.set ts_to_its ts its;
its),
Wts.find ts_to_its
(fun ts -> Wts.find ts_to_its ts)
let create_itysymbol name args pri mut regs fld def =
(* prepare arguments *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment