sample-ghci-script revision 560866529d0162896a3255aaa0f6e24177f0c151
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
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet Just entryNat = Map.lookup (mkSimpleId "Nat") (globalEnv libNumbers) -- get entry for "Nat" in global environment
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet SpecEntry gensigNat = entryNat -- Nat is a specification...
3cb9e8caabecd4d058b622c889e3b020c1ac099cChristian 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
45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet Just zeroProfile = Map.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
45cd3810666369a5a73b05ca43333de38f5ed342Christian 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...)