sample-ghci-script revision dd51c62f9422808985342b78b5161737f05f17c0
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox User-- show all types
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox UserJust (ln,libenv)<-process "../Hets-lib/Basic/Numbers.casl" -- load CASL library
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet Just libNumbers = Map.lookup ln libenv -- get library Numbers
fd2597f75693a2279fdf588bd40dfe2407c42028Tinderbox Userlet Just entryNat = Map.lookup (mkSimpleId "Nat") (globalEnv libNumbers) -- get entry for "Nat" in global environment
14a656f94b1fd0ababd84a772228dfa52276ba15Evan Huntlet SpecEntry gensigNat = entryNat -- Nat is a specification...
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet ExtGenSig _ nodeSigNat = gensigNat -- extract the nodeSig for the body
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet gSignNat = getSig nodeSigNat -- get the Grothendieck signature
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet Just (ExtSign sigNat _) = case gSignNat of G_sign lid x _ -> coerceSign lid CASL "" x
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox User-- coerce the Grothendieck signature to be a CASL signature
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet opsNat = opMap sigNat -- extract the operation symbols
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet Just zeroProfile = Map.lookup (stringToId "0") opsNat -- lookup the type of 0
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox UserzeroProfile -- and print it
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet nodeNat = getNode nodeSigNat -- get development graph node index for Nat
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet dgNodeLabNat = labDG libNumbers nodeNat -- get node label for Nat
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet gtheoryNat = dgn_theory dgNodeLabNat -- get G_theory for Nat
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet Just sensNat = case gtheoryNat of G_theory lid _ _ s _ -> coerceThSens lid CASL "" s
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox User-- extract CASL sentences from theory
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet Just power_Nat = Map.lookup "power_Nat" sensNat -- get formula named power_Nat
fae13836a33b474a6aa2c147df8334f5b1ffae45Tinderbox Userlet power_Nat' = sentence $ ele power_Nat -- get the sentences
fd2597f75693a2279fdf588bd40dfe2407c42028Tinderbox UserputStrLn $ showDoc power_Nat' "" -- and pretty print it (well, with all the profiles...)