45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder-- show all types
ec5ec8dd5bce3df1c42ff4f594dd7b69b9906e5bChristian MaederJust (ln,libenv)<-process "../Hets-lib/Basic/Numbers.casl" -- load CASL library
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet Just libNumbers = Map.lookup ln libenv -- get library Numbers
5df573260a6fcc663d4d59df49617a76eaf21f0dChristian Maederlet Just natIRI = parseIRIReference "Basic/Numbers#Nat"
5df573260a6fcc663d4d59df49617a76eaf21f0dChristian Maederlet Just entryNat = Map.lookup natIRI (globalEnv libNumbers) -- get entry for "Nat" in global environment
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet SpecEntry gensigNat = entryNat -- Nat is a specification...
40623ccebed1ff36996641f957a40dfd6f536073Christian Maederlet ExtGenSig _ nodeSigNat = gensigNat -- extract the nodeSig for the body
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet gSignNat = getSig nodeSigNat -- get the Grothendieck signature
560866529d0162896a3255aaa0f6e24177f0c151Christian Maederlet Just (ExtSign sigNat _) = case gSignNat of G_sign lid x _ -> coerceSign lid CASL "" x
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder-- coerce the Grothendieck signature to be a CASL signature
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet opsNat = opMap sigNat -- extract the operation symbols
93ad6e45774747cbd8e50f4a61cf5234236b7279Christian Maederlet zeroProfile = MapSet.lookup (stringToId "0") opsNat -- lookup the type of 0
45cd3810666369a5a73b05ca43333de38f5ed342Christian MaederzeroProfile -- and print it
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet nodeNat = getNode nodeSigNat -- get development graph node index for Nat
560866529d0162896a3255aaa0f6e24177f0c151Christian Maederlet dgNodeLabNat = labDG libNumbers nodeNat -- get node label for Nat
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet gtheoryNat = dgn_theory dgNodeLabNat -- get G_theory for Nat
112b34d5499e9d0f68abb03434f03bae6e4de06dChristian Maederlet Just sensNat = case gtheoryNat of G_theory lid _ _ _ s _ -> coerceThSens lid CASL "" s
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder-- extract CASL sentences from theory
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet Just power_Nat = Map.lookup "power_Nat" sensNat -- get formula named power_Nat
80d0480a60b409d9cf256d0a6c411dd99c672124Christian Maederlet power_Nat' = sentence $ ele power_Nat -- get the sentences
45cd3810666369a5a73b05ca43333de38f5ed342Christian MaederputStrLn $ showDoc power_Nat' "" -- and pretty print it (well, with all the profiles...)