Module looseEval:assert
Builds on looseEval:host
stmt ::= ...
| assert(expr, expr)
-------------------------------------------- [Proj-Assert]
Names |{stmt}- assert(E, Msg) ~~>
ifThenElse(E, noop,
/*printVal(error) never succeeds*/
printVal(errorExpr(Msg, intTy)))
typeOf FC TC E boolTy
typeOf FC TC Msg stringTy
------------------------------ [T-Assert]
stmtOK FC TC assert(E, Msg) TC
evalExpr FE EE E trueVal O
---------------------------------- [E-Assert]
evalStmt FE EE assert(E, Msg) EE O
Click on a command or tactic to see a detailed view of its use.
Module looseEval:assert. Prove_Constraint looseEval:host:proj_expr_unique. Prove_Constraint looseEval:host:proj_expr_is. Prove_Constraint looseEval:host:proj_stmt_unique. [Show Proof] Prove_Constraint looseEval:host:proj_stmt_is. [Show Proof] Prove_Constraint looseEval:host:proj_stmt_other. [Show Proof] 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. [Show Proof] 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. [Show Proof] Prove looseEval:host:stmtOK_keep_scopes. [Show Proof] Prove looseEval:host:stmtOK_older_scopes_same. [Show Proof] Prove looseEval:host:stmtOK_first_scope_lookup_same. [Show Proof] Prove looseEval:host:typeOf_unique. Prove looseEval:host:stmtOK_unique. [Show Proof] 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. [Show Proof] 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] Prove_Constraint looseEval:host:proj_evalExpr_exists. Theorem append_nil_output : forall O, is_list is_value O -> O ++ [] = O. [Show Proof] Prove_Constraint looseEval:host:proj_evalStmt_exists. [Show Proof] Prove_Constraint looseEval:host:proj_evalStmt_rel. [Show Proof] 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.