Fix all FIXME comments in src/

src/ecCoreGoal.ml

@@ -207,11 +207,10 @@ let mk_tcerror ?(catchable = true) ?penv ?loc msg =
 exception TcError of tcerror
 
 (* -------------------------------------------------------------------- *)
-let tc_error (penv : proofenv) ?(catchable = true) ?loc ?who fmt =
+let tc_error (penv : proofenv) ?(catchable = true) ?loc fmt =
   let buf  = Buffer.create 127 in
   let fbuf = Format.formatter_of_buffer buf in
   let loc  = loc |> omap (fun loc -> mk_location loc) in
-    ignore (who : string option);       (* FIXME: remove? *)
     Format.kfprintf
       (fun _ ->
          Format.pp_print_flush fbuf ();
@@ -221,8 +220,7 @@ let tc_error (penv : proofenv) ?(catchable = true) ?loc ?who fmt =
       fbuf fmt
 
 (* -------------------------------------------------------------------- *)
-let tc_error_exn (penv : proofenv) ?(catchable = true) ?loc ?who exn =
-  ignore (who : string option);
+let tc_error_exn (penv : proofenv) ?(catchable = true) ?loc exn =
   raise (TcError (
     { tc_catchable = catchable;
       tc_proofenv  = Some penv;
@@ -251,7 +249,7 @@ let tacuerror_exn ?(catchable = true) exn =
     tc_reloced   = None; })
 
 (* -------------------------------------------------------------------- *)
-let tc_error_lazy (penv : proofenv) ?(catchable = true) ?loc ?who msg =
+let tc_error_lazy (penv : proofenv) ?(catchable = true) ?loc msg =
   let getmsg () =
     let buf  = Buffer.create 127 in
     let fbuf = Format.formatter_of_buffer buf in
@@ -261,21 +259,20 @@ let tc_error_lazy (penv : proofenv) ?(catchable = true) ?loc ?who msg =
 
   let loc = loc |> omap (fun loc -> mk_location loc) in
 
-  ignore (who : string option);         (* FIXME: remove? *)
   raise (TcError (mk_tcerror ~catchable ~penv ?loc (lazy (getmsg ()))))
 
 (* -------------------------------------------------------------------- *)
 type symkind = [`Lemma | `Operator | `Local]
 
-let tc_lookup_error pe ?loc ?who kind qs =
+let tc_lookup_error pe ?loc kind qs =
   let string_of_kind kind =
     match kind with
     | `Lemma    -> "lemma"
     | `Operator -> "operator"
     | `Local    -> "local variable"
   in
 
-  tc_error_lazy pe ~catchable:true ?loc ?who
+  tc_error_lazy pe ~catchable:true ?loc
     (fun fmt ->
       Format.fprintf fmt "unknown %s `%s'"
         (string_of_kind kind)

src/ecCoreGoal.mli

@@ -207,15 +207,15 @@ val closed : proof -> bool
 
 (* -------------------------------------------------------------------- *)
 val tc_error :
-     proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string
+     proofenv -> ?catchable:bool -> ?loc:EcLocation.t
   -> ('a, Format.formatter, unit, 'b) format4 -> 'a
 
 val tc_error_exn :
-     proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string
+     proofenv -> ?catchable:bool -> ?loc:EcLocation.t
   -> exn -> 'a
 
 val tc_error_lazy :
-     proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string
+     proofenv -> ?catchable:bool -> ?loc:EcLocation.t
   -> (Format.formatter -> unit) -> 'a
 
 (* -------------------------------------------------------------------- *)
@@ -229,7 +229,7 @@ val tacuerror_exn :
 type symkind = [`Lemma | `Operator | `Local]
 
 val tc_lookup_error :
-  proofenv -> ?loc:EcLocation.t -> ?who:string -> symkind -> qsymbol -> 'a
+  proofenv -> ?loc:EcLocation.t -> symkind -> qsymbol -> 'a
 
 (* -------------------------------------------------------------------- *)
 val reloc : EcLocation.t -> ('a -> 'b) -> 'a -> 'b

src/ecEnv.ml

@@ -1685,8 +1685,8 @@ module Fun = struct
 
   let actmem_body me fun_ =
     match fun_.f_def with
-    | FBabs _   -> assert false (* FIXME error message *)
-    | FBalias _ -> assert false (* FIXME error message *)
+    | FBabs _   -> invalid_arg "actmem_body: function has no concrete body (abstract)"
+    | FBalias _ -> invalid_arg "actmem_body: function has no concrete body (alias)"
     | FBdef fd   ->
       let mem = EcMemory.empty_local ~witharg:false me in
       let mem = add_params mem fun_ in
@@ -3337,8 +3337,13 @@ module LDecl = struct
     | LD_hyp f ->
         LD_hyp (Fsubst.f_subst s f)
 
-    | LD_abs_st _ ->                    (* FIXME *)
-        assert false
+    | LD_abs_st us ->
+        let subst_pv_ty (pv, ty) = (pv_subst s pv, ty_subst s ty) in
+        LD_abs_st {
+          aus_calls  = List.map (x_subst s) us.aus_calls;
+          aus_reads  = List.map subst_pv_ty us.aus_reads;
+          aus_writes = List.map subst_pv_ty us.aus_writes;
+        }
 
   (* ------------------------------------------------------------------ *)
   let ld_fv = function

src/ecHiGoal.ml

@@ -1205,7 +1205,7 @@ let process_view1 pe tc =
 
         FApi.t_internal
           (FApi.t_seqsub (EcLowGoal.t_cut cutf)
-             [EcLowGoal.t_close ~who:"view" discharge;
+             [EcLowGoal.t_close discharge;
               EcLowGoal.t_clear top])
           tc
 

src/ecIo.ml

@@ -198,7 +198,7 @@ let parseall (ecreader : ecreader) =
     | EcParsetree.P_DocComment _ ->
         aux acc
     | EcParsetree.P_Undo _ | EcParsetree.P_Exit ->
-        assert false                    (* FIXME *)
+        raise (EcParsetree.ParseError (EcLocation.dummy, Some "unexpected undo/exit command"))
   in
     aux []
 

src/ecLowGoal.ml

@@ -280,14 +280,14 @@ let t_admit (tc : tcenv1) =
 
 (* -------------------------------------------------------------------- *)
 let t_fail (tc : tcenv1) =
-  tc_error !!tc ~who:"fail" "explicit call to [fail]"
+  tc_error !!tc "explicit call to [fail]"
 
 (* -------------------------------------------------------------------- *)
-let t_close ?who (t : FApi.backward) (tc : tcenv1) =
+let t_close (t : FApi.backward) (tc : tcenv1) =
   let tc = t tc in
 
   if not (FApi.tc_done tc) then
-    tc_error !$tc ?who "expecting a closed goal";
+    tc_error !$tc "expecting a closed goal";
   tc
 
 (* -------------------------------------------------------------------- *)

src/ecLowGoal.mli

@@ -32,7 +32,7 @@ val t_admit   : FApi.backward
 val t_true    : FApi.backward
 val t_fail    : FApi.backward
 val t_id      : FApi.backward
-val t_close   : ?who:string -> FApi.backward -> FApi.backward
+val t_close   : FApi.backward -> FApi.backward
 val t_shuffle : EcIdent.t list -> FApi.backward
 
 (* -------------------------------------------------------------------- *)

src/ecPV.ml

@@ -657,12 +657,13 @@ module Mpv2 = struct
 
   let add_glob env mp1 mp2 eqs =
     let mp1, mp2 = NormMp.norm_mpath env mp1, NormMp.norm_mpath env mp2 in
-    (* FIXME error message *)
-    if not (EcPath.m_equal mp1 mp2) then assert false;
-    if not (mp1.m_args = []) then assert false;
+    if not (EcPath.m_equal mp1 mp2) then
+      invalid_arg "add_glob: module paths are not equal";
+    if not (mp1.m_args = []) then
+      invalid_arg "add_glob: module path has functor arguments";
     begin match mp1.m_top with
     | `Local _ -> ()
-    | _ -> assert false
+    | _ -> invalid_arg "add_glob: module path is not local"
     end;
     { eqs with s_gl = Sm.add mp1 eqs.s_gl }
 
@@ -1075,13 +1076,13 @@ and i_eqobs_in_refl env i eqo =
 
   | Sraise e -> add_eqs_refl env PV.empty e
 
-  | Sabstract _ -> assert false
+  | Sabstract _ -> invalid_arg "i_eqobs_in_refl: abstract statement"
 
 and eqobs_inF_refl env f' eqo =
   let f = NormMp.norm_xfun env f' in
   let ffun = Fun.by_xpath f env in
   match ffun.f_def with
-  | FBalias _ -> assert false
+  | FBalias _ -> invalid_arg "eqobs_inF_refl: alias after normalization"
   | FBdef fdef ->
     let eqo =
       match fdef.f_ret with

src/ecPrinting.ml

@@ -245,7 +245,7 @@ module PPEnv = struct
         fun sm ->
           check_for_local sm;
           let ue = EcUnify.UniEnv.create None in
-          match  EcUnify.select_op ~hidden:true ~filter tvi ppe.ppe_env sm ue dom with
+          match  EcUnify.select_op ~filter tvi ppe.ppe_env sm ue dom with
           | [(p1, _), _, _, _] -> p1
           | _ -> raise (EcEnv.LookupFailure (`QSymbol sm)) in
 

src/ecProofTerm.ml

@@ -807,7 +807,7 @@ and apply_pterm_to_local ?loc pt id =
   | LD_mem _ ->
       apply_pterm_to_arg_r ?loc pt (PVAMemory id)
 
-  | LD_abs_st _ -> assert false
+  | LD_abs_st _ -> invalid_arg "apply_pterm_to_local: abstract statement"
 
 (* -------------------------------------------------------------------- *)
 and process_implicits ip ({ ptev_pt = pt; ptev_env = env; } as pe) =

src/ecScope.ml

@@ -2659,7 +2659,8 @@ module Ty = struct
     | _ ->
         if EcUtils.is_some tci.pti_args then
           hierror "unsupported-option";
-        failwith "unsupported"          (* FIXME *)
+        hierror "unsupported instance: %s"
+          (EcSymbols.string_of_qsymbol (EcLocation.unloc tci.pti_name))
 end
 
 (* -------------------------------------------------------------------- *)module Search = struct

src/ecTyping.ml

@@ -297,7 +297,7 @@ let (_i_inuse, s_inuse, se_inuse) =
       se_inuse map e
 
     | Sabstract _ ->
-      assert false (* FIXME *)
+      invalid_arg "i_inuse: unexpected abstract statement"
 
   and s_inuse (map : uses) (s : stmt) =
     List.fold_left i_inuse map s.s_node

src/ecUnify.ml

@@ -332,7 +332,6 @@ type select_result = (EcPath.path * ty list) * ty * unienv * sbody option
 
 (* -------------------------------------------------------------------- *)
 let select_op
-  ?(hidden : bool = false)
   ?(filter : EcPath.path -> operator -> bool = fun _ _ -> true)
    (tvi    : tvar_inst option)
    (env    : EcEnv.env)
@@ -341,7 +340,6 @@ let select_op
    (sig_   : ty list * ty option)
   : select_result list
 =
-  ignore hidden;                (* FIXME *)
 
   let module D = EcDecl in
 

src/ecUnify.mli

@@ -43,8 +43,7 @@ type sbody = ((EcIdent.t * ty) list * expr) Lazy.t
 type select_result = (EcPath.path * ty list) * ty * unienv * sbody option
 
 val select_op :
-     ?hidden:bool
-  -> ?filter:(path -> operator -> bool)
+     ?filter:(path -> operator -> bool)
   -> tvi
   -> EcEnv.env
   -> qsymbol

src/phl/ecPhlFel.ml

@@ -105,7 +105,9 @@ and callable_oracles_i env modv os i =
 
     | Sasgn _ | Srnd _ | Sraise _ -> os
 
-    | Sabstract _ -> assert false (* FIXME *)
+    | Sabstract id ->
+        let us = AbsStmt.byid id env in
+        List.fold_left (callable_oracles_f env modv) os us.aus_calls
 
 let callable_oracles_stmt env modv =
   callable_oracles_s env modv EcPath.Sx.empty

src/phl/ecPhlInline.ml

@@ -151,7 +151,7 @@ module LowInternal = struct
             me (List.combine sps bs)
           in me, [i_match (e, bs)]
 
-      | _, _ -> assert false (* FIXME error message *)
+      | _, _ -> tc_error !!tc "code pattern doesn't match instruction type"
 
     and inline_s me sp s =
       match sp with
@@ -259,7 +259,7 @@ module HiInternal = struct
       aux_s 0 s.s_node
 
   (* ------------------------------------------------------------------ *)
-  let pat_of_occs cond occs s =
+  let pat_of_occs tc cond occs s =
     let occs = ref occs in
 
     let rec aux_i occ i =
@@ -298,7 +298,10 @@ module HiInternal = struct
 
     let sp = snd (aux_s 0 0 s.s_node) in
 
-    assert (Sint.is_empty !occs); sp    (* FIXME error message *)
+    if not (Sint.is_empty !occs) then
+      tc_error !!tc "invalid occurrence(s): %s"
+        (String.concat ", " (List.map string_of_int (Sint.elements !occs)));
+    sp
 
   (* ------------------------------------------------------------------ *)
   let pat_of_spath =
@@ -390,15 +393,15 @@ let process_inline_occs ~use_tuple side cond occs tc =
   match concl.f_node, side with
   | FequivS es, Some b ->
       let st = sideif b es.es_sl es.es_sr in
-      let sp = HiInternal.pat_of_occs cond occs st in
+      let sp = HiInternal.pat_of_occs tc cond occs st in
         t_inline_equiv ~use_tuple b sp tc
 
   | FhoareS hs, None ->
-      let sp = HiInternal.pat_of_occs cond occs hs.hs_s in
+      let sp = HiInternal.pat_of_occs tc cond occs hs.hs_s in
         t_inline_hoare ~use_tuple sp tc
 
   | FbdHoareS bhs, None ->
-      let sp = HiInternal.pat_of_occs cond occs bhs.bhs_s in
+      let sp = HiInternal.pat_of_occs tc cond occs bhs.bhs_s in
         t_inline_bdhoare ~use_tuple sp tc
 
   | _, _ -> tc_error !!tc "invalid arguments"

src/phl/ecPhlSkip.ml

@@ -43,9 +43,9 @@ module LowInternal = struct
     let bhs = tc1_as_bdhoareS tc in
 
     if not (List.is_empty bhs.bhs_s.s_node) then
-      tc_error !!tc ~who:"skip" "instruction list is not empty";
+      tc_error !!tc "instruction list is not empty";
     if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then
-      tc_error !!tc ~who:"skip" "";
+      tc_error !!tc "skip requires comparison to be = or >=, got <=";
 
     let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in
     let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in
@@ -75,9 +75,9 @@ module LowInternal = struct
     let es = tc1_as_equivS tc in
 
     if not (List.is_empty es.es_sl.s_node) then
-      tc_error !!tc ~who:"skip" "left instruction list is not empty";
+      tc_error !!tc "left instruction list is not empty";
     if not (List.is_empty es.es_sr.s_node) then
-      tc_error !!tc ~who:"skip" "right instruction list is not empty";
+      tc_error !!tc "right instruction list is not empty";
 
     let concl = map_ts_inv2 f_imp (es_pr es) (es_po es) in
     let concl = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr concl in

src/phl/ecPhlUpto.ml

@@ -223,28 +223,28 @@ let t_uptobad_r tc =
   let pr1, pr2 =
     try t2_map destr_pr (destr_eq concl)
     with DestrError _ ->
-      tc_error !!tc ~who:"byupto" "expecting a formula of the form \"Pr[_] = Pr[_]\""
+      tc_error !!tc "expecting a formula of the form \"Pr[_] = Pr[_]\""
   in
   if not (EcMemory.mem_equal pr1.pr_mem pr2.pr_mem) then
-    tc_error !!tc ~who:"byupto" "the initial memories should be equal";
+    tc_error !!tc "the initial memories should be equal";
   if not (is_conv ~ri:full_red hyps pr1.pr_args pr2.pr_args) then
-    tc_error !!tc ~who:"byupto" "the initial arguments should be equal";
+    tc_error !!tc "the initial arguments should be equal";
   if not (ss_inv_alpha_eq hyps pr1.pr_event pr2.pr_event) then
-    tc_error !!tc ~who:"byupto" "the events should be equal";
+    tc_error !!tc "the events should be equal";
   let bad =
     try destr_event (pr1.pr_event)
     with DestrError _ ->
-      tc_error !!tc ~who:"byupto" "the event should have the form \"E /\ !bad\" or \"!bad\""
+      tc_error !!tc "the event should have the form \"E /\\ !bad\" or \"!bad\""
   in
   begin match f_upto_init env bad pr1.pr_fun pr2.pr_fun with
-  | false -> tc_error !!tc ~who:"byupto" "the two functions are not equal upto bad"
+  | false -> tc_error !!tc "the two functions are not equal upto bad"
   | true -> ()
   | exception BadAssign (f, i) ->
       let ppenv = EcPrinting.PPEnv.ofenv env in
       let pp_fun fmt = function
        | None -> ()
        | Some f -> Format.fprintf fmt " in function %a" (EcPrinting.pp_funname ppenv) f in
-      tc_error !!tc ~who:"byupto" "bad is assigned after being set to true%a, %a"
+      tc_error !!tc "bad is assigned after being set to true%a, %a"
         pp_fun f (EcPrinting.pp_instr ppenv) i
   end;
   FApi.xmutate1 tc `HlUpto []
@@ -422,4 +422,4 @@ let process_uptobad tc =
           "expecting a goal of the form \"Pr[_] <= Pr[_] + Pr[_]\" or \"`|Pr[_] - Pr[_]| <= _\""
     end
   | _ ->
-    tc_error !!tc ~who:"byupto" "expecting a goal of the form \" _ <= _\""
+    tc_error !!tc "expecting a goal of the form \" _ <= _\""