summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2012-08-23 00:04:16 +1000
committerJed Barber <jjbarber@y7mail.com>2012-08-23 00:04:16 +1000
commitd7b861b5d02b5cd0f1f13ab3845a17c30bac7db8 (patch)
treee70eb377cdc5de48bb194de094a0349980d601e2
parentae0f988490cde70c097a8b04b85cb68e67ace0d6 (diff)
Functions to convert internal datatypes to (unoptimised) proof trace snippets that generate them
-rw-r--r--Generator.hs82
1 files changed, 82 insertions, 0 deletions
diff --git a/Generator.hs b/Generator.hs
new file mode 100644
index 0000000..7377ec1
--- /dev/null
+++ b/Generator.hs
@@ -0,0 +1,82 @@
+module Generator (
+ listGen,
+ substitutionGen,
+ termGen,
+ varGen,
+ typeGen,
+ typeOpGen,
+ constGen,
+ nameGen
+ ) where
+
+
+import Data.List
+import Term
+import TypeVar
+
+
+
+listGen :: (a -> [String]) -> [a] -> [String]
+listGen f list =
+ concat (map f list) ++ ["nil"] ++ replicate (length list) "cons"
+
+
+
+substitutionGen :: Substitution -> [String]
+substitutionGen sub =
+ let varTermList = listGen varTermPair (snd sub)
+ nameTypeList = listGen nameTypePair (fst sub)
+ in nameTypeList ++ varTermList ++ ["nil", "cons", "cons"]
+
+
+
+varTermPair :: (Var, Term) -> [String]
+varTermPair (var, term) =
+ (varGen var) ++ (termGen term) ++ ["nil", "cons", "cons"]
+
+
+
+nameTypePair :: (Name, Type) -> [String]
+nameTypePair (name, ty) =
+ (nameGen name) ++ (typeGen ty) ++ ["nil", "cons", "cons"]
+
+
+
+termGen :: Term -> [String]
+termGen (TVar v) = (varGen v) ++ ["varTerm"]
+termGen (TConst c ty) = (constGen c) ++ (typeGen ty) ++ ["constTerm"]
+termGen (TApp h x) = (termGen h) ++ (termGen x) ++ ["appTerm"]
+termGen (TAbs x t) = (termGen x) ++ (termGen t) ++ ["absTerm"]
+
+
+
+varGen :: Var -> [String]
+varGen var =
+ (nameGen . varName $ var) ++ (typeGen . varTy $ var) ++ ["var"]
+
+
+
+typeGen :: Type -> [String]
+typeGen (TypeVar v) = (nameGen v) ++ ["varType"]
+typeGen (AType ty op) =
+ let list = listGen typeGen ty
+ in (typeOpGen op) ++ list ++ ["opType"]
+
+
+
+typeOpGen :: TypeOp -> [String]
+typeOpGen op =
+ (nameGen . tyOp $ op) ++ ["typeOp"]
+
+
+
+constGen :: Const -> [String]
+constGen c =
+ (nameGen . constName $ c) ++ ["const"]
+
+
+
+nameGen :: Name -> [String]
+nameGen name =
+ ["\"" ++ intercalate "." (nameSpace name ++ [nameId name]) ++ "\""]
+