Skip to content

cloning error: "body incompatible body" with hint simplify #646

@cassiersg

Description

@cassiersg

The following code example (minimized from work on jasmin's eclib) produces the error:

operator `ArrayWordsS.Wu8.Pack.map' body incompatible body

Removing the "hint simplify" line eliminates the error.

Example code:

require import AllCore List.

abstract theory MonoArray.
  type elem.
  op dfl : elem.
  op size: int.
  type t.
  op "_.[_]"  : t -> int -> elem.
  op init : (int -> elem) -> t.
  op of_list (l:elem list) = init (fun i => nth dfl l i).
  op to_list (t:t) = mkseq (fun i => t.[i]) size.
  op map (f: elem -> elem) (t:t) : t = init (fun i => f t.[i]).

  lemma map_to_list f t : map f t = of_list (map f (to_list t)). admitted.
end MonoArray.

abstract theory W_WS.
  clone export MonoArray as Pack.
  hint simplify Pack.map_to_list@1.
end W_WS.

abstract theory ArrayWords.
    clone W_WS as Wu8.
end ArrayWords.

abstract theory SubArrayDirect.
    clone ArrayWords as ArrayWordsS.
end SubArrayDirect.

clone export ArrayWords as ArrayWordsI.

clone export SubArrayDirect as SubArrayDirectI with
    theory ArrayWordsS <- ArrayWordsI.

cc @strub

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions