diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec index 6478ebfd68..be69fa347d 100644 --- a/examples/ChaChaPoly/chacha_poly.ec +++ b/examples/ChaChaPoly/chacha_poly.ec @@ -80,14 +80,17 @@ theory C. axiom gt0_max_counter : 0 < max_counter. + type counter. + clone include Subtype with - type T <- int, - op P <- fun (i:int) => 0 <= i < max_counter + 1 - rename (* [type] "sT" as "counter" *) (* Gives error. *) - [op] "insubd" as "ofint" - proof *. - realize inhabited. exists 0. smt(gt0_max_counter). qed. - type counter = sT. + type sT <- counter, + type T <- int, + op P <- fun (i:int) => 0 <= i < max_counter + 1 + rename [op] "insubd" as "ofint" + proof *. + + realize inhabited. + proof. by exists 0; smt(gt0_max_counter). qed. clone FinType with type t = counter, @@ -116,16 +119,20 @@ abstract theory GenBlock. op block_size : int. axiom ge0_block_size : 0 <= block_size. + type block. + clone include Subtype with - type T <- bytes, - op P <- fun (l:bytes) => size l = block_size + type sT <- block, + type T <- bytes, + op P <- fun (l:bytes) => size l = block_size rename [op] "val" as "bytes_of_block" proof *. + realize inhabited. + proof. exists (nseq block_size witness). smt(size_nseq ge0_block_size). qed. - type block = sT. op dblock = dmap (dlist dbyte block_size) insubd. diff --git a/examples/MEE-CBC/FunctionalSpec.ec b/examples/MEE-CBC/FunctionalSpec.ec index 29acabb5d9..5e05aa9f81 100644 --- a/examples/MEE-CBC/FunctionalSpec.ec +++ b/examples/MEE-CBC/FunctionalSpec.ec @@ -492,7 +492,6 @@ proof. (size (pad _p (hmac_sha256 _mk _p))) (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) (size (pad _p (hmac_sha256 _mk _p)))). - smt(). split=> //=. split; 1:by rewrite /mee_enc /= size_cbc_enc addzC. by rewrite take_size. diff --git a/examples/ehoare/adversary.ec b/examples/ehoare/adversary.ec index 1f22debbc2..6117ad1639 100644 --- a/examples/ehoare/adversary.ec +++ b/examples/ehoare/adversary.ec @@ -74,7 +74,7 @@ proof. rewrite (eq_Ep _ _ ((fun r => (inv p)%xr * (! test r)%xr) + (fun r => (1 + size log)%xr))). + move => x xx /=. rewrite of_realM; 1,2:smt(of_realM invr_ge0 ge0_mu). smt(). - rewrite EpD EpC EpZ /=; 1: smt(invr_gt0 dr_mu_test of_realK). + rewrite EpD EpC EpZ /=; 1: smt(invr_gt0 dr_mu_test of_realdK). rewrite Ep_mu mu_not dr_ll /= -/p. rewrite !to_pos_pos; 1,2,3,4:smt(mu_bounded dr_mu_test size_ge0). by auto. diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 8114cbac50..1f86a41b4a 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -411,6 +411,13 @@ let rec process_type (scope : EcScope.scope) (tyd : ptydecl located) = and process_types (scope : EcScope.scope) tyds = List.fold_left process_type scope tyds +(* -------------------------------------------------------------------- *) +and process_subtype (scope : EcScope.scope) (subtype : psubtype located) = + EcScope.check_state `InTop "subtype" scope; + let scope = EcScope.Ty.add_subtype scope subtype in + EcScope.notify scope `Info "added subtype: `%s'" (unloc subtype.pl_desc.pst_name); + scope + (* -------------------------------------------------------------------- *) and process_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) = EcScope.check_state `InTop "type class" scope; @@ -743,6 +750,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g = match match g.pl_desc with | Gtype t -> `Fct (fun scope -> process_types scope (List.map (mk_loc loc) t)) + | Gsubtype t -> `Fct (fun scope -> process_subtype scope (mk_loc loc t)) | Gtypeclass t -> `Fct (fun scope -> process_typeclass scope (mk_loc loc t)) | Gtycinstance t -> `Fct (fun scope -> process_tycinst scope (mk_loc loc t)) | Gmodule m -> `Fct (fun scope -> process_module scope m) diff --git a/src/ecCoreLib.ml b/src/ecCoreLib.ml index 365213fe54..6e884a4e8c 100644 --- a/src/ecCoreLib.ml +++ b/src/ecCoreLib.ml @@ -116,7 +116,7 @@ module CI_Xreal = struct let mk_Rpbar = fun x -> EcPath.pqname p_Rpbar x let p_realp = mk_Rp "realp" - let p_of_real = mk_Rp "of_real" + let p_of_real = mk_Rp "of_reald" let p_xreal = mk_Rpbar "xreal" let p_rp = mk_Rpbar "rp" diff --git a/src/ecLexer.mll b/src/ecLexer.mll index c1225b0720..f3552cb5ca 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -195,6 +195,7 @@ "theory" , THEORY ; (* KW: global *) "abstract" , ABSTRACT ; (* KW: global *) "section" , SECTION ; (* KW: global *) + "subtype" , SUBTYPE ; (* KW: global *) "type" , TYPE ; (* KW: global *) "class" , CLASS ; (* KW: global *) "instance" , INSTANCE ; (* KW: global *) diff --git a/src/ecParser.mly b/src/ecParser.mly index b612e28d57..5d9c453d36 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -558,6 +558,7 @@ %token SPLITWHILE %token STAR %token SUBST +%token SUBTYPE %token SUFF %token SWAP %token SYMMETRY @@ -1644,6 +1645,21 @@ typedecl: | locality=locality TYPE td=tyd_name EQ te=datatype_def { [mk_tydecl ~locality td (PTYD_Datatype te)] } +(* -------------------------------------------------------------------- *) +(* Subtypes *) +subtype: +| SUBTYPE name=lident cname=prefix(AS, uident)? EQ LBRACE + x=lident COLON carrier=loc(type_exp) PIPE pred=form + RBRACE rename=subtype_rename? + { { pst_name = name; + pst_cname = cname; + pst_carrier = carrier; + pst_pred = (x, pred); + pst_rename = rename; } } + +subtype_rename: +| RENAME x=STRING COMMA y=STRING { (x, y) } + (* -------------------------------------------------------------------- *) (* Type classes *) typeclass: @@ -3763,6 +3779,7 @@ global_action: | mod_def_or_decl { Gmodule $1 } | sig_def { Ginterface $1 } | typedecl { Gtype $1 } +| subtype { Gsubtype $1 } | typeclass { Gtypeclass $1 } | tycinstance { Gtycinstance $1 } | operator { Goperator $1 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index a93ada6c8f..dad99459d8 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -384,6 +384,15 @@ let rec pf_ident ?(raw = false) f = | PFtuple [f] when not raw -> pf_ident ~raw f | _ -> None +(* -------------------------------------------------------------------- *) +type psubtype = { + pst_name : psymbol; + pst_cname : psymbol option; + pst_carrier : pty; + pst_pred : (psymbol * pformula); + pst_rename : (string * string) option; +} + (* -------------------------------------------------------------------- *) type ptyvardecls = (psymbol * pqsymbol list) list @@ -1261,6 +1270,7 @@ type global_action = | Gabbrev of pabbrev | Gaxiom of paxiom | Gtype of ptydecl list + | Gsubtype of psubtype | Gtypeclass of ptypeclass | Gtycinstance of ptycinstance | Gaddrw of (is_local * pqsymbol * pqsymbol list) diff --git a/src/ecScope.ml b/src/ecScope.ml index ac291529da..17e1b1a4a4 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1548,760 +1548,838 @@ module ModType = struct end (* -------------------------------------------------------------------- *) -module Ty = struct - open EcDecl - open EcTyping +module Theory = struct + open EcTheory - module TT = EcTyping - module ELI = EcInductive - module EHI = EcHiInductive + exception TopScope (* ------------------------------------------------------------------ *) - let check_name_available scope x = - let pname = EcPath.pqname (EcEnv.root (env scope)) x.pl_desc in - - if EcEnv.Ty .by_path_opt pname (env scope) <> None - || EcEnv.TypeClass.by_path_opt pname (env scope) <> None then - hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc + let bind (scope : scope) (cth : thloaded) = + assert (scope.sc_pr_uc = None); + { scope with + sc_env = EcSection.add_th ~import:EcTheory.import0 cth scope.sc_env } (* ------------------------------------------------------------------ *) - let bind ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) = + let required (scope : scope) (name : required_info) = assert (scope.sc_pr_uc = None); - let item = EcTheory.mkitem import (EcTheory.Th_type (x, tydecl)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } + List.exists (fun x -> + if x.rqd_name = name.rqd_name then ( + (* FIXME: raise an error message *) + assert (x.rqd_digest = name.rqd_digest); + true) + else false) + scope.sc_required (* ------------------------------------------------------------------ *) - let add scope (tyd : ptydecl located) = - let loc = loc tyd in + let mark_as_direct (scope : scope) (name : symbol) = + let for1 rq = + if rq.rqd_name = name + then { rq with rqd_direct = true } + else rq + in { scope with sc_required = List.map for1 scope.sc_required } - let { pty_name = name; pty_tyvars = args; - pty_body = body; pty_locality = tyd_loca } = unloc tyd in + (* ------------------------------------------------------------------ *) + let enter (scope : scope) (mode : thmode) (name : symbol) = + assert (scope.sc_pr_uc = None); + subscope scope mode name - check_name_available scope name; - let env = env scope in - let tyd_params, tyd_type = - match body with - | PTYD_Abstract tcs -> - let tcs = - List.map - (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env)) - tcs in - let ue = TT.transtyvars env (loc, Some args) in - EcUnify.UniEnv.tparams ue, `Abstract (Sp.of_list tcs) + (* ------------------------------------------------------------------ *) + let rec require_loaded (id : required_info) scope = + if required scope id then + scope + else + match Msym.find_opt id.rqd_name scope.sc_loaded with + | Some (rth, ids) -> + let scope = List.fold_right require_loaded ids scope in + let env = EcSection.require rth scope.sc_env in + { scope with + sc_env = env; + sc_required = id :: scope.sc_required; } - | PTYD_Alias bd -> - let ue = TT.transtyvars env (loc, Some args) in - let body = transty tp_tydecl env ue bd in - EcUnify.UniEnv.tparams ue, `Concrete body + | None -> assert false - | PTYD_Datatype dt -> - let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in - let tparams, tydt = - try ELI.datatype_as_ty_dtype datatype - with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive - in - tparams, `Datatype tydt + (* ------------------------------------------------------------------ *) + let update_with_required ~(dst : scope) ~(src : scope) = + let dst = + let sc_loaded = + Msym.union + (fun _ x y -> assert (x ==(*phy*) y); Some x) + dst.sc_loaded src.sc_loaded + in { dst with sc_loaded } + in List.fold_right require_loaded src.sc_required dst - | PTYD_Record rt -> - let record = EHI.trans_record env (mk_loc loc (args,name)) rt in - let scheme = ELI.indsc_of_record record in - record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields) - in + (* ------------------------------------------------------------------ *) + let add_clears clears scope = + let clears = + let for1 = function + | None -> EcEnv.root (env scope) + | Some { pl_loc = loc; pl_desc = (xs, x) as q } -> + let xp = EcEnv.root (env scope) in + let xp = EcPath.pqname (EcPath.extend xp xs) x in + if is_none (EcEnv.Theory.by_path_opt xp (env scope)) then + hierror ~loc "unknown theory: `%s`" (string_of_qsymbol q); + xp + in List.map for1 clears + in { scope with sc_clears = scope.sc_clears @ clears } - bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; }) + (* -------------------------------------------------------------------- *) + let exit_r ?pempty (scope : scope) = + match scope.sc_top with + | None -> raise TopScope + | Some sup -> + let clears = scope.sc_clears in + let _, cth, _ = EcSection.exit_theory ?pempty ~clears scope.sc_env in + let loaded = scope.sc_loaded in + let required = scope.sc_required in + let sup = { sup with sc_loaded = loaded; } in + ((cth, required), scope.sc_name, sup) (* ------------------------------------------------------------------ *) - let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) = + let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) = assert (scope.sc_pr_uc = None); - let item = EcTheory.mkitem import (EcTheory.Th_typeclass(x, tc)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } + + let cth = exit_r ~pempty (add_clears clears scope) in + let ((cth, required), (name, _), scope) = cth in + let scope = List.fold_right require_loaded required scope in + let scope = ofold (fun cth scope -> bind scope cth) scope cth in + (name, scope) (* ------------------------------------------------------------------ *) - let add_class (scope : scope) { pl_desc = tcd } = - assert (scope.sc_pr_uc = None); - let lc = tcd.ptc_loca in - let name = unloc tcd.ptc_name in - let scenv = (env scope) in + let bump_prelude (scope : scope) = + match scope.sc_prelude with + | `InPrelude, _ -> + { scope with sc_prelude = (`InPrelude, + { pr_env = env scope; + pr_required = scope.sc_required; }) } + | _ -> scope - check_name_available scope tcd.ptc_name; + (* ------------------------------------------------------------------ *) + let import (scope : scope) (name : qsymbol) = + assert (scope.sc_pr_uc = None); - let tclass = - let uptc = - tcd.ptc_inth |> omap - (fun { pl_loc = uploc; pl_desc = uptc } -> - match EcEnv.TypeClass.lookup_opt uptc scenv with - | None -> hierror ~loc:uploc "unknown type-class: `%s'" - (string_of_qsymbol uptc) - | Some (tcp, _) -> tcp) - in + match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with + | None -> + hierror + "cannot import the non-existent theory `%s'" + (string_of_qsymbol name) - let asty = - let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in - { tyd_params = []; - tyd_type = `Abstract body; - tyd_loca = (lc :> locality); - tyd_resolve = true; } in - let scenv = EcEnv.Ty.bind name asty scenv in + | Some (path, cth) -> + if cth.cth_mode = `Abstract then + hierror "cannot import an abstract theory"; + bump_prelude + { scope with + sc_env = EcSection.import path scope.sc_env } - (* Check for duplicated field names *) - Msym.odup unloc (List.map fst tcd.ptc_ops) - |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc - "duplicated operator name: `%s'" x.pl_desc); - Msym.odup unloc (List.map fst tcd.ptc_axs) - |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc - "duplicated axiom name: `%s'" x.pl_desc); + (* ------------------------------------------------------------------ *) + let export_p scope (p, lc) = + let item = mkitem EcTheory.import0 (EcTheory.Th_export (p, lc)) in + { scope with sc_env = EcSection.add_item item scope.sc_env } - (* Check operators types *) - let operators = - let check1 (x, ty) = - let ue = EcUnify.UniEnv.create (Some []) in - let ty = transty tp_tydecl scenv ue ty in - let uidmap = EcUnify.UniEnv.close ue in - let ty = ty_subst (Tuni.subst uidmap) ty in - (EcIdent.create (unloc x), ty) - in - tcd.ptc_ops |> List.map check1 in + let export (scope : scope) (name : qsymbol) = + assert (scope.sc_pr_uc = None); - (* Check axioms *) - let axioms = - let scenv = EcEnv.Var.bind_locals operators scenv in - let check1 (x, ax) = - let ue = EcUnify.UniEnv.create (Some []) in - let ax = trans_prop scenv ue ax in - let uidmap = EcUnify.UniEnv.close ue in - let fs = Tuni.subst uidmap in - let ax = Fsubst.f_subst fs ax in - (unloc x, ax) - in - tcd.ptc_axs |> List.map check1 in + match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with + | None -> + hierror + "cannot export the non-existent theory `%s'" + (string_of_qsymbol name) - (* Construct actual type-class *) - { tc_prt = uptc; tc_ops = operators; tc_axs = axioms; tc_loca = lc} - in - bindclass scope (name, tclass) + | Some (path, cth) -> + if cth.cth_mode = `Abstract then + hierror "cannot export an abstract theory"; + (* The section will fix the locality *) + bump_prelude (export_p scope (path, `Global)) (* ------------------------------------------------------------------ *) - let check_tci_operators env tcty ops reqs = - let ue = EcUnify.UniEnv.create (Some (fst tcty)) in - let rmap = Mstr.of_list reqs in + let check_end_required scope thname = + if fst scope.sc_name <> thname then + hierror "end-of-file while processing external theory %s %s" + (fst scope.sc_name) thname; + if scope.sc_pr_uc <> None then + hierror + "end-of-file while processing proof %s" (fst scope.sc_name) - let ops = - let tt1 m (x, (tvi, op)) = - if not (Mstr.mem (unloc x) rmap) then - hierror ~loc:x.pl_loc "invalid operator name: `%s'" (unloc x); + (* -------------------------------------------------------------------- *) + let require (scope : scope) ((name, mode) : required_info * thmode) loader = + assert (scope.sc_pr_uc = None); - let tvi = List.map (TT.transty tp_tydecl env ue) tvi in - let selected = - EcUnify.select_op ~filter:(fun _ -> EcDecl.is_oper) - (Some (EcUnify.TVIunamed tvi)) env (unloc op) ue ([], None) - in - let op = - match selected with - | [] -> hierror ~loc:op.pl_loc "unknown operator" - | op1::op2::_ -> - hierror ~loc:op.pl_loc - "ambiguous operator (%s / %s)" - (EcPath.tostring (fst (proj4_1 op1))) - (EcPath.tostring (fst (proj4_1 op2))) - | [((p, _), _, _, _)] -> - let op = EcEnv.Op.by_path p env in - let opty = - Tvar.subst - (Tvar.init (List.map fst op.op_tparams) tvi) - op.op_ty - in - (p, opty) - - in - Mstr.change - (function - | None -> Some (x.pl_loc, op) - | Some _ -> hierror ~loc:(x.pl_loc) - "duplicated operator name: `%s'" (unloc x)) - (unloc x) m - in - List.fold_left tt1 Mstr.empty ops - in - List.iter - (fun (x, (req, _)) -> - if req && not (Mstr.mem x ops) then - hierror "no definition for operator `%s'" x) - reqs; - List.fold_left - (fun m (x, (_, ty)) -> - match Mstr.find_opt x ops with - | None -> m - | Some (loc, (p, opty)) -> - if not (EcReduction.EqTest.for_type env ty opty) then - hierror ~loc "invalid type for operator `%s'" x; - Mstr.add x p m) - Mstr.empty reqs + if required scope name then begin + if name.rqd_direct + then mark_as_direct scope name.rqd_name + else scope + end else + match Msym.find_opt name.rqd_name scope.sc_loaded with + | Some _ -> require_loaded name scope - (* ------------------------------------------------------------------ *) - let check_tci_axioms scope mode axs reqs lc = - let rmap = Mstr.of_list reqs in - let symbs, axs = - List.map_fold - (fun m (x, t) -> - if not (Mstr.mem (unloc x) rmap) then - hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x); - if Sstr.mem (unloc x) m then - hierror ~loc:(x.pl_loc) "duplicated axiom name: `%s'" (unloc x); - (Sstr.add (unloc x) m, (unloc x, t, Mstr.find (unloc x) rmap))) - Sstr.empty axs in + | None -> + try + let imported = enter (for_loading scope) mode name.rqd_name `Global in + let imported = { imported with sc_env = EcSection.astop imported.sc_env } in + let thname = fst imported.sc_name in + let imported = loader imported in - let interactive = - List.pmap - (fun (x, req) -> - if not (Mstr.mem x symbs) then - let ax = { - ax_tparams = []; - ax_spec = req; - ax_kind = `Lemma; - ax_loca = lc; - ax_visibility = `NoSmt; - } in Some ((None, ax), EcPath.psymbol x, scope.sc_env) - else None) - reqs in - List.iter - (fun (x, pt, f) -> - let x = "$" ^ x in - let t = { pt_core = pt; pt_intros = []; } in - let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in - let t = { pt_core = t; pt_intros = []; } in - let ax = { - ax_tparams = []; - ax_spec = f; - ax_kind = `Lemma; - ax_visibility = `NoSmt; - ax_loca = lc; - } in + check_end_required imported thname; - let pucflags = { puc_visibility = `Visible; puc_local = false; } in - let pucflags = (([], None), pucflags) in - let check = Check_mode.check scope.sc_options in + let cth = exit_r ~pempty:`No imported in + let (cth, rqs), (name1, _), imported = cth in + assert (name.rqd_name = name1); + let scope = { scope with sc_loaded = + Msym.add name.rqd_name (oget cth, rqs) imported.sc_loaded; } in - let escope = scope in - let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in - let escope = Tactics.proof escope in - let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in - ignore (Ax.save_r escope)) - axs; - interactive + bump_prelude (require_loaded name scope) - (* ------------------------------------------------------------------ *) - (* FIXME section: those path does not exists ... - futhermode Ring.ZModule is an abstract theory *) - let p_zmod = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ZModule"], "zmodule") - let p_ring = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ComRing"], "ring" ) - let p_idomain = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "IDomain"], "idomain") - let p_field = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field" ], "field" ) + with e -> begin + match toperror_of_exn_r e with + | Some (l, e) when not (EcLocation.isdummy l) -> + raise (ImportError (Some l, name.rqd_name, e)) + | _ -> + raise (ImportError (None, name.rqd_name, e)) + end - (* ------------------------------------------------------------------ *) - let ring_of_symmap env ty kind symbols = - { r_type = ty; - r_zero = oget (Mstr.find_opt "rzero" symbols); - r_one = oget (Mstr.find_opt "rone" symbols); - r_add = oget (Mstr.find_opt "add" symbols); - r_opp = (Mstr.find_opt "opp" symbols); - r_mul = oget (Mstr.find_opt "mul" symbols); - r_exp = (Mstr.find_opt "expr" symbols); - r_sub = (Mstr.find_opt "sub" symbols); - r_kind = kind; - r_embed = - (match Mstr.find_opt "ofint" symbols with - | None when EcReduction.EqTest.for_type env ty tint -> `Direct - | None -> `Default | Some p -> `Embed p); } + let required scope = scope.sc_required +end - let addring ~import (scope : scope) mode (kind, { pl_desc = tci; pl_loc = loc }) = - let env = env scope in - if not (EcAlgTactic.is_module_loaded env) then - hierror "load AlgTactic/Ring first"; +(* -------------------------------------------------------------------- *) +module Section = struct + module T = EcTheory - let ty = - let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in - let ty = transty tp_tydecl env ue (snd tci.pti_type) in - assert (EcUnify.UniEnv.closed ue); - let uidmap = EcUnify.UniEnv.close ue in - (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty) - in - if not (List.is_empty (fst ty)) then - hierror "ring instances cannot be polymorphic"; + let enter (scope : scope) (name : psymbol option) = + assert (scope.sc_pr_uc = None); + { scope with + sc_env = EcSection.enter_section (omap unloc name) scope.sc_env } - let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in - let symbols = check_tci_operators env ty tci.pti_ops symbols in - let cr = ring_of_symmap env (snd ty) kind symbols in - let axioms = EcAlgTactic.ring_axioms env cr in - let lc = (tci.pti_loca :> locality) in - let inter = check_tci_axioms scope mode tci.pti_axs axioms lc in - let add env p = - let item = EcTheory.Th_instance (ty,`General p, tci.pti_loca) in - let item = EcTheory.mkitem import item in - EcSection.add_item item env in + let exit (scope : scope) (name : psymbol option) = + let sc_env = EcSection.exit_section (omap unloc name) scope.sc_env in + { scope with sc_env } +end - let scope = - { scope with sc_env = - List.fold_left add - (let item = - EcTheory.Th_instance (([], snd ty), `Ring cr, tci.pti_loca) in - let item = EcTheory.mkitem import item in - EcSection.add_item item scope.sc_env) - [p_zmod; p_ring; p_idomain] } +(* -------------------------------------------------------------------- *) +module Reduction = struct + (* FIXME: section -> allow "local" flag *) + let add_reduction scope (opts, reds) = + check_state `InTop "hint simplify" scope; - in Ax.add_defer scope inter + let rules = + let for1 idx name = + let idx = odfl 0 idx in + let ax_p = EcEnv.Ax.lookup_path (unloc name) (env scope) in + let opts = EcTheory.{ + ur_delta = List.mem `Delta opts; + ur_eqtrue = List.mem `EqTrue opts; + } in - (* ------------------------------------------------------------------ *) - let field_of_symmap env ty symbols = - { f_ring = ring_of_symmap env ty `Integer symbols; - f_inv = oget (Mstr.find_opt "inv" symbols); - f_div = Mstr.find_opt "div" symbols; } + let red_info = + EcReduction.User.compile ~opts ~prio:idx (env scope) ax_p in + (ax_p, opts, Some red_info) in - let addfield ~import (scope : scope) mode { pl_desc = tci; pl_loc = loc; } = - let env = env scope in - if not (EcAlgTactic.is_module_loaded env) then - hierror "load AlgTactic/Ring first"; + let rules = List.map (fun (xs, idx) -> List.map (for1 idx) xs) reds in + List.flatten rules - let ty = - let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in - let ty = transty tp_tydecl env ue (snd tci.pti_type) in - assert (EcUnify.UniEnv.closed ue); - let uidmap = EcUnify.UniEnv.close ue in - (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty) in - if not (List.is_empty (fst ty)) then - hierror "field instances cannot be polymorphic"; - let symbols = EcAlgTactic.field_symbols env (snd ty) in - let symbols = check_tci_operators env ty tci.pti_ops symbols in - let cr = field_of_symmap env (snd ty) symbols in - let axioms = EcAlgTactic.field_axioms env cr in - let lc = (tci.pti_loca :> locality) in - let inter = check_tci_axioms scope mode tci.pti_axs axioms lc; in - let add env p = - let item = EcTheory.Th_instance(ty,`General p, tci.pti_loca) in - let item = EcTheory.mkitem import item in - EcSection.add_item item env in - let scope = - { scope with - sc_env = - List.fold_left add - (let item = - EcTheory.Th_instance (([], snd ty), `Field cr, tci.pti_loca) in - let item = EcTheory.mkitem import item in - EcSection.add_item item scope.sc_env) - [p_zmod; p_ring; p_idomain; p_field] } - in Ax.add_defer scope inter + let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_reduction rules) in + { scope with sc_env = EcSection.add_item item scope.sc_env } +end +(* -------------------------------------------------------------------- *) +module Cloning = struct (* ------------------------------------------------------------------ *) - let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) = - let subst = EcSubst.add_tydef EcSubst.empty tcp ([], ty) in - List.map (fun (x, opty) -> - (EcIdent.name x, (true, EcSubst.subst_ty subst opty))) - tc.tc_ops + open EcTheory + open EcThCloning + + module C = EcThCloning + module R = EcTheoryReplay -(* (* ------------------------------------------------------------------ *) - let add_generic_tc (scope : scope) _mode { pl_desc = tci; pl_loc = loc; } = - let ty = - let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in - let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in - assert (EcUnify.UniEnv.closed ue); - (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty) - in + let hooks : scope R.ovrhooks = + let thexit sc pempty = snd (Theory.exit ?clears:None ~pempty sc) in + let add_item scope import item = + let item = EcTheory.mkitem import item in + { scope with sc_env = EcSection.add_item item scope.sc_env } in + { R.henv = (fun scope -> scope.sc_env); + R.hadd_item = add_item; + R.hthenter = Theory.enter; + R.hthexit = thexit; + R.herr = (fun ?loc -> hierror ?loc "%s"); } - let (tcp, tc) = - match EcEnv.TypeClass.lookup_opt (unloc tci.pti_name) (env scope) with + (* ------------------------------------------------------------------ *) + module Options = struct + open EcTheoryReplay + + let default = { clo_abstract = false; } + + let merge1 opts (b, (x : theory_cloning_option)) = + match x with + | `Abstract -> { opts with clo_abstract = b; } + + let merge opts (specs : theory_cloning_options) = + List.fold_left merge1 opts specs + end + + + (* ------------------------------------------------------------------ *) + let replay_proofs (scope : scope) (mode : Tactics.proofmode) (proofs : _) = + proofs |> List.pmap (fun axc -> + match axc.C.axc_tac with | None -> - hierror ~loc:tci.pti_name.pl_loc - "unknown type-class: %s" (string_of_qsymbol (unloc tci.pti_name)) - | Some tc -> tc - in + Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env) - let symbols = symbols_of_tc scope.sc_env (snd ty) (tcp, tc) in - let _symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in + | Some pt -> + let t = { pt_core = pt; pt_intros = []; } in + let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in + let t = { pt_core = t; pt_intros = []; } in + let (x, ax) = axc.C.axc_axiom in - { scope with - sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env } + let pucflags = { puc_visibility = `Visible; puc_local = false; } in + let pucflags = (([], None), pucflags) in + let check = Check_mode.check scope.sc_options in -(* - let ue = EcUnify.UniEnv.create (Some []) in - let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in - try EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc - with EcUnify.UnificationFailure _ -> - hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc)) -*) -*) + let escope = { scope with sc_env = axc.C.axc_env; } in + let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in + let escope = Tactics.proof escope in + let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in + ignore (Ax.save_r escope); None + ) (* ------------------------------------------------------------------ *) - let add_instance - ?(import = EcTheory.import0) (scope : scope) mode ({ pl_desc = tci } as toptci) - = - match unloc tci.pti_name with - | ([], "bring") -> begin - if EcUtils.is_some tci.pti_args then - hierror "unsupported-option"; - addring ~import scope mode (`Boolean, toptci) - end + let clone (scope : scope) mode (thcl : theory_cloning) = + assert (scope.sc_pr_uc = None); - | ([], "ring") -> begin - let kind = - match tci.pti_args with - | None -> `Integer - | Some (`Ring (c, p)) -> - if odfl false (c |> omap (fun c -> c <^ BI.of_int 2)) then - hierror "invalid coefficient modulus"; - if odfl false (p |> omap (fun p -> p <^ BI.of_int 2)) then - hierror "invalid power modulus"; - if opt_equal BI.equal c (Some (BI.of_int 2)) - && opt_equal BI.equal p (Some (BI.of_int 2)) - then `Boolean - else `Modulus (c, p) - in addring ~import scope mode (kind, toptci) - end + let { cl_name = name; + cl_theory = (opath, oth); + cl_clone = ovrds; + cl_rename = rnms; + cl_ntclr = ntclr; } - | ([], "field") -> addfield ~import scope mode toptci + = C.clone scope.sc_env thcl in + + let incl = thcl.pthc_import = Some `Include in + let opts = Options.merge Options.default thcl.pthc_opts in + + if thcl.pthc_import = Some `Include && opts.R.clo_abstract then + hierror "cannot include an abstract theory"; + if thcl.pthc_import = Some `Include && EcUtils.is_some thcl.pthc_name then + hierror "cannot give an alias to an included clone"; + + let cpath = EcEnv.root (env scope) in + let npath = if incl then cpath else EcPath.pqname cpath name in + + let (proofs, scope) = + EcTheoryReplay.replay hooks + ~abstract:opts.R.clo_abstract ~local:thcl.pthc_local ~incl + ~clears:ntclr ~renames:rnms ~opath ~npath ovrds + scope (name, oth.cth_items) + in + + let proofs = replay_proofs scope mode proofs in + + let scope = + thcl.pthc_import |> ofold (fun flag scope -> + match flag with + | `Import -> + { scope with sc_env = EcSection.import npath scope.sc_env; } + | `Export -> + let item = EcTheory.mkitem EcTheory.import0 (Th_export (npath, `Global)) in + { scope with sc_env = EcSection.add_item item scope.sc_env; } + | `Include -> scope) + scope + + in Ax.add_defer scope proofs - | _ -> - if EcUtils.is_some tci.pti_args then - hierror "unsupported-option"; - failwith "unsupported" (* FIXME *) end (* -------------------------------------------------------------------- *) -module Theory = struct - open EcTheory - - exception TopScope +module Ty = struct + open EcDecl + open EcTyping - (* ------------------------------------------------------------------ *) - let bind (scope : scope) (cth : thloaded) = - assert (scope.sc_pr_uc = None); - { scope with - sc_env = EcSection.add_th ~import:EcTheory.import0 cth scope.sc_env } + module TT = EcTyping + module ELI = EcInductive + module EHI = EcHiInductive (* ------------------------------------------------------------------ *) - let required (scope : scope) (name : required_info) = - assert (scope.sc_pr_uc = None); - List.exists (fun x -> - if x.rqd_name = name.rqd_name then ( - (* FIXME: raise an error message *) - assert (x.rqd_digest = name.rqd_digest); - true) - else false) - scope.sc_required + let check_name_available scope x = + let pname = EcPath.pqname (EcEnv.root (env scope)) x.pl_desc in - (* ------------------------------------------------------------------ *) - let mark_as_direct (scope : scope) (name : symbol) = - let for1 rq = - if rq.rqd_name = name - then { rq with rqd_direct = true } - else rq - in { scope with sc_required = List.map for1 scope.sc_required } + if EcEnv.Ty .by_path_opt pname (env scope) <> None + || EcEnv.TypeClass.by_path_opt pname (env scope) <> None then + hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc (* ------------------------------------------------------------------ *) - let enter (scope : scope) (mode : thmode) (name : symbol) = + let bind ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) = assert (scope.sc_pr_uc = None); - subscope scope mode name + let item = EcTheory.mkitem import (EcTheory.Th_type (x, tydecl)) in + { scope with sc_env = EcSection.add_item item scope.sc_env } (* ------------------------------------------------------------------ *) - let rec require_loaded (id : required_info) scope = - if required scope id then - scope - else - match Msym.find_opt id.rqd_name scope.sc_loaded with - | Some (rth, ids) -> - let scope = List.fold_right require_loaded ids scope in - let env = EcSection.require rth scope.sc_env in - { scope with - sc_env = env; - sc_required = id :: scope.sc_required; } - - | None -> assert false + let add scope (tyd : ptydecl located) = + let loc = loc tyd in - (* ------------------------------------------------------------------ *) - let update_with_required ~(dst : scope) ~(src : scope) = - let dst = - let sc_loaded = - Msym.union - (fun _ x y -> assert (x ==(*phy*) y); Some x) - dst.sc_loaded src.sc_loaded - in { dst with sc_loaded } - in List.fold_right require_loaded src.sc_required dst + let { pty_name = name; pty_tyvars = args; + pty_body = body; pty_locality = tyd_loca } = unloc tyd in - (* ------------------------------------------------------------------ *) - let add_clears clears scope = - let clears = - let for1 = function - | None -> EcEnv.root (env scope) - | Some { pl_loc = loc; pl_desc = (xs, x) as q } -> - let xp = EcEnv.root (env scope) in - let xp = EcPath.pqname (EcPath.extend xp xs) x in - if is_none (EcEnv.Theory.by_path_opt xp (env scope)) then - hierror ~loc "unknown theory: `%s`" (string_of_qsymbol q); - xp - in List.map for1 clears - in { scope with sc_clears = scope.sc_clears @ clears } + check_name_available scope name; + let env = env scope in + let tyd_params, tyd_type = + match body with + | PTYD_Abstract tcs -> + let tcs = + List.map + (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env)) + tcs in + let ue = TT.transtyvars env (loc, Some args) in + EcUnify.UniEnv.tparams ue, `Abstract (Sp.of_list tcs) - (* -------------------------------------------------------------------- *) - let exit_r ?pempty (scope : scope) = - match scope.sc_top with - | None -> raise TopScope - | Some sup -> - let clears = scope.sc_clears in - let _, cth, _ = EcSection.exit_theory ?pempty ~clears scope.sc_env in - let loaded = scope.sc_loaded in - let required = scope.sc_required in - let sup = { sup with sc_loaded = loaded; } in - ((cth, required), scope.sc_name, sup) + | PTYD_Alias bd -> + let ue = TT.transtyvars env (loc, Some args) in + let body = transty tp_tydecl env ue bd in + EcUnify.UniEnv.tparams ue, `Concrete body - (* ------------------------------------------------------------------ *) - let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) = - assert (scope.sc_pr_uc = None); + | PTYD_Datatype dt -> + let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in + let tparams, tydt = + try ELI.datatype_as_ty_dtype datatype + with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive + in + tparams, `Datatype tydt - let cth = exit_r ~pempty (add_clears clears scope) in - let ((cth, required), (name, _), scope) = cth in - let scope = List.fold_right require_loaded required scope in - let scope = ofold (fun cth scope -> bind scope cth) scope cth in - (name, scope) + | PTYD_Record rt -> + let record = EHI.trans_record env (mk_loc loc (args,name)) rt in + let scheme = ELI.indsc_of_record record in + record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields) + in - (* ------------------------------------------------------------------ *) - let bump_prelude (scope : scope) = - match scope.sc_prelude with - | `InPrelude, _ -> - { scope with sc_prelude = (`InPrelude, - { pr_env = env scope; - pr_required = scope.sc_required; }) } - | _ -> scope + bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; }) (* ------------------------------------------------------------------ *) - let import (scope : scope) (name : qsymbol) = - assert (scope.sc_pr_uc = None); + let add_subtype (scope : scope) ({ pl_desc = subtype } : psubtype located) = + let loced x = mk_loc _dummy x in + let env = env scope in - match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with - | None -> - hierror - "cannot import the non-existent theory `%s'" - (string_of_qsymbol name) + let scope = + let decl = EcDecl.{ + tyd_params = []; + tyd_type = `Abstract Sp.empty; + tyd_loca = `Global; (* FIXME:SUBTYPE *) + tyd_resolve = true; + } in bind scope (unloc subtype.pst_name, decl) in + + let carrier = + let ue = EcUnify.UniEnv.create None in + transty tp_tydecl env ue subtype.pst_carrier in + + let pred = + let x = EcIdent.create (fst subtype.pst_pred).pl_desc in + let env = EcEnv.Var.bind_local x carrier env in + let ue = EcUnify.UniEnv.create None in + let pred = EcTyping.trans_prop env ue (snd subtype.pst_pred) in + if not (EcUnify.UniEnv.closed ue) then + hierror ~loc:(snd subtype.pst_pred).pl_loc + "the predicate contains free type variables"; + let uidmap = EcUnify.UniEnv.close ue in + let fs = Tuni.subst uidmap in + f_lambda [(x, GTty carrier)] (Fsubst.f_subst fs pred) in + + let evclone = + { EcThCloning.evc_empty with + evc_types = Msym.of_list [ + "T", loced (`Direct carrier, `Inline `Clear); + "sT", loced ( + `ByPath (EcPath.pqname (EcEnv.root env) (unloc subtype.pst_name)), + `Inline `Clear + ); + ]; + evc_ops = Msym.of_list [ + "P", loced (`Direct pred, `Inline `Clear) + ]; + evc_lemmas = { + ev_bynames = Msym.empty; + ev_global = [ (None, Some [`Include, "prove"]) ] + } } in + + let cname = Option.map unloc subtype.pst_cname in + let npath = ofold ((^~) EcPath.pqname) (EcEnv.root env) cname in + let cpath = EcPath.fromqsymbol ([EcCoreLib.i_top], "Subtype") in + let theory = EcEnv.Theory.by_path ~mode:`Abstract cpath env in + + let renames = + match subtype.pst_rename with + | None -> [] + + | Some (insub, val_) -> [ + (`All, (EcRegexp.regexp "val", EcRegexp.subst val_)); + (`All, (EcRegexp.regexp "insub", EcRegexp.subst insub)); + ] in - | Some (path, cth) -> - if cth.cth_mode = `Abstract then - hierror "cannot import an abstract theory"; - bump_prelude - { scope with - sc_env = EcSection.import path scope.sc_env } + let (proofs, scope) = + EcTheoryReplay.replay Cloning.hooks + ~abstract:false ~local:`Global ~incl:(Option.is_none cname) + ~clears:Sp.empty ~renames ~opath:cpath ~npath + evclone scope + ( + Option.value ~default:(EcPath.basename cpath) cname, + theory.cth_items + ) in + + let proofs = Cloning.replay_proofs scope `Check proofs in + + Ax.add_defer scope proofs (* ------------------------------------------------------------------ *) - let export_p scope (p, lc) = - let item = mkitem EcTheory.import0 (EcTheory.Th_export (p, lc)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } - - let export (scope : scope) (name : qsymbol) = + let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) = assert (scope.sc_pr_uc = None); - - match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with - | None -> - hierror - "cannot export the non-existent theory `%s'" - (string_of_qsymbol name) - - | Some (path, cth) -> - if cth.cth_mode = `Abstract then - hierror "cannot export an abstract theory"; - (* The section will fix the locality *) - bump_prelude (export_p scope (path, `Global)) + let item = EcTheory.mkitem import (EcTheory.Th_typeclass(x, tc)) in + { scope with sc_env = EcSection.add_item item scope.sc_env } (* ------------------------------------------------------------------ *) - let check_end_required scope thname = - if fst scope.sc_name <> thname then - hierror "end-of-file while processing external theory %s %s" - (fst scope.sc_name) thname; - if scope.sc_pr_uc <> None then - hierror - "end-of-file while processing proof %s" (fst scope.sc_name) - - (* -------------------------------------------------------------------- *) - let require (scope : scope) ((name, mode) : required_info * thmode) loader = + let add_class (scope : scope) { pl_desc = tcd } = assert (scope.sc_pr_uc = None); + let lc = tcd.ptc_loca in + let name = unloc tcd.ptc_name in + let scenv = (env scope) in - if required scope name then begin - if name.rqd_direct - then mark_as_direct scope name.rqd_name - else scope - end else - match Msym.find_opt name.rqd_name scope.sc_loaded with - | Some _ -> require_loaded name scope - - | None -> - try - let imported = enter (for_loading scope) mode name.rqd_name `Global in - let imported = { imported with sc_env = EcSection.astop imported.sc_env } in - let thname = fst imported.sc_name in - let imported = loader imported in + check_name_available scope tcd.ptc_name; - check_end_required imported thname; + let tclass = + let uptc = + tcd.ptc_inth |> omap + (fun { pl_loc = uploc; pl_desc = uptc } -> + match EcEnv.TypeClass.lookup_opt uptc scenv with + | None -> hierror ~loc:uploc "unknown type-class: `%s'" + (string_of_qsymbol uptc) + | Some (tcp, _) -> tcp) + in - let cth = exit_r ~pempty:`No imported in - let (cth, rqs), (name1, _), imported = cth in - assert (name.rqd_name = name1); - let scope = { scope with sc_loaded = - Msym.add name.rqd_name (oget cth, rqs) imported.sc_loaded; } in + let asty = + let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in + { tyd_params = []; + tyd_type = `Abstract body; + tyd_loca = (lc :> locality); + tyd_resolve = true; } in + let scenv = EcEnv.Ty.bind name asty scenv in - bump_prelude (require_loaded name scope) + (* Check for duplicated field names *) + Msym.odup unloc (List.map fst tcd.ptc_ops) + |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc + "duplicated operator name: `%s'" x.pl_desc); + Msym.odup unloc (List.map fst tcd.ptc_axs) + |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc + "duplicated axiom name: `%s'" x.pl_desc); - with e -> begin - match toperror_of_exn_r e with - | Some (l, e) when not (EcLocation.isdummy l) -> - raise (ImportError (Some l, name.rqd_name, e)) - | _ -> - raise (ImportError (None, name.rqd_name, e)) - end + (* Check operators types *) + let operators = + let check1 (x, ty) = + let ue = EcUnify.UniEnv.create (Some []) in + let ty = transty tp_tydecl scenv ue ty in + let uidmap = EcUnify.UniEnv.close ue in + let ty = ty_subst (Tuni.subst uidmap) ty in + (EcIdent.create (unloc x), ty) + in + tcd.ptc_ops |> List.map check1 in - let required scope = scope.sc_required -end + (* Check axioms *) + let axioms = + let scenv = EcEnv.Var.bind_locals operators scenv in + let check1 (x, ax) = + let ue = EcUnify.UniEnv.create (Some []) in + let ax = trans_prop scenv ue ax in + let uidmap = EcUnify.UniEnv.close ue in + let fs = Tuni.subst uidmap in + let ax = Fsubst.f_subst fs ax in + (unloc x, ax) + in + tcd.ptc_axs |> List.map check1 in -(* -------------------------------------------------------------------- *) -module Section = struct - module T = EcTheory + (* Construct actual type-class *) + { tc_prt = uptc; tc_ops = operators; tc_axs = axioms; tc_loca = lc} + in + bindclass scope (name, tclass) - let enter (scope : scope) (name : psymbol option) = - assert (scope.sc_pr_uc = None); - { scope with - sc_env = EcSection.enter_section (omap unloc name) scope.sc_env } + (* ------------------------------------------------------------------ *) + let check_tci_operators env tcty ops reqs = + let ue = EcUnify.UniEnv.create (Some (fst tcty)) in + let rmap = Mstr.of_list reqs in - let exit (scope : scope) (name : psymbol option) = - let sc_env = EcSection.exit_section (omap unloc name) scope.sc_env in - { scope with sc_env } -end + let ops = + let tt1 m (x, (tvi, op)) = + if not (Mstr.mem (unloc x) rmap) then + hierror ~loc:x.pl_loc "invalid operator name: `%s'" (unloc x); -(* -------------------------------------------------------------------- *) -module Reduction = struct - (* FIXME: section -> allow "local" flag *) - let add_reduction scope (opts, reds) = - check_state `InTop "hint simplify" scope; + let tvi = List.map (TT.transty tp_tydecl env ue) tvi in + let selected = + EcUnify.select_op ~filter:(fun _ -> EcDecl.is_oper) + (Some (EcUnify.TVIunamed tvi)) env (unloc op) ue ([], None) + in + let op = + match selected with + | [] -> hierror ~loc:op.pl_loc "unknown operator" + | op1::op2::_ -> + hierror ~loc:op.pl_loc + "ambiguous operator (%s / %s)" + (EcPath.tostring (fst (proj4_1 op1))) + (EcPath.tostring (fst (proj4_1 op2))) + | [((p, _), _, _, _)] -> + let op = EcEnv.Op.by_path p env in + let opty = + Tvar.subst + (Tvar.init (List.map fst op.op_tparams) tvi) + op.op_ty + in + (p, opty) - let rules = - let for1 idx name = - let idx = odfl 0 idx in - let ax_p = EcEnv.Ax.lookup_path (unloc name) (env scope) in - let opts = EcTheory.{ - ur_delta = List.mem `Delta opts; - ur_eqtrue = List.mem `EqTrue opts; - } in + in + Mstr.change + (function + | None -> Some (x.pl_loc, op) + | Some _ -> hierror ~loc:(x.pl_loc) + "duplicated operator name: `%s'" (unloc x)) + (unloc x) m + in + List.fold_left tt1 Mstr.empty ops + in + List.iter + (fun (x, (req, _)) -> + if req && not (Mstr.mem x ops) then + hierror "no definition for operator `%s'" x) + reqs; + List.fold_left + (fun m (x, (_, ty)) -> + match Mstr.find_opt x ops with + | None -> m + | Some (loc, (p, opty)) -> + if not (EcReduction.EqTest.for_type env ty opty) then + hierror ~loc "invalid type for operator `%s'" x; + Mstr.add x p m) + Mstr.empty reqs - let red_info = - EcReduction.User.compile ~opts ~prio:idx (env scope) ax_p in - (ax_p, opts, Some red_info) in + (* ------------------------------------------------------------------ *) + let check_tci_axioms scope mode axs reqs lc = + let rmap = Mstr.of_list reqs in + let symbs, axs = + List.map_fold + (fun m (x, t) -> + if not (Mstr.mem (unloc x) rmap) then + hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x); + if Sstr.mem (unloc x) m then + hierror ~loc:(x.pl_loc) "duplicated axiom name: `%s'" (unloc x); + (Sstr.add (unloc x) m, (unloc x, t, Mstr.find (unloc x) rmap))) + Sstr.empty axs in - let rules = List.map (fun (xs, idx) -> List.map (for1 idx) xs) reds in - List.flatten rules + let interactive = + List.pmap + (fun (x, req) -> + if not (Mstr.mem x symbs) then + let ax = { + ax_tparams = []; + ax_spec = req; + ax_kind = `Lemma; + ax_loca = lc; + ax_visibility = `NoSmt; + } in Some ((None, ax), EcPath.psymbol x, scope.sc_env) + else None) + reqs in + List.iter + (fun (x, pt, f) -> + let x = "$" ^ x in + let t = { pt_core = pt; pt_intros = []; } in + let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in + let t = { pt_core = t; pt_intros = []; } in + let ax = { + ax_tparams = []; + ax_spec = f; + ax_kind = `Lemma; + ax_visibility = `NoSmt; + ax_loca = lc; + } in - in + let pucflags = { puc_visibility = `Visible; puc_local = false; } in + let pucflags = (([], None), pucflags) in + let check = Check_mode.check scope.sc_options in - let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_reduction rules) in - { scope with sc_env = EcSection.add_item item scope.sc_env } -end + let escope = scope in + let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in + let escope = Tactics.proof escope in + let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in + ignore (Ax.save_r escope)) + axs; + interactive -(* -------------------------------------------------------------------- *) -module Cloning = struct (* ------------------------------------------------------------------ *) - open EcTheory - open EcThCloning - - module C = EcThCloning - module R = EcTheoryReplay + (* FIXME section: those path does not exists ... + futhermode Ring.ZModule is an abstract theory *) + let p_zmod = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ZModule"], "zmodule") + let p_ring = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ComRing"], "ring" ) + let p_idomain = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "IDomain"], "idomain") + let p_field = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field" ], "field" ) (* ------------------------------------------------------------------ *) - let hooks : scope R.ovrhooks = - let thexit sc pempty = snd (Theory.exit ?clears:None ~pempty sc) in - let add_item scope import item = - let item = EcTheory.mkitem import item in - { scope with sc_env = EcSection.add_item item scope.sc_env } in - { R.henv = (fun scope -> scope.sc_env); - R.hadd_item = add_item; - R.hthenter = Theory.enter; - R.hthexit = thexit; - R.herr = (fun ?loc -> hierror ?loc "%s"); } + let ring_of_symmap env ty kind symbols = + { r_type = ty; + r_zero = oget (Mstr.find_opt "rzero" symbols); + r_one = oget (Mstr.find_opt "rone" symbols); + r_add = oget (Mstr.find_opt "add" symbols); + r_opp = (Mstr.find_opt "opp" symbols); + r_mul = oget (Mstr.find_opt "mul" symbols); + r_exp = (Mstr.find_opt "expr" symbols); + r_sub = (Mstr.find_opt "sub" symbols); + r_kind = kind; + r_embed = + (match Mstr.find_opt "ofint" symbols with + | None when EcReduction.EqTest.for_type env ty tint -> `Direct + | None -> `Default | Some p -> `Embed p); } - (* ------------------------------------------------------------------ *) - module Options = struct - open EcTheoryReplay + let addring ~import (scope : scope) mode (kind, { pl_desc = tci; pl_loc = loc }) = + let env = env scope in + if not (EcAlgTactic.is_module_loaded env) then + hierror "load AlgTactic/Ring first"; - let default = { clo_abstract = false; } + let ty = + let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in + let ty = transty tp_tydecl env ue (snd tci.pti_type) in + assert (EcUnify.UniEnv.closed ue); + let uidmap = EcUnify.UniEnv.close ue in + (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty) + in + if not (List.is_empty (fst ty)) then + hierror "ring instances cannot be polymorphic"; - let merge1 opts (b, (x : theory_cloning_option)) = - match x with - | `Abstract -> { opts with clo_abstract = b; } + let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in + let symbols = check_tci_operators env ty tci.pti_ops symbols in + let cr = ring_of_symmap env (snd ty) kind symbols in + let axioms = EcAlgTactic.ring_axioms env cr in + let lc = (tci.pti_loca :> locality) in + let inter = check_tci_axioms scope mode tci.pti_axs axioms lc in + let add env p = + let item = EcTheory.Th_instance (ty,`General p, tci.pti_loca) in + let item = EcTheory.mkitem import item in + EcSection.add_item item env in - let merge opts (specs : theory_cloning_options) = - List.fold_left merge1 opts specs - end + let scope = + { scope with sc_env = + List.fold_left add + (let item = + EcTheory.Th_instance (([], snd ty), `Ring cr, tci.pti_loca) in + let item = EcTheory.mkitem import item in + EcSection.add_item item scope.sc_env) + [p_zmod; p_ring; p_idomain] } - (* ------------------------------------------------------------------ *) - let clone (scope : scope) mode (thcl : theory_cloning) = - assert (scope.sc_pr_uc = None); + in Ax.add_defer scope inter - let { cl_name = name; - cl_theory = (opath, oth); - cl_clone = ovrds; - cl_rename = rnms; - cl_ntclr = ntclr; } + (* ------------------------------------------------------------------ *) + let field_of_symmap env ty symbols = + { f_ring = ring_of_symmap env ty `Integer symbols; + f_inv = oget (Mstr.find_opt "inv" symbols); + f_div = Mstr.find_opt "div" symbols; } - = C.clone scope.sc_env thcl in + let addfield ~import (scope : scope) mode { pl_desc = tci; pl_loc = loc; } = + let env = env scope in + if not (EcAlgTactic.is_module_loaded env) then + hierror "load AlgTactic/Ring first"; - let incl = thcl.pthc_import = Some `Include in - let opts = Options.merge Options.default thcl.pthc_opts in + let ty = + let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in + let ty = transty tp_tydecl env ue (snd tci.pti_type) in + assert (EcUnify.UniEnv.closed ue); + let uidmap = EcUnify.UniEnv.close ue in + (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty) + in + if not (List.is_empty (fst ty)) then + hierror "field instances cannot be polymorphic"; + let symbols = EcAlgTactic.field_symbols env (snd ty) in + let symbols = check_tci_operators env ty tci.pti_ops symbols in + let cr = field_of_symmap env (snd ty) symbols in + let axioms = EcAlgTactic.field_axioms env cr in + let lc = (tci.pti_loca :> locality) in + let inter = check_tci_axioms scope mode tci.pti_axs axioms lc; in + let add env p = + let item = EcTheory.Th_instance(ty,`General p, tci.pti_loca) in + let item = EcTheory.mkitem import item in + EcSection.add_item item env in + let scope = + { scope with + sc_env = + List.fold_left add + (let item = + EcTheory.Th_instance (([], snd ty), `Field cr, tci.pti_loca) in + let item = EcTheory.mkitem import item in + EcSection.add_item item scope.sc_env) + [p_zmod; p_ring; p_idomain; p_field] } - if thcl.pthc_import = Some `Include && opts.R.clo_abstract then - hierror "cannot include an abstract theory"; - if thcl.pthc_import = Some `Include && EcUtils.is_some thcl.pthc_name then - hierror "cannot give an alias to an included clone"; + in Ax.add_defer scope inter - let cpath = EcEnv.root (env scope) in - let npath = if incl then cpath else EcPath.pqname cpath name in + (* ------------------------------------------------------------------ *) + let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) = + let subst = EcSubst.add_tydef EcSubst.empty tcp ([], ty) in + List.map (fun (x, opty) -> + (EcIdent.name x, (true, EcSubst.subst_ty subst opty))) + tc.tc_ops - let (proofs, scope) = - EcTheoryReplay.replay hooks - ~abstract:opts.R.clo_abstract ~local:thcl.pthc_local ~incl - ~clears:ntclr ~renames:rnms ~opath ~npath ovrds - scope (name, oth.cth_items) +(* + (* ------------------------------------------------------------------ *) + let add_generic_tc (scope : scope) _mode { pl_desc = tci; pl_loc = loc; } = + let ty = + let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in + let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in + assert (EcUnify.UniEnv.closed ue); + (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty) in - let proofs = List.pmap (fun axc -> - match axc.C.axc_tac with + let (tcp, tc) = + match EcEnv.TypeClass.lookup_opt (unloc tci.pti_name) (env scope) with | None -> - Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env) + hierror ~loc:tci.pti_name.pl_loc + "unknown type-class: %s" (string_of_qsymbol (unloc tci.pti_name)) + | Some tc -> tc + in - | Some pt -> - let t = { pt_core = pt; pt_intros = []; } in - let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in - let t = { pt_core = t; pt_intros = []; } in - let (x, ax) = axc.C.axc_axiom in + let symbols = symbols_of_tc scope.sc_env (snd ty) (tcp, tc) in + let _symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in - let pucflags = { puc_visibility = `Visible; puc_local = false; } in - let pucflags = (([], None), pucflags) in - let check = Check_mode.check scope.sc_options in + { scope with + sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env } - let escope = { scope with sc_env = axc.C.axc_env; } in - let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in - let escope = Tactics.proof escope in - let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in - ignore (Ax.save_r escope); None) - proofs - in +(* + let ue = EcUnify.UniEnv.create (Some []) in + let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in + try EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc + with EcUnify.UnificationFailure _ -> + hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc)) +*) +*) - let scope = - thcl.pthc_import |> ofold (fun flag scope -> - match flag with - | `Import -> - { scope with sc_env = EcSection.import npath scope.sc_env; } - | `Export -> - let item = EcTheory.mkitem EcTheory.import0 (Th_export (npath, `Global)) in - { scope with sc_env = EcSection.add_item item scope.sc_env; } - | `Include -> scope) - scope + (* ------------------------------------------------------------------ *) + let add_instance + ?(import = EcTheory.import0) (scope : scope) mode ({ pl_desc = tci } as toptci) + = + match unloc tci.pti_name with + | ([], "bring") -> begin + if EcUtils.is_some tci.pti_args then + hierror "unsupported-option"; + addring ~import scope mode (`Boolean, toptci) + end - in Ax.add_defer scope proofs + | ([], "ring") -> begin + let kind = + match tci.pti_args with + | None -> `Integer + | Some (`Ring (c, p)) -> + if odfl false (c |> omap (fun c -> c <^ BI.of_int 2)) then + hierror "invalid coefficient modulus"; + if odfl false (p |> omap (fun p -> p <^ BI.of_int 2)) then + hierror "invalid power modulus"; + if opt_equal BI.equal c (Some (BI.of_int 2)) + && opt_equal BI.equal p (Some (BI.of_int 2)) + then `Boolean + else `Modulus (c, p) + in addring ~import scope mode (kind, toptci) + end + + | ([], "field") -> addfield ~import scope mode toptci + | _ -> + if EcUtils.is_some tci.pti_args then + hierror "unsupported-option"; + failwith "unsupported" (* FIXME *) end (* -------------------------------------------------------------------- *) diff --git a/src/ecScope.mli b/src/ecScope.mli index f04f9595aa..7b1abcbace 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -118,6 +118,7 @@ end module Ty : sig val add : scope -> ptydecl located -> scope + val add_subtype : scope -> psubtype located -> scope val add_class : scope -> ptypeclass located -> scope val add_instance : ?import:EcTheory.import -> scope -> Ax.proofmode -> ptycinstance located -> scope end diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 5ed2df1d2c..603b52914a 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -53,11 +53,23 @@ type axclone = { axc_tac : EcParsetree.ptactic_core option; } +(* ------------------------------------------------------------------ *) +type xty_override = + [ty_override_def genoverride | `Direct of EcAst.ty] * clmode + +(* ------------------------------------------------------------------ *) +type xop_override = + [op_override_def genoverride | `Direct of EcAst.form] * clmode + +(* ------------------------------------------------------------------ *) +type xpr_override = + [pr_override_def genoverride | `Direct of EcAst.form] * clmode + (* ------------------------------------------------------------------ *) type evclone = { - evc_types : (ty_override located) Msym.t; - evc_ops : (op_override located) Msym.t; - evc_preds : (pr_override located) Msym.t; + evc_types : (xty_override located) Msym.t; + evc_ops : (xop_override located) Msym.t; + evc_preds : (xpr_override located) Msym.t; evc_abbrevs : (nt_override located) Msym.t; evc_modexprs : (me_override located) Msym.t; evc_modtypes : (mt_override located) Msym.t; @@ -65,6 +77,7 @@ type evclone = { evc_ths : evclone Msym.t; } + and evlemma = { ev_global : (ptactic_core option * evtags option) list; ev_bynames : evinfo Msym.t; @@ -271,7 +284,8 @@ end = struct (fun evc -> if Msym.mem x evc.evc_types then clone_error oc.oc_env (CE_DupOverride (OVK_Type, name)); - { evc with evc_types = Msym.add x (mk_loc lc tyd) evc.evc_types }) + { evc with evc_types = + Msym.add x (mk_loc lc tyd :> xty_override located) evc.evc_types }) nm evc in (proofs, evc) @@ -288,13 +302,14 @@ end = struct (fun evc -> if Msym.mem x evc.evc_ops then clone_error oc.oc_env (CE_DupOverride (OVK_Operator, name)); - { evc with evc_ops = Msym.add x (mk_loc lc opd) evc.evc_ops }) + { evc with evc_ops = + Msym.add x (mk_loc lc opd :> xop_override located) evc.evc_ops }) nm evc in (proofs, evc) (* ------------------------------------------------------------------ *) - let pr_ovrd oc ((proofs, evc) : state) name (prd : pr_override) = + let pr_ovrd oc ((proofs, evc) : state) name (prd : EcParsetree.pr_override) = let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in if find_pr oc.oc_oth name = None then @@ -305,7 +320,8 @@ end = struct (fun evc -> if Msym.mem x evc.evc_preds then clone_error oc.oc_env (CE_DupOverride (OVK_Predicate, name)); - { evc with evc_preds = Msym.add x (mk_loc lc prd) evc.evc_preds }) + { evc with evc_preds = + Msym.add x (mk_loc lc prd :> xpr_override located) evc.evc_preds }) nm evc in (proofs, evc) diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli index b4206554d6..26806f6c14 100644 --- a/src/ecThCloning.mli +++ b/src/ecThCloning.mli @@ -39,11 +39,23 @@ exception CloneError of EcEnv.env * clone_error val clone_error : EcEnv.env -> clone_error -> 'a +(* ------------------------------------------------------------------ *) +type xty_override = + [ty_override_def genoverride | `Direct of EcAst.ty] * clmode + +(* ------------------------------------------------------------------ *) +type xop_override = + [op_override_def genoverride | `Direct of EcAst.form] * clmode + +(* ------------------------------------------------------------------ *) +type xpr_override = + [pr_override_def genoverride | `Direct of EcAst.form] * clmode + (* -------------------------------------------------------------------- *) type evclone = { - evc_types : (ty_override located) Msym.t; - evc_ops : (op_override located) Msym.t; - evc_preds : (pr_override located) Msym.t; + evc_types : (xty_override located) Msym.t; + evc_ops : (xop_override located) Msym.t; + evc_preds : (xpr_override located) Msym.t; evc_abbrevs : (nt_override located) Msym.t; evc_modexprs : (me_override located) Msym.t; evc_modtypes : (mt_override located) Msym.t; diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 0b122511bf..5d63690fbe 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -246,22 +246,33 @@ let operator_compatible env oper1 oper2 = | _ , _ -> raise exn (* -------------------------------------------------------------------- *) -let check_evtags (tags : evtags) (src : symbol list) = - let module E = struct exception Reject end in +let check_evtags ?(tags : evtags option) (src : symbol list) = + let exception Reject in + + let explicit = "explicit" in try - let dfl = not (List.exists (fun (mode, _) -> mode = `Include) tags) in - let stt = - List.map (fun src -> - let do1 status (mode, dst) = - match mode with - | `Exclude -> if sym_equal src dst then raise E.Reject; status - | `Include -> status || (sym_equal src dst) - in List.fold_left do1 dfl tags) - src - in List.mem true stt - - with E.Reject -> false + match tags with + | None -> + if List.mem explicit src then + raise Reject; + true + + | Some tags -> + let dfl = + not (List.mem explicit src) && + not (List.exists (fun (mode, _) -> mode = `Include) tags) in + let stt = + List.map (fun src -> + let do1 status (mode, dst) = + match mode with + | `Exclude -> if sym_equal src dst then raise Reject; status + | `Include -> status || (sym_equal src dst) + in List.fold_left do1 dfl tags) + src + in List.mem true stt + + with Reject -> false (* -------------------------------------------------------------------- *) let xpath ove x = @@ -284,12 +295,23 @@ let string_of_renaming_kind = function | `Theory -> "theory" (* -------------------------------------------------------------------- *) -let rename ove subst (kind, name) = +let rename ?(fold = true) ove subst (kind, name) = try let newname = - List.find_map - (fun rnm -> EcThCloning.rename rnm (kind, name)) - ove.ovre_rnms in + match fold with + | false -> + List.find_map + (fun rnm -> EcThCloning.rename rnm (kind, name)) + ove.ovre_rnms + | _ -> + let newname = + List.fold_left (* FIXME:parallel substitution *) + (fun name rnm -> + Option.value ~default:name (EcThCloning.rename rnm (kind, name))) + name ove.ovre_rnms in + if newname = name then raise Not_found; + newname + in let nameok = match kind with @@ -355,6 +377,17 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | _ -> assert false end + + | `Direct ty -> begin + assert (List.is_empty otyd.tyd_params); + let decl = + { tyd_params = []; + tyd_type = `Concrete ty; + tyd_resolve = otyd.tyd_resolve && (mode = `Alias); + tyd_loca = otyd.tyd_loca; } + + in (decl, ty) + end in let subst, x = @@ -484,6 +517,15 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = | _ -> clone_error env (CE_UnkOverride(OVK_Operator, EcPath.toqsymbol p)) end + + | `Direct body -> + assert (List.is_empty refop.op_tparams); + let newop = + mk_op + ~opaque:optransparent ~clinline:(opmode <> `Alias) + [] body.f_ty (Some (OP_Plain body)) refop.op_loca in + (newop, body) + in match opmode with | `Alias -> @@ -602,6 +644,18 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) = | _ -> clone_error env (CE_UnkOverride(OVK_Predicate, EcPath.toqsymbol p)) end + + | `Direct body -> + assert (List.is_empty refpr.op_tparams); + let newpr = + { op_tparams = []; + op_ty = body.f_ty; + op_kind = OB_pred (Some (PR_Plain body)); + op_opaque = oopr.op_opaque; + op_clinline = prmode <> `Alias; + op_loca = refpr.op_loca; + op_unfold = refpr.op_unfold; } in + (newpr, body) in match prmode with @@ -679,9 +733,13 @@ and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) = match Msym.find_opt x (ove.ovre_ovrd.evc_lemmas.ev_bynames) with | Some (pt, hide, explicit) -> Some (pt, hide, explicit) | None when is_axiom ax.ax_kind -> - List.Exceptionless.find_map - (function (pt, None) -> Some (pt, `Alias, false) | (pt, Some pttags) -> - if check_evtags pttags (Ssym.elements tags) then + List.Exceptionless.find_map (function + | (pt, None) -> + if check_evtags (Ssym.elements tags) then + Some (pt, `Alias, false) + else None + | (pt, Some pttags) -> + if check_evtags ~tags:pttags (Ssym.elements tags) then Some (pt, `Alias, false) else None) ove.ovre_glproof diff --git a/tests/subtype-clone-sugar.ec b/tests/subtype-clone-sugar.ec new file mode 100644 index 0000000000..94bc894913 --- /dev/null +++ b/tests/subtype-clone-sugar.ec @@ -0,0 +1,7 @@ +require import AllCore. +require Subtype. + +subtype zmod3 = + { x : int | 0 <= x < 3 }. + +realize inhabited. by exists 0. qed. diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index d2633cd5d7..a58e61ab4b 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -23,18 +23,11 @@ op ispoly (p : prepoly) = (forall c, c < 0 => p c = zeror) /\ (exists d, forall c, (d < c)%Int => p c = zeror). -clone include Subtype - with type T <- prepoly, - op P <- ispoly - rename "insub" as "to_poly" - rename "val" as "of_poly" -proof *. +subtype poly = { p : prepoly | ispoly p } + rename "to_poly", "of_poly". + realize inhabited. - exists (fun _, zeror). - rewrite /ispoly. - auto. -qed. -type poly = sT. +proof. by exists (fun _ => zeror). qed. op "_.[_]" (p : poly) (i : int) = (of_poly p) i. diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index 3d68db5ce2..df0e3127f9 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -11,15 +11,10 @@ abstract theory ZModRing. const p : { int | 2 <= p } as ge2_p. (* -------------------------------------------------------------------- *) -clone Subtype as Sub with - type T <- int, - op P (x : int) <- 0 <= x < p -proof *. -realize inhabited. -exists 0. smt(ge2_p). -qed. +subtype zmod as Sub = { x : int | 0 <= x < p }. -type zmod = Sub.sT. +realize inhabited. +proof. by exists 0; smt(ge2_p). qed. (* -------------------------------------------------------------------- *) op inzmod (z : int) = Sub.insubd (z %% p). diff --git a/theories/datatypes/Word.eca b/theories/datatypes/Word.eca index ee7dcfaa11..07582d5a47 100644 --- a/theories/datatypes/Word.eca +++ b/theories/datatypes/Word.eca @@ -14,19 +14,16 @@ op wordw : t list = mkseq (fun _ => dchar) n. lemma size_wordw: size wordw = n. proof. by rewrite size_mkseq ler_maxr ?ge0_n. qed. -clone include Subtype - with type T <- t list, - op P <- fun w => size w = n -proof *. -realize inhabited by exists wordw; exact size_wordw. +subtype word = { w : t list | size w = n }. + +realize inhabited. +proof. by exists wordw; exact: size_wordw. qed. -type word = sT. (* default value chosen for backward compatibility *) op mkword x = odflt (insubd wordw) (insub x). op ofword = val. (* -------------------------------------------------------------------- *) - lemma mkwordK : cancel ofword mkword. proof. smt(valK). qed. diff --git a/theories/datatypes/Xreal.ec b/theories/datatypes/Xreal.ec index e84ca54d2e..e2fac68d6d 100644 --- a/theories/datatypes/Xreal.ec +++ b/theories/datatypes/Xreal.ec @@ -62,18 +62,13 @@ end MonoidDI. theory Rp. -clone include Subtype - with type T <- real, - op P <- fun x => 0.0 <= x - rename "insubd" as "of_real" - rename "val" as "to_real" -proof*. -realize inhabited by exists 0%r. +subtype realp = { x : real | 0.0 <= x } + rename "of_real", "to_real". -type realp = sT. +realize inhabited by exists 0%r. abbrev (%r) = to_real. -abbrev (%rp) = of_real. +abbrev (%rp) = of_reald. theory IntNotation. abbrev (%rp) (n:int) = n%r%rp. @@ -82,13 +77,13 @@ end IntNotation. export IntNotation. axiom witness_0 : witness = 0%rp. lemma of_real_neg x : x < 0.0 => x%rp = 0%rp. -proof. smt(to_realK val_of_real witness_0). qed. +proof. smt(to_realK to_real_of_reald witness_0). qed. lemma of_real_le0 x : x <= 0%r => x%rp = 0%rp. proof. by rewrite ler_eqVlt; case => [->// | /of_real_neg]. qed. lemma to_realK_simpl (x:realp) : x%r%rp = x by apply: to_realKd. -hint simplify to_realK_simpl, of_realK. +hint simplify to_realK_simpl, of_realdK. lemma to_realP_simpl x : (0.0 <= x%r) = true by rewrite to_realP. hint simplify to_realP_simpl. @@ -106,33 +101,33 @@ abbrev (<) (x y : realp) = x%r < y%r. clone include MonoidDI with type t <- realp, - op zero <- of_real 0.0, - op MulMonoid.one <- of_real 1.0, + op zero <- of_reald 0.0, + op MulMonoid.one <- of_reald 1.0, op ( + ) <- Rp.( + ), op ( * ) <- Rp.( * ) -proof * by smt(of_realK to_realP to_real_inj). +proof * by smt(of_realdK to_realP to_real_inj). lemma to_realD (x y:realp) : (x + y)%r = x%r + y%r. -proof. smt (of_realK to_realP). qed. +proof. smt (of_realdK to_realP). qed. lemma to_realM (x y:realp) : (x * y)%r = x%r * y%r. -proof. smt (of_realK to_realP). qed. +proof. smt (of_realdK to_realP). qed. lemma to_realI x : (inv x)%r = inv x%r. -proof. smt (of_realK to_realP Real.invr0). qed. +proof. smt (of_realdK to_realP Real.invr0). qed. hint simplify to_realD, to_realM, to_realI. lemma of_realD x y : 0.0 <= x => 0.0 <= y => (x + y)%rp = x%rp + y%rp. -proof. smt (of_realK to_realP). qed. +proof. smt (of_realdK to_realP). qed. lemma of_realM x y : 0.0 <= x => 0.0 <= y => (x * y)%rp = x%rp * y%rp. -proof. smt (of_realK to_realP). qed. +proof. smt (of_realdK to_realP). qed. lemma of_realI (x:real) : (inv x)%rp = inv x%rp. -proof. smt (of_realK to_realP of_real_neg divr0). qed. +proof. smt (of_realdK to_realP of_real_neg divr0). qed. hint simplify of_realI. op (%pos) (x:real) = if 0.0 <= x then x else 0.0. @@ -148,7 +143,7 @@ lemma inv_pos x : inv x%pos = (inv x)%pos by smt(divr0). lemma to_real_of_real (x:real) : x%rp%r = x%pos. -proof. by rewrite val_of_real witness_0. qed. +proof. by rewrite to_real_of_reald witness_0. qed. hint simplify to_real_of_real. lemma to_pos_mu ['a] (d : 'a distr) (e: 'a -> bool) : @@ -283,19 +278,19 @@ proof. by rewrite /( ** ) one_neq0. qed. hint simplify smul0m, smul1m. lemma smulmDr x y z: x ** (y + z) = x ** y + x ** z. -proof. by rewrite /( ** ); case: (x = of_real 0%r) => //= ?; apply mulmDr. qed. +proof. by rewrite /( ** ); case: (x = of_reald 0%r) => //= ?; apply mulmDr. qed. lemma smulmCA d x y : d ** (rp x * y) = rp x * (d ** y). -proof. by rewrite /( ** ); case: (d = of_real 0.0) => //=; rewrite mulmCA. qed. +proof. by rewrite /( ** ); case: (d = of_reald 0.0) => //=; rewrite mulmCA. qed. lemma smulmA d x y : d ** (x * rp y) = (d ** x) * rp y. -proof. by rewrite /( ** ); case: (d = of_real 0.0) => //=;rewrite mulmA. qed. +proof. by rewrite /( ** ); case: (d = of_reald 0.0) => //=;rewrite mulmA. qed. lemma smulmAC d x y : d ** (x * rp y) = rp y * (d ** x) . proof. by rewrite mulmC smulmCA. qed. lemma smulrp x y : x ** rp y = rp (x * y). -proof. by rewrite /( ** ); case: (x = of_real 0.0). qed. +proof. by rewrite /( ** ); case: (x = of_reald 0.0). qed. hint simplify smulrp. (* -------------------------------------------------------------- *) @@ -355,7 +350,7 @@ lemma xler_pmul2l (x:realp) : 0%rp < x => forall (y z : xreal), rp x * y <= rp x * z <=> y <= z. proof. -rewrite (of_realK 0%r) //. +rewrite (of_realdK 0%r) //. move=> hx y z; case: z => // z; case: y => // y. by rewrite /= -!to_realM !to_realM ler_pmul2l. qed. @@ -368,7 +363,7 @@ lemma xler_pmul2r (x:realp) : 0%rp < x => forall (y z : xreal), y * rp x <= z * rp x <=> y <= z. proof. -rewrite (of_realK 0%r) //. +rewrite (of_realdK 0%r) //. move=> hx y z; case: z => // z; case: y => // y. by rewrite /= -!to_realM !to_realM ler_pmul2r. qed. @@ -390,7 +385,7 @@ lemma xler_md x y c : ((0%r < c) => x <= y) => c ** x <= c ** y. proof. move=> h; rewrite /( **). case: (0%r < c ) => hc. - + have -> /=: (c%rp <> 0%rp) by smt(to_realP of_realK to_realK_simpl). + + have -> /=: (c%rp <> 0%rp) by smt(to_realP of_realdK to_realK_simpl). by apply/xler_mull/h. by have -> : (c%rp = 0%rp) by smt(of_real_neg). qed. @@ -452,7 +447,7 @@ theory Lift. fun (x : 'a) => f1 x * f2 x. abbrev ( ** ) (d : 'a distr) (f : 'a -> xreal) = - fun (x : 'a) => of_real (mu1 d x) ** f x. + fun (x : 'a) => of_reald (mu1 d x) ** f x. op is_real ['a] (f : 'a -> xreal) = forall x, is_real (f x). @@ -542,7 +537,7 @@ theory Lift. is_real (d ** f1) <=> is_real (d ** f2). proof. move=> h; split => h1 x; have := h1 x; rewrite /( ** ); - case: (of_real (mu1 d x) = of_real 0.0) => // ?; rewrite !is_realM h //; smt(mu_bounded). + case: (of_reald (mu1 d x) = of_reald 0.0) => // ?; rewrite !is_realM h //; smt(mu_bounded). qed. lemma is_real_rp ['a] (f:'a -> realp) : is_real (fun x => rp (f x)). @@ -641,7 +636,7 @@ op Ep ['a] (d : 'a distr) (f : 'a -> xreal) = if is_real g then psuminf g else oo. lemma psuminfZ ['a] (c:realp) (f: 'a -> xreal) : - is_real f => c <> of_real 0.0 => + is_real f => c <> of_reald 0.0 => psuminf (fun x => rp c * f x) = rp c * psuminf f. proof. move=> hf hc; have heq := summableZ_iff (to_real f) (to_real c) _; 1:smt(@Rp). @@ -709,26 +704,26 @@ proof. have -> : !is_real (fun (x : 'a) => if (mu1 d x)%rp = 0%rp then 0%xr else oo). + apply/negP => his. move/neq0_mu : hw => -[x [hx _]]. - by have := his x; smt(of_realK to_realP ge0_weight). - by have -> : (weight d)%rp <> 0%rp by smt(of_realK to_realP ge0_weight). + by have := his x; smt(of_realdK to_realP ge0_weight). + by have -> : (weight d)%rp <> 0%rp by smt(of_realdK to_realP ge0_weight). qed. lemma EpZ ['a] (d: 'a distr) (c:realp) (f: 'a -> xreal) : - c <> of_real 0.0 => + c <> of_reald 0.0 => Ep d (fun x => rp c * f x) = rp c * Ep d f. proof. move=> hc; rewrite /Ep /= (is_realMd f); 1: by move=> x _ /=; rewrite is_realM. case: (is_real (d ** f)) => // hr; rewrite /psuminf. rewrite mdCA /= to_realM /=. rewrite -summableZ_iff 1:#smt:(@Rp); rewrite /to_real. - case: (summable (fun (x : 'a) => to_real (of_real (mu1 d x) ** f x))) => // ?. + case: (summable (fun (x : 'a) => to_real (of_reald (mu1 d x) ** f x))) => // ?. rewrite sumZ /= of_realM // ge0_sum => /= ?; apply to_realP. qed. lemma EpsZ ['a] (d: 'a distr) (c:realp) (f: 'a -> xreal) : Ep d (fun x => c ** f x) = c ** Ep d f. proof. - rewrite /( ** ); case: (c = of_real 0%r) => ?; last by apply EpZ. + rewrite /( ** ); case: (c = of_reald 0%r) => ?; last by apply EpZ. by rewrite EpC. qed. @@ -737,7 +732,7 @@ lemma EpD ['a] (d : 'a distr) (f1 f2 : 'a -> xreal) : proof. rewrite /Ep /= mdDr. have /= := is_realD (d ** f1) (d ** f2). - case: (is_real (fun x => of_real (mu1 d x) ** f1 x + of_real (mu1 d x) ** f2 x)) => h />. + case: (is_real (fun x => of_reald (mu1 d x) ** f1 x + of_reald (mu1 d x) ** f2 x)) => h />. + by move=> h1 h2; rewrite -psumifD. by case: (is_real (d ** f1)) => />. qed. @@ -883,7 +878,7 @@ proof. rewrite /dmap Ep_dlet; apply eq_Ep => x _ /=; apply Ep_dunit. qed. (* -------------------------------------------------------------------- *) lemma Ep_duniform ['a] (s : 'a list) (f : 'a -> xreal) : Ep (duniform s) f = - of_real (1%r / (size ((undup s)))%r) ** big predT f (undup s). + of_reald (1%r / (size ((undup s)))%r) ** big predT f (undup s). proof. rewrite (Ep_fin (undup s)) 1:undup_uniq. + move=> x hx; rewrite mem_undup -supp_duniform; smt(ge0_mu). @@ -893,7 +888,7 @@ qed. (* -------------------------------------------------------------------- *) lemma Ep_dbool (f : bool -> xreal) : - Ep {0,1} f = of_real 0.5 ** f true + of_real 0.5 ** f false. + Ep {0,1} f = of_reald 0.5 ** f true + of_reald 0.5 ** f false. proof. rewrite (Ep_fin [true; false]) 1://; 1: smt(supp_dbool). by rewrite big_consT big_seq1 /= !dbool1E. diff --git a/theories/structure/Quotient.ec b/theories/structure/Quotient.ec index 1e61798741..6626fd19a2 100644 --- a/theories/structure/Quotient.ec +++ b/theories/structure/Quotient.ec @@ -87,24 +87,22 @@ apply/(eqv_trans (canon x)); first by apply/eqv_canon. by rewrite eq &(eqv_refl). qed. -clone import Subtype with - type T <- T, - op P <- iscanon -proof *. +subtype qT as QSub = { x : T | iscanon x }. + realize inhabited. -smt(canonK). -qed. - -type qT = sT. +proof. smt(canonK). qed. + +import QSub. clone include CoreQuotient with type T <- T, type qT <- qT, - op pi = fun x => Subtype.insubd (canon x), - op repr = fun x => Subtype.val x + op pi = fun x => QSub.insubd (canon x), + op repr = fun x => QSub.val x proof *. + realize reprK. proof. by move=> q; rewrite /pi /repr /insubd canon_iscanon 1:valP valK. qed. diff --git a/theories/structure/Subtype.eca b/theories/structure/Subtype.eca index 7e01521967..6276df116c 100644 --- a/theories/structure/Subtype.eca +++ b/theories/structure/Subtype.eca @@ -1,7 +1,5 @@ -pragma +implicits. - - (* -------------------------------------------------------------------- *) +pragma +implicits. (* -------------------------------------------------------------------- *) (* This theory defines the subtype [sT] of [T] defined as {x : T | P x} *) @@ -21,89 +19,34 @@ pragma +implicits. require import AllCore. -(* These three parameters are to be instantiated by the user. *) -type T. -op P : T -> bool. -axiom inhabited: exists x, P x. - -(* This parameter must never be instantiated upon cloning, otherwise - unsoundness may ensure. Hence the name. *) -type do_not_instantiate_this_type. -(* TODO: we want a tag to make abstract types uninstantiable *) - -(* The lemma below is justified by the axiom [inhabited] and the fact - that the type [do_not_instantiate_this_type] is unspecified. It says - that there is an injective function [f] with range [P] - - The proof is admitted, essentially turning it into a global axiom - asserting the existence of subtypes. We cannot use [axiom] here, - because this would make the lemma a parameter of the theory *) - -lemma subtype_injection: - exists (f : do_not_instantiate_this_type -> T), - injective f /\ (forall x, P x <=> exists y, x = f y). -admitted. -(* TODO: together with uninstantiable abstract types, we also want - global axioms in (abstract) theories.that do not show up in [proof*] *) - -(* This is the subtype that the user sees. By making it a type-copy of - [do_not_instantiate_this_type], we make sure that the user cannot - do `type sT <- ...` when cloning. *) -type sT = do_not_instantiate_this_type wrapped. - -(* We define `val` in two steps so that `print val` does not show the - ugly internal stuff *) -op [opaque] internal_val = choiceb - (fun (f : do_not_instantiate_this_type -> T), - injective f /\ (forall (x:T), ((P x) <=> exists y, x = f y))) witness. +type T, sT. -(* -------------------------------------------------------------------- *) +op P : T -> bool. -(* Injection from [sT] to [T] *) -op [opaque] val (x : sT) : T = with x = Wrap x' => internal_val x'. +op insub : T -> sT option. +op val : sT -> T. -lemma val_range x: P x <=> exists y, x = val y. -proof. -have /= := choicebP _ witness subtype_injection; rewrite -/internal_val. -move => [ival_inj ival_range]. -split => [Px|[[y] ->]]; 2: smt(). -have := ival_range x; rewrite Px /= => -[z ?]. -by exists (Wrap z); smt(). -qed. +axiom [prove] inhabited : exists x, P x. -lemma val_inj: injective val. -proof. -have /= := choicebP _ witness subtype_injection; rewrite -/internal_val. -by move => [ival_inj _] [x] [y] /#. -qed. +axiom [explicit] insubN (x : T): !P x => insub x = None. +axiom [explicit] insubT (x : T): P x => omap val (insub x) = Some x. -lemma valP (x : sT): P (val x) by smt (val_range). +axiom [explicit] valP (x : sT): P (val x). +axiom [explicit] valK: pcancel val insub. (* -------------------------------------------------------------------- *) - -op [opaque] insub : T -> sT option = pinv val. - -lemma insubN (x : T): !P x => insub x = None. -proof. by rewrite /insub => not; apply pinvN; smt(val_range). qed. - -lemma valK: pcancel val insub. -proof. by rewrite /insub; apply/pcancel_pinv/val_inj. qed. - -lemma insubT (x : T): P x => omap val (insub x) = Some x. -proof. by move => Px @/insub; apply pinv_inv; smt(val_range). qed. +op insubd (x : T) = odflt witness (insub x). (* -------------------------------------------------------------------- *) - -(* TODO: Maybe this could be removed, it seems relatively -pointless. It's here for compatibility with the previous Subtype -implementation *) -op wsT = val witness. - -lemma insubW: insub wsT = Some witness<:sT>. -proof. by rewrite /wsT; smt (valK). qed. +lemma val_range x: P x <=> exists y, x = val y. +proof. split. +- by move/insubT; case (insub x) => // [y] /= <-; exists y. +- by case=> y ->; apply/valP. +qed. (* -------------------------------------------------------------------- *) -op insubd (x : T) = odflt witness (insub x). +lemma val_inj: injective val. +proof. by apply/(pcan_inj _ _ valK). qed. (* -------------------------------------------------------------------- *) lemma valKd: cancel val insubd. @@ -113,9 +56,9 @@ lemma insubP (x : T): (* We need inductive predicates *) (exists u, P x /\ insub x = Some u /\ val u = x) \/ (!P x /\ insub x = None). proof. (* this proof script is awful *) - case (P x)=> [Px | /insubN -> //]; left. - move: Px => /insubT; case {-2}(insub x) (eq_refl (insub x))=> //. - by move=> /= u eq_insub eqx; exists u => /=; move: eqx => ->. +case (P x)=> [Px | /insubN -> //]; left. +move: Px => /insubT; case {-2}(insub x) (eq_refl (insub x))=> //. +by move=> /= u eq_insub eqx; exists u => /=; move: eqx => ->. qed. lemma val_insubd x: val (insubd x) = if P x then x else val witness.