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