Commit a04cd4da authored by Andrei Paskevich's avatar Andrei Paskevich

Core: drop opacity annotations

parent 18bb62bc
......@@ -604,7 +604,6 @@ and tr_global_ts dep env (r : global_reference) =
let j = ith_mutual_inductive i j in
let ts = lookup_table global_ts (IndRef j) in
let tyj = Ty.ty_app ts (List.map Ty.ty_var ts.Ty.ts_args) in
let opaque = Ty.Stv.of_list ts.Ty.ts_args in
let constr = Array.length oib.mind_nf_lc in
let mk_constructor k _tyk = (* k-th constructor *)
let r = ConstructRef (j, k+1) in
......@@ -643,7 +642,7 @@ and tr_global_ts dep env (r : global_reference) =
in
let l = List.map (tr_type dep' tvm env) l in
let id = preid_of_id (Nametab.basename_of_global r) in
let ls = Term.create_fsymbol ~opaque ~constr id l tyj in
let ls = Term.create_fsymbol ~constr id l tyj in
add_table global_ls r (Some ls);
add_poly_arity ls vars;
ls, List.map (fun _ -> None) ls.ls_args
......
......@@ -45,7 +45,6 @@ type lsymbol = {
ls_name : ident;
ls_args : ty list;
ls_value : ty option;
ls_opaque : Stv.t;
ls_constr : int;
}
......@@ -63,29 +62,22 @@ let ls_equal : lsymbol -> lsymbol -> bool = (==)
let ls_hash ls = id_hash ls.ls_name
let ls_compare ls1 ls2 = id_compare ls1.ls_name ls2.ls_name
let check_opaque opaque args value =
if Stv.is_empty opaque then opaque else
let diff s ty = ty_v_fold (fun s tv -> Stv.remove tv s) s ty in
let s = List.fold_left diff (Opt.fold diff opaque value) args in
if Stv.is_empty s then opaque else invalid_arg "Term.create_lsymbol"
let check_constr constr _args value =
if constr = 0 || (constr > 0 && value <> None)
then constr else invalid_arg "Term.create_lsymbol"
let create_lsymbol ?(opaque=Stv.empty) ?(constr=0) name args value = {
let create_lsymbol ?(constr=0) name args value = {
ls_name = id_register name;
ls_args = args;
ls_value = value;
ls_opaque = check_opaque opaque args value;
ls_constr = check_constr constr args value;
}
let create_fsymbol ?opaque ?constr nm al vl =
create_lsymbol ?opaque ?constr nm al (Some vl)
let create_fsymbol ?constr nm al vl =
create_lsymbol ?constr nm al (Some vl)
let create_psymbol ?opaque nm al =
create_lsymbol ?opaque ~constr:0 nm al None
let create_psymbol nm al =
create_lsymbol ~constr:0 nm al None
let ls_ty_freevars ls =
let acc = oty_freevars Stv.empty ls.ls_value in
......@@ -905,11 +897,10 @@ let fs_tuple_ids = Hid.create 17
let fs_tuple = Hint.memo 17 (fun n ->
let ts = ts_tuple n in
let opaque = Stv.of_list ts.ts_args in
let tl = List.map ty_var ts.ts_args in
let ty = ty_app ts tl in
let id = id_fresh ("Tuple" ^ string_of_int n) in
let fs = create_fsymbol ~opaque ~constr:1 id tl ty in
let fs = create_fsymbol ~constr:1 id tl ty in
Hid.add fs_tuple_ids fs.ls_name n;
fs)
......
......@@ -38,7 +38,6 @@ type lsymbol = private {
ls_name : ident;
ls_args : ty list;
ls_value : ty option;
ls_opaque : Stv.t;
ls_constr : int;
}
......@@ -51,14 +50,11 @@ val ls_compare : lsymbol -> lsymbol -> int
val ls_equal : lsymbol -> lsymbol -> bool
val ls_hash : lsymbol -> int
val create_lsymbol :
?opaque:Stv.t -> ?constr:int -> preid -> ty list -> ty option -> lsymbol
val create_lsymbol : ?constr:int -> preid -> ty list -> ty option -> lsymbol
val create_fsymbol :
?opaque:Stv.t -> ?constr:int -> preid -> ty list -> ty -> lsymbol
val create_fsymbol : ?constr:int -> preid -> ty list -> ty -> lsymbol
val create_psymbol :
?opaque:Stv.t -> preid -> ty list -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol
val ls_ty_freevars : lsymbol -> Stv.t
......
......@@ -396,36 +396,6 @@ let add_prop uc (_,pr,_) = add_symbol add_pr pr.pr_name pr uc
let create_decl d = mk_tdecl (Decl d)
let check_subst_opacity ls ls' sbs =
(* the definition of ls contains ls' instantiated with sbs *)
let sbs = Mtv.set_diff sbs ls'.ls_opaque in
let check () tv = if Stv.mem tv ls.ls_opaque then
Loc.errorm "type parameter '%s is not opaque in symbol `%s'"
tv.tv_name.id_string ls.ls_name.id_string in
Mtv.iter (fun _ ty -> ty_v_fold check () ty) sbs
let check_decl_opacity d = match d.d_node with
(* All lsymbols declared in Ddata are safe, nothing to check.
We allow arbitrary ls_opaque in Dparam, but we check that
cloning in theories preserves opacity, see cl_init below. *)
| Dtype _ | Ddata _ | Dparam _ | Dprop _ -> ()
| Dlogic dl ->
let check (ols,ld) =
let check () ls args value =
let sbs = oty_match Mtv.empty ls.ls_value value in
let sbs = List.fold_left2 ty_match sbs ls.ls_args args in
check_subst_opacity ols ls sbs in
if not (Stv.is_empty ols.ls_opaque) then
t_app_fold check () (snd (open_ls_defn ld))
in
List.iter check dl
| Dind (_, dl) ->
(* TODO: are there safe classes of inductive predicates? *)
let check (ls,_) = if not (Stv.is_empty ls.ls_opaque) then
Loc.errorm ?loc:ls.ls_name.id_loc
"inductive predicates cannot have opaque type parameters" in
List.iter check dl
let warn_dubious_axiom uc k p syms =
match k with
| Plemma | Pgoal | Pskip -> ()
......@@ -444,7 +414,6 @@ let warn_dubious_axiom uc k p syms =
with Exit -> ()
let add_decl ?(warn=true) uc d =
check_decl_opacity d; (* we don't care about tasks *)
let uc = add_tdecl uc (create_decl d) in
match d.d_node with
| Dtype ts -> add_symbol add_ts ts.ts_name ts uc
......@@ -539,15 +508,11 @@ let cl_find_ls cl ls =
if not (Sid.mem ls.ls_name cl.cl_local) then ls
else try Mls.find ls cl.ls_table
with Not_found ->
let opaque = ls.ls_opaque in
let constr = ls.ls_constr in
let id = id_clone ls.ls_name in
let ta' = List.map (cl_trans_ty cl) ls.ls_args in
let vt' = Opt.map (cl_trans_ty cl) ls.ls_value in
let stv = Opt.fold ty_freevars Stv.empty vt' in
let stv = List.fold_left ty_freevars stv ta' in
let opaque = Stv.inter opaque stv in
let ls' = create_lsymbol ~opaque ~constr id ta' vt' in
let ls' = create_lsymbol ~constr id ta' vt' in
cl.ls_table <- Mls.add ls ls' cl.ls_table;
ls'
......@@ -585,10 +550,8 @@ let cl_init_ls cl ls ls' =
| None, None -> Mtv.empty
| _ -> raise (BadInstance (id, ls'.ls_name))
in
let sb = try List.fold_left2 mtch sb ls.ls_args ls'.ls_args
with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name))
in
check_subst_opacity ls ls' sb;
ignore (try List.fold_left2 mtch sb ls.ls_args ls'.ls_args
with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name)));
cl.ls_table <- Mls.add ls ls' cl.ls_table
let cl_init_pr cl pr =
......
......@@ -510,7 +510,6 @@ module Checksum = struct
ident b ls.ls_name;
list ty b ls.ls_args;
option ty b ls.ls_value;
list tvsymbol b (Ty.Stv.elements ls.ls_opaque);
int b ls.ls_constr
(* start: T D R L I P (C 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