45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:l Test.hs

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Common.Id

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Logic.Grothendieck

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Logic.Coerce

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +CASL.Logic_CASL

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +CASL.Sign

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Static.DevGraph

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Data.Graph.Inductive.Graph

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:set +t

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...

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet (_,_,_,nodeSigNat) = gensigNat -- extract the nodeSig for the body

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet gSignNat = getSig nodeSigNat -- get the Grothendieck signature

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet Just 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 Maeder

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet nodeNat = getNode nodeSigNat -- get development graph node index for Nat

6320552e8c3e1ada4389afbc22055a55472bbfdaChristian Maederlet dgNodeLabNat = lab' $ contextDG (devGraph 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

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Common.OrderedMap

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Logic.Prover

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maeder:m +Common.DocUtils

45cd3810666369a5a73b05ca43333de38f5ed342Christian Maederlet power_Nat' = value $ ele power_Nat -- get the sentences

45cd3810666369a5a73b05ca43333de38f5ed342Christian MaederputStrLn $ showDoc power_Nat' "" -- and pretty print it (well, with all the profiles...)