diff options
author | Jed Barber <jjbarber@y7mail.com> | 2012-08-23 00:04:16 +1000 |
---|---|---|
committer | Jed Barber <jjbarber@y7mail.com> | 2012-08-23 00:04:16 +1000 |
commit | d7b861b5d02b5cd0f1f13ab3845a17c30bac7db8 (patch) | |
tree | e70eb377cdc5de48bb194de094a0349980d601e2 | |
parent | ae0f988490cde70c097a8b04b85cb68e67ace0d6 (diff) |
Functions to convert internal datatypes to (unoptimised) proof trace snippets that generate them
-rw-r--r-- | Generator.hs | 82 |
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]) ++ "\""] + |