Safe Haskell	Safe-Inferred
Language	Haskell2010

Funcons.MetaProgramming

Description

This module implements HGMPification of funcons based on Berger et al. (2017) (First-order.)

Synopsis

ctRel :: Funcons -> MSOS Funcons
ulRel :: Funcons -> MSOS Funcons
dlRel :: Values -> Rewrite Funcons
evalRel :: Funcons -> MSOS Values
compile :: FunconLibrary -> TypeRelation -> Funcons -> Funcons -> Funcons
env_entity :: Name
store_entity :: Name
atom_gen_entity :: Name
translationStep :: ([Funcons] -> Funcons) -> StrictFuncon
cmp_MSOSReader :: forall {m :: Type -> TYPE LiftedRep}. Interactive m => FunconLibrary -> TypeRelation -> Funcons -> MSOSReader m
cmp_MSOSState :: forall {m :: Type -> Type}. MSOSState m
library :: FunconLibrary
meta_up_ :: [Funcons] -> Funcons
meta_down_ :: [Funcons] -> Funcons
meta_let_ :: [Funcons] -> Funcons
eval_ :: [Funcons] -> Funcons
code_ :: [Funcons] -> Funcons
step_meta_eval :: [Values] -> Rewrite Rewritten
step_code :: [Funcons] -> Rewrite Rewritten
ast_term :: [Funcons] -> Funcons
ast_value :: [Funcons] -> Funcons
type_of_ :: [Funcons] -> Funcons
step_ty_of :: [Values] -> Rewrite Rewritten

Documentation

ctRel :: Funcons -> MSOS Funcons Source #

This function implements the ==CT=> relation. Compiling programs to executable funcons terms, removing occurrences of `meta-up`, `meta-down` and `meta-let` and `meta-bound`.

ulRel :: Funcons -> MSOS Funcons Source #

This function implements the ==UL=> relation. Translating a funcon into its meta-representation

dlRel :: Values -> Rewrite Funcons Source #

This function implements the ==DL=> relation. Translating a meta-representation of a program into the actual program

evalRel :: Funcons -> MSOS Values Source #

compile :: FunconLibrary -> TypeRelation -> Funcons -> Funcons -> Funcons Source #

env_entity :: Name Source #

store_entity :: Name Source #

atom_gen_entity :: Name Source #

translationStep :: ([Funcons] -> Funcons) -> StrictFuncon Source #

cmp_MSOSReader :: forall {m :: Type -> TYPE LiftedRep}. Interactive m => FunconLibrary -> TypeRelation -> Funcons -> MSOSReader m Source #

cmp_MSOSState :: forall {m :: Type -> Type}. MSOSState m Source #

library :: FunconLibrary Source #

meta_up_ :: [Funcons] -> Funcons Source #

meta_down_ :: [Funcons] -> Funcons Source #

meta_let_ :: [Funcons] -> Funcons Source #

eval_ :: [Funcons] -> Funcons Source #

code_ :: [Funcons] -> Funcons Source #

step_meta_eval :: [Values] -> Rewrite Rewritten Source #

step_code :: [Funcons] -> Rewrite Rewritten Source #

ast_term :: [Funcons] -> Funcons Source #

ast_value :: [Funcons] -> Funcons Source #

type_of_ :: [Funcons] -> Funcons Source #

step_ty_of :: [Values] -> Rewrite Rewritten Source #