Commit 298ef03b authored by Andrei Paskevich's avatar Andrei Paskevich

simplify implicit tuple declarations

parent ff7b2bdd
......@@ -759,14 +759,21 @@ let ps_equ =
let t_equ t1 t2 = ps_app ps_equ [t1; t2]
let t_neq t1 t2 = t_not (ps_app ps_equ [t1; t2])
let fs_tuple_ids = Hid.create 17
let fs_tuple = Util.memo_int 17 (fun n ->
let ts = ts_tuple n in
let tl = List.map ty_var ts.ts_args in
let ty = ty_app ts tl in
create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) tl ty)
let fs = create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) tl ty in
Hid.add fs_tuple_ids fs.ls_name n;
fs)
let is_fs_tuple fs = ls_equal fs (fs_tuple (List.length fs.ls_args))
let is_fs_tuple_id id =
try Some (Hid.find fs_tuple_ids id) with Not_found -> None
let t_tuple tl =
let ty = ty_tuple (List.map t_type tl) in
fs_app (fs_tuple (List.length tl)) tl ty
......
......@@ -280,6 +280,7 @@ val fs_tuple : int -> lsymbol (* n-tuple *)
val t_tuple : term list -> term
val is_fs_tuple : lsymbol -> bool
val is_fs_tuple_id : ident -> int option
val fs_func_app : lsymbol (* value-typed higher-order application *)
val ps_pred_app : lsymbol (* prop-typed higher-order application *)
......
......@@ -733,7 +733,6 @@ let on_meta _meta fn acc theory =
acc tdecls
(** Base theories *)
let builtin_theory =
......@@ -769,6 +768,15 @@ let tuple_theory_name s =
if q <> string_of_int i then None else
Some i
let add_decl_with_tuples uc d =
let ids = Mid.set_diff d.d_syms uc.uc_known in
let add id s = match is_ts_tuple_id id with
| Some n -> Sint.add n s
| None -> s in
let ixs = Sid.fold add ids Sint.empty in
let add n uc = use_export uc (tuple_theory n) in
add_decl (Sint.fold add ixs uc) d
(* Exception reporting *)
let print_meta_arg_type fmt = function
......
......@@ -194,6 +194,8 @@ val tuple_theory : int -> theory
val tuple_theory_name : string -> int option
val add_decl_with_tuples : theory_uc -> decl -> theory_uc
(* exceptions *)
exception NonLocal of ident
......
......@@ -235,15 +235,22 @@ let ts_pred =
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_ids = Hid.create 17
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;
create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None)
let ts = create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None in
Hid.add ts_tuple_ids ts.ts_name n;
ts)
let ty_tuple tyl = ty_app (ts_tuple (List.length tyl)) tyl
let is_ts_tuple ts = ts_equal ts (ts_tuple (List.length ts.ts_args))
let is_ts_tuple_id id =
try Some (Hid.find ts_tuple_ids id) with Not_found -> None
(** {2 Operations on [ty option]} *)
exception UnexpectedProp
......
......@@ -127,6 +127,7 @@ val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
val is_ts_tuple : tysymbol -> bool
val is_ts_tuple_id : ident -> int option
(** {2 Operations on [ty option]} *)
......
......@@ -173,30 +173,10 @@ let specialize_tysymbol loc p uc =
(* lazy declaration of tuples *)
let tuples_needed = Hashtbl.create 17
let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n
let add_tuple_decls uc =
Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
tuples_needed uc
let with_tuples ?(reset=false) f uc x =
let uc = f (add_tuple_decls uc) x in
if reset then Hashtbl.clear tuples_needed;
uc
let add_ty_decl = with_tuples add_ty_decl
let add_ty_decls = with_tuples ~reset:true add_ty_decl
let add_logic_decl = with_tuples add_logic_decl
let add_logic_decls = with_tuples ~reset:true add_logic_decl
let add_ind_decl = with_tuples add_ind_decl
let add_ind_decls = with_tuples ~reset:true add_ind_decl
let add_prop_decl = with_tuples ~reset:true add_prop_decl
let add_ty_decl uc dl = add_decl_with_tuples uc (create_ty_decl dl)
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
let add_ind_decl uc dl = add_decl_with_tuples uc (create_ind_decl dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
let rec dty uc env = function
| PPTtyvar {id=x} ->
......@@ -915,7 +895,7 @@ let add_types dl th =
in
ts, d
in
let th = try add_ty_decls th (List.map decl dl)
let th = try add_ty_decl th (List.map decl dl)
with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
in
List.fold_left add_projections th dl
......@@ -1015,7 +995,7 @@ let add_logics dl th =
make_ls_defn fs vl (term env t)
end
in
add_logic_decls th (List.map type_decl dl)
add_logic_decl th (List.map type_decl dl)
let type_term uc denv env t =
let t = dterm uc denv t in
......@@ -1059,7 +1039,7 @@ let add_inductives dl th =
in
ps, List.map clause d.in_def
in
try add_ind_decls th (List.map type_decl dl)
try add_ind_decl th (List.map type_decl dl)
with
| ClashSymbol s -> error ~loc:(Hashtbl.find propsyms s) (Clash s)
| InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)
......
......@@ -79,12 +79,6 @@ val split_qualid : Ptree.qualid -> string list * string
val string_list_of_qualid : string list -> Ptree.qualid -> string list
val qloc : Ptree.qualid -> Loc.position
val ts_tuple : int -> tysymbol
val fs_tuple : int -> lsymbol
val with_tuples :
?reset:bool -> (theory_uc -> 'a -> 'b) -> theory_uc -> 'a -> 'b
val is_projection : theory_uc -> lsymbol -> (tysymbol * lsymbol * int) option
(** [is_projection uc ls] returns
- [Some (ts, lsc, i)] if [ls] is the i-th projection of an
......
......@@ -143,15 +143,15 @@ let add_decl d uc =
{ uc with uc_decls = d :: uc.uc_decls }
let add_impure_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_impure d in
let th = Theory.add_decl_with_tuples uc.uc_impure d in
{ uc with uc_impure = th }
let add_effect_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_effect d in
let th = Theory.add_decl_with_tuples uc.uc_effect d in
{ uc with uc_effect = th }
let add_pure_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_pure d in
let th = Theory.add_decl_with_tuples uc.uc_pure d in
{ uc with uc_pure = th }
(**
......
......@@ -450,9 +450,9 @@ and dexpr_desc ~ghost env loc = function
DEletrec (dl, e1), e1.dexpr_type
| Ptree.Etuple el ->
let n = List.length el in
let s = Typing.fs_tuple n in
let s = fs_tuple n in
let tyl = List.map (fun _ -> create_type_var loc) el in
let ty = tyapp (Typing.ts_tuple n) tyl in
let ty = tyapp (ts_tuple n) tyl in
let create d ty = { dexpr_desc = d; dexpr_type = ty; dexpr_loc = loc } in
let apply e1 e2 ty2 =
let e2 = dexpr ~ghost env e2 in
......
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