[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
exception not_a_datatype_exp fun raised

Subject: exception not_a_datatype_exp fun raised
From: Chris Warburton
Date: Tue, 30 Jan 2018 15:23:23 +0000
Resolution: fixed
State: resolved
chris@nixos:~/Programming/Isabelle/IsaPlannerTip$ /nix/store/bkq7g5dab8pq8d4ga6acjhi4s35pkx71-isacosy-runner-choose-100-2
Sending raw equations to stderr
### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)
### Using bulky 64bit version of Poly/ML instead
### No line editor: "rlwrap"
> val it = (): unit
ML> ### load_lib </nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so> : /nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### load_lib </nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so> : /nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
Loading theory "A" (required by "ISACOSY")
### theory "A"
### 114.879s elapsed time, 114.043s cpu time, 16.219s GC time
Loading theory "ISACOSY"
Exception trace - exception not_a_datatype_exp fun raised (line 62 of "~~/contrib/IsaPlanner/src/synthesis/thy_constraint_params.ML")
<top level>
CODETREE().genCode(3)(1)
COMPILER_BODY().baseCompiler(3)executeCode(1)
val functions =
   [(A.global70726f642f70726f705f32382e736d743271726576666c6174,
     "'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
      => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    (A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243,
     "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
    (A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258,
     "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
    (A.global636f6e7374727563746f722d437573746f6d53,
     "Global437573746f6d4e6174 => Global437573746f6d4e6174"),
    (A.global697361706c616e6e65722f70726f705f33372e736d743264656c657465,
     "Global437573746f6d4e6174
      => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    (A.global637573746f6d2d696e63,
     "Global437573746f6d496e74 => Global437573746f6d496e74"),
    (A.global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465,
     "Global437573746f6d496e74
      => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    (A.global697361706c616e6e65722f70726f705f30362e736d74326d696e7573,
     "Global437573746f6d4e6174
      => Global437573746f6d4e6174 => Global437573746f6d4e6174"),
    (A.global70726f642f70726f705f34372e736d7432756e657175616c,
     "Global437573746f6d4e6174
      => Global437573746f6d4e6174 => Global437573746f6d426f6f6c"),
    (A.global746970323031352f736f72745f42536f7274436f756e742e736d7432737469746368,
     "Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
      => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    ...]:
   (string * typ) list
val def_thrms =
   [["global70726f642f70726f705f32382e736d743271726576666c6174
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c
       ?local3.0 =
      ?local3.0",
     "global70726f642f70726f705f32382e736d743271726576666c6174
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local4.0 ?local5.0)
       ?local3.0 =
      global70726f642f70726f705f32382e736d743271726576666c6174 ?local5.0
       (global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432617070656e64
         (global697361706c616e6e65722f70726f705f35322e736d7432726576
           ?local4.0)
         ?local3.0)"],
    ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243 =
      Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243"],
    ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258 =
      Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258"],
    ["global636f6e7374727563746f722d437573746f6d53 ?local1.0 =
      Global437573746f6d53 ?local1.0"],
    ["global697361706c616e6e65722f70726f705f33372e736d743264656c657465
       ?local1.0
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
      Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
     "global697361706c616e6e65722f70726f705f33372e736d743264656c657465
       ?local1.0
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0 ?local4.0) =
      global637573746f6d2d697465
       (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
         ?local1.0 ?local3.0)
       (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
         ?local1.0 ?local4.0)
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0
         (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
           ?local1.0 ?local4.0))"],
    ["global637573746f6d2d696e63
       (Global437573746f6d4e6567 Global437573746f6d5a) =
      Global437573746f6d5a65726f",
     "global637573746f6d2d696e63
       (Global437573746f6d4e6567 (Global437573746f6d53 ?local3.0)) =
      Global437573746f6d4e6567 ?local3.0",
     "global637573746f6d2d696e63 Global437573746f6d5a65726f =
      Global437573746f6d506f73 Global437573746f6d5a",
     "global637573746f6d2d696e63 (Global437573746f6d506f73 ?local22.0) =
      Global437573746f6d506f73 (Global437573746f6d53 ?local22.0)"],
    ["global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
       ?local1.0
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
      Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
     "global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
       ?local1.0
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0 ?local4.0) =
      global637573746f6d2d697465
       (global637573746f6d2d626f6f6c2d636f6e766572746572
         (?local1.0 = ?local3.0))
       ?local4.0
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0
         (global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
           ?local1.0 ?local4.0))"],
    ["global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       Global437573746f6d5a ?local2.0 =
      Global437573746f6d5a",
     "global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       (Global437573746f6d53 ?local4.0) Global437573746f6d5a =
      Global437573746f6d53 ?local4.0",
     "global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       (Global437573746f6d53 ?local4.0) (Global437573746f6d53 ?local3.0) =
      global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       ?local4.0 ?local3.0"],
    ["global70726f642f70726f705f34372e736d7432756e657175616c ?local1.0
       ?local2.0 =
      global637573746f6d2d6e6f74
       (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
         ?local1.0 ?local2.0)"],
    ["global746970323031352f736f72745f42536f7274436f756e742e736d7432737469746368
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c
       ?local2.0 =
      ?local2.0",
     ...],
    ...]:
   thm list list
val fundefs =
   [((A.global70726f642f70726f705f32382e736d743271726576666c6174,
      "'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
       => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     ["global70726f642f70726f705f32382e736d743271726576666c6174
        Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c
        ?local3.0 =
       ?local3.0",
      "global70726f642f70726f705f32382e736d743271726576666c6174
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local4.0 ?local5.0)
        ?local3.0 =
       global70726f642f70726f705f32382e736d743271726576666c6174 ?local5.0
        (global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432617070656e64
          (global697361706c616e6e65722f70726f705f35322e736d7432726576
            ?local4.0)
          ?local3.0)"]),
    ((A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243,
      "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
     ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243 =
       Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243"]),
    ((A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258,
      "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
     ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258 =
       Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258"]),
    ((A.global636f6e7374727563746f722d437573746f6d53,
      "Global437573746f6d4e6174 => Global437573746f6d4e6174"),
     ["global636f6e7374727563746f722d437573746f6d53 ?local1.0 =
       Global437573746f6d53 ?local1.0"]),
    ((A.global697361706c616e6e65722f70726f705f33372e736d743264656c657465,
      "Global437573746f6d4e6174
       => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     ["global697361706c616e6e65722f70726f705f33372e736d743264656c657465
        ?local1.0
        Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
      "global697361706c616e6e65722f70726f705f33372e736d743264656c657465
        ?local1.0
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0 ?local4.0) =
       global637573746f6d2d697465
        (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
          ?local1.0 ?local3.0)
        (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
          ?local1.0 ?local4.0)
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0
          (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
            ?local1.0 ?local4.0))"]),
    ((A.global637573746f6d2d696e63,
      "Global437573746f6d496e74 => Global437573746f6d496e74"),
     ["global637573746f6d2d696e63
        (Global437573746f6d4e6567 Global437573746f6d5a) =
       Global437573746f6d5a65726f",
      "global637573746f6d2d696e63
        (Global437573746f6d4e6567 (Global437573746f6d53 ?local3.0)) =
       Global437573746f6d4e6567 ?local3.0",
      "global637573746f6d2d696e63 Global437573746f6d5a65726f =
       Global437573746f6d506f73 Global437573746f6d5a",
      "global637573746f6d2d696e63 (Global437573746f6d506f73 ?local22.0) =
       Global437573746f6d506f73 (Global437573746f6d53 ?local22.0)"]),
    ((A.global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465,
      "Global437573746f6d496e74
       => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     ["global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
        ?local1.0
        Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
      "global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
        ?local1.0
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0 ?local4.0) =
       global637573746f6d2d697465
        (global637573746f6d2d626f6f6c2d636f6e766572746572
          (?local1.0 = ?local3.0))
        ?local4.0
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0
          (global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
            ?local1.0 ?local4.0))"]),
    ((A.global697361706c616e6e65722f70726f705f30362e736d74326d696e7573,
      "Global437573746f6d4e6174
       => Global437573746f6d4e6174 => Global437573746f6d4e6174"),
     ["global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
        Global437573746f6d5a ?local2.0 =
       Global437573746f6d5a",
      "global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
        (Global437573746f6d53 ?local4.0) Global437573746f6d5a =
       Global437573746f6d53 ?local4.0",
      ...]),
    ((A.global70726f642f70726f705f34372e736d7432756e657175616c,
      "Global437573746f6d4e6174
       => Global437573746f6d4e6174 => Global437573746f6d426f6f6c"),
     ["global70726f642f70726f705f34372e736d7432756e657175616c ?local1.0
        ?local2.0 =
       global637573746f6d2d6e6f74
        (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
          ?local1.0 ?local2.0)"]),
    ((A.global746970323031352f736f72745f42536f7274436f756e742e736d7432737469746368,
      "Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
       => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     [...]),
    ...]:
   ((string * typ) * thm list) list
val constr_trms =
   [Const (A.global64657374727563746f722d746970323031352f73756273745f5375627374467265654e6f2e736d74325661725f30,
           "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
            => Global437573746f6d496e74") $
      (Const (A.Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072.Global746970323031352f73756273745f5375627374467265654e6f2e736d74324c616d,
              "Global437573746f6d496e74
               => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
                  => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072") $
        Var ((free0, 0), "Global437573746f6d496e74") $
        Var ((free1, 0),
             "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072")),
    Const (A.global64657374727563746f722d746970323031352f73756273745f5375627374467265654e6f2e736d74325661725f30,
           "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
            => Global437573746f6d496e74") $
      (Const (A.Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072.Global746970323031352f73756273745f5375627374467265654e6f2e736d7432417070,
              "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
               => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
                  => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072") $
        Var ((free0, 0),
             "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072") $
        Var ((free1, 0),
             "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072")),
    Const (A.global64657374727563746f722d746970323031352f686561705f536f72745065726d75746573272e736d74324e6f64655f32,
           "Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170
            => Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170") $
      Const (A.Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170.Global746970323031352f686561705f536f72745065726d75746573272e736d74324e696c,
             "Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170"),
    Const (A.global64657374727563746f722d746970323031352f736f72745f48536f7274436f756e742e736d74324e6f64655f31,
           "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170
            => ?'a") $
      Const (A.Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170.Global746970323031352f736f72745f48536f7274436f756e742e736d74324e696c,
             "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170"),
    Const (A.global64657374727563746f722d746970323031352f736f72745f48536f7274436f756e742e736d74324e6f64655f30,
           "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170
            => ?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170") $
      Const (A.Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170.Global746970323031352f736f72745f48536f7274436f756e742e736d74324e696c,
             "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170"),
    Const (A.global64657374727563746f722d637573746f6d2d70,
           "Global437573746f6d4e6174 => Global437573746f6d4e6174") $
      Const (A.Global437573746f6d4e6174.Global437573746f6d5a,
             "Global437573746f6d4e6174"),
    Const (A.global64657374727563746f722d746970323031352f696e745f6164645f6173736f632e736d74324e5f30,
           "Global746970323031352f696e745f6164645f6173736f632e736d74325a
            => Global437573746f6d4e6174") $
      (Const (A.Global746970323031352f696e745f6164645f6173736f632e736d74325a.Global746970323031352f696e745f6164645f6173736f632e736d743250,
              "Global437573746f6d4e6174
               => Global746970323031352f696e745f6164645f6173736f632e736d74325a") $
        ...)]:
   Trm.T list
Exception trace - exception not_a_datatype_exp fun raised (line 62 of "~~/contrib/IsaPlanner/src/synthesis/thy_constraint_params.ML")

Library.setmp_thread_data(5)
ML_Context.exec(2)
Toplevel.generic_theory(1)(1)(1)
### theory "ISACOSY"
### 3.404s elapsed time, 3.373s cpu time, 0.769s GC time
*** exception not_a_datatype_exp fun raised (line 62 of "~~/contrib/IsaPlanner/src/synthesis/thy_constraint_params.ML")
***
*** At command "ML" (line 6 of "/nix/store/14p8gxklv9sm7y89m3m3yflvaxwzaw3q-merged/ISACOSY.thy")
Exception- TOPLEVEL_ERROR raised
ML> No 'BEGIN OUTPUT' sentinel found. Dumping whole output:
### No line editor: "rlwrap"
> val it = (): unit
ML> ### load_lib </nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so> : /nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### load_lib </nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so> : /nix/store/xlw2bsclwf840asqzg9bqzggphxzk3s6-polyml-5.5.2/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
Loading theory "A" (required by "ISACOSY")
### theory "A"
### 114.879s elapsed time, 114.043s cpu time, 16.219s GC time
Loading theory "ISACOSY"
Exception trace - exception not_a_datatype_exp fun raised (line 62 of "~~/contrib/IsaPlanner/src/synthesis/thy_constraint_params.ML")
<top level>
CODETREE().genCode(3)(1)
COMPILER_BODY().baseCompiler(3)executeCode(1)
val functions =
   [(A.global70726f642f70726f705f32382e736d743271726576666c6174,
     "'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
      => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    (A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243,
     "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
    (A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258,
     "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
    (A.global636f6e7374727563746f722d437573746f6d53,
     "Global437573746f6d4e6174 => Global437573746f6d4e6174"),
    (A.global697361706c616e6e65722f70726f705f33372e736d743264656c657465,
     "Global437573746f6d4e6174
      => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    (A.global637573746f6d2d696e63,
     "Global437573746f6d496e74 => Global437573746f6d496e74"),
    (A.global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465,
     "Global437573746f6d496e74
      => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    (A.global697361706c616e6e65722f70726f705f30362e736d74326d696e7573,
     "Global437573746f6d4e6174
      => Global437573746f6d4e6174 => Global437573746f6d4e6174"),
    (A.global70726f642f70726f705f34372e736d7432756e657175616c,
     "Global437573746f6d4e6174
      => Global437573746f6d4e6174 => Global437573746f6d426f6f6c"),
    (A.global746970323031352f736f72745f42536f7274436f756e742e736d7432737469746368,
     "Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
      => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
         => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
    ...]:
   (string * typ) list
val def_thrms =
   [["global70726f642f70726f705f32382e736d743271726576666c6174
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c
       ?local3.0 =
      ?local3.0",
     "global70726f642f70726f705f32382e736d743271726576666c6174
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local4.0 ?local5.0)
       ?local3.0 =
      global70726f642f70726f705f32382e736d743271726576666c6174 ?local5.0
       (global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432617070656e64
         (global697361706c616e6e65722f70726f705f35322e736d7432726576
           ?local4.0)
         ?local3.0)"],
    ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243 =
      Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243"],
    ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258 =
      Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258"],
    ["global636f6e7374727563746f722d437573746f6d53 ?local1.0 =
      Global437573746f6d53 ?local1.0"],
    ["global697361706c616e6e65722f70726f705f33372e736d743264656c657465
       ?local1.0
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
      Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
     "global697361706c616e6e65722f70726f705f33372e736d743264656c657465
       ?local1.0
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0 ?local4.0) =
      global637573746f6d2d697465
       (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
         ?local1.0 ?local3.0)
       (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
         ?local1.0 ?local4.0)
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0
         (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
           ?local1.0 ?local4.0))"],
    ["global637573746f6d2d696e63
       (Global437573746f6d4e6567 Global437573746f6d5a) =
      Global437573746f6d5a65726f",
     "global637573746f6d2d696e63
       (Global437573746f6d4e6567 (Global437573746f6d53 ?local3.0)) =
      Global437573746f6d4e6567 ?local3.0",
     "global637573746f6d2d696e63 Global437573746f6d5a65726f =
      Global437573746f6d506f73 Global437573746f6d5a",
     "global637573746f6d2d696e63 (Global437573746f6d506f73 ?local22.0) =
      Global437573746f6d506f73 (Global437573746f6d53 ?local22.0)"],
    ["global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
       ?local1.0
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
      Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
     "global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
       ?local1.0
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0 ?local4.0) =
      global637573746f6d2d697465
       (global637573746f6d2d626f6f6c2d636f6e766572746572
         (?local1.0 = ?local3.0))
       ?local4.0
       (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
         ?local3.0
         (global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
           ?local1.0 ?local4.0))"],
    ["global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       Global437573746f6d5a ?local2.0 =
      Global437573746f6d5a",
     "global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       (Global437573746f6d53 ?local4.0) Global437573746f6d5a =
      Global437573746f6d53 ?local4.0",
     "global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       (Global437573746f6d53 ?local4.0) (Global437573746f6d53 ?local3.0) =
      global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
       ?local4.0 ?local3.0"],
    ["global70726f642f70726f705f34372e736d7432756e657175616c ?local1.0
       ?local2.0 =
      global637573746f6d2d6e6f74
       (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
         ?local1.0 ?local2.0)"],
    ["global746970323031352f736f72745f42536f7274436f756e742e736d7432737469746368
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c
       ?local2.0 =
      ?local2.0",
     ...],
    ...]:
   thm list list
val fundefs =
   [((A.global70726f642f70726f705f32382e736d743271726576666c6174,
      "'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
       => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => 'local1 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     ["global70726f642f70726f705f32382e736d743271726576666c6174
        Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c
        ?local3.0 =
       ?local3.0",
      "global70726f642f70726f705f32382e736d743271726576666c6174
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local4.0 ?local5.0)
        ?local3.0 =
       global70726f642f70726f705f32382e736d743271726576666c6174 ?local5.0
        (global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432617070656e64
          (global697361706c616e6e65722f70726f705f35322e736d7432726576
            ?local4.0)
          ?local3.0)"]),
    ((A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243,
      "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
     ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243 =
       Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743243"]),
    ((A.global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258,
      "Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d7432546f6b"),
     ["global636f6e7374727563746f722d6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258 =
       Global6772616d6d6172732f73696d705f657870725f756e616d626967312e736d743258"]),
    ((A.global636f6e7374727563746f722d437573746f6d53,
      "Global437573746f6d4e6174 => Global437573746f6d4e6174"),
     ["global636f6e7374727563746f722d437573746f6d53 ?local1.0 =
       Global437573746f6d53 ?local1.0"]),
    ((A.global697361706c616e6e65722f70726f705f33372e736d743264656c657465,
      "Global437573746f6d4e6174
       => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => Global437573746f6d4e6174 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     ["global697361706c616e6e65722f70726f705f33372e736d743264656c657465
        ?local1.0
        Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
      "global697361706c616e6e65722f70726f705f33372e736d743264656c657465
        ?local1.0
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0 ?local4.0) =
       global637573746f6d2d697465
        (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
          ?local1.0 ?local3.0)
        (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
          ?local1.0 ?local4.0)
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0
          (global697361706c616e6e65722f70726f705f33372e736d743264656c657465
            ?local1.0 ?local4.0))"]),
    ((A.global637573746f6d2d696e63,
      "Global437573746f6d496e74 => Global437573746f6d496e74"),
     ["global637573746f6d2d696e63
        (Global437573746f6d4e6567 Global437573746f6d5a) =
       Global437573746f6d5a65726f",
      "global637573746f6d2d696e63
        (Global437573746f6d4e6567 (Global437573746f6d53 ?local3.0)) =
       Global437573746f6d4e6567 ?local3.0",
      "global637573746f6d2d696e63 Global437573746f6d5a65726f =
       Global437573746f6d506f73 Global437573746f6d5a",
      "global637573746f6d2d696e63 (Global437573746f6d506f73 ?local22.0) =
       Global437573746f6d506f73 (Global437573746f6d53 ?local22.0)"]),
    ((A.global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465,
      "Global437573746f6d496e74
       => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     ["global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
        ?local1.0
        Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c =
       Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326e696c",
      "global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
        ?local1.0
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0 ?local4.0) =
       global637573746f6d2d697465
        (global637573746f6d2d626f6f6c2d636f6e766572746572
          (?local1.0 = ?local3.0))
        ?local4.0
        (Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d7432636f6e73
          ?local3.0
          (global746970323031352f6c6973745f53656c6563745065726d75746174696f6e732e736d743264656c657465
            ?local1.0 ?local4.0))"]),
    ((A.global697361706c616e6e65722f70726f705f30362e736d74326d696e7573,
      "Global437573746f6d4e6174
       => Global437573746f6d4e6174 => Global437573746f6d4e6174"),
     ["global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
        Global437573746f6d5a ?local2.0 =
       Global437573746f6d5a",
      "global697361706c616e6e65722f70726f705f30362e736d74326d696e7573
        (Global437573746f6d53 ?local4.0) Global437573746f6d5a =
       Global437573746f6d53 ?local4.0",
      ...]),
    ((A.global70726f642f70726f705f34372e736d7432756e657175616c,
      "Global437573746f6d4e6174
       => Global437573746f6d4e6174 => Global437573746f6d426f6f6c"),
     ["global70726f642f70726f705f34372e736d7432756e657175616c ?local1.0
        ?local2.0 =
       global637573746f6d2d6e6f74
        (global697361706c616e6e65722f70726f705f30322e736d7432657175616c
          ?local1.0 ?local2.0)"]),
    ((A.global746970323031352f736f72745f42536f7274436f756e742e736d7432737469746368,
      "Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
       => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374
          => Global437573746f6d496e74 Global6772616d6d6172732f7061636b7261745f756e616d6269675061636b7261742e736d74326c697374"),
     [...]),
    ...]:
   ((string * typ) * thm list) list
val constr_trms =
   [Const (A.global64657374727563746f722d746970323031352f73756273745f5375627374467265654e6f2e736d74325661725f30,
           "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
            => Global437573746f6d496e74") $
      (Const (A.Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072.Global746970323031352f73756273745f5375627374467265654e6f2e736d74324c616d,
              "Global437573746f6d496e74
               => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
                  => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072") $
        Var ((free0, 0), "Global437573746f6d496e74") $
        Var ((free1, 0),
             "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072")),
    Const (A.global64657374727563746f722d746970323031352f73756273745f5375627374467265654e6f2e736d74325661725f30,
           "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
            => Global437573746f6d496e74") $
      (Const (A.Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072.Global746970323031352f73756273745f5375627374467265654e6f2e736d7432417070,
              "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
               => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072
                  => Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072") $
        Var ((free0, 0),
             "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072") $
        Var ((free1, 0),
             "Global746970323031352f73756273745f5375627374467265654e6f2e736d743245787072")),
    Const (A.global64657374727563746f722d746970323031352f686561705f536f72745065726d75746573272e736d74324e6f64655f32,
           "Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170
            => Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170") $
      Const (A.Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170.Global746970323031352f686561705f536f72745065726d75746573272e736d74324e696c,
             "Global746970323031352f686561705f536f72745065726d75746573272e736d743248656170"),
    Const (A.global64657374727563746f722d746970323031352f736f72745f48536f7274436f756e742e736d74324e6f64655f31,
           "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170
            => ?'a") $
      Const (A.Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170.Global746970323031352f736f72745f48536f7274436f756e742e736d74324e696c,
             "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170"),
    Const (A.global64657374727563746f722d746970323031352f736f72745f48536f7274436f756e742e736d74324e6f64655f30,
           "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170
            => ?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170") $
      Const (A.Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170.Global746970323031352f736f72745f48536f7274436f756e742e736d74324e696c,
             "?'a Global746970323031352f736f72745f48536f7274436f756e742e736d743248656170"),
    Const (A.global64657374727563746f722d637573746f6d2d70,
           "Global437573746f6d4e6174 => Global437573746f6d4e6174") $
      Const (A.Global437573746f6d4e6174.Global437573746f6d5a,
             "Global437573746f6d4e6174"),
    Const (A.global64657374727563746f722d746970323031352f696e745f6164645f6173736f632e736d74324e5f30,
           "Global746970323031352f696e745f6164645f6173736f632e736d74325a
            => Global437573746f6d4e6174") $
      (Const (A.Global746970323031352f696e745f6164645f6173736f632e736d74325a.Global746970323031352f696e745f6164645f6173736f632e736d743250,
              "Global437573746f6d4e6174
               => Global746970323031352f696e745f6164645f6173736f632e736d74325a") $
        ...)]:
   Trm.T list
Exception trace - exception not_a_datatype_exp fun raised (line 62 of "~~/contrib/IsaPlanner/src/synthesis/thy_constraint_params.ML")

Library.setmp_thread_data(5)
ML_Context.exec(2)
Toplevel.generic_theory(1)(1)(1)
### theory "ISACOSY"
### 3.404s elapsed time, 3.373s cpu time, 0.769s GC time
*** exception not_a_datatype_exp fun raised (line 62 of "~~/contrib/IsaPlanner/src/synthesis/thy_constraint_params.ML")
***
*** At command "ML" (line 6 of "/nix/store/14p8gxklv9sm7y89m3m3yflvaxwzaw3q-merged/ISACOSY.thy")
Exception- TOPLEVEL_ERROR raised
ML>
End of dump
[]
Follow-Ups:
- Re: exception not_a_datatype_exp fun raised
  - From: Chris Warburton
- Re: exception not_a_datatype_exp fun raised
  - From: Chris Warburton
Prev by Date: Re: "UnequalLengths" error
Next by Date: Re: exception not_a_datatype_exp fun raised
Previous by thread: Re: "UnequalLengths" error
Next by thread: Re: exception not_a_datatype_exp fun raised
Index(es):
- Date
- Thread