ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:l Test.hs

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Common.Id

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Logic.Grothendieck

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Logic.Coerce

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +CASL.Logic_CASL

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +CASL.Sign

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Static.DevGraph

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Data.Graph.Inductive.Graph

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:set +t

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim-- show all types

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon KimJust (ln,libenv)<-process "../Hets-lib/Basic/Numbers.casl" -- load CASL library

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet Just libNumbers = Map.lookup ln libenv -- get library Numbers

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet Just entryNat = Map.lookup (mkSimpleId "Nat") (globalEnv libNumbers) -- get entry for "Nat" in global environment

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet SpecEntry gensigNat = entryNat -- Nat is a specification...

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet (_,_,_,nodeSigNat) = gensigNat -- extract the nodeSig for the body

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet gSignNat = getSig nodeSigNat -- get the Grothendieck signature

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet Just sigNat = case gSignNat of (G_sign lid x _) -> coerceSign lid CASL "" x

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim-- coerce the Grothendieck signature to be a CASL signature

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet opsNat = opMap sigNat -- extract the operation symbols

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet Just zeroProfile = Map.lookup (stringToId "0") opsNat -- lookup the type of 0

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon KimzeroProfile -- and print it

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet nodeNat = getNode nodeSigNat -- get development graph node index for Nat

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet dgNodeLabNat = lab' $ contextDG libNumbers nodeNat -- get node label for Nat

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet gtheoryNat = dgn_theory dgNodeLabNat -- get G_theory for Nat

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet Just sensNat = case gtheoryNat of G_theory lid _ _ s _ -> coerceThSens lid CASL "" s

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim-- extract CASL sentences from theory

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kimlet Just power_Nat = Map.lookup "power_Nat" sensNat -- get formula named power_Nat

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Common.OrderedMap

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Logic.Prover

ac88567a7a5bb7f01cf22cf366bc9d6203e24d7aHyon Kim:m +Common.DocUtils

let power_Nat' = value $ ele power_Nat -- get the sentences

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