Closed LorenNuyts closed 4 years ago
The boundVarFunctions in String.hs does not always generate the correct recursive function. For example
namespace TermVar: Term sort Term inh ctx TermVar | Var (x@ctx) | Lam (t: Term) [x: TermVar] t.ctx = lhs.ctx, x | App (t1: Term) (t2: Term) | Prod (t1: Term) (t2: Term) | Let (p: Pat) (t1: Term) (t2: Term) p.ictx = lhs.ctx t2.ctx = p.sctx sort Pat inh ictx TermVar syn sctx TermVar | PVar [x: TermVar] lhs.sctx = lhs.ictx, x | PProd (p1: Pat) (p2: Pat) p1.ictx = lhs.ictx p2.ictx = p1.sctx lhs.sctx = p2.sctx
generates the following boundVar functions:
boundVariablesTerm c (Var var) = [] boundVariablesTerm c (Lam b t) = (nub (concat [c,[b],[]])) boundVariablesTerm c (App t1 t2) = (nub (concat [c,[]])) boundVariablesTerm c (Prod t1 t2) = (nub (concat [c,[]])) boundVariablesTerm c (Let p t1 t2) = (nub (concat [c,[]])) boundVariablesPat c (PVar b) = (nub (concat [c,[b],[]])) boundVariablesPat c (PProd p1 p2) = (nub (concat [c,(boundVariablesPat (boundVariablesPat [] p1) p2)]))
boundVariablesTerm is not recursive while boundVariablesPat is, which results in different behaviour.
The boundVarFunctions in String.hs does not always generate the correct recursive function. For example
generates the following boundVar functions:
boundVariablesTerm is not recursive while boundVariablesPat is, which results in different behaviour.