@@ -56,7 +56,7 @@ let ctype_of_ty (env: env) (ty: ty) : ctype =
56
56
| _ ->
57
57
Format. eprintf " Missing binding for type %a@."
58
58
EcPrinting. (pp_type (PPEnv. ofenv env)) ty;
59
- assert false
59
+ raise ( CircError " Failed to convert EC type to Circuit type " )
60
60
end
61
61
end
62
62
@@ -291,7 +291,7 @@ let circuit_of_op (env: env) (p: path) : circuit =
291
291
let op = try
292
292
EcEnv.Circuit. reverse_operator env p |> List. hd
293
293
with Failure _ ->
294
- assert false
294
+ raise ( CircError " Failed reverse operator " )
295
295
in
296
296
match op with
297
297
| `Bitstring (bs , op ) -> assert false
@@ -303,7 +303,7 @@ let circuit_of_op_with_args (env: env) (p: path) (args: arg list) : circuit =
303
303
let op = try
304
304
EcEnv.Circuit. reverse_operator env p |> List. hd
305
305
with Failure _ ->
306
- assert false
306
+ raise ( CircError " Failed reverse operator " )
307
307
in
308
308
match op with
309
309
| `Bitstring bsbnd -> circuit_of_bsop env (`BSBinding bsbnd) args
@@ -430,7 +430,7 @@ let circuit_of_form
430
430
| _ ->
431
431
if debug then Format. eprintf " Failed to get body for op: %a\n "
432
432
(EcPrinting. pp_form (EcPrinting.PPEnv. ofenv (LDecl. toenv hyps))) op;
433
- assert false
433
+ raise ( CircError " Failed to get body for op in propagate integer arg " )
434
434
in
435
435
(*
436
436
if debug then Format.eprintf "Propagating arguments for op: %a@\n"
@@ -478,7 +478,8 @@ let circuit_of_form
478
478
doit cache hyps f) hyps (form_list_of_form ~ppenv: (EcPrinting.PPEnv. ofenv (LDecl. toenv hyps)) f)
479
479
in
480
480
hyps, arg_of_circuits cs
481
- | _ -> assert false
481
+ | _ -> Format. eprintf " Failed to convert form to arg: %a@." EcPrinting. (pp_form (PPEnv. ofenv env)) f;
482
+ raise (CircError " Failed to convert arg to form" )
482
483
in
483
484
484
485
match f_.f_node with
@@ -506,7 +507,11 @@ let circuit_of_form
506
507
hyps, op
507
508
| None ->
508
509
if op_is_base env pth then
509
- let circ = circuit_of_op env pth in
510
+ let circ = try
511
+ circuit_of_op env pth
512
+ with
513
+ | CircError e -> Format. eprintf " (%s ->)" (EcPath. tostring pth); raise (CircError e)
514
+ in
510
515
let hyps = EcEnv.Circuit. add_circuit_cache_hyps hyps pth circ in
511
516
hyps, circ
512
517
else
@@ -529,7 +534,7 @@ let circuit_of_form
529
534
let hyps = EcEnv.Circuit. add_circuit_cache_hyps hyps pth circ in
530
535
hyps, circ
531
536
end
532
- | Fapp (f , fs ) ->
537
+ | Fapp (f , fs ) -> begin try
533
538
(* TODO: find a way to properly propagate int arguments. Done? *)
534
539
begin match f with
535
540
| {f_node = Fop (pth , _ )} when op_is_parametric_base env pth ->
@@ -600,6 +605,10 @@ let circuit_of_form
600
605
in
601
606
hyps, circuit_compose f_c fcs
602
607
end
608
+ with CircError e ->
609
+ Format. eprintf " Call %a ->" EcPrinting. (pp_form (PPEnv. ofenv env)) f;
610
+ raise (CircError e)
611
+ end
603
612
604
613
| Fquant (qnt , binds , f ) ->
605
614
let binds = List. map (fun (idn , t ) -> (idn, gty_as_ty t |> ctype_of_ty env)) binds in
@@ -672,8 +681,8 @@ let circuit_of_form
672
681
let hyps, fn = doit cache hyps fn in
673
682
hyps, circuit_compose fn [f]
674
683
) (doit cache hyps base) fs
675
- | ({f_node = Fop (p , _ )} , [rep ; fn ; base ]) when p = EcCoreLib.CI_Int. p_iter -> assert false
676
- | ({f_node = Fop (p , _ )} , [rep ; fn ; base ]) when p = EcCoreLib.CI_Int. p_fold -> assert false
684
+ | ({f_node = Fop (p , _ )} , [rep ; fn ; base ]) when p = EcCoreLib.CI_Int. p_iter -> assert false
685
+ | ({f_node = Fop (p , _ )} , [rep ; fn ; base ]) when p = EcCoreLib.CI_Int. p_fold -> assert false
677
686
| _ -> assert false
678
687
in
679
688
(*
0 commit comments