Skip to content

Instantly share code, notes, and snippets.

@MSoegtropIMC

MSoegtropIMC/ocamldebug.log Secret

Created April 3, 2021 14:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save MSoegtropIMC/4f96106054fc6aac106879a4a5ea807e to your computer and use it in GitHub Desktop.
Save MSoegtropIMC/4f96106054fc6aac106879a4a5ea807e to your computer and use it in GitHub Desktop.
Download ZIP
Coq kernel reduction case
Raw
ocamldebug.log
(ocd) start
Time: 20479987639 - pc: 3104612 - module Reduction
369 <|b|>try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
(ocd) p term1
term1: CClosure.fconstr =
(if rlt_ident_eq _x21 _x01
then
if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x01
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75))))
(if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))))
(ocd) p term2
term2: CClosure.fconstr =
(if rlt_ident_eq _x21 _x01
then
if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x01
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75))))
(if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))))
(ocd) bt 20
Backtrace:
#0 Reduction kernel/reduction.ml:369:3
#1 CArray clib/cArray.ml:267:53
#2 Reduction kernel/reduction.ml:706:21
#3 Reduction kernel/reduction.ml:419:56
#4 Reduction kernel/reduction.ml:369:73
#5 CArray clib/cArray.ml:267:53
#6 Reduction kernel/reduction.ml:706:21
#7 Reduction kernel/reduction.ml:419:56
#8 Reduction kernel/reduction.ml:369:73
#9 CArray clib/cArray.ml:267:53
#10 Reduction kernel/reduction.ml:706:21
#11 Reduction kernel/reduction.ml:419:56
#12 Reduction kernel/reduction.ml:369:73
#13 CArray clib/cArray.ml:241:41
#14 Reduction kernel/reduction.ml:369:73
#15 CArray clib/cArray.ml:267:53
#16 Reduction kernel/reduction.ml:706:21
#17 Reduction kernel/reduction.ml:419:56
#18 Reduction kernel/reduction.ml:369:73
#19 CArray clib/cArray.ml:241:41
(More frames follow)
(ocd) finish
Time: 20480012668 - pc: 2528924 - module CArray
267 fold (f (uget v1 k) (uget v2 k) (uget v3 k) a)<|a|> k in
(ocd) back
Time: 20480012667 - pc: 3104744 - module Reduction
369 try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv<|a|>
(ocd) p term1
term1: CClosure.fconstr =
(if rlt_ident_eq _x21 _x01
then
if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x01
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75))))
(if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))))
(ocd) p term2
term2: CClosure.fconstr =
(if rlt_ident_eq _x21 _x01
then
if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x01
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75))))
(if rlt_ident_eq _x21 _x00
then
if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef)
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _x00
(CSTR.val._0._2
(my_add_Fspec (repr (CSTR.Z._0._2 CSTR.positive._0._3))
_UNBOUND_REL_75)))
(if rlt_ident_eq _x21 _val
then CSTR.list._0._1 localdef
else
CSTR.list._0._2 localdef
(CSTR.localdef._0._1 _val (CSTR.val._0._2 _UNBOUND_REL_75))
(CSTR.list._0._1 localdef))))
(ocd) bt 20
Backtrace:
#0 Reduction kernel/reduction.ml:369:73
#1 CArray clib/cArray.ml:267:53
#2 Reduction kernel/reduction.ml:706:21
#3 Reduction kernel/reduction.ml:419:56
#4 Reduction kernel/reduction.ml:369:73
#5 CArray clib/cArray.ml:267:53
#6 Reduction kernel/reduction.ml:706:21
#7 Reduction kernel/reduction.ml:419:56
#8 Reduction kernel/reduction.ml:369:73
#9 CArray clib/cArray.ml:267:53
#10 Reduction kernel/reduction.ml:706:21
#11 Reduction kernel/reduction.ml:419:56
#12 Reduction kernel/reduction.ml:369:73
#13 CArray clib/cArray.ml:241:41
#14 Reduction kernel/reduction.ml:369:73
#15 CArray clib/cArray.ml:267:53
#16 Reduction kernel/reduction.ml:706:21
#17 Reduction kernel/reduction.ml:419:56
#18 Reduction kernel/reduction.ml:369:73
#19 CArray clib/cArray.ml:241:41
(More frames follow)
(ocd)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment