Module looseEval:condExpr
Builds on looseEval:host
expr ::= ...
| condExpr(expr, expr, expr) /*condExpr(C, T, F): C ? T : F*/
------------------------------------------------------ [Proj-CondExpr]
|{expr}- condExpr(C, T, F) ~~>
or(and(eq(C, true), or(eq(T, num(0)), true)),
eq(F, num(0)))
vars C V1
vars T V2
vars F V3
V1 ++ V2 = V4
V4 ++ V3 = V
------------------------ [V-CondExpr]
vars condExpr(C, T, F) V
typeOf FT ET C boolTy
typeOf FT ET T Ty
typeOf FT ET F Ty
--------------------------------- [T-CondExpr]
typeOf FT ET condExpr(C, T, F) Ty
evalExpr FE EE C trueVal O1
evalExpr FE EE T V O2
O1 ++ O2 = O
------------------------------------ [E-CondExpr-True]
evalExpr FE EE condExpr(C, T, F) V O
evalExpr FE EE C falseVal O1
evalExpr FE EE F V O2
O1 ++ O2 = O
------------------------------------ [E-CondExpr-False]
evalExpr FE EE condExpr(C, T, F) V O
Click on a command or tactic to see a detailed view of its use.
Module looseEval:condExpr. Prove_Constraint looseEval:host:proj_expr_unique. [Show Proof] Prove_Constraint looseEval:host:proj_expr_is. [Show Proof] 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. [Show Proof] 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. [Show Proof] Prove looseEval:host:vars_is. [Show Proof] Prove looseEval:host:vars_exist, looseEval:host:varsArgs_exist, looseEval:host:varsRecFields_exist. [Show Proof] Prove_Constraint looseEval:host:proj_vars. [Show Proof] /******************************************************************** Typing ********************************************************************/ Prove looseEval:host:typeOf_isTy. [Show Proof] 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. [Show Proof] 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. [Show Proof] Prove looseEval:host:evalExpr_isOutput, looseEval:host:evalStmt_isOutput, looseEval:host:evalArgs_isOutput, looseEval:host:evalRecFields_isOutput. [Show Proof] 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. [Show Proof] 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. [Show Proof] 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. [Show Proof] 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. [Show Proof] Theorem append_nil_output : forall O, is_list is_value O -> O ++ [] = O. [Show Proof] Prove_Constraint looseEval:host:proj_evalExpr_exists. [Show Proof] 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. [Show Proof] 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. [Show Proof] 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. [Show Proof] Prove looseEval:host:evalProgram_output_forms. Prove looseEval:host:paramName_exists. Prove looseEval:host:getFunEvalInfo_exists.