[ CONSLI : list_inst, inst -> list_inst ] [ NULL : list_inst ] [ RETURN : exp, exp -> inst ] [ BRANCH : cond, list_inst, list_inst -> inst ] [ AFFECT : exp, exp -> inst ] [ HILE : nat, cond, list_inst -> inst ] [ CONSE : elt_env, env -> env ] [ EMPTY : env ] [ GE : list_inst, env -> env ] [ COMP : inst, env -> env ] [ RT : elt_env, env -> env ] [ CHOICE : env, env -> env ] [ AF : cond, env -> env ] [ HILE2 : nat, cond, env, list_var, env -> env] [ FOL : nat, list_var, list_exp -> env ] [ GIE : env -> env ] [ MERGE : env, env -> env] [ MP : elt_env, env -> env ] [ PAIR : exp, exp -> elt_env ] [ AW : nat, cond, env, list_var -> elt_env ] [ CONSLV : exp, list_var -> list_var ] [ ENDV : list_var ] [ CONSLEX : exp, list_exp -> list_exp ] [ ENDEX : list_exp ] [ GLOV : env -> list_var ] [ GLOV2 : env -> list_var ] [ LEX : env -> list_exp ] [ PE : exp -> exp ] [ LOOP : nat, exp, list_exp -> exp ] [ MAJ : cond, env -> cond ] [ ET : cond, cond -> cond ] [ NON : cond -> cond ] [ OU : cond, cond -> cond ] [ * : exp, exp -> exp ] [ / : exp, exp -> exp ] [ + : exp, exp -> exp ] [ - : exp, exp -> exp ] [ === : exp, exp -> cond ] [ != : exp, exp -> cond ] [ >= : exp, exp -> cond ] [ <= : exp, exp -> cond ] [ > : exp, exp -> cond ] [ < : exp, exp -> cond ] [ ! : cond -> cond ] [ 0 : exp ] [ S : exp -> exp ] [ CONS : exp, exp -> exp ] [ NUL : exp ] [ --> : exp,exp -> exp] [FUNCNAME : exp ] GE(CONSLI(uS, uS1), uE) := COMP(uS1, GE(uS, uE)) GE(NULL, uE) := uE COMP(AFFECT(ua, ue), EMPTY) := CONSE(PAIR(ua, ue), EMPTY) COMP(AFFECT(ua, ue), CONSE(up, uenv)) := RT(PAIR(ua, ue), CONSE(up, uenv)) COMP(RETURN(uFunc, ue), CONSE(up, uenv)) := RT(PAIR(uFunc, ue), CONSE(up, uenv)) COMP(RETURN(uFunc, ue), EMPTY) := CONSE(PAIR(uFunc, ue), EMPTY) COMP(BRANCH(uc, uS1, uS2), EMPTY) := CHOICE(AF(uc, GE(uS1, EMPTY)), AF(NON(uc), GE(uS2, EMPTY))) COMP(BRANCH(uc, uS1, uS2), CONSE(up, uenv)) := CHOICE(AF(MAJ(uc, CONSE(up, uenv)), GE(uS1, CONSE(up, uenv))), AF(NON(MAJ(uc, CONSE(up, uenv))), GE(uS2, CONSE(up, uenv)))) MAJ(uc, CONSE(PAIR(uv, uexp), uenv)) := MAJ(SUBST(uv, uc, uexp), uenv) MAJ(uc, EMPTY):= uc MAJ(uc, CONSE(AW(uw, ux, uy, uz), uenv)) := MAJ(uc, uenv) COMP(uI, CHOICE(uE1, uE2)) := CHOICE(COMP(uI, uE1), COMP(uI, uE2)) COMP(uI, AF(uc, uE)) := AF(uc, COMP(uI, uE)) RT(PAIR(ua, ue1), CONSE(PAIR(ua, ue2), uE)) := RT(PAIR(ua, SUBST(ua, ue1, ue2)), uE) RT(PAIR(ua, ue1), CONSE(PAIR(ub, ue2), uE)) := CONSE(PAIR(ub ,ue2), RT(PAIR(ua, SUBST(ub, ue1, ue2)), uE)) if not eq(ua, ub) RT(PAIR(ua, ue), EMPTY) := CONSE(PAIR(ua, ue), EMPTY) RT(PAIR(ua, ue1), CONSE(AW(uW, uX, uY, uZ), uE)) := CONSE(AW(uW, uX, uY, uZ), RT(PAIR(ua, ue1), uE)) AF(uc, CHOICE(uA, uB)) := CHOICE(AF(uc, uA), AF(uc, uB)) AF(uc1, AF(uc2, uE)) := AF(ET(uc1, uc2), uE) COMP(HILE(uNUM, uC, uS), CONSE(uP, uLP)) := CONSE(AW(uNUM, uC, GE(uS, GIE(CONSE(uP, uLP))), GLOV(CONSE(uP, uLP))), MERGE(FOL(uNUM, GLOV2(GE(uS, GIE(CONSE(uP, uLP)))), LEX(CONSE(uP, uLP))), CONSE(uP, uLP))) GIE(EMPTY) := EMPTY GIE(CONSE(PAIR(uV, uEXP), uL)) := CONSE(PAIR(uV, PE(uV)), GIE(uL)) GIE(CONSE(AW(uW, uX, uY, uZ), uL)) := GIE(uL) GLOV(EMPTY) := ENDV GLOV(CONSE(PAIR(uV, uEXP), uL)) := CONSLV(uV, GLOV(uL)) GLOV(CONSE(AW(uW, uX, uY, uZ), uL)) := GLOV(uL) GLOV2(EMPTY) := ENDV GLOV2(CONSE(PAIR(uV, PE(uV)), uL)) := GLOV2(uL) GLOV2(CONSE(PAIR(uV, uEXP), uL)) := CONSLV(uV, GLOV2(uL)) if not eq(PE(uV), uEXP) GLOV2(CONSE(AW(uW, uX, uY, uZ), uL)) := GLOV2(uL) GLOV2(CHOICE(AF(uC1, uE1), AF(uC2, uE2))) := MERGE2(GLOV2(uE1), GLOV2(uE2)) MERGE2(CONSLV(uT, uQ), uENV) := MV(uT, MERGE2(uQ, uENV)) MERGE2(ENDV, uENV) := uENV MV(uV, CONSLV(uV, uLV)) := CONSLV(uV, uLV) MV(uV1, CONSLV(uV2, uLV)) := CONSLV(uV2, MV(uV1, uLV)) if not eq(uV1, uV2) MV(uV, ENDV) := CONSLV(uV, ENDV) LEX(EMPTY) := ENDEX LEX(CONSE(PAIR(uV, uExp), uL)) := CONSLEX(uExp, LEX(uL)) LEX(CONSE(AW(uW, uX, uY, uZ), uL)) := LEX(uL) FOL(uNUM, CONSLV(uV, uL), CONSLEX(uEXP, uLEXP)) := CONSE(PAIR(uV, LOOP(uNUM, uV, CONSLEX(uEXP, uLEXP))), FOL(uNUM, uL, CONSLEX(uEXP, uLEXP))) FOL(uNUM, ENDV, CONSLEX(uEXP, uLEXP)) := EMPTY MERGE(CONSE(uT, uQ), uENV) := MP(uT, MERGE(uQ, uENV)) MERGE(EMPTY, uENV) := uENV MP(PAIR(uV, uEX), CONSE(AW(uW, uX, uY, uZ), uENV)) := CONSE(AW(uW, uX, uY, uZ), MP(PAIR(uV, uEX), uENV)) MP(PAIR(uX, uEX), CONSE(PAIR(uX, uEY), uENV)) := CONSE(PAIR(uX, uEX), uENV) MP(PAIR(uX, uEX), CONSE(PAIR(uY, uEY), uENV)) := CONSE(PAIR(uY, uEY), MP(PAIR(uX, uEX), uENV)) if not eq(uX, uY) MP(PAIR(uX, uEX), EMPTY) := CONSE(PAIR(uX, uEX), EMPTY)