Module matchEval:wrapper
Builds on matchEval:host
/*
This extension seems somewhat useless, but it stands in for any
extension that might want to mark certain values as being special in
some way.
*/
value ::= ... | wrapVal(value)
-------------------------- [Proj-WrapVal]
|{value}- wrapVal(V) ~~> V
expr ::= ... | wrap(expr)
---------------------- [Proj-Wrap]
|{expr}- wrap(E) ~~> E
vars E V
-------------- [V-Wrap]
vars wrap(E) V
typeOf FC TC E Ty
----------------------- [T-Wrap]
typeOf FC TC wrap(E) Ty
valueType V Ty
----------------------- [VT-WrapVal]
valueType wrapVal(V) Ty
evalExpr FE EE E V O
----------------------------------- [E-Wrap]
evalExpr FE EE wrap(E) wrapVal(V) O
matchInt V I
--------------------- [MI-Wrap]
matchInt wrapVal(V) I
matchTrue V
-------------------- [MT-Wrap]
matchTrue wrapVal(V)
matchFalse V
--------------------- [MF-Wrap]
matchFalse wrapVal(V)
matchString V S
------------------------ [MS-Wrap]
matchString wrapVal(V) S
matchRec V Fs
---------------------- [MR-Wrap]
matchRec wrapVal(V) Fs
Click on a command or tactic to see a detailed view of its use.
Module matchEval:wrapper. Prove_Constraint matchEval:host:proj_expr_unique. [Show Proof] Prove_Constraint matchEval:host:proj_expr_is. [Show Proof] Prove_Constraint matchEval:host:proj_stmt_unique. Prove_Constraint matchEval:host:proj_stmt_is. Prove_Constraint matchEval:host:proj_stmt_other. Prove_Constraint matchEval:host:proj_fun_unique. Prove_Constraint matchEval:host:proj_fun_is. Prove_Constraint matchEval:host:proj_param_unique. Prove_Constraint matchEval:host:proj_param_is. Prove_Constraint matchEval:host:proj_program_unique. Prove_Constraint matchEval:host:proj_program_is. Prove_Constraint matchEval:host:proj_typ_unique. Prove_Constraint matchEval:host:proj_typ_is. Prove_Constraint matchEval:host:proj_value_unique. [Show Proof] Prove_Constraint matchEval:host:proj_value_is. [Show Proof] Add_Proj_Rel matchEval:host:is_expr, matchEval:host:is_args, matchEval:host:is_recFieldExprs. Prove_Ext_Ind matchEval:host:is_expr, matchEval:host:is_args, matchEval:host:is_recFieldExprs. [Show Proof] Add_Proj_Rel matchEval:host:is_stmt. Prove_Ext_Ind matchEval:host:is_stmt. Prove matchEval:host:is_args_nilArgs_or_consArgs. Prove matchEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. Prove matchEval:host:vars_unique. [Show Proof] Prove matchEval:host:vars_is. [Show Proof] Prove matchEval:host:vars_exist, matchEval:host:varsArgs_exist, matchEval:host:varsRecFields_exist. [Show Proof] Prove_Constraint matchEval:host:proj_expr_vars. [Show Proof] Prove matchEval:host:typeOf_isTy. [Show Proof] Prove matchEval:host:stmtOK_isCtx. Prove matchEval:host:stmtOK_keep_scopes. Prove matchEval:host:stmtOK_older_scopes_same. Prove matchEval:host:stmtOK_first_scope_lookup_same. Prove matchEval:host:typeOf_unique. [Show Proof] Prove matchEval:host:stmtOK_unique. Prove matchEval:host:paramTy_is. Prove matchEval:host:getFunInfo_is. Prove matchEval:host:paramTy_exists. Prove matchEval:host:getFunInfo_exists. Prove matchEval:host:matchInt_is. [Show Proof] Prove matchEval:host:matchString_is. [Show Proof] Prove matchEval:host:matchRec_is. [Show Proof] Prove matchEval:host:evalExpr_isValue, matchEval:host:evalStmt_isCtx, matchEval:host:evalArgs_isValue, matchEval:host:evalRecFields_isValue. [Show Proof] Prove matchEval:host:evalExpr_isOutput, matchEval:host:evalStmt_isOutput, matchEval:host:evalArgs_isOutput, matchEval:host:evalRecFields_isOutput. [Show Proof] Prove matchEval:host:paramName_is. Prove matchEval:host:getFunEvalInfo_is. Prove matchEval:host:evalProgram_isOutput. Prove matchEval:host:evalStmt_names_same. Prove matchEval:host:matchInt_unique. [Show Proof] Prove matchEval:host:matchTrue_matchFalse_exclusive. [Show Proof] Prove matchEval:host:matchString_unique. [Show Proof] Prove matchEval:host:matchRec_unique. [Show Proof] Prove matchEval:host:matchInt_matchTrue_exclusive. [Show Proof] Prove matchEval:host:matchInt_matchFalse_exclusive. [Show Proof] Prove matchEval:host:matchInt_matchString_exclusive. [Show Proof] Prove matchEval:host:matchInt_matchRec_exclusive. [Show Proof] Prove matchEval:host:matchString_matchTrue_exclusive. [Show Proof] Prove matchEval:host:matchString_matchFalse_exclusive. [Show Proof] Prove matchEval:host:matchString_matchRec_exclusive. [Show Proof] Prove matchEval:host:matchRec_matchTrue_exclusive. [Show Proof] Prove matchEval:host:matchRec_matchFalse_exclusive. [Show Proof] Prove matchEval:host:evalExpr_rel, matchEval:host:evalExpr_rel_output, matchEval:host:evalStmt_newNameScopes_output, matchEval:host:evalStmt_newNameScopes, matchEval:host:evalArgs_rel, matchEval:host:evalArgs_rel_output, matchEval:host:evalRecFields_rel, matchEval:host:evalRecFields_rel_output. [Show Proof] Add_Ext_Size matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt. Add_Proj_Rel matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt. Prove matchEval:host:evalExpr_rel_exists_ES, matchEval:host:evalStmt_newNameScopes_exists_ES, matchEval:host:evalArgs_rel_exists_ES, matchEval:host:evalRecFields_rel_exists_ES. [Show Proof] Prove matchEval:host:evalExpr_scopes_same, matchEval:host:evalStmt_scopes_same, matchEval:host:evalStmt_scopes_same_ctx, matchEval:host:evalArgs_scopes_same, matchEval:host:evalRecFields_scopes_same. [Show Proof] Prove matchEval:host:evalExpr_scopes_same_exists, matchEval:host:evalStmt_scopes_same_exists, matchEval:host:evalArgs_scopes_same_exists, matchEval:host:evalRecFields_scopes_same_exists. [Show Proof] Prove_Constraint matchEval:host:proj_matchInt. [Show Proof] Prove_Constraint matchEval:host:proj_matchTrue. [Show Proof] Prove_Constraint matchEval:host:proj_matchFalse. [Show Proof] Prove_Constraint matchEval:host:proj_matchString. [Show Proof] Prove_Constraint matchEval:host:proj_matchRec. [Show Proof] Add_Proj_Rel matchEval:host:matchInt. Prove_Ext_Ind matchEval:host:matchInt. [Show Proof] Add_Proj_Rel matchEval:host:matchTrue. Prove_Ext_Ind matchEval:host:matchTrue. [Show Proof] Add_Proj_Rel matchEval:host:matchFalse. Prove_Ext_Ind matchEval:host:matchFalse. [Show Proof] Add_Proj_Rel matchEval:host:matchRec. Prove_Ext_Ind matchEval:host:matchRec. [Show Proof] Add_Proj_Rel matchEval:host:matchString. Prove_Ext_Ind matchEval:host:matchString. [Show Proof] Prove matchEval:host:projedVal_is. Prove matchEval:host:projedVal_matchInt. Prove matchEval:host:projedVal_matchString. Prove matchEval:host:projedVal_matchTrue. Prove matchEval:host:projedVal_matchFalse. Prove matchEval:host:projedVal_matchRec. Prove_Constraint matchEval:host:matchInt_proj. [Show Proof] Prove_Constraint matchEval:host:matchTrue_proj. [Show Proof] Prove_Constraint matchEval:host:matchFalse_proj. [Show Proof] Prove_Constraint matchEval:host:matchString_proj. [Show Proof] Prove_Constraint matchEval:host:matchRec_proj. [Show Proof] Prove matchEval:host:matchInt_projedVal. Prove matchEval:host:matchTrue_projedVal. Prove matchEval:host:matchFalse_projedVal. Prove matchEval:host:matchString_projedVal. Prove matchEval:host:matchRec_projedVal. Prove_Constraint matchEval:host:proj_evalExpr_forward. [Show Proof] Prove_Constraint matchEval:host:proj_evalStmt_forward. Prove_Ext_Ind matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt. [Show Proof] Prove matchEval:host:paramName_unique. Prove_Constraint matchEval:host:proj_paramName_forward. Prove_Constraint matchEval:host:proj_paramName_back. Prove matchEval:host:getFunEvalInfo_unique. Prove_Constraint matchEval:host:proj_getFunEvalInfo_forward. Prove_Constraint matchEval:host:proj_getFunEvalInfo_back. Prove matchEval:host:evalProgram_unique. Prove_Constraint matchEval:host:proj_evalProgram_forward. Prove_Constraint matchEval:host:proj_evalProgram_back. Prove matchEval:host:matchRec_typePres. [Show Proof] Prove matchEval:host:evalExpr_typePres, matchEval:host:evalStmt_typePres, matchEval:host:evalArgs_typePres, matchEval:host:evalRecFields_typePres. [Show Proof] Prove matchEval:host:paramTy_paramName_same. Prove matchEval:host:funOK_getFunEvalInfo_related. Prove matchEval:host:evalExpr_output_forms, matchEval:host:evalStmt_output_forms, matchEval:host:evalArgs_output_forms, matchEval:host:evalRecFields_output_forms. [Show Proof] Prove matchEval:host:evalProgram_output_forms. Prove matchEval:host:paramName_exists. Prove matchEval:host:getFunEvalInfo_exists. /* What seems strange about this extension, in combination with the others, specifically the list extension, is that wrap(3) + wrap(4) evaluates, and similarly for other host-introduced constructs, but head(wrap(cons(3, nil))) will not evaluate because that doesn't use matching. Thus we don't have any apparent problems in proving properties here, but we do end up having what is likely unexpected behavior in a composition. */