Internals: ax_spec is no more a form option

src/ecAlgTactic.ml

@@ -132,8 +132,8 @@ module Axioms = struct
 
     let for1 axname =
       let ax = EcEnv.Ax.by_path (EcPath.pqname tmod axname) env in
-        assert (ax.ax_tparams = [] && is_axiom ax.ax_kind && is_some ax.ax_spec);
-        (axname, EcSubst.subst_form subst (oget ax.ax_spec))
+        assert (ax.ax_tparams = [] && is_axiom ax.ax_kind);
+        (axname, EcSubst.subst_form subst ax.ax_spec)
     in
       List.map for1 axs
 

src/ecCommands.ml

@@ -750,7 +750,7 @@ let pp_current_goal ?(all = false) stream =
            let ppe = EcPrinting.PPEnv.ofenv env in
            Format.fprintf stream " %s: %a@\n%!"
              (EcPath.tostring p)
-             (EcPrinting.pp_form ppe) (oget ax.EcDecl.ax_spec))
+             (EcPrinting.pp_form ppe) ax.EcDecl.ax_spec)
         (fst ct)
 
   | Some { S.puc_active = Some (puc, _) } -> begin

src/ecDecl.ml

@@ -135,7 +135,7 @@ type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
 
 type axiom = {
   ax_tparams : ty_params;
-  ax_spec    : EcCoreFol.form option;
+  ax_spec    : EcCoreFol.form;
   ax_kind    : axiom_kind;
   ax_nosmt   : bool; }
 
@@ -261,7 +261,7 @@ let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, bd) =
   let axspec = f_forall args (f_eq op axbd) in
 
   { ax_tparams = axpm;
-    ax_spec    = Some axspec;
+    ax_spec    = axspec;
     ax_kind    = `Axiom (Ssym.empty, false);
     ax_nosmt   = nosmt; }
 

src/ecDecl.mli

@@ -133,7 +133,7 @@ type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
 
 type axiom = {
   ax_tparams : ty_params;
-  ax_spec    : form option;
+  ax_spec    : form;
   ax_kind    : axiom_kind;
   ax_nosmt   : bool;
 }

src/ecEnv.ml

@@ -684,7 +684,7 @@ module MC = struct
       let ax   =
         { ax_kind    = `Axiom (Ssym.empty, false);
           ax_tparams = tv;
-          ax_spec    = Some cl;
+          ax_spec    = cl;
           ax_nosmt   = false; } in
       (name, (axp, ax))) ax in
 
@@ -730,7 +730,7 @@ module MC = struct
             let do1 scheme name =
               let scname = Printf.sprintf "%s_%s" x name in
                 (scname, { ax_tparams = tyd.tyd_params;
-                           ax_spec    = Some scheme;
+                           ax_spec    = scheme;
                            ax_kind    = `Axiom (Ssym.empty, false);
                            ax_nosmt   = true; })
             in
@@ -765,7 +765,7 @@ module MC = struct
           let scheme =
             let scname = Printf.sprintf "%s_ind" x in
               (scname, { ax_tparams = tyd.tyd_params;
-                         ax_spec    = Some scheme;
+                         ax_spec    = scheme;
                          ax_kind    = `Axiom (Ssym.empty, false);
                          ax_nosmt   = true; })
           in
@@ -850,7 +850,7 @@ module MC = struct
           (fun (x, ax) ->
             let ax = Fsubst.f_subst fsubst ax in
               (x, { ax_tparams = [(self, Sp.singleton mypath)];
-                    ax_spec    = Some ax;
+                    ax_spec    = ax;
                     ax_kind    = `Axiom (Ssym.empty, false);
                     ax_nosmt   = true; }))
           tc.tc_axs
@@ -2329,7 +2329,7 @@ module NormMp = struct
         op_ty   = norm_ty env op.op_ty; }
 
   let norm_ax env ax =
-    { ax with ax_spec = ax.ax_spec |> omap (norm_form env) }
+    { ax with ax_spec = norm_form env ax.ax_spec }
 
   let is_abstract_fun f env =
     let f = norm_xfun env f in
@@ -2586,7 +2586,7 @@ module Ax = struct
 
   let instanciate p tys env =
     match by_path_opt p env with
-    | Some ({ ax_spec = Some f } as ax) ->
+    | Some ({ ax_spec = f } as ax) ->
         Fsubst.subst_tvar
           (EcTypes.Tvar.init (List.map fst ax.ax_tparams) tys) f
     | _ -> raise (LookupFailure (`Path p))

src/ecPrinting.ml

@@ -1860,9 +1860,7 @@ let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) =
   let basename = P.basename x in
 
   let pp_spec fmt =
-    match ax.ax_spec with
-    | None   -> pp_string fmt "<why3-imported>"
-    | Some f -> pp_form ppe fmt f 
+    pp_form ppe fmt ax.ax_spec
 
   and pp_name fmt =
     match ax.ax_tparams with

src/ecProofTerm.ml

@@ -179,7 +179,7 @@ let pt_of_uglobal pf hyps p =
   let ptenv   = ptenv_of_penv hyps pf in
   let env     = LDecl.toenv hyps in
   let ax      = oget (EcEnv.Ax.by_path_opt p env) in
-  let typ, ax = (ax.EcDecl.ax_tparams, oget ax.EcDecl.ax_spec) in
+  let typ, ax = (ax.EcDecl.ax_tparams, ax.EcDecl.ax_spec) in
 
   (* FIXME: TC HOOK *)
   let fs  = EcUnify.UniEnv.opentvi ptenv.pte_ue typ None in
@@ -362,7 +362,7 @@ let lookup_named_psymbol (hyps : LDecl.hyps) ~hastyp fp =
 
   | _ ->
     match EcEnv.Ax.lookup_opt fp (LDecl.toenv hyps) with
-    | Some (p, ({ EcDecl.ax_spec = Some fp } as ax)) ->
+    | Some (p, ({ EcDecl.ax_spec = fp } as ax)) ->
         Some (`Global p, (ax.EcDecl.ax_tparams, fp))
     | _ -> None
 

src/ecScope.ml

@@ -778,7 +778,7 @@ module Ax = struct
       | false -> PSNoCheck
       | true  ->
           let hyps  = EcEnv.LDecl.init scope.sc_env axd.ax_tparams in
-          let proof = EcCoreGoal.start hyps (oget axd.ax_spec) in
+          let proof = EcCoreGoal.start hyps axd.ax_spec in
           PSCheck proof
     in
     let puc =
@@ -833,7 +833,7 @@ module Ax = struct
         | _ -> `Lemma
 
       in { ax_tparams = tparams;
-           ax_spec    = Some concl;
+           ax_spec    = concl;
            ax_kind    = kind;
            ax_nosmt   = ax.pa_nosmt; }
     in
@@ -1166,7 +1166,7 @@ module Op = struct
                List.combine axpm (List.map snd tparams)) in
           let ax =
             { ax_tparams = axpm;
-              ax_spec    = Some ax;
+              ax_spec    = ax;
               ax_kind    = `Axiom (Ssym.empty, false);
               ax_nosmt   = false; }
           in Ax.bind scope false (unloc rname, ax))
@@ -1530,7 +1530,7 @@ module Ty = struct
            if not (Mstr.mem x symbs) then
              let ax = {
                ax_tparams = [];
-               ax_spec    = Some req;
+               ax_spec    = req;
                ax_kind    = `Lemma;
                ax_nosmt   = true;
              } in Some ((None, ax), EcPath.psymbol x, scope.sc_env)
@@ -1543,7 +1543,7 @@ module Ty = struct
           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    = Some f;
+                     ax_spec    = f;
                      ax_kind    = `Axiom (Ssym.empty, false);
                      ax_nosmt   = true; } in
 
@@ -2005,7 +2005,7 @@ module Section = struct
                   if not (EcSection.is_local `Lemma axp locals) then
                     Ax.bind scope false
                       (x, { ax with ax_spec =
-                              ax.ax_spec |> omap (EcSection.generalize scenv locals) })
+                              EcSection.generalize scenv locals ax.ax_spec })
                   else
                     scope
           end

src/ecSearch.ml

@@ -71,11 +71,7 @@ let match_ (env : EcEnv.env) (search : search list) f =
 
 (* -------------------------------------------------------------------- *)
 let search (env : EcEnv.env) (search : search list) =
-  let check _ ax =
-    match ax.EcDecl.ax_spec with
-    | None   -> false
-    | Some f -> match_ env search f
-
+  let check _ ax = match_ env search ax.EcDecl.ax_spec
   in EcEnv.Ax.all ~check env
 
 (* -------------------------------------------------------------------- *)
@@ -88,14 +84,11 @@ let sort (relevant:Sp.t) (res:(path * EcDecl.axiom) list) =
   let fr = Frequency.create unwanted_ops in
   let do1 (p, ax) = 
     Frequency.add fr ax;
-    let used = 
-      omap_dfl (Frequency.f_ops unwanted_ops) 
-        Frequency.r_empty ax.ax_spec in
+    let used = Frequency.f_ops unwanted_ops ax.ax_spec in
     (p,ax), used in
   let res = List.map do1 res in
 
   (* compute the weight of each axiom *)
-
   let rs = relevant, Sx.empty in
   let frequency_function freq = 1. +. log1p (float_of_int freq) in
 
@@ -112,8 +105,3 @@ let sort (relevant:Sp.t) (res:(path * EcDecl.axiom) list) =
   let res = List.map do1 res in
   let res = List.sort (fun (_,p1) (_,p2) -> compare p1 p2) res in
   List.map fst res
-
-
-
-
-

src/ecSection.ml

@@ -420,7 +420,7 @@ let generalize env lc (f : EcFol.form) =
     let f =
       let do1 p f =
         let ax = EcEnv.Ax.by_path p env in
-          EcFol.f_imp (oget ax.ax_spec) f
+        EcFol.f_imp ax.ax_spec f
       in
           List.fold_right do1 axioms f in
     let f =

src/ecSmt.ml

@@ -999,11 +999,9 @@ let lenv_of_hyps genv (hyps : hyps) : lenv =
 
 (* -------------------------------------------------------------------- *)
 let trans_axiom genv (p, ax) = 
-  match ax.ax_spec with
-  | Some f when not ax.ax_nosmt ->
-      let lenv = fst (lenv_of_tparams ax.ax_tparams) in    
-      add_axiom (genv, lenv) (preid_p p) f
-  | _ -> ()
+  if not ax.ax_nosmt then
+    let lenv = fst (lenv_of_tparams ax.ax_tparams) in    
+    add_axiom (genv, lenv) (preid_p p) ax.ax_spec
 
 (* -------------------------------------------------------------------- *)
 let mk_predb1 f l _ = f (Cast.force_prop (as_seq1 l))
@@ -1242,7 +1240,7 @@ module Frequency = struct
       | Fproj    (e, _)       -> add e
       | Fpr      pr           -> addx pr.pr_fun;add pr.pr_event;add pr.pr_args
       | _ -> () in
-    oiter add ax.ax_spec 
+    add ax.ax_spec 
 
   let create unwanted_op : frequency =
     { f_unwanted_op = unwanted_op;
@@ -1295,9 +1293,7 @@ let init_relevant env pi rs =
     let wanted = wanted_ax p in
     if wanted || (not ax.ax_nosmt && not (unwanted_ax p)) then begin
       Frequency.add fr ax;
-      let used = 
-        omap_dfl (Frequency.f_ops unwanted_ops) 
-          Frequency.r_empty ax.ax_spec in
+      let used = Frequency.f_ops unwanted_ops ax.ax_spec in
       let paxu = (p,ax), used in
       if wanted then push paxu rel else push paxu other
     end in

src/ecStrongRing.ml

@@ -46,7 +46,7 @@ let get_injection env p =
   try 
     let ax = EcEnv.Ax.by_path p env in
     (* try to match a term of the form  _ = _ <=> inj _ = inj _ *)
-    let _, concl = decompose_forall (oget ax.EcDecl.ax_spec) in
+    let _, concl = decompose_forall ax.EcDecl.ax_spec in
     let _, f = destr_iff concl in
     let f1, f2 = destr_eq f in
     match f1.f_node, f2.f_node with

src/ecSubst.ml

@@ -407,17 +407,12 @@ let subst_op (s : _subst) (op : operator) =
 let subst_ax (s : _subst) (ax : axiom) =
   let params = List.map (subst_typaram s) ax.ax_tparams in
   let s      = init_tparams s ax.ax_tparams params in
-  let spec   = 
-    match ax.ax_spec with
-    | None -> None
-    | Some f -> 
-        let s = f_subst_of_subst s in
-          Some (Fsubst.f_subst s f)
-  in
-     { ax_tparams = params;
-       ax_spec    = spec;
-       ax_kind    = ax.ax_kind;
-       ax_nosmt   = ax.ax_nosmt; }
+  let spec   = Fsubst.f_subst (f_subst_of_subst s) ax.ax_spec in
+
+  { ax_tparams = params;
+    ax_spec    = spec;
+    ax_kind    = ax.ax_kind;
+    ax_nosmt   = ax.ax_nosmt; }
 
 (* -------------------------------------------------------------------- *)
 let subst_ring (s : _subst) cr =

src/ecThCloning.ml

@@ -364,7 +364,7 @@ end = struct
          let ovrd = (ovrd, `Inline) in
          pr_ovrd ~cancrt:true oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
 
-      | CTh_axiom (x, ({ ax_spec = Some _ } as ax)) ->
+      | CTh_axiom (x, ax) ->
          if is_axiom ax.ax_kind then
            let params = List.map (EcIdent.name |- fst) ax.ax_tparams in
            let params = List.map (mk_loc lc) params in
@@ -478,7 +478,7 @@ end = struct
         clone_error oc.oc_env (CE_UnkOverride (OVK_Lemma, name))
 
     | Some ax ->
-        if not (is_axiom ax.ax_kind) || ax.ax_spec = None then
+        if not (is_axiom ax.ax_kind) then
           clone_error oc.oc_env (CE_CrtOverride (OVK_Lemma, name));
 
         let update1 evc =