Module looseEval:translation Builds on looseEval:host /* We define here a "translation" from the language to itself. This represents an extension translating to another language (e.g. translating to assembly) and lets us explore what we can and cannot prove about a translation, but without the overhead of defining another language. */ Judgment transE : expr* expr Judgment transRF : recFieldExprs* recFieldExprs Judgment transA : args* args /*the [string] argument here needs to be passed down for translation in the default rule*/ Judgment transS : [string] stmt* stmt [string] /*updates known names*/ Judgment transF : fun* fun Fixed Judgment transFuns : [fun] [fun] Judgment transP : program* program -------------------- [TE-Num] transE num(I) num(I) transE E1 E11 transE E2 E21 ---------------------------------- [TE-Plus] transE plus(E1, E2) plus(E11, E21) transE E1 E11 transE E2 E21 ------------------------------------ [TE-Minus] transE minus(E1, E2) minus(E11, E21) transE E1 E11 transE E2 E21 ---------------------------------- [TE-Mult] transE mult(E1, E2) mult(E11, E21) transE E1 E11 transE E2 E21 -------------------------------- [TE-Div] transE div(E1, E2) div(E11, E21) ---------------- [TE-True] transE true true ------------------ [TE-False] transE false false transE E1 E11 transE E2 E21 -------------------------------- [TE-And] transE and(E1, E2) and(E11, E21) transE E1 E11 transE E2 E21 ------------------------------ [TE-Or] transE or(E1, E2) or(E11, E21) transE E E1 --------------------- [TE-Not] transE not(E) not(E1) transE E1 E11 transE E2 E21 ----------------------------------- [TE-Greater] transE greater(E1, E2) eq(E11, E21) transE E1 E11 transE E2 E21 ------------------------------ [TE-Eq] transE eq(E1, E2) eq(E11, E21) -------------------------------- [TE-String] transE stringLit(S) stringLit(S) transE E1 E11 transE E2 E21 -------------------------------------------- [TE-StringApp] transE appString(E1, E2) appString(E11, E21) ---------------------- [TE-Name] transE name(X) name(X) transA A A1 ----------------------------- [TE-Call] transE call(F, A) call(F, A1) transRF RF RF1 --------------------------------- [TE-RecBuild] transE recBuild(RF) recBuild(RF1) transE E E1 --------------------------------- [TE-RecFieldAccess] {transE recFieldAccess(E, F) recFieldAccess(E1, F)} transE E E1 ----------------------------------------- [TE-ErrorExpr] transE errorExpr(E, Ty) errorExpr(E1, Ty) |{expr}- E ~~> E_T transE E_T E1 ------------------ [TE-Default]* transE E E1 ----------------------------------------- [TRF-Nil] transRF nilRecFieldExprs nilRecFieldExprs transE E E1 transRF RF RF1 --------------------------------------- [TRF-Cons] {transRF consRecFieldExprs(F, E, RF) consRecFieldExprs(F, E1, RF1)} |{recFieldExprs}- RF ~~> RF_T transRF RF_T RF1 ----------------------------- [TRF-Default]* transRF RF RF1 ---------------------- [TA-Nil] transA nilArgs nilArgs transE E E1 transA A A1 -------------------------------------- [TA-Cons] transA consArgs(E, A) consArgs(E1, A1) |{args}- A ~~> A_T transA A_T A1 ------------------ [TRA-Default]* transA A A1 ---------------------------- [TS-Noop] transS Names noop noop Names transS Names S1 S11 Names1 transS Names1 S2 S21 Names2 --------------------------------------------- [TS-Seq] transS Names seq(S1, S2) seq(S11, S21) Names2 transE E E1 ---------------------------------------------------------- [TS-Declare] transS Names declare(Ty, X, E) declare(Ty, X, E1) X::Names transE E E1 --------------------------------------------- [TS-Assign] transS Names assign(X, E) assign(X, E1) Names transE E E1 ---------------------------------------------- [TS-RecUpdate] {transS Names recUpdate(Rec, Fs, E) recUpdate(Rec, Fs, E1) Names} transE Cond Cond1 transS Names Th Th1 NamesTh transS Names El El1 NamesEl ------------------------------------------------ [TS-If] {transS Names ifThenElse(Cond, Th, El) ifThenElse(Cond1, Th1, El1) Names} transE Cond Cond1 transS Names Body Body1 Names1 -------------------------------------------------------- [TS-While] transS Names while(Cond, Body) while(Cond1, Body1) Names transS Names S S1 Names1 --------------------------------------------- [TS-ScopeStmt] transS Names scopeStmt(S) scopeStmt(S1) Names transE E E1 -------------------------------------------- [TS-Print] transS Names printVal(E) printVal(E1) Names1 Names |{stmt}- S ~~> S_T transS Names S_T S1 Names1 -------------------------- [TS-Default]* transS Names S S1 Names1 paramTys Params PTys domain PTys Names transS RetVar::Names Body Body1 Names1 --------------------------------------------------------- [TF-Fun] {transF fun(F, RetTy, RetVar, InitVal, Params, Body) fun(F, RetTy, RetVar, InitVal, Params, Body1)} |{fun}- F ~~> F_T transF F_T F1 ----------------- [TF-Default]* transF F F1 =============== [TFs-Nil] transFuns [] [] transF F F1 transFuns Rest Rest1 =========================== [TFs-Cons] transFuns F::Rest F1::Rest1 transFuns Funs Funs1 ------------------------------------------------ [TP-Program] transP program(Funs, Main) program(Funs1, Main1) |{program}- P ~~> P_T transP P_T P1 --------------------- [TP-Default]* transP P P1
Click on a command or tactic to see a detailed view of its use.
Module looseEval:translation. Prove_Constraint looseEval:host:proj_expr_unique. Prove_Constraint looseEval:host:proj_expr_is. Prove_Constraint looseEval:host:proj_stmt_unique. Prove_Constraint looseEval:host:proj_stmt_is. Prove_Constraint looseEval:host:proj_stmt_other. Prove_Constraint looseEval:host:proj_fun_unique. Prove_Constraint looseEval:host:proj_fun_is. Prove_Constraint looseEval:host:proj_param_unique. Prove_Constraint looseEval:host:proj_param_is. Prove_Constraint looseEval:host:proj_program_unique. Prove_Constraint looseEval:host:proj_program_is. Prove_Constraint looseEval:host:proj_typ_unique. Prove_Constraint looseEval:host:proj_typ_is. Prove_Constraint looseEval:host:proj_value_unique. Prove_Constraint looseEval:host:proj_value_is. /******************************************************************** Decidable Equality ********************************************************************/ Add_Proj_Rel looseEval:host:is_expr, looseEval:host:is_args, looseEval:host:is_recFieldExprs. Prove_Ext_Ind looseEval:host:is_expr, looseEval:host:is_args, looseEval:host:is_recFieldExprs. Add_Proj_Rel looseEval:host:is_stmt. Prove_Ext_Ind looseEval:host:is_stmt. Prove looseEval:host:is_args_nilArgs_or_consArgs. Prove looseEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. Add_Proj_Rel looseEval:host:is_value, looseEval:host:is_recFieldVals. Prove_Ext_Ind looseEval:host:is_value, looseEval:host:is_recFieldVals. Prove looseEval:host:is_value_intVal_or_not. Prove looseEval:host:is_value_trueVal_or_not. Prove looseEval:host:is_value_falseVal_or_not. Prove looseEval:host:is_value_stringVal_or_not. Prove looseEval:host:is_value_recVal_or_not. Prove looseEval:host:is_recFieldVals_nil_or_cons. Prove looseEval:host:is_value_eq_or_not, looseEval:host:is_recFieldVals_eq_or_not. /******************************************************************** Variables ********************************************************************/ Prove looseEval:host:vars_unique. Prove looseEval:host:vars_is. Prove looseEval:host:vars_exist, looseEval:host:varsArgs_exist, looseEval:host:varsRecFields_exist. Prove_Constraint looseEval:host:proj_vars. /******************************************************************** Typing ********************************************************************/ Prove looseEval:host:typeOf_isTy. Prove looseEval:host:stmtOK_isCtx. Prove looseEval:host:stmtOK_keep_scopes. Prove looseEval:host:stmtOK_older_scopes_same. Prove looseEval:host:stmtOK_first_scope_lookup_same. Prove looseEval:host:typeOf_unique. Prove looseEval:host:stmtOK_unique. Prove looseEval:host:paramTy_is. Prove looseEval:host:getFunInfo_is. Prove looseEval:host:paramTy_exists. Prove looseEval:host:getFunInfo_exists. /******************************************************************** Evaluation ********************************************************************/ Prove looseEval:host:evalExpr_isValue, looseEval:host:evalStmt_isCtx, looseEval:host:evalArgs_isValue, looseEval:host:evalRecFields_isValue. Prove looseEval:host:evalExpr_isOutput, looseEval:host:evalStmt_isOutput, looseEval:host:evalArgs_isOutput, looseEval:host:evalRecFields_isOutput. Prove looseEval:host:paramName_is. Prove looseEval:host:getFunEvalInfo_is. Prove looseEval:host:evalProgram_isOutput. Prove looseEval:host:evalStmt_names_same. Add_Ext_Size looseEval:host:evalExpr, looseEval:host:evalArgs, looseEval:host:evalRecFields, looseEval:host:evalStmt. Add_Proj_Rel looseEval:host:evalExpr, looseEval:host:evalArgs, looseEval:host:evalRecFields, looseEval:host:evalStmt. Prove looseEval:host:evalExpr_rel, looseEval:host:evalStmt_newNameScopes_output, looseEval:host:evalStmt_newNameScopes, looseEval:host:evalArgs_rel, looseEval:host:evalRecFields_rel. Prove looseEval:host:evalExpr_rel_exists_ES, looseEval:host:evalStmt_newNameScopes_exists_ES, looseEval:host:evalArgs_rel_exists_ES, looseEval:host:evalRecFields_rel_exists_ES. Prove looseEval:host:evalExpr_scopes_same, looseEval:host:evalStmt_scopes_same, looseEval:host:evalStmt_scopes_same_ctx, looseEval:host:evalArgs_scopes_same, looseEval:host:evalRecFields_scopes_same. Prove looseEval:host:evalExpr_scopes_same_exists, looseEval:host:evalStmt_scopes_same_exists, looseEval:host:evalArgs_scopes_same_exists, looseEval:host:evalRecFields_scopes_same_exists. Prove_Constraint looseEval:host:proj_evalExpr_exists. Prove_Constraint looseEval:host:proj_evalStmt_exists. Prove_Constraint looseEval:host:proj_evalStmt_rel. Prove_Ext_Ind looseEval:host:evalExpr, looseEval:host:evalArgs, looseEval:host:evalRecFields, looseEval:host:evalStmt. Prove looseEval:host:paramName_unique. Prove_Constraint looseEval:host:proj_paramName_forward. Prove_Constraint looseEval:host:proj_paramName_back. Prove looseEval:host:getFunEvalInfo_unique. Prove_Constraint looseEval:host:proj_getFunEvalInfo_forward. Prove_Constraint looseEval:host:proj_getFunEvalInfo_back. Prove looseEval:host:evalProgram_unique. Prove_Constraint looseEval:host:proj_evalProgram. Prove_Constraint looseEval:host:proj_evalProgram_back. Prove looseEval:host:evalExpr_typePres, looseEval:host:evalStmt_typePres, looseEval:host:evalArgs_typePres, looseEval:host:evalRecFields_typePres. Prove looseEval:host:paramTy_paramName_same. Prove looseEval:host:funOK_getFunEvalInfo_related. Prove looseEval:host:evalExpr_output_forms, looseEval:host:evalStmt_output_forms, looseEval:host:evalArgs_output_forms, looseEval:host:evalRecFields_output_forms. Prove looseEval:host:evalProgram_output_forms. Prove looseEval:host:paramName_exists. Prove looseEval:host:getFunEvalInfo_exists. /* We can't prove anything here about evaluation of the original and the translation being related, or about the translation evaluating if the original evaluates or vice versa. Our projection constraints are not constraining enough on evaluation to allow us to prove much about it, since the values for an original and its projection do not have to be related. The fact that statement and evaluation projections are required to have the same output seems like it might let us prove something like the output of the translation is related to the output of the original when both evaluate. However, projection constraints hold only for the initial projection, not also projecting sub-terms, as the translation may do. Since this can change the values in evaluation, we cannot guarantee the same branches are taken in evaluation, or even that the same output is given from any particular print statement. In this language, with these projection constraints, this extension and its translation are nothing more than aspirations. It seems like something nice to do, translating it to another language for implementation, but it doesn't mean anything. Any implementation translation in a language with constraints like this needs to be part of the host language so each extension can write its own portion. It cannot be left to an extension. */