Commit 1ad10d0f authored by Andrei Paskevich's avatar Andrei Paskevich

treat Unit as a built-in theory

the type alias "type unit = tuple0" goes into tasks and
therefore should be retrievable via Env
parent 0bd118d0
......@@ -167,6 +167,7 @@ let read_lib_file lib path =
let get_builtin s =
if s = builtin_theory.th_name.id_string then builtin_theory else
if s = bool_theory.th_name.id_string then bool_theory else
if s = unit_theory.th_name.id_string then unit_theory else
if s = highord_theory.th_name.id_string then highord_theory else
match tuple_theory_name s with
| Some n -> tuple_theory n
......
......@@ -848,6 +848,13 @@ let tuple_theory = Hint.memo 17 (fun n ->
let uc = add_data_decl uc [ts, [fs,pl]] in
close_theory uc)
let unit_theory =
let uc = empty_theory (id_fresh "Unit") ["why3"] in
let ts = create_tysymbol (id_fresh "unit") [] (Some (ty_tuple [])) in
let uc = use_export uc (tuple_theory 0) in
let uc = add_ty_decl uc ts in
close_theory uc
let tuple_theory_name s =
let l = String.length s in
if l < 6 then None else
......
......@@ -198,6 +198,8 @@ val builtin_theory : theory
val bool_theory : theory
val unit_theory : theory
val highord_theory : theory
val tuple_theory : int -> theory
......
......@@ -383,13 +383,6 @@ let add_invariant uc its p =
(* create module *)
let th_unit =
let ts = create_tysymbol (id_fresh "unit") [] (Some ty_unit) in
let uc = create_theory ~path:["why3"] (id_fresh "Unit") in
let uc = Theory.use_export uc (tuple_theory 0) in
let uc = Theory.add_ty_decl uc ts in
close_theory uc
let xs_exit = create_xsymbol (id_fresh "%Exit") ity_unit
let mod_prelude env =
......@@ -412,7 +405,7 @@ let mod_prelude =
let create_module env ?(path=[]) n =
let m = empty_module env n path in
let m = use_export_theory m bool_theory in
let m = use_export_theory m th_unit in
let m = use_export_theory m unit_theory in
let m = use_export m (mod_prelude env) in
m
......
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