Module matchEval:host /*Expressions*/ expr ::= num(int) | plus(expr, expr) | minus(expr, expr) | mult(expr, expr) | div(expr, expr) | true | false | and(expr, expr) | or(expr, expr) | not(expr) | greater(expr, expr) | eq(expr, expr) | stringLit(string) | appString(expr, expr) | name(string) | call(string, args) | recBuild(recFieldExprs) | recFieldAccess(expr, string) | errorExpr(expr, typ) /*errorExpr represents a failure case expr: string-typed error message expression typ: for proving typing properties*/ Projection expr : recFieldExprs ::= nilRecFieldExprs | consRecFieldExprs(string, expr, recFieldExprs) Projection recFieldExprs : args ::= nilArgs | consArgs(expr, args) Projection args : /*Statements*/ stmt ::= noop | seq(stmt, stmt) | declare(typ, string, expr) | assign(string, expr) | recUpdate(string, [string], expr) | ifThenElse(expr, stmt, stmt) | while(expr, stmt) | scopeStmt(stmt) | printVal(expr) /*[string] is list of names used in the program thus far; lets us generate fresh names for extension constructs*/ Projection stmt : [string] /*Functions*/ fun ::= fun(string, typ, string, value, [param], stmt) /*name, ret ty, ret var, init ret var val, params, body*/ Projection fun : param ::= param(string, typ) Projection param : /*Full Program*/ program ::= program([fun], fun) /*list of auxiliary functions, main function*/ Projection program : /*Types (cannot name it "type" because of Extensibella keyword*/ typ ::= intTy | boolTy | stringTy | recTy(recFieldTys) recFieldTys ::= nilRecFieldTys | consRecFieldTys(string, typ, recFieldTys) Projection typ : Projection recFieldTys : /*Values*/ value ::= intVal(int) | trueVal | falseVal | stringVal(string) | recVal([(string, value)]) Projection value :
Module matchEval:host Judgment vars : expr* [string] Fixed Judgment varsArgs : args [string] Fixed Judgment varsRecFields : recFieldExprs [string] /******************************************************************** Expression Variables ********************************************************************/ -------------- [V-Num] vars num(I) [] vars E1 V1 vars E2 V2 V1 ++ V2 = V ------------------- [V-Plus] vars plus(E1, E2) V vars E1 V1 vars E2 V2 V1 ++ V2 = V -------------------- [V-Minus] vars minus(E1, E2) V vars E1 V1 vars E2 V2 V1 ++ V2 = V ------------------- [V-Mult] vars mult(E1, E2) V vars E1 V1 vars E2 V2 V1 ++ V2 = V ------------------ [V-Div] vars div(E1, E2) V ------------ [V-True] vars true [] ------------- [V-False] vars false [] vars E1 V1 vars E2 V2 V1 ++ V2 = V ------------------ [V-And] vars and(E1, E2) V vars E1 V1 vars E2 V2 V1 ++ V2 = V ----------------- [V-Or] vars or(E1, E2) V vars E V ------------- [V-Not] vars not(E) V vars E1 V1 vars E2 V2 V1 ++ V2 = V ---------------------- [V-Greater] vars greater(E1, E2) V vars E1 V1 vars E2 V2 V1 ++ V2 = V ----------------- [V-Eq] vars eq(E1, E2) V -------------------- [V-String] vars stringLit(S) [] vars E1 V1 vars E2 V2 V1 ++ V2 = V ------------------------ [V-AppString] vars appString(E1, E2) V ---------------- [V-Name] vars name(X) [X] varsArgs Args V ---------------------- [V-Call] vars call(Fun, Args) V varsRecFields RF V ------------------- [V-RecBuild] vars recBuild(RF) V vars Rec V --------------------------------- [V-RecAccess] vars recFieldAccess(Rec, Field) V vars Msg V ------------------------- [V-Error] vars errorExpr(Msg, Ty) V /*Arguments*/ =================== [VA-Nil] varsArgs nilArgs [] vars E VE varsArgs Rest VRest VE ++ VRest = V ============================ [VA-Cons] varsArgs consArgs(E, Rest) V /*Record Fields*/ ================================= [VRF-Nil] varsRecFields nilRecFieldExprs [] vars E VE varsRecFields Rest VRest VE ++ VRest = V ============================================= [VRF-Cons] varsRecFields consRecFieldExprs(F, E, Rest) V Fixed Judgment mems : A [[A]] Fixed Judgment not_mems : A [[A]] mem X S ============== [Mems-Here] mems X S::Rest mems X Rest ============== [Mems-Later] mems X S::Rest ============= [NMems-Nil] not_mems X [] not_mem X S not_mems X Rest ================== [NMems-Cons] not_mems X S::Rest
Module matchEval:host /*Find a name in the closest scope*/ Fixed Judgment lookupScopes : Key [[(Key, Item)]] Item lookup L Key Item ============================= [LS-FirstScope] lookupScopes Key L::Rest Item no_lookup L Key lookupScopes Key Rest Item ============================= [LS-Later] lookupScopes Key L::Rest Item /*Find a name in the closest scope and replace its associated item Fails if name does not exist*/ Fixed Judgment replaceScopes : Key Item [[(Key, Item)]] [[(Key, Item)]] /*We use remove_all here rather than something like select because we want to make evaluation uniqueness not be dependent on typing. If we use select instead, we need to assume there is only one binding so the selection of an element to remove is unique. However, for a declaration, we are only ensuring there is a single binding if it is well-typed. Thus evaluation uniqueness would depend on it being well-typed. This is simpler.*/ mem (Key, I) L remove_all L Key LRemain ============================================ [RS-FirstScope] {replaceScopes Key Item L::Rest ((Key, Item)::LRemain)::Rest} no_lookup L Key replaceScopes Key Item Rest New ===================================== [RS-Later] replaceScopes Key Item L::Rest L::New Fixed Judgment remove_all : [(Key, Item)] Key [(Key, Item)] ==================== [RA-Nil] remove_all [] Key [] remove_all Rest Key R ================================== [RA-Remove] remove_all (Key, Item)::Rest Key R K != Key remove_all Rest Key R =========================================== [RA-Keep] remove_all (K, Item)::Rest Key (K, Item)::R /*get the names that occur in all scopes*/ Fixed Judgment names : [[(Key, Item)]] [Key] =========== [Names-Nil] names [] [] domain Scope NScope names Rest NRest NScope ++ NRest = Names ======================= [Names-Cons] names Scope::Rest Names /*Create a name not in the list with the given base fresh_name base existingNames freshName We don't use fresh_name in the host at all; however, it will be useful for extensions introducing new statement forms requiring new variables.*/ Fixed Judgment fresh_name : string [string] string not_mem Base Names ========================== [FN-Final] fresh_name Base Names Base mem Base Names Base ++ "_" = NewBase fresh_name NewBase Names Fresh ============================== [FN-Step] fresh_name Base Names Fresh
Module matchEval:host /* The type [[(string, typ)]] is a set of scopes for typing. The most recent scope is the first one in the list The type [(string, (typ, [typ]))] is the function context, listing the known functions with their return types and argument types */ /*funCtx, tyCtx, expression, type*/ Judgment typeOf : {[(string, (typ, [typ]))] [[(string, typ)]] expr* typ} /*funCtx, tyCtx, args, types*/ Fixed Judgment typeOfArgs : { [(string, (typ, [typ]))] [[(string, typ)]] args [typ]} /*funCtx, tyCtx, fields, types*/ Fixed Judgment typeOfRecFields : { [(string, (typ, [typ]))] [[(string, typ)]] recFieldExprs recFieldTys} /*record fields, field, type*/ Fixed Judgment lookupRecFieldTy : recFieldTys string typ /*funCtx, starting tyCtx, statement, ending tyCtx*/ Judgment stmtOK : {[(string, (typ, [typ]))] [[(string, typ)]] stmt* [[(string, typ)]]} /*fields, field types, final type found*/ Fixed Judgment nestedFieldTy : [string] recFieldTys typ Judgment funOK : [(string, (typ, [typ]))] fun* Fixed Judgment paramTys : [param] [(string, typ)] Judgment paramTy : param* string typ /*param name and type*/ Fixed Judgment funsOK : [(string, (typ, [typ]))] [fun] /*function, name, ret ty, arg tys*/ Judgment getFunInfo : fun* string typ [typ] Fixed Judgment gatherFunInfo : [fun] [(string, (typ, [typ]))] /*Check a full program is well-typed*/ Judgment programOK : program* /******************************************************************** Expression Typing ********************************************************************/ ------------------------- [T-Num] typeOf FC TC num(I) intTy typeOf FC TC E1 intTy typeOf FC TC E2 intTy ------------------------------- [T-Plus] typeOf FC TC plus(E1, E2) intTy typeOf FC TC E1 intTy typeOf FC TC E2 intTy -------------------------------- [T-Minus] typeOf FC TC minus(E1, E2) intTy typeOf FC TC E1 intTy typeOf FC TC E2 intTy ------------------------------- [T-Mult] typeOf FC TC mult(E1, E2) intTy typeOf FC TC E1 intTy typeOf FC TC E2 intTy ------------------------------ [T-Div] typeOf FC TC div(E1, E2) intTy ------------------------ [T-True] typeOf FC TC true boolTy ------------------------- [T-False] typeOf FC TC false boolTy typeOf FC TC E1 boolTy typeOf FC TC E2 boolTy ------------------------------- [T-And] typeOf FC TC and(E1, E2) boolTy typeOf FC TC E1 boolTy typeOf FC TC E2 boolTy ------------------------------ [T-Or] typeOf FC TC or(E1, E2) boolTy typeOf FC TC E boolTy -------------------------- [T-Not] typeOf FC TC not(E) boolTy typeOf FC TC E1 intTy typeOf FC TC E2 intTy ----------------------------------- [T-Greater] typeOf FC TC greater(E1, E2) boolTy typeOf FC TC E1 intTy typeOf FC TC E2 intTy ------------------------------ [T-Eq-Int] typeOf FC TC eq(E1, E2) boolTy typeOf FC TC E1 boolTy typeOf FC TC E2 boolTy ------------------------------ [T-Eq-Bool] typeOf FC TC eq(E1, E2) boolTy typeOf FC TC E1 stringTy typeOf FC TC E2 stringTy ------------------------------ [T-Eq-String] typeOf FC TC eq(E1, E2) boolTy ---------------------------------- [T-String] typeOf FC TC stringLit(S) stringTy typeOf FC TC E1 stringTy typeOf FC TC E2 stringTy --------------------------------------- [T-AppString] typeOf FC TC appString(E1, E2) stringTy lookupScopes X TC Ty ----------------------- [T-Name] typeOf FC TC name(X) Ty lookup FC Fun (RetTy, ArgTys) typeOfArgs FC TC Args ArgTys ---------------------------------- [T-Call] typeOf FC TC call(Fun, Args) RetTy typeOfRecFields FC TC Fields FieldTys --------------------------------------------- [T-RecBuild] typeOf FC TC recBuild(Fields) recTy(FieldTys) typeOf FC TC E recTy(FieldTys) lookupRecFieldTy FieldTys Field Ty ---------------------------------------- [T-RecAccess] typeOf FC TC recFieldAccess(E, Field) Ty /*any type*/ ---------------------------------- [T-Error] typeOf GC TC errorExpr(Msg, Ty) Ty /*Arguments*/ =========================== [TA-Nil] typeOfArgs FC TC nilArgs [] typeOf FC TC E ETy typeOfArgs FC TC Rest ETys ============================================ [TA-Cons] typeOfArgs FC TC consArgs(E, Rest) ETy::ETys /*Record Fields*/ ===================================================== [TRF-Nil] typeOfRecFields FC TC nilRecFieldExprs nilRecFieldTys typeOf FC TC E ETy typeOfRecFields FC TC Rest RestTys ======================================================= [TRF-Cons] {typeOfRecFields FC TC consRecFieldExprs(Name, E, Rest) consRecFieldTys(Name, ETy, RestTys)} /*Record Field Types for Specific Fields*/ ================================================== [LRF-Here] lookupRecFieldTy consRecFieldTys(F, Ty, Rest) F Ty X != F lookupRecFieldTy Rest F Ty =================================================== [LRF-Later] lookupRecFieldTy consRecFieldTys(X, XTy, Rest) F Ty /******************************************************************** Statement Typing ********************************************************************/ -------------------- [T-Noop] stmtOK FC TC noop TC stmtOK FC TC S1 TC1 stmtOK FC TC1 S2 TC2 ---------------------------- [T-Seq] stmtOK FC TC seq(S1, S2) TC2 no_lookup Scope X /*can't redeclare in scope*/ typeOf FC Scope::RestTC E Ty ------------------------------------------ [T-Declare] {stmtOK FC Scope::RestTC declare(Ty, X, E) ((X, Ty)::Scope)::RestTC} /*Implicit simplifying assumption: Record fields are always in the same order in types, so we don't have to do more than check strict equality here. If we didn't want to require the same order, we could have a type equality check relation.*/ lookupScopes X TC Ty typeOf FC TC E Ty ---------------------------- [T-Assign] stmtOK FC TC assign(X, E) TC lookupScopes Rec TC recTy(FieldTys) typeOf FC TC E Ty nestedFieldTy Fields FieldTys Ty ----------------------------------------- [T-RecUpdate] stmtOK FC TC recUpdate(Rec, Fields, E) TC typeOf FC TC Cond boolTy stmtOK FC []::TC Th TCTh /*branches are new scopes*/ stmtOK FC []::TC El TCEl ---------------------------------------- [T-IfThenElse] stmtOK FC TC ifThenElse(Cond, Th, El) TC typeOf FC TC Cond boolTy stmtOK FC []::TC Body TC2 /*body is new scope*/ --------------------------------- [T-While] stmtOK FC TC while(Cond, Body) TC stmtOK FC []::TC S TC2 ---------------------------- [T-ScopeStmt] stmtOK FC TC scopeStmt(S) TC typeOf FC TC E intTy --------------------------- [T-Print-Int] stmtOK FC TC printVal(E) TC typeOf FC TC E boolTy --------------------------- [T-Print-Bool] stmtOK FC TC printVal(E) TC typeOf FC TC E stringTy --------------------------- [T-Print-String] stmtOK FC TC printVal(E) TC /*Nested Field Type*/ lookupRecFieldTy FTys F Ty ========================== [NFT-LastField] nestedFieldTy [F] FTys Ty lookupRecFieldTy FTys F recTy(NextFields) nestedFieldTy Rest NextFields Ty ========================================= [NFT-StepField] nestedFieldTy F::Rest FTys Ty /******************************************************************** Function Typing ********************************************************************/ /*check the function is well-typed with given types*/ paramTys Params ParamTys stmtOK FC [(RetVar, RetTy)::ParamTys] Body FinalTC /*check the function ctx contains the given types for this function*/ lookup FC FunName (RetTy, PTys) values ParamTys PTys /*no param with same name as return variable*/ no_lookup ParamTys RetVar valueType RVVal RetTy --------------------------------------------------------- [T-Fun] funOK FC fun(FunName, RetTy, RetVar, RVVal, Params, Body) /*Types in Lists of Parameters*/ ============== [PT-Nil] paramTys [] [] paramTy P PName PTy paramTys Rest RestTys ====================================== [PT-Cons] paramTys P::Rest (PName, PTy)::RestTys /*Types of Parameters*/ ------------------------------- [PT-Param] paramTy param(Name, Ty) Name Ty /*Types for a List of Functions*/ ============ [FOK-Nil] funsOK FC [] funOK FC F funsOK FC Rest ================= [FOK-Cons] funsOK FC F::Rest /******************************************************************** Gather Functions ********************************************************************/ paramTys Params NameTys values NameTys PTys ------------------------------------------------------------ [GFI-Fun] {getFunInfo fun(FunName, RetTy, RetVar, RVVal, Params, Body) FunName RetTy PTys} =================== [GFI-Nil] gatherFunInfo [] [] getFunInfo F Name RetTy PTys gatherFunInfo Rest RestTys ==================================================== [GFI-Cons] gatherFunInfo F::Rest (Name, (RetTy, PTys))::RestTys /******************************************************************** Program Typing ********************************************************************/ gatherFunInfo Funs FC funsOK FC Funs funOK FC Main /*Main must be named "main" and return int*/ getFunInfo Main "main" intTy ArgTys ----------------------------------- [T-Program] programOK program(Funs, Main) /******************************************************************** Value Typing ********************************************************************/ Judgment valueType : value* typ Fixed Judgment valFieldTys : [(string, value)] recFieldTys ------------------------- [VT-Int] valueType intVal(I) intTy ------------------------ [VT-True] valueType trueVal boolTy ------------------------- [VT-False] valueType falseVal boolTy ------------------------------- [VT-String] valueType stringVal(S) stringTy valFieldTys Fields FieldTys ---------------------------------------- [VT-Rec] valueType recVal(Fields) recTy(FieldTys) ============================= [VFT-Nil] valFieldTys [] nilRecFieldTys valueType V Ty valFieldTys Rest RestTys ======================================================== [VFT-Cons] valFieldTys (F, V)::Rest consRecFieldTys(F, Ty, RestTys)
Module matchEval:host /* The type [(string, (string, value, [string], stmt))] is the function environment, listing the known functions with their return vars, initial return var values, parameter names, and body The type [[(string, value)]] is a set of scopes for evaluation. The most recent scope is the first one in the list. */ /*fun env, val env, expr, value, printed output*/ Judgment evalExpr : {[(string, (string, value, [string], stmt))] [[(string, value)]] expr* value [value]} Judgment evalArgs : {[(string, (string, value, [string], stmt))] [[(string, value)]] args* [value] [value]} Judgment evalRecFields : { [(string, (string, value, [string], stmt))] [[(string, value)]] recFieldExprs* [(string, value)] [value]} /*match value forms through projection*/ Judgment matchInt : value* int Judgment matchTrue : value* Judgment matchFalse : value* Judgment matchString : value* string Judgment matchRec : value* [(string, value)] /*fun env, val envin, stmt, val env out, printed output*/ Judgment evalStmt : {[(string, (string, value, [string], stmt))] [[(string, value)]] stmt* [[(string, value)]] [value]} /*fields, new val, original field vals, updated field vals*/ Fixed Judgment updateRecFields : { [string] value [(string, value)] [(string, value)]} /*field to replace, new value, original list, output list*/ Fixed Judgment replaceRecVal : string value [(string, value)] [(string, value)] Fixed Judgment paramNames : [param] [string] Judgment paramName : param* string Fixed Judgment getFunEvalCtx : [fun] [(string, (string, value, [string], stmt))] /*fun, fun name, ret var, ret var init val, param names, body*/ Judgment getFunEvalInfo : fun* string string value [string] stmt /*Given arguments to main, run program*/ Judgment evalProgram : [value] program* [value] /******************************************************************** Expression Evaluation ********************************************************************/ ---------------------------------- [E-Num] evalExpr FE EE num(I) intVal(I) [] evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 + I2 = I O1 ++ O2 = O --------------------------------------- [E-Plus] evalExpr FE EE plus(E1, E2) intVal(I) O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 - I2 = I O1 ++ O2 = O ---------------------------------------- [E-Minus] evalExpr FE EE minus(E1, E2) intVal(I) O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 * I2 = I O1 ++ O2 = O --------------------------------------- [E-Mult] evalExpr FE EE mult(E1, E2) intVal(I) O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 / I2 = I O1 ++ O2 = O -------------------------------------- [E-Div] evalExpr FE EE div(E1, E2) intVal(I) O ------------------------------ [E-True] evalExpr FE EE true trueVal [] -------------------------------- [E-False] evalExpr FE EE false falseVal [] evalExpr FE EE E1 V1 O1 matchTrue V1 evalExpr FE EE E2 V2 O2 matchTrue V2 O1 ++ O2 = O ------------------------------------ [E-And-True] evalExpr FE EE and(E1, E2) trueVal O evalExpr FE EE E1 V O matchFalse V ------------------------------------- [E-And-False1] evalExpr FE EE and(E1, E2) falseVal O evalExpr FE EE E1 V1 O1 matchTrue V1 evalExpr FE EE E2 V2 O2 matchFalse V2 O1 ++ O2 = O ------------------------------------- [E-And-False2] evalExpr FE EE and(E1, E2) falseVal O evalExpr FE EE E1 V O matchTrue V ----------------------------------- [E-Or-True1] evalExpr FE EE or(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 matchFalse V1 evalExpr FE EE E2 V2 O2 matchTrue V2 O1 ++ O2 = O ----------------------------------- [E-Or-True2] evalExpr FE EE or(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 matchFalse V1 evalExpr FE EE E2 V2 O2 matchFalse V2 O1 ++ O2 = O ------------------------------------ [E-Or-False] evalExpr FE EE or(E1, E2) falseVal O evalExpr FE EE E V O matchFalse V ------------------------------- [E-Not-True] evalExpr FE EE not(E) trueVal O evalExpr FE EE E V O matchTrue V -------------------------------- [E-Not-False] evalExpr FE EE not(E) falseVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 > I2 O1 ++ O2 = O ---------------------------------------- [E-Greater-True] evalExpr FE EE greater(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 <= I2 O1 ++ O2 = O ----------------------------------------- [E-Greater-False] evalExpr FE EE greater(E1, E2) falseVal O /* We need to define equality evaluation like this to make it be the same across projected values. Unfortunately, this means matching down to the simplest values and checking those for equality. This is less general than the other versions of the language, but anything that would check less primitive values would seem to pose a problem when things start projecting, as they might project to more primitive values that no longer match each other. */ evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I matchInt V2 I O1 ++ O2 = O ----------------------------------- [E-Eq-Int-True] evalExpr FE EE eq(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchInt V1 I1 matchInt V2 I2 I1 != I2 O1 ++ O2 = O ------------------------------------ [E-Eq-Int-False] evalExpr FE EE eq(E1, E2) falseVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchTrue V1 matchTrue V2 O1 ++ O2 = O ----------------------------------- [E-Eq-Bool-TrueT] evalExpr FE EE eq(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchFalse V1 matchFalse V2 O1 ++ O2 = O ----------------------------------- [E-Eq-Bool-TrueF] evalExpr FE EE eq(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchTrue V1 matchFalse V2 O1 ++ O2 = O ------------------------------------ [E-Eq-Bool-False1] evalExpr FE EE eq(E1, E2) falseVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchFalse V1 matchTrue V2 O1 ++ O2 = O ------------------------------------ [E-Eq-Bool-False2] evalExpr FE EE eq(E1, E2) falseVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchString V1 S matchString V2 S O1 ++ O2 = O ----------------------------------- [E-Eq-String-True] evalExpr FE EE eq(E1, E2) trueVal O evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchString V1 S1 matchString V2 S2 S1 != S2 O1 ++ O2 = O ------------------------------------ [E-Eq-String-False] evalExpr FE EE eq(E1, E2) falseVal O ------------------------------------------- [E-String] evalExpr FE EE stringLit(S) stringVal(S) [] evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 matchString V1 S1 matchString V2 S2 S1 ++ S2 = S O1 ++ O2 = O ----------------------------------------------- [E-AppString] evalExpr FE EE appString(E1, E2) stringVal(S) O lookupScopes X EE V --------------------------- [E-Name] evalExpr FE EE name(X) V [] lookup FE Fun (RetVar, RVVal, ArgNames, Body) evalArgs FE EE Args ArgVals O1 zip ArgNames ArgVals InitEnv evalStmt FE [(RetVar, RVVal)::InitEnv] Body EE2 O2 O1 ++ O2 = O lookupScopes RetVar EE2 V -------------------------------------------------- [E-Call] evalExpr FE EE call(Fun, Args) V O evalRecFields FE EE RF VF O ---------------------------------------- [E-RecBuild] evalExpr FE EE recBuild(RF) recVal(VF) O evalExpr FE EE Rec VR O matchRec VR Fields lookup Fields F V ----------------------------------------- [E-RecAccess] evalExpr FE EE recFieldAccess(Rec, F) V O Extensibella_Stand_In { |{expr}- E ~~> E_P evalExpr FE EE E_P V_P O_P -------------------------- [E-Expr-Q] evalExpr FE EE E V O } /*Arguments*/ ---------------------------- [EA-Nil] evalArgs FE EE nilArgs [] [] evalExpr FE EE E V O1 evalArgs FE EE Rest VRest O2 O1 ++ O2 = O ------------------------------------------- [EA-Cons] evalArgs FE EE consArgs(E, Rest) V::VRest O /*No Extensibella stand-in rule because the args type isn't intended to be extended*/ /*Record Fields*/ ------------------------------------------ [ERF-Nil] evalRecFields FE EE nilRecFieldExprs [] [] evalExpr FE EE E V O1 evalRecFields FE EE Rest VRest O2 O1 ++ O2 = O -------------------------------------------------- [ERF-Cons] {evalRecFields FE EE consRecFieldExprs(F, E, Rest) (F, V)::VRest O} /*recFields isn't intended to be extended either*/ /******************************************************************** Statement Evaluation ********************************************************************/ -------------------- [MI-IntVal] matchInt intVal(I) I Extensibella_Stand_In { |{value}- V ~~> V_P matchInt V_P I ------------------- [MI-Q] matchInt V I } ----------------- [MT-True] matchTrue trueVal Extensibella_Stand_In { |{value}- V ~~> V_P matchTrue V_P ------------------- [MT-Q] matchTrue V } ------------------- [MF-False] matchFalse falseVal Extensibella_Stand_In { |{value}- V ~~> V_P matchFalse V_P ------------------- [MF-Q] matchFalse V } -------------------------- [MS-String] matchString stringVal(S) S Extensibella_Stand_In { |{value}- V ~~> V_P matchString V_P S ------------------- [MS-Q] matchString V S } ------------------------------ [MR-Rec] matchRec recVal(Fields) Fields Extensibella_Stand_In { |{value}- V ~~> V_P matchRec V_P Fs ------------------- [MR-Q] matchRec V Fs } /******************************************************************** Statement Evaluation ********************************************************************/ ------------------------- [E-Noop] evalStmt FE EE noop EE [] evalStmt FE EE S1 EE1 O1 evalStmt FE EE1 S2 EE2 O2 O1 ++ O2 = O --------------------------------- [E-Seq] evalStmt FE EE seq(S1, S2) EE2 O evalExpr FE Scope::EE E V O ------------------------------------------------------- [E-Declare] {evalStmt FE Scope::EE declare(Ty, X, E) ((X, V)::Scope)::EE O} evalExpr FE EE E V O replaceScopes X V EE EE1 /*find and replace value*/ --------------------------------- [E-Assign] evalStmt FE EE assign(X, E) EE1 O evalExpr FE EE E V O lookupScopes Rec EE RV matchRec RV FieldVals updateRecFields Fields V FieldVals NewVals replaceScopes Rec recVal(NewVals) EE EE1 /*find and replace value*/ ---------------------------------------------- [E-RecUpdate] evalStmt FE EE recUpdate(Rec, Fields, E) EE1 O evalExpr FE EE Cond V O1 matchTrue V evalStmt FE []::EE Th Scope::EE1 O2 O1 ++ O2 = O --------------------------------------------- [E-If-True] evalStmt FE EE ifThenElse(Cond, Th, El) EE1 O evalExpr FE EE Cond V O1 matchFalse V evalStmt FE []::EE El Scope::EE1 O2 O1 ++ O2 = O --------------------------------------------- [E-If-False] evalStmt FE EE ifThenElse(Cond, Th, El) EE1 O evalExpr FE EE Cond V O1 matchTrue V evalStmt FE []::EE Body Scope::EE1 O2 evalStmt FE EE1 while(Cond, Body) EE2 O3 O1 ++ O2 = O12 O12 ++ O3 = O ---------------------------------------- [E-While-True] evalStmt FE EE while(Cond, Body) EE2 O evalExpr FE EE Cond V O matchFalse V ------------------------------------- [E-While-False] evalStmt FE EE while(Cond, Body) EE O evalStmt FE []::EE S Scope::EE1 O --------------------------------- [E-ScopeStmt] evalStmt FE EE scopeStmt(S) EE1 O evalExpr FE EE E intVal(I) O1 O1 ++ [intVal(I)] = O -------------------------------- [E-Print-Int] evalStmt FE EE printVal(E) EE O evalExpr FE EE E trueVal O1 O1 ++ [trueVal] = O ------------------------------- [E-Print-True] evalStmt FE EE printVal(E) EE O evalExpr FE EE E falseVal O1 O1 ++ [falseVal] = O ------------------------------- [E-Print-False] evalStmt FE EE printVal(E) EE O evalExpr FE EE E stringVal(S) O1 O1 ++ [stringVal(S)] = O -------------------------------- [E-Print-String] evalStmt FE EE printVal(E) EE O Extensibella_Stand_In { names EE Names Names |{stmt}- S ~~> S_P evalStmt FE EE S_P EE_P O_P --------------------------- [E-Stmt-Q] evalStmt FE EE S EE1 O } /*Update Record Fields*/ replaceRecVal F V L Replaced ================================ [URF-One] updateRecFields [F] V L Replaced lookup L F RV /*find field value*/ matchRec RV Fields /*make it a record*/ updateRecFields FRest V Fields Updated /*update that record*/ replaceRecVal F recVal(Updated) L Rest /*put that one back in*/ ====================================== [URF-Step] updateRecFields F::FRest V L Rest ==================================================== [RRV-Here] replaceRecVal F VNew (F, VOld)::Rest (F, VNew)::Rest F != O replaceRecVal F VNew Rest RRest ================================================= [RRV-Later] replaceRecVal F VNew (O, VO)::Rest (O, VO)::RRest /******************************************************************** Build Function Evaluation Context ********************************************************************/ /*Evaluation-relevant information for a single function*/ paramNames Params PNames ---------------------------------------------------- [GFEI-Fun] {getFunEvalInfo fun(FunName, RetTy, RetVar, RVVal, Params, Body) FunName RetVar RVVal PNames Body} /*Evaluation-relevant information for a list of functions*/ =================== [GFEC-Empty] getFunEvalCtx [] [] getFunEvalInfo F FName RetVar RVVal PNames Body getFunEvalCtx FRest CRest ================================================== [GFEC-Cons] {getFunEvalCtx F::FRest (FName, (RetVar, RVVal, PNames, Body))::CRest} /*Name for a single parameter*/ ------------------------------ [PN-Param] paramName param(Name, Ty) Name /*Gather names*/ ================ [PNs-Empty] paramNames [] [] paramName P N paramNames PRest NRest ============================ [PNs-Cons] paramNames P::PRest N::NRest /******************************************************************** Program Evaluation ********************************************************************/ /*Build fun ctx*/ getFunEvalCtx Funs FCtx getFunEvalInfo Main MainName RetVar RetVal PNames Body /*Run main*/ zip PNames Args InitEnv {evalStmt (MainName, (RetVar, RetVal, PNames, Body))::FCtx [(RetVar, RetVal)::InitEnv] Body EE O} ---------------------------------------------------------- [E-Program] evalProgram Args program(Funs, Main) O
Module matchEval:host /*projedVal A B: A is related to B by taking some (zero or more) projection steps, either at the root or under constructors*/ Judgment projedVal : value* value /*same, but for record fields*/ Fixed Judgment projedFields : [(string, value)] [(string, value)] ------------- [PR-Zero] projedVal V V /*Note this is not a default rule; it applies to anything*/ |{value}- V1 ~~> V2 ------------------- [PR-Proj] projedVal V1 V2 /*This allows us to take separate rules and put them together, like an extension-introduced construct projecting to a record and values within the fields also projecting*/ projedVal V1 V2 projedVal V2 V3 --------------- [PR-Trans] projedVal V1 V3 projedFields Fs1 Fs2 --------------------------------- [PR-Rec] projedVal recVal(Fs1) recVal(Fs2) /*This rule requires extension-introduced rules to be equivalent to PR-Proj above. Basically, extensions can't introduced any new rules, since they need to be equivalent to PR-Proj anyway.*/ Extensibella_Stand_In{ |{value}- V1 ~~> V2 ------------------- [PR-Q] projedVal V1 V2 } ================== [PF-Nil] projedFields [] [] projedVal VA VB projedFields ARest BRest ========================================== [PF-Cons] projedFields (F, VA)::ARest (F, VB)::BRest
Click on a command or tactic to see a detailed view of its use.
Module matchEval:host. %can use fresh_name to generate new names for stmt projection Theorem fresh_name_unique : forall Base Names FA FB, fresh_name Base Names FA -> fresh_name Base Names FB -> FA = FB. [Show Proof] Theorem fresh_name_unique_mems : forall Base NamesA NamesB FA FB, fresh_name Base NamesA FA -> fresh_name Base NamesB FB -> (forall X, mem X NamesA -> mem X NamesB) -> (forall X, mem X NamesB -> mem X NamesA) -> FA = FB. [Show Proof] Theorem fresh_name_is : forall Base Names F, is_string Base -> fresh_name Base Names F -> is_string F. [Show Proof] /* The rest of this is proving fresh_name_exists: */ Theorem mem_string_list_or_not : forall S L, is_string S -> is_list is_string L -> mem S L \/ (mem S L -> false). [Show Proof] Theorem mem_is_string : forall L X, is_list is_string L -> mem X L -> is_string X. [Show Proof] Theorem select_string_list_is : forall S L L', is_list is_string L -> select S L' L -> is_list is_string L'. [Show Proof] Theorem select_length[A] : forall (X : A) L L' N N', select X L' L -> length L N -> 1 + N' = N -> length L' N'. [Show Proof] Theorem length_exists_string : forall L, is_list is_string L -> exists N, length L N. [Show Proof] Theorem not_mem_not_mem : forall X L, is_list is_string L -> (mem X L -> false) -> not_mem X L. [Show Proof] Define adds_ : string -> string -> prop by adds_ S S; adds_ S U := exists S', S ++ "_" = S' /\ adds_ S' U. Theorem fresh_name_remove : forall Base Names F S Names', fresh_name Base Names F -> (adds_ Base S -> false) -> select S Names' Names -> fresh_name Base Names' F. [Show Proof] Theorem fresh_name_add : forall Base Names F S Names', fresh_name Base Names F -> (adds_ Base S -> false) -> select S Names Names' -> fresh_name Base Names' F. [Show Proof] Theorem length_adds_ : forall A B NA NB, adds_ A B -> length A NA -> length B NB -> NA <= NB. [Show Proof] Theorem not_adds_ : forall Base S, is_string Base -> adds_ S Base -> Base ++ "_" = S -> false. [Show Proof] Theorem fresh_name_exists_acc : forall Base Names Len, is_string Base -> is_list is_string Names -> length Names Len -> acc Len -> exists F, fresh_name Base Names F. [Show Proof] Theorem fresh_name_exists : forall Base Names, is_string Base -> is_list is_string Names -> exists F, fresh_name Base Names F. [Show Proof] Theorem fresh_name_not_mem : forall Base Names F, fresh_name Base Names F -> mem F Names -> false. [Show Proof] Theorem fresh_name_start : forall Base Names F, is_string Base -> fresh_name Base Names F -> exists S, Base ++ S = F. [Show Proof] /******************************************************************** ____ _ | __ ) __ _ ___(_) ___ | _ \ / _` / __| |/ __| | |_) | (_| \__ \ | (__ |____/ \__,_|___/_|\___| ____ _ _ _ | _ \ _ __ ___ (_) ___ ___| |_(_) ___ _ __ | |_) | '__/ _ \| |/ _ \/ __| __| |/ _ \| '_ \ | __/| | | (_) | | __/ (__| |_| | (_) | | | | |_| |_| \___// |\___|\___|\__|_|\___/|_| |_| ____ |_/ _ _ _ / ___|___ _ __ ___| |_ _ __ __ _(_)_ __ | |_ ___ | | / _ \| '_ \/ __| __| '__/ _` | | '_ \| __/ __| | |__| (_) | | | \__ \ |_| | | (_| | | | | | |_\__ \ \____\___/|_| |_|___/\__|_| \__,_|_|_| |_|\__|___/ Basic Projection Constraints ********************************************************************/ Projection_Constraint proj_expr_unique : forall E E1 E2, PrA : |{expr}- E ~~> E1 -> PrB : |{expr}- E ~~> E2 -> IsE : is_expr E -> E1 = E2. Projection_Constraint proj_expr_is : forall E E', Pr : |{expr}- E ~~> E' -> IsE : is_expr E -> is_expr E'. Projection_Constraint proj_stmt_unique : forall L1 L2 S S1 S2, PrA : L1 |{stmt}- S ~~> S1 -> PrB : L2 |{stmt}- S ~~> S2 -> IsS : is_stmt S -> IsL1 : is_list is_string L1 -> IsL2 : is_list is_string L2 -> Rel12 : (forall X, mem X L1 -> mem X L2) -> Rel21 : (forall X, mem X L2 -> mem X L1) -> S1 = S2. Projection_Constraint proj_stmt_is : forall L S S', Pr : L |{stmt}- S ~~> S' -> IsS : is_stmt S -> IsL : is_list is_string L -> is_stmt S'. Projection_Constraint proj_stmt_other : forall L S S' L', Pr : L |{stmt}- S ~~> S' -> IsS : is_stmt S -> IsL : is_list is_string L -> IsL' : is_list is_string L' -> exists S'', L' |{stmt}- S ~~> S''. Projection_Constraint proj_fun_unique : forall F F1 F2, PrA : |{fun}- F ~~> F1 -> PrB : |{fun}- F ~~> F2 -> IsF : is_fun F -> F1 = F2. Projection_Constraint proj_fun_is : forall F F', Pr : |{fun}- F ~~> F' -> IsF : is_fun F -> is_fun F'. Projection_Constraint proj_param_unique : forall P P1 P2, PrA : |{param}- P ~~> P1 -> PrB : |{param}- P ~~> P2 -> IsP : is_param P -> P1 = P2. Projection_Constraint proj_param_is : forall P P', Pr : |{param}- P ~~> P' -> IsP : is_param P -> is_param P'. Projection_Constraint proj_program_unique : forall P P1 P2, PrA : |{program}- P ~~> P1 -> PrB : |{program}- P ~~> P2 -> IsP : is_program P -> P1 = P2. Projection_Constraint proj_program_is : forall P P', Pr : |{program}- P ~~> P' -> IsP : is_program P -> is_program P'. Projection_Constraint proj_typ_unique : forall T T1 T2, PrA : |{typ}- T ~~> T1 -> PrB : |{typ}- T ~~> T2 -> IsT : is_typ T -> T1 = T2. Projection_Constraint proj_typ_is : forall T T', Pr : |{typ}- T ~~> T' -> IsT : is_typ T -> is_typ T'. Projection_Constraint proj_value_unique : forall V V1 V2, PrA : |{value}- V ~~> V1 -> PrB : |{value}- V ~~> V2 -> IsV : is_value V -> V1 = V2. Projection_Constraint proj_value_is : forall V V', Pr : |{value}- V ~~> V' -> IsV : is_value V -> is_value V'. /******************************************************************** ____ _ _ _ _ | _ \ ___ ___(_) __| | __ _| |__ | | ___ | | | |/ _ \/ __| |/ _` |/ _` | '_ \| |/ _ \ | |_| | __/ (__| | (_| | (_| | |_) | | __/ |____/ \___|\___|_|\__,_|\__,_|_.__/|_|\___| _____ _ _ _ | ____|__ _ _ _ __ _| (_) |_ _ _ | _| / _` | | | |/ _` | | | __| | | | | |__| (_| | |_| | (_| | | | |_| |_| | |_____\__, |\__,_|\__,_|_|_|\__|\__, | |_| |___/ Decidable Equality ********************************************************************/ Theorem is_list_is_string_eq_or_not : forall L1 L2, is_list is_string L1 -> is_list is_string L2 -> L1 = L2 \/ (L1 = L2 -> false). [Show Proof] Proj_Rel is_expr E, is_args A, is_recFieldExprs RF. Ext_Ind forall E, is_expr E; forall A, is_args A; forall RF, is_recFieldExprs RF. [Show Proof] Proj_Rel is_stmt S. Ext_Ind forall S, is_stmt S. [Show Proof] /* With these properties, we make the args and recFieldExprs types nonextensible. */ Extensible_Theorem is_args_nilArgs_or_consArgs : forall A, Is : is_args A -> A = nilArgs \/ (exists E A', A = consArgs E A') on Is. [Show Proof] Extensible_Theorem is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs : forall RF, Is : is_recFieldExprs RF -> RF = nilRecFieldExprs \/ (exists F E RF', RF = consRecFieldExprs F E RF') on Is. [Show Proof] /******************************************************************** ____ / ___| ___ ___ _ __ ___ ___ \___ \ / __/ _ \| '_ \ / _ \/ __| ___) | (_| (_) | |_) | __/\__ \ |____/ \___\___/| .__/ \___||___/ |_| Scopes ********************************************************************/ Theorem lookupScopes_unique[Key, Item] : forall L (K : Key) (I1 I2 : Item), lookupScopes K L I1 -> lookupScopes K L I2 -> I1 = I2. [Show Proof] Theorem lookupScopes_names [K, V] : forall Ctx (X : K) (V : V) Names, lookupScopes X Ctx V -> names Ctx Names -> mem X Names. [Show Proof] Theorem lookup_after_dual_select[Key, Item] : forall (K X : Key) (V1 V2 I1 I2 : Item) L R1 R2, select (K, V1) R1 L -> select (K, V2) R2 L -> (K = X -> false) -> lookup R1 X I1 -> lookup R2 X I2 -> I1 = I2. [Show Proof] Theorem remove_all_unique[Key, Item] : forall (L : list (pair Key Item)) X A B, remove_all L X A -> remove_all L X B -> A = B. [Show Proof] Theorem replaceScopes_unique[Key, Item] : forall X V (L : list (list (pair Key Item))) RA RB, replaceScopes X V L RA -> replaceScopes X V L RB -> RA = RB. [Show Proof] Theorem replaceScopes_names [K, V] : forall Ctx (X : K) (V : V) Names R, replaceScopes X V Ctx R -> names Ctx Names -> mem X Names. [Show Proof] Theorem remove_all_names [K, V] : forall (X : K) (L R : list (pair K V)) NL NR Z, remove_all L X R -> domain L NL -> domain R NR -> mem Z NL -> (X = Z -> false) -> mem Z NR. [Show Proof] Theorem mem_after_remove_all_before [K, V] : forall L R X (Z : pair K V), remove_all L X R -> mem Z R -> mem Z L. [Show Proof] Theorem mem_before_remove_all_after [K, V] : forall L R X (K : K) (V : V), remove_all L X R -> mem (K, V) L -> (K = X -> false) -> mem (K, V) R. [Show Proof] Theorem names_unique [K, V] : forall (L : list (list (pair K V))) NA NB, names L NA -> names L NB -> NA = NB. [Show Proof] %two sets of scopes where the names in the first are associated with %the same items in the second one Define lookup_all_scopes : list (list (pair string Item)) -> list (list (pair string Item)) -> prop by lookup_all_scopes [] []; lookup_all_scopes (A::ARest) (B::BRest) := (forall X V, lookup A X V -> lookup B X V) /\ %We will need is_string for proving things with remove_all later (forall X, is_string X -> no_lookup A X -> no_lookup B X) /\ lookup_all_scopes ARest BRest. Theorem lookup_all_scopes_lookupScopes[Item] : forall A B X (V : Item), is_string X -> lookup_all_scopes A B -> lookupScopes X A V -> lookupScopes X B V. [Show Proof] Theorem lookup_all_scopes_add[Item] : forall A B AS BS X (V : Item), lookup_all_scopes (AS::A) (BS::B) -> lookup_all_scopes (((X, V)::AS)::A) (((X, V)::BS)::B). [Show Proof] %all scopes contain the same values for the same names %order within scope does not matter Define scopes_same : list (list (pair string value)) -> list (list (pair string value)) -> prop by scopes_same [] []; scopes_same (A::ARest) (B::BRest) := (forall X V, lookup A X V -> lookup B X V) /\ (forall X V, lookup B X V -> lookup A X V) /\ scopes_same ARest BRest. Theorem scopes_same_reflexive : forall L, is_list (is_list (is_pair is_string is_value)) L -> scopes_same L L. [Show Proof] Theorem scopes_same_trans : forall A B C, scopes_same A B -> scopes_same B C -> scopes_same A C. [Show Proof] Theorem scopes_same_symm : forall A B, scopes_same A B -> scopes_same B A. [Show Proof] /******************************************************************** __ __ _ _ _ \ \ / /_ _ _ __(_) __ _| |__ | | ___ ___ \ \ / / _` | '__| |/ _` | '_ \| |/ _ \/ __| \ V / (_| | | | | (_| | |_) | | __/\__ \ \_/ \__,_|_| |_|\__,_|_.__/|_|\___||___/ Variables ********************************************************************/ /******************************************************************** Variables are unique ********************************************************************/ Extensible_Theorem vars_unique : forall E V1 V2, IsE : is_expr E -> VarsA : vars E V1 -> VarsB : vars E V2 -> V1 = V2 on VarsA also varsArgs_unique : forall A V1 V2, IsA : is_args A -> VarsA : varsArgs A V1 -> VarsB : varsArgs A V2 -> V1 = V2 on VarsA, varsRecFields_unique : forall RF V1 V2, IsRF : is_recFieldExprs RF -> VarsA : varsRecFields RF V1 -> VarsB : varsRecFields RF V2 -> V1 = V2 on VarsA. [Show Proof] /******************************************************************** Variables is_list is_string ********************************************************************/ Theorem append_list_string_is : forall L1 L2 L3, is_list is_string L1 -> is_list is_string L2 -> L1 ++ L2 = L3 -> is_list is_string L3. [Show Proof] Extensible_Theorem vars_is : forall E V, IsE : is_expr E -> V : vars E V -> is_list is_string V on V also varsArgs_is : forall A V, IsA : is_args A -> V : varsArgs A V -> is_list is_string V on V, varsRecFields_is : forall RF V, IsRF : is_recFieldExprs RF -> V : varsRecFields RF V -> is_list is_string V on V. [Show Proof] /******************************************************************** Variables exist for anything ********************************************************************/ Theorem append_list_string_total : forall L1 L2, is_list is_string L1 -> is_list is_string L2 -> exists L3, L1 ++ L2 = L3. [Show Proof] Extensible_Theorem vars_exist : forall E, IsE : is_expr E -> exists V, vars E V on IsE, varsArgs_exist : forall A, IsA : is_args A -> exists V, varsArgs A V on IsA, varsRecFields_exist : forall RF, IsRF : is_recFieldExprs RF -> exists V, varsRecFields RF V on IsRF. [Show Proof] /******************************************************************** Variables are maintained in projection ********************************************************************/ Projection_Constraint proj_expr_vars : forall E E_P V V_P X, Pr : |{expr}- E ~~> E_P -> IsE : is_expr E -> V : vars E V -> V_P : vars E_P V_P -> Mem : mem X V -> mem X V_P. %Note we have vars exists for any expression (defined by is_expr) and %projections have is_expr, so we don't need a projection constraint %that vars exist for the projection. /******************************************************************** _____ _ |_ _| _ _ __ (_)_ __ __ _ | || | | | '_ \| | '_ \ / _` | | || |_| | |_) | | | | | (_| | |_| \__, | .__/|_|_| |_|\__, | |___/|_| |___/ Typing ********************************************************************/ /******************************************************************** Basic lemmas around types and typing ********************************************************************/ %-------------------------------------------- % Theorems about [(string, typ)] %-------------------------------------------- Theorem is_list_mem_lookup_type : forall L ID E, is_list (is_pair is_string is_typ) L -> mem (ID, E) L -> is_string ID -> exists E', lookup L ID E'. [Show Proof] Theorem lookup_is_type : forall L ID E, is_list (is_pair is_string is_typ) L -> lookup L ID E -> is_typ E. [Show Proof] Theorem lookup_is_key_type : forall L ID E, is_list (is_pair is_string is_typ) L -> lookup L ID E -> is_string ID. [Show Proof] Theorem mem_is_type : forall L IDE, is_list (is_pair is_string is_typ) L -> mem IDE L -> is_pair is_string is_typ IDE. [Show Proof] Theorem zip_is_type : forall A B L, is_list is_string A -> is_list is_typ B -> zip A B L -> is_list (is_pair is_string is_typ) L. [Show Proof] Theorem length_exists_list_pair_string_ty : forall L, is_list (is_list (is_pair is_string is_typ)) L -> exists N, length L N. [Show Proof] %-------------------------------------------- % Theorems about function contexts % [(string, (type, [type]))] %-------------------------------------------- Theorem is_list_mem_lookup_funTyCtx : forall L ID E, is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) L -> mem (ID, E) L -> is_string ID -> exists E', lookup L ID E'. [Show Proof] Theorem mem_is_funTyCtx : forall L IDE, is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) L -> mem IDE L -> is_pair is_string (is_pair is_typ (is_list is_typ)) IDE. [Show Proof] Theorem lookup_is_value_funTyCtx : forall L ID E, is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) L -> lookup L ID E -> is_pair is_typ (is_list is_typ) E. [Show Proof] Theorem lookup_is_key_funTyCtx : forall L ID E, is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) L -> lookup L ID E -> is_string ID. [Show Proof] %------------------------------------------------- Theorem lookupScopes_isTy : forall L X Ty, is_list (is_list (is_pair is_string is_typ)) L -> lookupScopes X L Ty -> is_typ Ty. [Show Proof] Theorem zip_is_string_ty : forall A B Z, is_list is_string A -> is_list is_typ B -> zip A B Z -> is_list (is_pair is_string is_typ) Z. [Show Proof] Theorem length_exists_ty : forall L, is_list is_typ L -> exists N, length L N. [Show Proof] %-------------------------------------------- % Theorems about recFieldTys %-------------------------------------------- Theorem lookupRecFieldTy_is : forall Fields F Ty, is_recFieldTys Fields -> lookupRecFieldTy Fields F Ty -> is_typ Ty. [Show Proof] Theorem lookupRecFieldTy_unique : forall Fields F TyA TyB, lookupRecFieldTy Fields F TyA -> lookupRecFieldTy Fields F TyB -> TyA = TyB. [Show Proof] /******************************************************************** Types/Contexts produced in typing have is relations ********************************************************************/ Extensible_Theorem typeOf_isTy : forall E FT ET Ty, IsE : is_expr E -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> Ty : typeOf FT ET E Ty -> is_typ Ty on Ty also typeOfArgs_isTy : forall A FT ET Tys, IsA : is_args A -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> Ty : typeOfArgs FT ET A Tys -> is_list is_typ Tys on Ty, typeOfRecFields_isTy : forall RF FT ET Fields, IsRF : is_recFieldExprs RF -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> Ty : typeOfRecFields FT ET RF Fields -> is_recFieldTys Fields on Ty. [Show Proof] Extensible_Theorem stmtOK_isCtx : forall S FT ET ET', IsS : is_stmt S -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> Ty : stmtOK FT ET S ET' -> is_list (is_list (is_pair is_string is_typ)) ET' on Ty. [Show Proof] /******************************************************************** Statements do not make unwanted modifications to contexts ********************************************************************/ Extensible_Theorem stmtOK_keep_scopes : forall FT ET S ET' N, IsS : is_stmt S -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> Ty : stmtOK FT ET S ET' -> L : length ET N -> length ET' N on Ty. [Show Proof] Extensible_Theorem stmtOK_older_scopes_same : forall FT ET S ET' Scope, IsS : is_stmt S -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) (Scope::ET) -> Ty : stmtOK FT (Scope::ET) S ET' -> exists Scope', ET' = Scope'::ET on Ty. [Show Proof] %Don't overwrite existing names in current scope %Can't say lookupScopes because can overwrite names from older scopes % in this scope Extensible_Theorem stmtOK_first_scope_lookup_same : forall FT ET S Scope Scope' X Ty, IsS : is_stmt S -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) (Scope::ET) -> Ty : stmtOK FT (Scope::ET) S (Scope'::ET) -> L : lookup Scope X Ty -> lookup Scope' X Ty on Ty. [Show Proof] /******************************************************************** Typing unique ********************************************************************/ Extensible_Theorem typeOf_unique : forall FT ET_A ET_B E TyA TyB, IsE : is_expr E -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsA : is_list (is_list (is_pair is_string is_typ)) ET_A -> IsB : is_list (is_list (is_pair is_string is_typ)) ET_B -> TyA : typeOf FT ET_A E TyA -> TyB : typeOf FT ET_B E TyB -> Lkp : lookup_all_scopes ET_A ET_B -> TyA = TyB on TyA as IH_E also typeOfArgs_unique : forall FT ET_A ET_B A TysA TysB, IsA : is_args A -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsA : is_list (is_list (is_pair is_string is_typ)) ET_A -> IsB : is_list (is_list (is_pair is_string is_typ)) ET_B -> TyA : typeOfArgs FT ET_A A TysA -> TyB : typeOfArgs FT ET_B A TysB -> Lkp : lookup_all_scopes ET_A ET_B -> TysA = TysB on TyA as IH_A, typeOfRecFields_unique : forall FT ET_A ET_B RF FieldsA FieldsB, IsRF : is_recFieldExprs RF -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsA : is_list (is_list (is_pair is_string is_typ)) ET_A -> IsB : is_list (is_list (is_pair is_string is_typ)) ET_B -> TyA : typeOfRecFields FT ET_A RF FieldsA -> TyB : typeOfRecFields FT ET_B RF FieldsB -> Lkp : lookup_all_scopes ET_A ET_B -> FieldsA = FieldsB on TyA as IH_RF. [Show Proof] Extensible_Theorem stmtOK_unique : forall FT ET_A ET_B S ET_A' ET_B', IsS : is_stmt S -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsA : is_list (is_list (is_pair is_string is_typ)) ET_A -> IsB : is_list (is_list (is_pair is_string is_typ)) ET_B -> TyA : stmtOK FT ET_A S ET_A' -> TyB : stmtOK FT ET_B S ET_B' -> Lkp : lookup_all_scopes ET_A ET_B -> lookup_all_scopes ET_A' ET_B' on TyA. [Show Proof] /******************************************************************** Gathered function typing information has is relations ********************************************************************/ Extensible_Theorem paramTy_is : forall P N T, IsP : is_param P -> PT : paramTy P N T -> is_string N /\ is_typ T on PT. [Show Proof] Theorem paramTys_is : forall Ps PTys, is_list is_param Ps -> paramTys Ps PTys -> is_list (is_pair is_string is_typ) PTys. [Show Proof] Theorem values_is_ty : forall L V, is_list (is_pair is_string is_typ) L -> values L V -> is_list is_typ V. [Show Proof] Extensible_Theorem getFunInfo_is : forall F N R P, IsF : is_fun F -> GFI : getFunInfo F N R P -> is_string N /\ is_typ R /\ is_list is_typ P on GFI. [Show Proof] Theorem gatherFunInfo_is : forall Fs Ctx, is_list is_fun Fs -> gatherFunInfo Fs Ctx -> is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) Ctx. [Show Proof] /******************************************************************** Gathered function typing information always exists ********************************************************************/ Extensible_Theorem paramTy_exists : forall P, IsP : is_param P -> exists N T, paramTy P N T on IsP. [Show Proof] Theorem paramTys_exists : forall Ps, is_list is_param Ps -> exists PTys, paramTys Ps PTys. [Show Proof] Theorem values_exists_ty : forall L, is_list (is_pair is_string is_typ) L -> exists V, values L V. [Show Proof] Extensible_Theorem getFunInfo_exists : forall F, IsF : is_fun F -> exists N R P, getFunInfo F N R P on IsF. [Show Proof] Theorem gatherFunInfo_exists : forall Fs, is_list is_fun Fs -> exists Ctx, gatherFunInfo Fs Ctx. [Show Proof] /******************************************************************** _____ _ _ _ | ____|_ ____ _| |_ _ __ _| |_(_) ___ _ __ | _| \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \ | |___ \ V / (_| | | |_| | (_| | |_| | (_) | | | | |_____| \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_| Evaluation ********************************************************************/ /******************************************************************** Basic lemmas around values and evaluation ********************************************************************/ %-------------------------------------------- % Theorems about [(string, value)] %-------------------------------------------- Theorem is_list_mem_lookup : forall L ID E, is_list (is_pair is_string is_value) L -> mem (ID, E) L -> is_string ID -> exists E', lookup L ID E'. [Show Proof] Theorem lookup_is_value : forall L ID E, is_list (is_pair is_string is_value) L -> lookup L ID E -> is_value E. [Show Proof] Theorem lookup_is_key : forall L ID E, is_list (is_pair is_string is_value) L -> lookup L ID E -> is_string ID. [Show Proof] Theorem lookup_string_value_list_or_no : forall L X, is_list (is_pair is_string is_value) L -> is_string X -> (exists V, lookup L X V) \/ no_lookup L X. [Show Proof] Theorem mem_is : forall L IDE, is_list (is_pair is_string is_value) L -> mem IDE L -> is_pair is_string is_value IDE. [Show Proof] Theorem zip_is : forall A B L, is_list is_string A -> is_list is_value B -> zip A B L -> is_list (is_pair is_string is_value) L. [Show Proof] Theorem select_is : forall L X L', is_list (is_pair is_string is_value) L -> select X L' L -> is_list (is_pair is_string is_value) L'. [Show Proof] Theorem domain_is : forall L D, is_list (is_pair is_string is_value) L -> domain L D -> is_list is_string D. [Show Proof] Theorem names_is : forall L N, is_list (is_list (is_pair is_string is_value)) L -> names L N -> is_list is_string N. [Show Proof] Theorem domain_exists : forall L, is_list (is_pair is_string is_value) L -> exists D, domain L D. [Show Proof] Theorem names_exists : forall L, is_list (is_list (is_pair is_string is_value)) L -> exists N, names L N. [Show Proof] %-------------------------------------------- % Theorems about function contexts % [(string, (string, value, [string], stmt))] %-------------------------------------------- Theorem is_list_mem_lookup_funCtx : forall L ID E, is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) L -> mem (ID, E) L -> is_string ID -> exists E', lookup L ID E'. [Show Proof] Theorem mem_is_funCtx : forall L IDE, is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) L -> mem IDE L -> is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt))) IDE. [Show Proof] Theorem lookup_is_value_funCtx : forall L ID E, is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) L -> lookup L ID E -> is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)) E. [Show Proof] Theorem lookup_is_key_funCtx : forall L ID E, is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) L -> lookup L ID E -> is_string ID. [Show Proof] %-------------------------------------------- % Theorems about remove_all %-------------------------------------------- Theorem remove_all_mem[Key, Item] : forall (L : list (pair Key Item)) K L' I, remove_all L K L' -> mem (K, I) L' -> false. [Show Proof] Theorem remove_all_lookup_other[Key, Item] : forall (L : list (pair Key Item)) K L' X I, remove_all L K L' -> lookup L' X I -> (K = X -> false) -> lookup L X I. [Show Proof] Theorem remove_all_lookup_other_back[Key, Item] : forall (L : list (pair Key Item)) K L' X I, remove_all L K L' -> lookup L X I -> (K = X -> false) -> lookup L' X I. [Show Proof] Theorem remove_all_lookups : forall LA LB K LA' LB' X I, is_list (is_pair is_string is_value) LA -> is_list (is_pair is_string is_value) LB -> is_string K -> is_string X -> (forall X I, lookup LA X I -> lookup LB X I) -> remove_all LA K LA' -> remove_all LB K LB' -> lookup LA' X I -> lookup LB' X I. [Show Proof] Theorem remove_all_no_lookup_back[Key, Item] : forall (L : list (pair Key Item)) K L' X, remove_all L K L' -> no_lookup L X -> no_lookup L' X. [Show Proof] Theorem remove_all_no_lookup : forall L K L' X, is_list (is_pair is_string is_value) L -> is_string K -> is_string X -> remove_all L K L' -> no_lookup L' X -> no_lookup L X \/ X = K. [Show Proof] %-------------------------------------------- % Theorems about length %-------------------------------------------- Theorem length_exists_list_pair_string_value : forall L, is_list (is_list (is_pair is_string is_value)) L -> exists N, length L N. [Show Proof] Theorem length_exists_value : forall L, is_list is_value L -> exists N, length L N. [Show Proof] %-------------------------------------------- % Theorems about zip %-------------------------------------------- Theorem zip_exists[A, B] : forall (A : list A) (B : list B) N, length A N -> length B N -> exists Z, zip A B Z. [Show Proof] Theorem zip_is_string_value : forall A B Z, is_list is_string A -> is_list is_value B -> zip A B Z -> is_list (is_pair is_string is_value) Z. [Show Proof] %-------------------------------------------- Theorem mem_lookup : forall L X V, is_list (is_pair is_string is_value) L -> mem (X, V) L -> exists V', lookup L X V'. [Show Proof] Theorem replaceScopes_lookup_all_scopes : forall X V A B A' B', is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> lookup_all_scopes A B -> replaceScopes X V A A' -> replaceScopes X V B B' -> lookup_all_scopes A' B'. [Show Proof] /******************************************************************** Evaluation-produced values and contexts have is relations ********************************************************************/ Theorem lookupScopes_is : forall L X V, is_list (is_list (is_pair is_string is_value)) L -> lookupScopes X L V -> is_value V. [Show Proof] Theorem remove_all_is : forall L X L', is_list (is_pair is_string is_value) L -> remove_all L X L' -> is_list (is_pair is_string is_value) L'. [Show Proof] Theorem replaceScopes_is : forall L X V L', is_list (is_list (is_pair is_string is_value)) L -> is_value V -> replaceScopes X V L L' -> is_list (is_list (is_pair is_string is_value)) L'. [Show Proof] Extensible_Theorem matchInt_is : forall V I, IsV : is_value V -> MI : matchInt V I -> is_integer I on MI. [Show Proof] Extensible_Theorem matchString_is : forall V S, IsV : is_value V -> MS : matchString V S -> is_string S on MS. [Show Proof] Extensible_Theorem matchRec_is : forall V Fs, IsV : is_value V -> MR : matchRec V Fs -> is_list (is_pair is_string is_value) Fs on MR. [Show Proof] Theorem replaceRecVal_is : forall F V L L', is_value V -> is_list (is_pair is_string is_value) L -> replaceRecVal F V L L' -> is_list (is_pair is_string is_value) L'. [Show Proof] Theorem updateRecFields_is : forall Fs V L L', is_value V -> is_list is_string Fs -> is_list (is_pair is_string is_value) L -> updateRecFields Fs V L L' -> is_list (is_pair is_string is_value) L'. [Show Proof] Extensible_Theorem evalExpr_isValue : forall FE EE E V O, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalExpr FE EE E V O -> is_value V on Ev as IH_V_E, evalStmt_isCtx : forall FE EE EE' S O, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalStmt FE EE S EE' O -> is_list (is_list (is_pair is_string is_value)) EE' on Ev as IH_C_S, evalArgs_isValue : forall FE EE A V O, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalArgs FE EE A V O -> is_list is_value V on Ev as IH_V_A, evalRecFields_isValue : forall FE EE RF V O, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalRecFields FE EE RF V O -> is_list (is_pair is_string is_value) V on Ev as IH_V_RF. [Show Proof] Theorem append_values_is : forall LA LB L, is_list is_value LA -> is_list is_value LB -> LA ++ LB = L -> is_list is_value L. [Show Proof] /* We put this in a separate group from the other is theorems above as a deliberate choice to prevent extensions from making their values depend on printed values. */ Extensible_Theorem evalExpr_isOutput : forall FE EE E V O, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalExpr FE EE E V O -> is_list is_value O on Ev as IH_E, evalStmt_isOutput : forall FE EE EE' S O, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalStmt FE EE S EE' O -> is_list is_value O on Ev as IH_S, evalArgs_isOutput : forall FE EE A V O, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalArgs FE EE A V O -> is_list is_value O on Ev as IH_A, evalRecFields_isOutput : forall FE EE RF V O, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalRecFields FE EE RF V O -> is_list is_value O on Ev as IH_RF. [Show Proof] /******************************************************************** Gathered function evaluation information has is relations ********************************************************************/ Extensible_Theorem paramName_is : forall P N, IsP : is_param P -> PN : paramName P N -> is_string N on PN. [Show Proof] Theorem paramNames_is : forall Ps Ns, is_list is_param Ps -> paramNames Ps Ns -> is_list is_string Ns. [Show Proof] Extensible_Theorem getFunEvalInfo_is : forall F Name RetVar RVVal PNames Body, IsF : is_fun F -> GEFI : getFunEvalInfo F Name RetVar RVVal PNames Body -> is_string Name /\ is_string RetVar /\ is_value RVVal /\ is_list is_string PNames /\ is_stmt Body on GEFI. [Show Proof] Theorem getFunEvalCtx_is : forall Fs Ctx, is_list is_fun Fs -> getFunEvalCtx Fs Ctx -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) Ctx. [Show Proof] /******************************************************************** Program evaluation results have is_list is_value ********************************************************************/ Extensible_Theorem evalProgram_isOutput : forall A P O, IsP : is_program P -> IsA : is_list is_value A -> Ev : evalProgram A P O -> is_list is_value O on Ev. [Show Proof] /******************************************************************** Evaluation does not make unwanted modifications to contexts ********************************************************************/ Define names_same : list (list (pair string ItemA)) -> list (list (pair string ItemB)) -> prop by names_same [] []; names_same (A::ARest) (B::BRest) := (forall X IA, mem (X, IA) A -> exists IB, mem (X, IB) B) /\ (forall X IB, mem (X, IB) B -> exists IA, mem (X, IA) A) /\ names_same ARest BRest. Theorem names_same_symmetric[A, B] : forall (A : list (list (pair string A))) (B : list (list (pair string B))), names_same A B -> names_same B A. [Show Proof] Theorem names_same_reflexive : forall L, is_list (is_list (is_pair is_string is_value)) L -> names_same L L. [Show Proof] Theorem names_same_transitive[ItemA, ItemB, ItemC] : forall (A : list (list (pair string ItemA))) (B : list (list (pair string ItemB))) (C : list (list (pair string ItemC))), names_same A B -> names_same B C -> names_same A C. [Show Proof] Theorem names_same_names[ItemA, ItemB] : forall (A : list (list (pair string ItemA))) (B : list (list (pair string ItemB))) NA NB X, names_same A B -> names A NA -> names B NB -> mem X NA -> mem X NB. [Show Proof] Theorem names_same_names_back[ItemA, ItemB] : forall (A : list (list (pair string ItemA))) (B : list (list (pair string ItemB))) NA NB X, names_same A B -> names A NA -> names B NB -> mem X NB -> mem X NA. [Show Proof] Theorem replaceScopes_names_same : forall L K I R, is_list (is_list (is_pair is_string is_value)) L -> replaceScopes K I L R -> names_same L R. [Show Proof] Theorem names_same_add_scope[I, V] : forall (A : list (list (pair string I))) (B : list (list (pair string V))), names_same A B -> names_same ([]::A) ([]::B). [Show Proof] %Evaluation doesn't change the names present in older scopes in ctxs %This will be important for extension evaluation and projection, % showing fresh_names still holds after evaluating one term Extensible_Theorem evalStmt_names_same : forall S FE Scope EE EE' O, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> Ev : evalStmt FE (Scope::EE) S EE' O -> exists Scope' EE'', EE' = Scope'::EE'' /\ names_same EE EE'' on Ev as IH_S. [Show Proof] Theorem names_same_length[A, B] : forall (A : list (list (pair string A))) (B : list (list (pair string B))) L, names_same A B -> length A L -> length B L. [Show Proof] Theorem evalStmt_keep_scopes : forall FE Scope EE S EE' N O, is_stmt S -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> evalStmt FE (Scope::EE) S EE' O -> length (Scope::EE) N -> length EE' N. [Show Proof] /******************************************************************** Evaluation unique ********************************************************************/ Extensible_Theorem matchInt_unique : forall V IA IB, IsV : is_value V -> MIA : matchInt V IA -> MIB : matchInt V IB -> IA = IB on MIA. [Show Proof] Extensible_Theorem matchTrue_matchFalse_exclusive : forall V, IsV : is_value V -> MT : matchTrue V -> MF : matchFalse V -> false on MT. [Show Proof] Extensible_Theorem matchString_unique : forall V SA SB, IsV : is_value V -> MSA : matchString V SA -> MSB : matchString V SB -> SA = SB on MSA. [Show Proof] Extensible_Theorem matchRec_unique : forall V FA FB, IsV : is_value V -> MRA : matchRec V FA -> MRB : matchRec V FB -> FA = FB on MRA. [Show Proof] Extensible_Theorem matchInt_matchTrue_exclusive : forall V I, IsV : is_value V -> MI : matchInt V I -> MT : matchTrue V -> false on MI. [Show Proof] Extensible_Theorem matchInt_matchFalse_exclusive : forall V I, IsV : is_value V -> MI : matchInt V I -> MF : matchFalse V -> false on MI. [Show Proof] Extensible_Theorem matchInt_matchString_exclusive : forall V I S, IsV : is_value V -> MI : matchInt V I -> MS : matchString V S -> false on MI. [Show Proof] Extensible_Theorem matchInt_matchRec_exclusive : forall V I Fs, IsV : is_value V -> MI : matchInt V I -> MR : matchRec V Fs -> false on MI. [Show Proof] Extensible_Theorem matchString_matchTrue_exclusive : forall V S, IsV : is_value V -> MS : matchString V S -> MT : matchTrue V -> false on MS. [Show Proof] Extensible_Theorem matchString_matchFalse_exclusive : forall V S, IsV : is_value V -> MS : matchString V S -> MF : matchFalse V -> false on MS. [Show Proof] Extensible_Theorem matchString_matchRec_exclusive : forall V S Fs, IsV : is_value V -> MS : matchString V S -> MR : matchRec V Fs -> false on MS. [Show Proof] Extensible_Theorem matchRec_matchTrue_exclusive : forall V Fs, IsV : is_value V -> MR : matchRec V Fs -> MT : matchTrue V -> false on MR. [Show Proof] Extensible_Theorem matchRec_matchFalse_exclusive : forall V Fs, IsV : is_value V -> MR : matchRec V Fs -> MF : matchFalse V -> false on MR. [Show Proof] Theorem replaceRecVal_unique : forall F V L A B, replaceRecVal F V L A -> replaceRecVal F V L B -> A = B. [Show Proof] Theorem updateRecFields_unique : forall F V L OutA OutB, is_list (is_pair is_string is_value) L -> updateRecFields F V L OutA -> updateRecFields F V L OutB -> OutA = OutB. [Show Proof] /******************************************************************** Evaluation doesn't change if you add extra scopes with new names ********************************************************************/ /* Two contexts are related by adding some scopes declaring only fresh names relative to the rest of the context. Note the length of the last bit ensures there is only one valid splitting location, a fact important for dropping added scopes in proving evaluation is maintained under newNameScopes-related contexts. The one with added scopes is the first one. */ Define newNameScopes : list (list (pair string Item)) -> integer -> list (list (pair string Item)) -> list (list (pair string Item)) -> prop by newNameScopes Scopes Len A B := exists N SNames BNames, length B Len /\ %B has Len scopes in it drop N A B /\ %A is just B with N new scopes %extra scopes only have new names take N A Scopes /\ names Scopes SNames /\ names B BNames /\ (forall X, mem X SNames -> mem X BNames -> false); %same scope on front, related rest newNameScopes Scopes Len (S::AR) (S::BR) := newNameScopes Scopes Len AR BR. Theorem lookupScopes_drop_not_mem : forall X B (V : value) N A Scopes SNames BNames, is_list (is_list (is_pair is_string is_value)) A -> is_string X -> lookupScopes X B V -> drop N A B -> take N A Scopes -> names Scopes SNames -> names B BNames -> (forall Z, mem Z SNames -> mem Z BNames -> false) -> lookupScopes X A V. [Show Proof] Theorem newNameScopes_lookupScopes : forall N Len A B X V, is_list (is_list (is_pair is_string is_value)) A -> is_string X -> newNameScopes N Len A B -> lookupScopes X B V -> lookupScopes X A V. [Show Proof] Theorem replaceScopes_drop_not_mem : forall A X V B RB N Scopes SNames BNames, is_list (is_list (is_pair is_string is_value)) A -> is_string X -> replaceScopes X V B RB -> drop N A B -> take N A Scopes -> names Scopes SNames -> names B BNames -> (forall Z, mem Z SNames -> mem Z BNames -> false) -> exists RA, Scopes ++ RB = RA /\ replaceScopes X V A RA. [Show Proof] Theorem replaceScopes_names_forward : forall X V L R LN RN Z, is_list (is_list (is_pair is_string is_value)) L -> is_string X -> replaceScopes X V L R -> names L LN -> names R RN -> mem Z LN -> mem Z RN. [Show Proof] Theorem replaceScopes_names_backward : forall X V L R LN RN Z, is_list (is_list (is_pair is_string is_value)) L -> is_string X -> replaceScopes X V L R -> names L LN -> names R RN -> mem Z RN -> mem Z LN. [Show Proof] Theorem replaceScopes_keep_scopes[Key, Item] : forall L (K : Key) (I : Item) R N, replaceScopes K I L R -> length L N -> length R N. [Show Proof] Theorem newNameScopes_replaceScopes : forall S Len A B X V RB, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> is_value V -> newNameScopes S Len A B -> replaceScopes X V B RB -> exists RA, replaceScopes X V A RA /\ newNameScopes S Len RA RB. [Show Proof] Theorem newNameScopes_length [V] : forall S Len (A B : list (list (pair string V))) BLen, newNameScopes S Len A B -> length B BLen -> Len <= BLen. [Show Proof] Theorem newNameScopes_reflexive : forall EE, is_list (is_list (is_pair is_string is_value)) EE -> exists Len, length EE Len /\ newNameScopes [] Len EE EE. [Show Proof] Theorem newNameScopes_same[V] : forall Len (A B : list (list (pair string V))), newNameScopes [] Len A B -> A = B. [Show Proof] Theorem lookupScopes_is_key : forall X S V, is_list (is_list (is_pair is_string is_value)) S -> lookupScopes X S V -> is_string X. [Show Proof] Extensible_Theorem evalExpr_rel : forall FE EE_A EE_B E VA VB O_A O_B Vars, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvA : evalExpr FE EE_A E VA O_A -> EvB : evalExpr FE EE_B E VB O_B -> Vars : vars E Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> VA = VB on EvA as IH_V_E, evalExpr_rel_output : forall FE EE_A EE_B E VA VB O_A O_B Vars, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvA : evalExpr FE EE_A E VA O_A -> EvB : evalExpr FE EE_B E VB O_B -> Vars : vars E Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> O_A = O_B on EvA as IH_O_E, /* Note we have the same scope on the front of both contexts for evaluation. This is necessary for declare, where we will add a new binding to the front scope on both and still need newNameScopes for the result. **For extensions introducing new statements, this means they must introduce a new scope before adding any new assignments.** */ evalStmt_newNameScopes_output : forall FE EE_A EE_B S EE_A' EE_B' O_A O_B N Len Scope, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) (Scope::EE_A) -> IsB : is_list (is_list (is_pair is_string is_value)) (Scope::EE_B) -> EvA : evalStmt FE (Scope::EE_A) S EE_A' O_A -> EvB : evalStmt FE (Scope::EE_B) S EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> O_A = O_B on EvA as IH_O_S, evalStmt_newNameScopes : forall FE EE_A EE_B S EE_A' EE_B' O_A O_B N Len Scope, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) (Scope::EE_A) -> IsB : is_list (is_list (is_pair is_string is_value)) (Scope::EE_B) -> EvA : evalStmt FE (Scope::EE_A) S EE_A' O_A -> EvB : evalStmt FE (Scope::EE_B) S EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> newNameScopes N Len EE_A' EE_B' on EvA as IH_C_S, evalArgs_rel : forall FE EE_A EE_B A VA VB O_A O_B Vars, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvA : evalArgs FE EE_A A VA O_A -> EvB : evalArgs FE EE_B A VB O_B -> Vars : varsArgs A Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> VA = VB on EvA as IH_V_A, evalArgs_rel_output : forall FE EE_A EE_B A VA VB O_A O_B Vars, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvA : evalArgs FE EE_A A VA O_A -> EvB : evalArgs FE EE_B A VB O_B -> Vars : varsArgs A Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> O_A = O_B on EvA as IH_O_A, evalRecFields_rel : forall FE EE_A EE_B RF VA VB O_A O_B Vars, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvA : evalRecFields FE EE_A RF VA O_A -> EvB : evalRecFields FE EE_B RF VB O_B -> Vars : varsRecFields RF Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> VA = VB on EvA as IH_V_RF, evalRecFields_rel_output : forall FE EE_A EE_B RF VA VB O_A O_B Vars, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvA : evalRecFields FE EE_A RF VA O_A -> EvB : evalRecFields FE EE_B RF VB O_B -> Vars : varsRecFields RF Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> O_A = O_B on EvA as IH_O_RF. [Show Proof] /******************************************************************** Evaluation is Unique ********************************************************************/ Theorem evalExpr_unique : forall FE EE E VA OA VB OB, is_expr E -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE -> evalExpr FE EE E VA OA -> evalExpr FE EE E VB OB -> VA = VB /\ OA = OB. [Show Proof] Theorem evalStmt_unique : forall FE Scope EE S EE_A OA EE_B OB, is_stmt S -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> evalStmt FE (Scope::EE) S EE_A OA -> evalStmt FE (Scope::EE) S EE_B OB -> EE_A = EE_B /\ OA = OB. [Show Proof] Theorem evalArgs_unique : forall FE EE A VA OA VB OB, is_args A -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE -> evalArgs FE EE A VA OA -> evalArgs FE EE A VB OB -> VA = VB /\ OA = OB. [Show Proof] Theorem evalRecFields_unique : forall FE EE RF VA OA VB OB, is_recFieldExprs RF -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE -> evalRecFields FE EE RF VA OA -> evalRecFields FE EE RF VB OB -> VA = VB /\ OA = OB. [Show Proof] /******************************************************************** Extension size and projection versions of evaluation ********************************************************************/ Ext_Size evalExpr FE EE E V O, evalArgs FE EE E V O, evalRecFields FE EE E F O, evalStmt FE EE S EE' O. Proj_Rel evalExpr FE EE E V O, evalArgs FE EE E V O, evalRecFields FE EE E F O, evalStmt FE EE S EE' O. /******************************************************************** Evaluation across newNameScopes exists ********************************************************************/ /* Not only is evaluation related when the same term evaluates across newNameScopes, but a term must evaluate under the added-to context when it evaluates under the original one. We will use this fact for proving projection constraints and Ext_Ind for evaluation. Due to its use for Ext_Ind, we use the extension size versions of the various evaluation relations so we can use the inductive hypotheses there with the new derivations we produce with this. */ Extensible_Theorem evalExpr_rel_exists_ES : forall FE EE_A EE_B E V O ES Vars, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvB : <evalExpr {ES}> FE EE_B E V O ES -> Vars : vars E Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> <evalExpr {ES}> FE EE_A E V O ES on EvB as IH_E, evalStmt_newNameScopes_exists_ES : forall FE EE_A EE_B S EE_B' O N Len Scope ES, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) (Scope::EE_A) -> IsB : is_list (is_list (is_pair is_string is_value)) (Scope::EE_B) -> EvB : <evalStmt {ES}> FE (Scope::EE_B) S EE_B' O ES -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_A', <evalStmt {ES}> FE (Scope::EE_A) S EE_A' O ES on EvB as IH_S, evalArgs_rel_exists_ES : forall FE EE_A EE_B A V O ES Vars, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvB : <evalArgs {ES}> FE EE_B A V O ES -> Vars : varsArgs A Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> <evalArgs {ES}> FE EE_A A V O ES on EvB as IH_A, evalRecFields_rel_exists_ES : forall FE EE_A EE_B RF V O ES Vars, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> EvB : <evalRecFields {ES}> FE EE_B RF V O ES -> Vars : varsRecFields RF Vars -> Rel : (forall X V, mem X Vars -> lookupScopes X EE_B V -> lookupScopes X EE_A V) -> <evalRecFields {ES}> FE EE_A RF V O ES on EvB as IH_RF. [Show Proof] Theorem evalExpr_rel_exists : forall FE EE_A EE_B E V O Vars, is_expr E -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE_A -> is_list (is_list (is_pair is_string is_value)) EE_B -> evalExpr FE EE_B E V O -> vars E Vars -> (forall X XV, mem X Vars -> lookupScopes X EE_B XV -> lookupScopes X EE_A XV) -> evalExpr FE EE_A E V O. [Show Proof] Theorem evalStmt_newNameScopes_exists : forall FE EE_A EE_B S EE_B' O N Len Scope, is_stmt S -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) (Scope::EE_A) -> is_list (is_list (is_pair is_string is_value)) (Scope::EE_B) -> evalStmt FE (Scope::EE_B) S EE_B' O -> newNameScopes N Len EE_A EE_B -> exists EE_A', evalStmt FE (Scope::EE_A) S EE_A' O. [Show Proof] Theorem evalArgs_rel_exists : forall FE EE_A EE_B A V O Vars, is_args A -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE_A -> is_list (is_list (is_pair is_string is_value)) EE_B -> evalArgs FE EE_B A V O -> varsArgs A Vars -> (forall X XV, mem X Vars -> lookupScopes X EE_B XV -> lookupScopes X EE_A XV) -> evalArgs FE EE_A A V O. [Show Proof] Theorem evalRecFields_rel_exists : forall FE EE_A EE_B RF V O Vars, is_recFieldExprs RF -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE_A -> is_list (is_list (is_pair is_string is_value)) EE_B -> evalRecFields FE EE_B RF V O -> varsRecFields RF Vars -> (forall X XV, mem X Vars -> lookupScopes X EE_B XV -> lookupScopes X EE_A XV) -> evalRecFields FE EE_A RF V O. [Show Proof] /******************************************************************** Evaluation with scopes_same ********************************************************************/ Theorem scopes_same_lookupScopes_exists : forall A B X V, is_list (is_list (is_pair is_string is_value)) B -> is_string X -> scopes_same A B -> lookupScopes X A V -> lookupScopes X B V. [Show Proof] Theorem scopes_same_lookupScopes : forall A B X VA VB, is_list (is_list (is_pair is_string is_value)) B -> is_string X -> scopes_same A B -> lookupScopes X A VA -> lookupScopes X B VB -> VA = VB. [Show Proof] Theorem remove_all_exists : forall X EE, is_list (is_pair is_string is_value) EE -> is_string X -> exists EE', remove_all EE X EE'. [Show Proof] Theorem scopes_same_replaceScopes_exists : forall A B X V A', is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> scopes_same A B -> replaceScopes X V A A' -> exists B', replaceScopes X V B B'. [Show Proof] Theorem scopes_same_replaceScopes_scopes_same : forall A B X V A' B', is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> scopes_same A B -> replaceScopes X V A A' -> replaceScopes X V B B' -> scopes_same A' B'. [Show Proof] Theorem scopes_same_add_scope : forall A B, scopes_same A B -> scopes_same ([]::A) ([]::B). [Show Proof] Extensible_Theorem evalExpr_scopes_same : forall E FE EE_A VA OA EE_B VB OB, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalExpr FE EE_A E VA OA -> EvB : evalExpr FE EE_B E VB OB -> VA = VB /\ OA = OB on EvA as IH_E, evalStmt_scopes_same : forall S FE EE_A EE_A' OA EE_B EE_B' OB, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalStmt FE EE_A S EE_A' OA -> EvB : evalStmt FE EE_B S EE_B' OB -> OA = OB on EvA as IH_S, evalStmt_scopes_same_ctx : forall S FE EE_A EE_A' OA EE_B EE_B' OB, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalStmt FE EE_A S EE_A' OA -> EvB : evalStmt FE EE_B S EE_B' OB -> scopes_same EE_A' EE_B' on EvA as IH_S_C, evalArgs_scopes_same : forall A FE EE_A VA OA EE_B VB OB, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalArgs FE EE_A A VA OA -> EvB : evalArgs FE EE_B A VB OB -> VA = VB /\ OA = OB on EvA as IH_A, evalRecFields_scopes_same : forall RF FE EE_A VA OA EE_B VB OB, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalRecFields FE EE_A RF VA OA -> EvB : evalRecFields FE EE_B RF VB OB -> VA = VB /\ OA = OB on EvA as IH_RF. [Show Proof] Extensible_Theorem evalExpr_scopes_same_exists : forall E FE EE_A V O EE_B, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalExpr FE EE_A E V O -> evalExpr FE EE_B E V O on EvA as IH_E, evalStmt_scopes_same_exists : forall S FE EE_A EE_A' O EE_B, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalStmt FE EE_A S EE_A' O -> exists EE_B', evalStmt FE EE_B S EE_B' O on EvA as IH_S, evalArgs_scopes_same_exists : forall A FE EE_A V O EE_B, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalArgs FE EE_A A V O -> evalArgs FE EE_B A V O on EvA as IH_A, evalRecFields_scopes_same_exists : forall RF FE EE_A V O EE_B, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsA : is_list (is_list (is_pair is_string is_value)) EE_A -> IsB : is_list (is_list (is_pair is_string is_value)) EE_B -> SS : scopes_same EE_A EE_B -> EvA : evalRecFields FE EE_A RF V O -> evalRecFields FE EE_B RF V O on EvA as IH_RF. [Show Proof] /******************************************************************** Evaluation and Projected Values ********************************************************************/ Theorem projedFields_reflexive : forall Fs, is_list (is_pair is_string is_value) Fs -> projedFields Fs Fs. [Show Proof] Theorem projedFields_transitive : forall A B C, % IsA : is_list (is_pair is_string is_value) A -> % IsB : is_list (is_pair is_string is_value) B -> % IsC : is_list (is_pair is_string is_value) C -> projedFields A B -> projedFields B C -> projedFields A C. [Show Proof] /* Matching across projection gives the same results. Note we go back from the projection, not forward. */ Projection_Constraint proj_matchInt : forall V V_P I, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MI : matchInt V_P I -> matchInt V I. Projection_Constraint proj_matchTrue : forall V V_P, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MT : matchTrue V_P -> matchTrue V. Projection_Constraint proj_matchFalse : forall V V_P, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MF : matchFalse V_P -> matchFalse V. Projection_Constraint proj_matchString : forall V V_P S, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MS : matchString V_P S -> matchString V S. Projection_Constraint proj_matchRec : forall V V_P Fs, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MR : matchRec V_P Fs -> matchRec V Fs. Proj_Rel matchInt V I. Ext_Ind forall V I, matchInt V I with IsV : is_value V. [Show Proof] Proj_Rel matchTrue V. Ext_Ind forall V, matchTrue V with IsV : is_value V. [Show Proof] Proj_Rel matchFalse V. Ext_Ind forall V, matchFalse V with IsV : is_value V. [Show Proof] Proj_Rel matchRec V Fs. Ext_Ind forall V Fs, matchRec V Fs with IsV : is_value V. [Show Proof] Proj_Rel matchString V S. Ext_Ind forall V S, matchString V S with IsV : is_value V. [Show Proof] Extensible_Theorem projedVal_is : forall VA VB, IsVA : is_value VA -> Pr : projedVal VA VB -> is_value VB on Pr also projedFields_is : forall FA FB, IsFA : is_list (is_pair is_string is_value) FA -> Pr : projedFields FA FB -> is_list (is_pair is_string is_value) FB on Pr. [Show Proof] /* Note that these also go back from the second value */ Extensible_Theorem projedVal_matchInt : forall VA VB I, PV : projedVal VA VB -> IsVA : is_value VA -> MI : matchInt VB I -> matchInt VA I on PV. [Show Proof] Extensible_Theorem projedVal_matchString : forall VA VB S, PV : projedVal VA VB -> IsVA : is_value VA -> MS : matchString VB S -> matchString VA S on PV. [Show Proof] Extensible_Theorem projedVal_matchTrue : forall VA VB, PV : projedVal VA VB -> IsVA : is_value VA -> MT : matchTrue VB -> matchTrue VA on PV. [Show Proof] Extensible_Theorem projedVal_matchFalse : forall VA VB, PV : projedVal VA VB -> IsVA : is_value VA -> MF : matchFalse VB -> matchFalse VA on PV. [Show Proof] Extensible_Theorem projedVal_matchRec : forall VA VB Fs, PV : projedVal VA VB -> IsVA : is_value VA -> MR : matchRec VB Fs -> exists Fs', matchRec VA Fs' /\ projedFields Fs' Fs on PV. [Show Proof] /* Here are versions that go forward */ Projection_Constraint matchInt_proj : forall V V_P I, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MI : matchInt V I -> matchInt V_P I. Projection_Constraint matchTrue_proj : forall V V_P, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MT : matchTrue V -> matchTrue V_P. Projection_Constraint matchFalse_proj : forall V V_P, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MF : matchFalse V -> matchFalse V_P. Projection_Constraint matchString_proj : forall V V_P S, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MS : matchString V S -> matchString V_P S. Projection_Constraint matchRec_proj : forall V V_P Fs, Pr : |{value}- V ~~> V_P -> IsV : is_value V -> MR : matchRec V Fs -> matchRec V_P Fs. Extensible_Theorem matchInt_projedVal : forall VA VB I, PV : projedVal VA VB -> IsVA : is_value VA -> MI : matchInt VA I -> matchInt VB I on PV. [Show Proof] Extensible_Theorem matchTrue_projedVal : forall VA VB, PV : projedVal VA VB -> IsVA : is_value VA -> MT : matchTrue VA -> matchTrue VB on PV. [Show Proof] Extensible_Theorem matchFalse_projedVal : forall VA VB, PV : projedVal VA VB -> IsVA : is_value VA -> MF : matchFalse VA -> matchFalse VB on PV. [Show Proof] Extensible_Theorem matchString_projedVal : forall VA VB S, PV : projedVal VA VB -> IsVA : is_value VA -> MS : matchString VA S -> matchString VB S on PV. [Show Proof] Extensible_Theorem matchRec_projedVal : forall VA VB Fs, PV : projedVal VA VB -> IsVA : is_value VA -> MR : matchRec VA Fs -> exists Fs', matchRec VB Fs' /\ projedFields Fs Fs' on PV. [Show Proof] Theorem projedFields_lookup : forall FA FB X VA VB, projedFields FA FB -> lookup FA X VA -> lookup FB X VB -> projedVal VA VB. [Show Proof] Theorem projedFields_replaceRecVal : forall FA FB F VA VB RA RB, projedFields FA FB -> projedVal VA VB -> replaceRecVal F VA FA RA -> replaceRecVal F VB FB RB -> projedFields RA RB. [Show Proof] Theorem projedFields_updateRecFields : forall FA FB Fs VA VB RA RB, is_list (is_pair is_string is_value) FA -> is_list (is_pair is_string is_value) FB -> projedFields FA FB -> projedVal VA VB -> updateRecFields Fs VA FA RA -> updateRecFields Fs VB FB RB -> projedFields RA RB. [Show Proof] /******************************************************************** Projection Constraints for Evaluation ********************************************************************/ %projection evaluates to a related value Projection_Constraint proj_evalExpr_forward : forall E E' FE EE V O, Pr : |{expr}- E ~~> E' -> IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalExpr FE EE E V O -> exists V', evalExpr FE EE E' V' O /\ projedVal V V'. %projection evaluates to a related context Projection_Constraint proj_evalStmt_forward : forall Names S S' FE EE EE' O, Pr : Names |{stmt}- S ~~> S' -> Names : names EE Names -> IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalStmt FE EE S EE' O -> exists EE'', evalStmt FE EE S' EE'' O /\ scopes_same EE' EE''. /* We don't include any projection constraints for argument and record field expression evaluation because we introduced properties above to make the types nonextensible, so there cannot actually be projecting syntax for them. */ /******************************************************************** Evaluation Ext_Ind for statements, expressions, and associated terms ********************************************************************/ Ext_Ind forall FE EE E V O, evalExpr FE EE E V O with IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE, IsEE : is_list (is_list (is_pair is_string is_value)) EE, IsE : is_expr E; forall FE EE A V O, evalArgs FE EE A V O with IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE, IsEE : is_list (is_list (is_pair is_string is_value)) EE, IsA : is_args A; forall FE EE RF V O, evalRecFields FE EE RF V O with IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE, IsEE : is_list (is_list (is_pair is_string is_value)) EE, IsRF : is_recFieldExprs RF; forall FE EE S EE' O, evalStmt FE EE S EE' O with IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE, IsEE : is_list (is_list (is_pair is_string is_value)) EE, IsS : is_stmt S. [Show Proof] /******************************************************************** Gathered function evaluation information unique ********************************************************************/ Extensible_Theorem paramName_unique : forall P NA NB, IsP : is_param P -> PA : paramName P NA -> PB : paramName P NB -> NA = NB on PA. [Show Proof] Theorem paramNames_unique : forall P NA NB, is_list is_param P -> paramNames P NA -> paramNames P NB -> NA = NB. [Show Proof] %a parameter's projection has the same name as it; %new parameter constructors should just be extra info around same name Projection_Constraint proj_paramName_forward : forall P P' N, Pr : |{param}- P ~~> P' -> IsP : is_param P -> PN : paramName P N -> paramName P' N. %if a parameter's projection gives info, the original gives the same Projection_Constraint proj_paramName_back : forall P P' N, Pr : |{param}- P ~~> P' -> IsP : is_param P -> PN : paramName P' N -> paramName P N. Extensible_Theorem getFunEvalInfo_unique : forall F NA RA VA PA BA NB RB VB PB BB, IsF : is_fun F -> GFEIA : getFunEvalInfo F NA RA VA PA BA -> GFEIB : getFunEvalInfo F NB RB VB PB BB -> NA = NB /\ RA = RB /\ VA = VB /\ PA = PB /\ BA = BB on GFEIA. [Show Proof] Theorem getFunEvalCtx_unique : forall Fs FCA FCB, is_list is_fun Fs -> getFunEvalCtx Fs FCA -> getFunEvalCtx Fs FCB -> FCA = FCB. [Show Proof] %a function's projection gives the same information as it Projection_Constraint proj_getFunEvalInfo_forward : forall F F' N R V P B, Pr : |{fun}- F ~~> F' -> IsF : is_fun F -> GFEI : getFunEvalInfo F N R V P B -> getFunEvalInfo F' N R V P B. %if a function's projection gives info, the original gives the same Projection_Constraint proj_getFunEvalInfo_back : forall F F' N R V P B, Pr : |{fun}- F ~~> F' -> IsF : is_fun F -> GFEI : getFunEvalInfo F' N R V P B -> getFunEvalInfo F N R V P B. /******************************************************************** Program evaluation unique ********************************************************************/ Extensible_Theorem evalProgram_unique : forall A P OA OB, IsA : is_list is_value A -> IsP : is_program P -> EvA : evalProgram A P OA -> EvB : evalProgram A P OB -> OA = OB on EvA. [Show Proof] %a program's projection evaluates the same as it Projection_Constraint proj_evalProgram_forward : forall P P' A O, Pr : |{program}- P ~~> P' -> IsP : is_program P -> IsA : is_list is_value A -> Ev : evalProgram A P O -> evalProgram A P' O. %if a program's projection evaluates, the original evaluates the same Projection_Constraint proj_evalProgram_back : forall P P' A O, Pr : |{program}- P ~~> P' -> IsP : is_program P -> IsA : is_list is_value A -> Ev : evalProgram A P' O -> evalProgram A P O. /******************************************************************** Type preservation ********************************************************************/ Define related_all_scopes : list (list (pair string typ)) -> list (list (pair string value)) -> prop by related_all_scopes [] []; related_all_scopes (A::ARest) (B::BRest) := (forall X T, lookup A X T -> exists V, lookup B X V /\ valueType V T) /\ (forall X, no_lookup A X -> no_lookup B X) /\ related_all_scopes ARest BRest. Theorem related_all_scopes_add : forall A B AS BS X V T, related_all_scopes (AS::A) (BS::B) -> valueType V T -> related_all_scopes (((X, T)::AS)::A) (((X, V)::BS)::B). [Show Proof] Theorem related_all_scopes_add_scope : forall A B, related_all_scopes A B -> related_all_scopes ([]::A) ([]::B). [Show Proof] Theorem related_all_scopes_lookupScopes : forall A B X V T, related_all_scopes A B -> lookupScopes X A T -> lookupScopes X B V -> valueType V T. [Show Proof] Define valueTypeList : list value -> list typ -> prop by valueTypeList [] []; valueTypeList (V::VRest) (T::TRest) := valueType V T /\ valueTypeList VRest TRest. Theorem valueTypeList_related_all_scopes : forall Vs Tys Ns VScope TScope, valueTypeList Vs Tys -> zip Ns Vs VScope -> zip Ns Tys TScope -> related_all_scopes [TScope] [VScope]. [Show Proof] Theorem valFieldTys_lookup : forall Fields FieldTys F V Ty, valFieldTys Fields FieldTys -> lookup Fields F V -> lookupRecFieldTy FieldTys F Ty -> valueType V Ty. [Show Proof] Theorem related_all_scopes_replaceScopes : forall ET EE X V EE' Ty, is_list (is_list (is_pair is_string is_typ)) ET -> is_list (is_list (is_pair is_string is_value)) EE -> related_all_scopes ET EE -> replaceScopes X V EE EE' -> lookupScopes X ET Ty -> valueType V Ty -> related_all_scopes ET EE'. [Show Proof] Extensible_Theorem matchRec_typePres : forall V Fs FTys, IsV : is_value V -> MR : matchRec V Fs -> VTy : valueType V (recTy FTys) -> valFieldTys Fs FTys on MR. [Show Proof] Theorem replaceRecVal_typePres : forall L Tys F VTy V L', valFieldTys L Tys -> lookupRecFieldTy Tys F VTy -> valueType V VTy -> replaceRecVal F V L L' -> valFieldTys L' Tys. [Show Proof] Theorem updateRecFields_typePres : forall Fs FTys Ty V FVals Out, is_list (is_pair is_string is_value) FVals -> nestedFieldTy Fs FTys Ty -> updateRecFields Fs V FVals Out -> valueType V Ty -> valFieldTys FVals FTys -> valFieldTys Out FTys. [Show Proof] Extensible_Theorem evalExpr_typePres : forall E FT ET Ty FE EE O V, IsE : is_expr E -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ty : typeOf FT ET E Ty -> Ev : evalExpr FE EE E V O -> Funs : (forall F RetTy ArgTys ArgNames Body RetVar RVVal, lookup FT F (RetTy, ArgTys) -> lookup FE F (RetVar, RVVal, ArgNames, Body) -> exists Scope TyEnv', zip ArgNames ArgTys Scope /\ valueType RVVal RetTy /\ stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv') -> Ctxs : related_all_scopes ET EE -> valueType V Ty on Ev as IH_E, evalStmt_typePres : forall S FT ET ET' FE EE EE' O, IsS : is_stmt S -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ty : stmtOK FT ET S ET' -> Ev : evalStmt FE EE S EE' O -> Funs : (forall F RetTy ArgTys ArgNames Body RetVar RVVal, lookup FT F (RetTy, ArgTys) -> lookup FE F (RetVar, RVVal, ArgNames, Body) -> exists Scope TyEnv', zip ArgNames ArgTys Scope /\ valueType RVVal RetTy /\ stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv') -> Ctxs : related_all_scopes ET EE -> related_all_scopes ET' EE' on Ev as IH_S, evalArgs_typePres : forall A FT ET Tys FE EE O Vs, IsA : is_args A -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ty : typeOfArgs FT ET A Tys -> Ev : evalArgs FE EE A Vs O -> Funs : (forall F RetTy ArgTys ArgNames Body RetVar RVVal, lookup FT F (RetTy, ArgTys) -> lookup FE F (RetVar, RVVal, ArgNames, Body) -> exists Scope TyEnv', zip ArgNames ArgTys Scope /\ valueType RVVal RetTy /\ stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv') -> Ctxs : related_all_scopes ET EE -> valueTypeList Vs Tys on Ev as IH_A, evalRecFields_typePres : forall RF FT ET FTys FE EE O FVs, IsRF : is_recFieldExprs RF -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> IsET : is_list (is_list (is_pair is_string is_typ)) ET -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ty : typeOfRecFields FT ET RF FTys -> Ev : evalRecFields FE EE RF FVs O -> Funs : (forall F RetTy ArgTys ArgNames Body RetVar RVVal, lookup FT F (RetTy, ArgTys) -> lookup FE F (RetVar, RVVal, ArgNames, Body) -> exists Scope TyEnv', zip ArgNames ArgTys Scope /\ valueType RVVal RetTy /\ stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv') -> Ctxs : related_all_scopes ET EE -> valFieldTys FVs FTys on Ev as IH_RF. [Show Proof] /******************************************************************** Gathered function typing and evaluation information agrees ********************************************************************/ Extensible_Theorem paramTy_paramName_same : forall P NT T N, PT : paramTy P NT T -> PN : paramName P N -> NT = N on PT. [Show Proof] Theorem paramTys_values_names_zip_same : forall Ps PTys Tys Ns, paramTys Ps PTys -> values PTys Tys -> paramNames Ps Ns -> zip Ns Tys PTys. [Show Proof] Extensible_Theorem funOK_getFunEvalInfo_related : forall F FT Name RetVar RVVal PNames Body, IsF : is_fun F -> IsFT : is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> FOK : funOK FT F -> GFEI : getFunEvalInfo F Name RetVar RVVal PNames Body -> exists RetTy ArgTys Scope TyEnv', lookup FT Name (RetTy, ArgTys) /\ zip PNames ArgTys Scope /\ valueType RVVal RetTy /\ stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv' /\ lookup FT Name (RetTy, ArgTys) on FOK. [Show Proof] Theorem funsOK_getFunEvalCtx_related : forall Fs FT FE, is_list is_fun Fs -> is_list (is_pair is_string (is_pair is_typ (is_list is_typ))) FT -> funsOK FT Fs -> getFunEvalCtx Fs FE -> %literally what we require for type preservation (forall F RetTy ArgTys ArgNames Body RetVar RVVal, lookup FT F (RetTy, ArgTys) -> lookup FE F (RetVar, RVVal, ArgNames, Body) -> exists Scope TyEnv', zip ArgNames ArgTys Scope /\ valueType RVVal RetTy /\ stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv'). [Show Proof] /******************************************************************** Evaluation prints only basic values ********************************************************************/ /* Only basic values can be printed. Record values can only be printed by printing primitive values representing them. */ Define output_forms : list value -> prop by output_forms []; output_forms (intVal I::Rest) := output_forms Rest; output_forms (trueVal::Rest) := output_forms Rest; output_forms (falseVal::Rest) := output_forms Rest; output_forms (stringVal S::Rest) := output_forms Rest. Theorem output_forms_append : forall OA OB O, output_forms OA -> output_forms OB -> OA ++ OB = O -> output_forms O. [Show Proof] Extensible_Theorem evalExpr_output_forms : forall E FE EE V O, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalExpr FE EE E V O -> output_forms O on Ev as IH_E, evalStmt_output_forms : forall S FE EE EE' O, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalStmt FE EE S EE' O -> output_forms O on Ev as IH_S, evalArgs_output_forms : forall A FE EE Vs O, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalArgs FE EE A Vs O -> output_forms O on Ev as IH_A, evalRecFields_output_forms : forall RF FE EE Fields O, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> Ev : evalRecFields FE EE RF Fields O -> output_forms O on Ev as IH_RF. [Show Proof] /******************************************************************** Program evaluation prints only basic values ********************************************************************/ Extensible_Theorem evalProgram_output_forms : forall A P O, IsA : is_list is_value A -> IsP : is_program P -> Ev : evalProgram A P O -> output_forms O on Ev. [Show Proof] /******************************************************************** Gathered function evaluation information always exists ********************************************************************/ Extensible_Theorem paramName_exists : forall P, IsP : is_param P -> exists N, paramName P N on IsP. [Show Proof] Theorem paramNames_exists : forall Ps, is_list is_param Ps -> exists Ns, paramNames Ps Ns. [Show Proof] Extensible_Theorem getFunEvalInfo_exists : forall F, IsF : is_fun F -> exists N R V P B, getFunEvalInfo F N R V P B on IsF. [Show Proof] Theorem getFunEvalCtx_exists : forall Fs, is_list is_fun Fs -> exists Ctx, getFunEvalCtx Fs Ctx. [Show Proof]