coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] extract CompCert dependend type

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] extract CompCert dependend type
Date: Thu, 4 Apr 2019 13:54:15 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT smtp.uni-bremen.de
Ironport-phdr: 9a23:p1b5/hyZGnm31sXXCy+O+j09IxM/srCxBDY+r6Qd2+sfIJqq85mqBkHD//Il1AaPAdyCraoZwLaN++C4ACpcuM7H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjMusUMnYdvKqk9xxTHr3BVf+ha2X5kKUickhrh+su85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyJPDIOiYYUSDOQOMvpXoJTmqlsSsRezHxWgCP/zxjJKgHL9wK000/4mEQHDxAEuH8gOsHXIrNX3M6cSX/2+wbTPzTXZafNZxyzy6JXTch89ofGHQLV9ccTLyUkuCwPFjFKQqYL+MjOI0OQNsnGX4PF6Ve2xjm4otQdxriKyycgyk4TEgJ8exF7D9SV82ok1JNu4RVZ0Yd6lDJtQtzyaOJBsTsw+RGFovSA3waAFt56jZCUG1ZoqyhHFZ/Cab4SE/AjvWeaNLTtimX5oeqqziwu8/EWv0OHwS9W43EhQoiZbj9XBtWoB2wLO5sWFTPZ2412v1iyV1w/J7+FJOUA0mrTfK54m2rMwjZ8TsVjbHiPshUX2iq6Welw/9eiy9evnZ6vpppmGO4BplA7yKqUumsqhDuQkKgUCQmaW9Oum2LH+4UH1Xq9Gg/0qnqXDrZzXJ9wXpqujDA9U1oYj5Qy/DzCj0NkAk3kHNlNFeA6Fj4juNVHDO+34DfG+g1i1izhr3e7JPrj/DZXLNHTMjanuca5n60FA0Aoz0cxf55VMB74dJ/LzQ1b9u8DcDh8kKAO52P3nCdV41oMGQ22DGK6ZMKXIsV+J/O0jOeeMZJVG8Ar6fvMi/rvliWIzsV4bZ6igm5UNO16iGfEzDV+YfXjrjJ8rFn0MswAjV+fqwAmMSz9PZXG8d78653QxEo+jAIGFSo370+/J5zuyApADPjMOMVuLC3q9L9zVCcdJUzqbJ4paqhJBULGgT4E70hT36V3nzbsiJPDZ/yAe857uhoEsu7/j0Coq/DkxNPyzlnmXRjgpzH4ORno8xq16rEo7xlrRifEl0cwdLsRa4rZyail/NZPYyLYiWcv3RhqHY9GIDVy8T9CrB3c9Q4Bpzg==

Hi,

I have a CompCert Unsigned32 type and want to extract it:

Module Wordsize_32.
Definition wordsize := 32%nat.
Remark wordsize_not_zero: wordsize <> 0%nat.
Proof.
unfold wordsize.
congruence.
Qed.

End Wordsize_32.

Strategy opaque [Wordsize_32.wordsize].

Module Unsigned32 := Make(Wordsize_32).

Strategy 0 [Wordsize_32.wordsize].

If I extract it to Integer, I got all the additional definitions, like
wordsize, add, add_overflow, etc:
https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v.

Does someone know, why these additional definitions are also being extracted?
I replaced all definitions I need,
such as *mul* or *divu* with the operations of the target language, Haskell
in this case. None of the above
are called explicitly in my code.

regards,
--f.

[Coq-Club] extract CompCert dependend type, Fritjof Bornebusch, 04/04/2019
- Re: [Coq-Club] extract CompCert dependend type, Xavier Leroy, 04/05/2019