diff options
| author | Son Ho | 2023-01-08 09:42:33 +0100 |
|---|---|---|
| committer | Son HO | 2023-02-03 11:21:46 +0100 |
| commit | 1302f2830905dc63f294aad00d78d03486e13d73 (patch) | |
| tree | 6a541816ba00323a30318f918fc06ce229a3508b /compiler/Pure.ml | |
| parent | 47c09ce99feb3e84967407d30c21bbcf42ab9736 (diff) | |
Implement a pass to filter the unused input arguments in the loop functions
Diffstat (limited to 'compiler/Pure.ml')
| -rw-r--r-- | compiler/Pure.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml index fe30a650..777d4308 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -312,9 +312,13 @@ type pure_assumed_fun_id = | FuelEqZero (** Test if some fuel is equal to 0 - TODO: ugly *) [@@deriving show, ord] +(** A function id for a non-assumed function *) +type regular_fun_id = A.fun_id * LoopId.id option * T.RegionGroupId.id option +[@@deriving show, ord] + (** A function identifier *) type fun_id = - | FromLlbc of A.fun_id * LoopId.id option * T.RegionGroupId.id option + | FromLlbc of regular_fun_id (** A function coming from LLBC. The loop id is [None] if the function is actually the auxiliary function |