Commit 22f8d955 authored by Andrei Paskevich's avatar Andrei Paskevich

built-in symbols for higher-order

parent f8ea7876
......@@ -39,6 +39,7 @@ let create_env = let c = ref (-1) in fun retrieve ->
let add th m = Mnm.add th.th_name.id_string th m in
let m = Mnm.empty in
let m = add builtin_theory m in
let m = add highord_theory m in
let m = add (tuple_theory 0) m in
let m = add (tuple_theory 1) m in
let m = add (tuple_theory 2) m in
......
......@@ -571,28 +571,6 @@ let f_or = f_binary For
let f_implies = f_binary Fimplies
let f_iff = f_binary Fiff
(* built-in symbols *)
let ps_equ =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix =") [v; v]
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_not (f_app ps_equ [t1; t2])
let fs_tuple = Util.memo_int 17 (fun n ->
let tyl = ref [] in
for i = 1 to n
do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
let ty = ty_tuple !tyl in
create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty)
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)
let t_tuple tl =
let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
t_app (fs_tuple (List.length tl)) tl ty
(* unsafe map *)
let bound_map fnT fnE (u,b,e) = (u, bnd_map fnT b, fnE e)
......@@ -1044,6 +1022,46 @@ let f_let_close v t1 f2 = f_let t1 (f_close_bound v f2)
let t_eps_close v f = t_eps (f_close_bound v f)
(* built-in symbols *)
let ps_equ =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix =") [v; v]
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_not (f_app ps_equ [t1; t2])
let fs_func_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
let ty_b = ty_var (create_tvsymbol (id_fresh "b")) in
create_fsymbol (id_fresh "infix @!") [ty_func ty_a ty_b; ty_a] ty_b
let ps_pred_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "infix @?") [ty_pred ty_a; ty_a]
let t_func_app fn t = t_app_infer fs_func_app [fn; t]
let f_pred_app pr t = f_app ps_pred_app [pr; t]
let t_func_app_l = List.fold_left t_func_app
let f_pred_app_l pr tl = match List.rev tl with
| t::tl -> f_pred_app (t_func_app_l pr (List.rev tl)) t
| _ -> Pervasives.invalid_arg "f_pred_app_l"
let fs_tuple = Util.memo_int 17 (fun n ->
let tyl = ref [] in
for i = 1 to n
do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
let ty = ty_tuple !tyl in
create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty)
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)
let t_tuple tl =
let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
t_app (fs_tuple (List.length tl)) tl ty
(** Term library *)
(* generic map over types, symbols and variables *)
......
......@@ -353,6 +353,15 @@ val f_neq : term -> term -> fmla
val f_equ_simp : term -> term -> fmla
val f_neq_simp : term -> term -> fmla
val fs_func_app : lsymbol
val ps_pred_app : lsymbol
val t_func_app : term -> term -> term
val f_pred_app : term -> term -> fmla
val t_func_app_l : term -> term list -> term
val f_pred_app_l : term -> term list -> fmla
val fs_tuple : int -> lsymbol
val t_tuple : term list -> term
......
......@@ -696,6 +696,14 @@ let builtin_theory =
let uc = add_logic_decl uc [ps_equ, None] in
close_theory uc
let highord_theory =
let uc = empty_theory (id_fresh "HighOrd") in
let uc = add_ty_decl uc [ts_func, Tabstract] in
let uc = add_ty_decl uc [ts_pred, Tabstract] in
let uc = add_logic_decl uc [fs_func_app, None] in
let uc = add_logic_decl uc [ps_pred_app, None] in
close_theory uc
let create_theory n = use_export (empty_theory n) builtin_theory
let tuple_theory = Util.memo_int 17 (fun n ->
......
......@@ -172,6 +172,8 @@ val clone_meta : tdecl -> theory -> tdecl -> tdecl
val builtin_theory : theory
val highord_theory : theory
val tuple_theory : int -> theory
(* exceptions *)
......
......@@ -218,6 +218,18 @@ let ts_real = create_tysymbol (id_fresh "real") [] None
let ty_int = ty_app ts_int []
let ty_real = ty_app ts_real []
let ts_func =
let tv_a = create_tvsymbol (id_fresh "a") in
let tv_b = create_tvsymbol (id_fresh "b") in
create_tysymbol (id_fresh "func") [tv_a;tv_b] None
let ts_pred =
let tv_a = create_tvsymbol (id_fresh "a") in
create_tysymbol (id_fresh "pred") [tv_a] None
let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]
let ty_pred ty_a = ty_app ts_pred [ty_a]
let ts_tuple = Util.memo_int 17 (fun n ->
let vl = ref [] in
for i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
......
......@@ -102,6 +102,12 @@ val ts_real : tysymbol
val ty_int : ty
val ty_real : ty
val ts_func : tysymbol
val ts_pred : tysymbol
val ty_func : ty -> ty -> ty
val ty_pred : ty -> ty
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
......
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