Module exactEval: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) | stmtExpr(stmt, expr) | recBuild(recFieldExprs) | recFieldAccess(expr, string) | errorExpr(expr, typ) /*errorExpr represents a failure case expr: string-typed error message expression typ: for proving typing properties*/ /*[string] is list of names used in the program thus far; lets us generate fresh names for extension constructs*/ Projection expr : [string] 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 exactEval: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 vars E V --------------------- [V-StmtExpr] vars stmtExpr(S, E) 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 /******************************************************************** Statement Names ********************************************************************/ /*names to ignore, stmt, other names referenced, new ignore*/ Judgment stmtNames : [[string]] stmt* [string] [[string]] /* Find the set of non-local names referenced in a statement, meaning the names declared outside it but used in it. The first argument is the scopes for names we want to ignore. This is used to ignore declarations within the statement. This basically finds the free variables in a statement. */ Judgment exprNames : [[string]] expr* [string] Fixed Judgment argsNames : [[string]] args [string] Fixed Judgment recFieldNames : [[string]] recFieldExprs [string] Fixed Judgment mems : A [[A]] Fixed Judgment not_mems : A [[A]] ------------------------- [SN-Noop] stmtNames Ctx noop [] Ctx stmtNames Ctx S1 N1 Ctx1 stmtNames Ctx1 S2 N2 Ctx2 N1 ++ N2 = N -------------------------------- [SN-Seq] stmtNames Ctx seq(S1, S2) N Ctx2 exprNames (Scope::Ctx) E N ------------------------------------------- [SN-Declare] {stmtNames (Scope::Ctx) declare(Ty, X, E) N ((X::Scope)::Ctx)} mems X Ctx exprNames Ctx E N -------------------------------- [SN-Assign-Ignore] stmtNames Ctx assign(X, E) N Ctx not_mems X Ctx exprNames Ctx E N ----------------------------------- [SN-Assign-Take] stmtNames Ctx assign(X, E) X::N Ctx /*assigning is use-ish*/ mems R Ctx exprNames Ctx E N ------------------------------------------- [SN-RecUpdate-Ignore] stmtNames Ctx recUpdate(R, Fields, E) N Ctx not_mems R Ctx exprNames Ctx E N ---------------------------------------------- [SN-RecUpdate-Take] stmtNames Ctx recUpdate(R, Fields, E) R::N Ctx exprNames Ctx C CN stmtNames []::Ctx T TN CtxT stmtNames []::Ctx F FN CtxF CN ++ TN = N1 N1 ++ FN = N --------------------------------------- [SN-IfThenElse] stmtNames Ctx ifThenElse(C, T, F) N Ctx exprNames Ctx Cond CN stmtNames []::Ctx Body BN CtxB CN ++ BN = N ------------------------------------- [SN-While] stmtNames Ctx while(Cond, Body) N Ctx stmtNames []::Ctx S N Ctx1 -------------------------------- [SN-ScopeStmt] stmtNames Ctx scopeStmt(S) N Ctx exprNames Ctx E N ------------------------------- [SN-PrintVal] stmtNames Ctx printVal(E) N Ctx ----------------------- [EN-Num] exprNames Ctx num(I) [] exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N ---------------------------- [EN-Plus] exprNames Ctx plus(E1, E2) N exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N ----------------------------- [EN-Minus] exprNames Ctx minus(E1, E2) N exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N ---------------------------- [EN-Mult] exprNames Ctx mult(E1, E2) N exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N --------------------------- [EN-Div] exprNames Ctx div(E1, E2) N --------------------- [EN-True] exprNames Ctx true [] ---------------------- [EN-False] exprNames Ctx false [] exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N --------------------------- [EN-And] exprNames Ctx and(E1, E2) N exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N -------------------------- [EN-Or] exprNames Ctx or(E1, E2) N exprNames Ctx E N ---------------------- [EN-Not] exprNames Ctx not(E) N exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N ------------------------------- [EN-Greater] exprNames Ctx greater(E1, E2) N exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N -------------------------- [EN-Eq] exprNames Ctx eq(E1, E2) N ----------------------------- [EN-String] exprNames Ctx stringLit(S) [] exprNames Ctx E1 N1 exprNames Ctx E2 N2 N1 ++ N2 = N --------------------------------- [EN-AppString] exprNames Ctx appString(E1, E2) N mems X Ctx /*in Ctx, so declared in relevant stmt*/ ------------------------ [EN-Name-Ignore] exprNames Ctx name(X) [] not_mems X Ctx /*not in Ctx, so declared outside*/ ------------------------- [EN-Name-Take] exprNames Ctx name(X) [X] argsNames Ctx Args N ----------------------------- [EN-Call] exprNames Ctx call(F, Args) N stmtNames []::Ctx S NS CtxS exprNames CtxS E NE NS ++ NE = N ------------------------------ [EN-StmtExpr] exprNames Ctx stmtExpr(S, E) N recFieldNames Ctx RF N ---------------------------- [EN-RecBuild] exprNames Ctx recBuild(RF) N exprNames Ctx E N ------------------------------------ [EN-RecFieldAccess] exprNames Ctx recFieldAccess(E, F) N exprNames Ctx E N -------------------------------- [EN-ErrorExpr] exprNames Ctx errorExpr(E, Ty) N ======================== [AN-Nil] argsNames Ctx nilArgs [] exprNames Ctx E EN argsNames Ctx A AN EN ++ AN = N ============================== [AN-Cons] argsNames Ctx consArgs(E, A) N ===================================== [RFN-Nil] recFieldNames Ctx nilRecFieldExprs [] exprNames Ctx E EN recFieldNames Ctx RF RN EN ++ RN = N =============================================== [RFN-Cons] recFieldNames Ctx consRecFieldExprs(F, E, RF) N ============= [NMems-Nil] not_mems X [] not_mem X S not_mems X Rest ================== [NMems-Cons] not_mems X S::Rest mem X S ============== [Mems-Here] mems X S::Rest mems X Rest ============== [Mems-Later] mems X S::Rest
Module exactEval: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 exactEval: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 stmtOK FC []::TC S TC1 /*stmt is a new scope, containing E*/ typeOf FC TC1 E Ty ------------------------------ [T-StmtExpr] typeOf FC TC stmtExpr(S, E) Ty 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 ********************************************************************/ /* At first glance, this primary component seems backward. It appears we should have it be that *value* forms cannot have their types redefined. However, in our language we are essentially disallowing extending value forms, as an expression and its projection need to evaluate to the same value. In order to have type preservation, we then need the old values forms produced by new constructs that may have new types also to have those new types. Having the type be the primary component here allows us to do that. */ 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 exactEval: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 in, expr, value, val env out, printed output*/ Judgment evalExpr : {[(string, (string, value, [string], stmt))] [[(string, value)]] expr* value [[(string, value)]] [value]} Judgment evalArgs : {[(string, (string, value, [string], stmt))] [[(string, value)]] args* [value] [[(string, value)]] [value]} Judgment evalRecFields : { [(string, (string, value, [string], stmt))] [[(string, value)]] recFieldExprs* [(string, value)] [[(string, value)]] [value]} 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) EE [] evalExpr FE EE E1 intVal(I1) EE1 O1 evalExpr FE EE1 E2 intVal(I2) EE2 O2 I1 + I2 = I O1 ++ O2 = O ------------------------------------------- [E-Plus] evalExpr FE EE plus(E1, E2) intVal(I) EE2 O evalExpr FE EE E1 intVal(I1) EE1 O1 evalExpr FE EE1 E2 intVal(I2) EE2 O2 I1 - I2 = I O1 ++ O2 = O -------------------------------------------- [E-Minus] evalExpr FE EE minus(E1, E2) intVal(I) EE2 O evalExpr FE EE E1 intVal(I1) EE1 O1 evalExpr FE EE1 E2 intVal(I2) EE2 O2 I1 * I2 = I O1 ++ O2 = O ------------------------------------------- [E-Mult] evalExpr FE EE mult(E1, E2) intVal(I) EE2 O evalExpr FE EE E1 intVal(I1) EE1 O1 evalExpr FE EE1 E2 intVal(I2) EE2 O2 I1 / I2 = I O1 ++ O2 = O ------------------------------------------ [E-Div] evalExpr FE EE div(E1, E2) intVal(I) EE2 O --------------------------------- [E-True] evalExpr FE EE true trueVal EE [] ----------------------------------- [E-False] evalExpr FE EE false falseVal EE [] evalExpr FE EE E1 trueVal EE1 O1 evalExpr FE EE1 E2 trueVal EE2 O2 O1 ++ O2 = O ---------------------------------------- [E-And-True] evalExpr FE EE and(E1, E2) trueVal EE2 O evalExpr FE EE E1 falseVal EE1 O ----------------------------------------- [E-And-False1] evalExpr FE EE and(E1, E2) falseVal EE1 O evalExpr FE EE E1 trueVal EE1 O1 evalExpr FE EE1 E2 falseVal EE2 O2 O1 ++ O2 = O ----------------------------------------- [E-And-False2] evalExpr FE EE and(E1, E2) falseVal EE2 O evalExpr FE EE E1 trueVal EE1 O --------------------------------------- [E-Or-True1] evalExpr FE EE or(E1, E2) trueVal EE1 O evalExpr FE EE E1 falseVal EE1 O1 evalExpr FE EE1 E2 trueVal EE2 O2 O1 ++ O2 = O --------------------------------------- [E-Or-True2] evalExpr FE EE or(E1, E2) trueVal EE2 O evalExpr FE EE E1 falseVal EE1 O1 evalExpr FE EE1 E2 falseVal EE2 O2 O1 ++ O2 = O ---------------------------------------- [E-Or-False] evalExpr FE EE or(E1, E2) falseVal EE2 O evalExpr FE EE E falseVal EE1 O ----------------------------------- [E-Not-True] evalExpr FE EE not(E) trueVal EE1 O evalExpr FE EE E trueVal EE1 O ------------------------------------ [E-Not-False] evalExpr FE EE not(E) falseVal EE1 O evalExpr FE EE E1 intVal(I1) EE1 O1 evalExpr FE EE1 E2 intVal(I2) EE2 O2 I1 > I2 O1 ++ O2 = O -------------------------------------------- [E-Greater-True] evalExpr FE EE greater(E1, E2) trueVal EE2 O evalExpr FE EE E1 intVal(I1) EE1 O1 evalExpr FE EE1 E2 intVal(I2) EE2 O2 I1 <= I2 O1 ++ O2 = O --------------------------------------------- [E-Greater-False] evalExpr FE EE greater(E1, E2) falseVal EE2 O evalExpr FE EE E1 V EE1 O1 evalExpr FE EE1 E2 V EE2 O2 O1 ++ O2 = O --------------------------------------- [E-Eq-True] evalExpr FE EE eq(E1, E2) trueVal EE2 O evalExpr FE EE E1 V1 EE1 O1 evalExpr FE EE1 E2 V2 EE2 O2 V1 != V2 O1 ++ O2 = O ---------------------------------------- [E-Eq-False] evalExpr FE EE eq(E1, E2) falseVal EE2 O ---------------------------------------------- [E-String] evalExpr FE EE stringLit(S) stringVal(S) EE [] evalExpr FE EE E1 stringVal(S1) EE1 O1 evalExpr FE EE1 E2 stringVal(S2) EE2 O2 S1 ++ S2 = S O1 ++ O2 = O --------------------------------------------------- [E-AppString] evalExpr FE EE appString(E1, E2) stringVal(S) EE2 O lookupScopes X EE V ------------------------------ [E-Name] evalExpr FE EE name(X) V EE [] lookup FE Fun (RetVar, RVVal, ArgNames, Body) evalArgs FE EE Args ArgVals EE1 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 EE1 O evalStmt FE []::EE S EE1 O1 evalExpr FE EE1 E V Scope::EE2 O2 /*drop added scope*/ O1 ++ O2 = O ------------------------------------- [E-StmtExpr] evalExpr FE EE stmtExpr(S, E) V EE2 O evalRecFields FE EE RF VF EE1 O -------------------------------------------- [E-RecBuild] evalExpr FE EE recBuild(RF) recVal(VF) EE1 O evalExpr FE EE Rec recVal(Fields) EE1 O lookup Fields F V --------------------------------------------- [E-RecAccess] evalExpr FE EE recFieldAccess(Rec, F) V EE1 O Extensibella_Stand_In { names EE Names Names |{expr}- E ~~> E_P evalExpr FE EE E_P V_P EE_P O_P ------------------------------- [E-Expr-Q] evalExpr FE EE E V EE1 O } /*Arguments*/ ------------------------------- [EA-Nil] evalArgs FE EE nilArgs [] EE [] evalExpr FE EE E V EE1 O1 evalArgs FE EE1 Rest VRest EE2 O2 O1 ++ O2 = O ----------------------------------------------- [EA-Cons] evalArgs FE EE consArgs(E, Rest) V::VRest EE2 O /*No Extensibella stand-in rule because the args type isn't intended to be extended*/ /*Record Fields*/ --------------------------------------------- [ERF-Nil] evalRecFields FE EE nilRecFieldExprs [] EE [] evalExpr FE EE E V EE1 O1 evalRecFields FE EE1 Rest VRest EE2 O2 O1 ++ O2 = O -------------------------------------------------- [ERF-Cons] {evalRecFields FE EE consRecFieldExprs(F, E, Rest) (F, V)::VRest EE2 O} /*recFields isn't intended to be extended either*/ /******************************************************************** 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 EE E V Scope::EE1 O ------------------------------------------------------- [E-Declare] evalStmt FE EE declare(Ty, X, E) ((X, V)::Scope)::EE1 O evalExpr FE EE E V EE1 O replaceScopes X V EE1 EE2 /*find and replace value*/ --------------------------------- [E-Assign] evalStmt FE EE assign(X, E) EE2 O evalExpr FE EE E V EE1 O lookupScopes Rec EE recVal(FieldVals) updateRecFields Fields V FieldVals NewVals replaceScopes Rec recVal(NewVals) EE1 EE2 /*find and replace value*/ ---------------------------------------------- [E-RecUpdate] evalStmt FE EE recUpdate(Rec, Fields, E) EE2 O evalExpr FE EE Cond trueVal EE1 O1 evalStmt FE []::EE1 Th Scope::EE2 O2 O1 ++ O2 = O --------------------------------------------- [E-If-True] evalStmt FE EE ifThenElse(Cond, Th, El) EE2 O evalExpr FE EE Cond falseVal EE1 O1 evalStmt FE []::EE1 El Scope::EE2 O2 O1 ++ O2 = O --------------------------------------------- [E-If-False] evalStmt FE EE ifThenElse(Cond, Th, El) EE2 O evalExpr FE EE Cond trueVal EE1 O1 evalStmt FE []::EE1 Body Scope::EE2 O2 evalStmt FE EE2 while(Cond, Body) EE3 O3 O1 ++ O2 = O12 O12 ++ O3 = O ---------------------------------------- [E-While-True] evalStmt FE EE while(Cond, Body) EE3 O evalExpr FE EE Cond falseVal EE1 O -------------------------------------- [E-While-False] evalStmt FE EE while(Cond, Body) EE1 O evalStmt FE []::EE S Scope::EE1 O --------------------------------- [E-ScopeStmt] evalStmt FE EE scopeStmt(S) EE1 O evalExpr FE EE E intVal(I) EE1 O1 O1 ++ [intVal(I)] = O --------------------------------- [E-Print-Int] evalStmt FE EE printVal(E) EE1 O evalExpr FE EE E trueVal EE1 O1 O1 ++ [trueVal] = O -------------------------------- [E-Print-True] evalStmt FE EE printVal(E) EE1 O evalExpr FE EE E falseVal EE1 O1 O1 ++ [falseVal] = O -------------------------------- [E-Print-False] evalStmt FE EE printVal(E) EE1 O evalExpr FE EE E stringVal(S) EE1 O1 O1 ++ [stringVal(S)] = O ------------------------------------ [E-Print-String] evalStmt FE EE printVal(E) EE1 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 recVal(Fields) /*find 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
Click on a command or tactic to see a detailed view of its use.
Module exactEval: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 L1 L2 E E1 E2, PrA : L1 |{expr}- E ~~> E1 -> PrB : L2 |{expr}- E ~~> E2 -> IsE : is_expr E -> 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) -> E1 = E2. Projection_Constraint proj_expr_is : forall L E E', Pr : L |{expr}- E ~~> E' -> IsE : is_expr E -> IsL : is_list is_string L -> is_expr E'. Projection_Constraint proj_expr_other : forall L E E' L', Pr : L |{expr}- E ~~> E' -> IsE : is_expr E -> IsL : is_list is_string L -> IsL' : is_list is_string L' -> exists E'', L' |{expr}- E ~~> 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'. /******************************************************************** ____ _ _ _ _ | _ \ ___ ___(_) __| | __ _| |__ | | ___ | | | |/ _ \/ __| |/ _` |/ _` | '_ \| |/ _ \ | |_| | __/ (__| | (_| | (_| | |_) | | __/ |____/ \___|\___|_|\__,_|\__,_|_.__/|_|\___| _____ _ _ _ | ____|__ _ _ _ __ _| (_) |_ _ _ | _| / _` | | | |/ _` | | | __| | | | | |__| (_| | |_| | (_| | | | |_| |_| | |_____\__, |\__,_|\__,_|_|_|\__|\__, | |_| |___/ 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, is_stmt S. Ext_Ind forall E, is_expr E; forall A, is_args A; forall RF, is_recFieldExprs RF; 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] /* We do not have decidable equality for expressions, arguments, record fields, or statements because they are all dependent on types. The problem there is that extensions need to have properties that, e.g., an expression has the form of a new constructor or not, and these properties need to use the is relation as the key relation. Thus we need Ext_Ind for all the is relations. This is a problem for the typing one as extensions may find it useful to introduce new types that project to recursive record types (e.g. our list extension's list type projects to a record type containing the list type) and thus we cannot prove Ext_Ind for it, as we need a derivation of <is_typ {P}> for listTy(T) in order to build a derivation of <is_typ {P}> for listTy(T). Then we cannot prove decidable equality for most things as we cannot prove the auxiliary things we need to do so. */ /******************************************************************** ____ / ___| ___ ___ _ __ ___ ___ \___ \ / __/ _ \| '_ \ / _ \/ __| ___) | (_| (_) | |_) | __/\__ \ |____/ \___\___/| .__/ \___||___/ |_| 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] /******************************************************************** _____ _ _ _ / ____| | | | | | | (___ | |_ __ _| |_ ___ _ __ ___ ___ _ __ | |_ \___ \| __/ _` | __/ _ \ '_ ` _ \ / _ \ '_ \| __| ____) | || (_| | || __/ | | | | | __/ | | | |_ |_____/ \__\__,_|\__\___|_| |_| |_|\___|_| |_|\__| | \ | | | \| | __ _ _ __ ___ ___ ___ | . ` |/ _` | '_ ` _ \ / _ \/ __| | |\ | (_| | | | | | | __/\__ \ |_| \_|\__,_|_| |_| |_|\___||___/ Statement Names ********************************************************************/ /******************************************************************** Statement names is ********************************************************************/ Extensible_Theorem stmtNames_is : forall Ctx S N Ctx', IsS : is_stmt S -> IsCtx : is_list (is_list is_string) Ctx -> SN : stmtNames Ctx S N Ctx' -> is_list is_string N on SN as IH_S, stmtNames_isCtx : forall Ctx S N Ctx', IsS : is_stmt S -> IsCtx : is_list (is_list is_string) Ctx -> SN : stmtNames Ctx S N Ctx' -> is_list (is_list is_string) Ctx' on SN as IH_S_C, exprNames_is : forall Ctx E N, IsE : is_expr E -> IsCtx : is_list (is_list is_string) Ctx -> EN : exprNames Ctx E N -> is_list is_string N on EN as IH_E also argsNames_is : forall Ctx A N, IsA : is_args A -> IsCtx : is_list (is_list is_string) Ctx -> AN : argsNames Ctx A N -> is_list is_string N on AN as IH_A, recFieldNames_is : forall Ctx RF N, IsRF : is_recFieldExprs RF -> IsCtx : is_list (is_list is_string) Ctx -> RFN : recFieldNames Ctx RF N -> is_list is_string N on RFN as IH_RF. [Show Proof] /******************************************************************** Statement names unique ********************************************************************/ Theorem not_mems[A] : forall LS (A : A), not_mems A LS -> mems A LS -> false. [Show Proof] Extensible_Theorem stmtNames_unique : forall Ctx S NA CtxA NB CtxB, IsS : is_stmt S -> IsCtx : is_list (is_list is_string) Ctx -> SNA : stmtNames Ctx S NA CtxA -> SNB : stmtNames Ctx S NB CtxB -> NA = NB /\ CtxA = CtxB on SNA as IH_S, exprNames_unique : forall Ctx E NA NB, IsE : is_expr E -> IsCtx : is_list (is_list is_string) Ctx -> ENA : exprNames Ctx E NA -> ENB : exprNames Ctx E NB -> NA = NB on ENA as IH_E also argsNames_unique : forall Ctx A NA NB, IsA : is_args A -> IsCtx : is_list (is_list is_string) Ctx -> ANA : argsNames Ctx A NA -> ANB : argsNames Ctx A NB -> NA = NB on ANA as IH_A, recFieldNames_unique : forall Ctx RF NA NB, IsRF : is_recFieldExprs RF -> IsCtx : is_list (is_list is_string) Ctx -> RFNA : recFieldNames Ctx RF NA -> RFNB : recFieldNames Ctx RF NB -> NA = NB on RFNA as IH_RF. [Show Proof] /******************************************************************** Statement names doesn't modify existing parts of the context ********************************************************************/ Extensible_Theorem stmtNames_keep_older : forall Scope Ctx S N Ctx', IsS : is_stmt S -> IsCtx : is_list (is_list is_string) (Scope::Ctx) -> SN : stmtNames (Scope::Ctx) S N Ctx' -> exists Scope', Ctx' = Scope'::Ctx /\ (forall X, mem X Scope -> mem X Scope') on SN. [Show Proof] /******************************************************************** Statement names exists ********************************************************************/ Theorem mems_or_not_mems : forall LS X, is_list (is_list is_string) LS -> is_string X -> mems X LS \/ not_mems X LS. [Show Proof] Extensible_Theorem stmtNames_exists : forall Scope Ctx S, IsS : is_stmt S -> %need a scope on the front for declare IsCtx : is_list (is_list is_string) (Scope::Ctx) -> exists N Ctx', stmtNames (Scope::Ctx) S N Ctx' on IsS as IH_S, exprNames_exists : forall Ctx E, IsE : is_expr E -> IsCtx : is_list (is_list is_string) Ctx -> exists N, exprNames Ctx E N on IsE as IH_E, argsNames_exists : forall Ctx A, IsA : is_args A -> IsCtx : is_list (is_list is_string) Ctx -> exists N, argsNames Ctx A N on IsA as IH_A, recFieldNames_exists : forall Ctx RF, IsRF : is_recFieldExprs RF -> IsCtx : is_list (is_list is_string) Ctx -> exists N, recFieldNames Ctx RF N on IsRF as IH_RF. [Show Proof] /******************************************************************** Statement names not in ctx ********************************************************************/ Extensible_Theorem stmtNames_not_in_ctx : forall Scope Ctx S N Ctx' X, IsS : is_stmt S -> IsCtx : is_list (is_list is_string) (Scope::Ctx) -> SN : stmtNames (Scope::Ctx) S N Ctx' -> MemN : mem X N -> MemsCtx : mems X (Scope::Ctx) -> false on SN as IH_S, exprNames_not_in_ctx : forall Ctx E N X, IsE : is_expr E -> IsCtx : is_list (is_list is_string) Ctx -> EN : exprNames Ctx E N -> MemN : mem X N -> MemsCtx : mems X Ctx -> false on EN as IH_E also argsNames_not_in_ctx : forall Ctx A N X, IsA : is_args A -> IsCtx : is_list (is_list is_string) Ctx -> AN : argsNames Ctx A N -> MemN : mem X N -> MemsCtx : mems X Ctx -> false on AN as IH_A, recFieldNames_not_in_ctx : forall Ctx RF N X, IsRF : is_recFieldExprs RF -> IsCtx : is_list (is_list is_string) Ctx -> RFN : recFieldNames Ctx RF N -> MemN : mem X N -> MemsCtx : mems X Ctx -> false on RFN as IH_RF. [Show Proof] /******************************************************************** Statement names only depend on context members, not order ********************************************************************/ Extensible_Theorem stmtNames_relatedCtxs : forall ScopeA CtxA S N CtxA' ScopeB CtxB, IsS : is_stmt S -> IsCtxA : is_list (is_list is_string) (ScopeA::CtxA) -> IsCtxB : is_list (is_list is_string) (ScopeB::CtxB) -> RelAB : (forall X, mems X (ScopeA::CtxA) -> mems X (ScopeB::CtxB)) -> RelBA : (forall X, mems X (ScopeB::CtxB) -> mems X (ScopeA::CtxA)) -> SN : stmtNames (ScopeA::CtxA) S N CtxA' -> exists CtxB', stmtNames (ScopeB::CtxB) S N CtxB' on SN as IH_S, %The names on these for SNA and SNB are actually the same, as shown %by stmtNames_relatedCtxs and stmtNames_unique together, but it is %easier to prove this way stmtNames_relatedCtxs_ctx_fwd : forall CtxA S NA CtxA' CtxB NB CtxB' X, IsS : is_stmt S -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> SNA : stmtNames CtxA S NA CtxA' -> SNB : stmtNames CtxB S NB CtxB' -> Mems : mems X CtxA' -> mems X CtxB' on SNA as IH_S_CAB, stmtNames_relatedCtxs_ctx_back : forall CtxA S NA CtxA' CtxB NB CtxB' X, IsS : is_stmt S -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelBA : (forall X, mems X CtxB -> mems X CtxA) -> SNA : stmtNames CtxA S NA CtxA' -> SNB : stmtNames CtxB S NB CtxB' -> Mems : mems X CtxB' -> mems X CtxA' on SNA as IH_S_CBA, exprNames_relatedCtxs : forall CtxA CtxB E N, IsE : is_expr E -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> RelBA : (forall X, mems X CtxB -> mems X CtxA) -> EN : exprNames CtxA E N -> exprNames CtxB E N on EN as IH_E also argsNames_relatedCtxs : forall CtxA CtxB A N, IsA : is_args A -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> RelBA : (forall X, mems X CtxB -> mems X CtxA) -> AN : argsNames CtxA A N -> argsNames CtxB A N on AN as IH_A, recFieldNames_relatedCtxs : forall CtxA CtxB RF N, IsRF : is_recFieldExprs RF -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> RelBA : (forall X, mems X CtxB -> mems X CtxA) -> RFN : recFieldNames CtxA RF N -> recFieldNames CtxB RF N on RFN as IH_RF. [Show Proof] /******************************************************************** Statement names with larger contexts only removes some names ********************************************************************/ Extensible_Theorem stmtNames_increaseCtxs : forall ScopeA CtxA S NA CtxA' ScopeB CtxB NB CtxB' X, IsS : is_stmt S -> IsCtxA : is_list (is_list is_string) (ScopeA::CtxA) -> IsCtxB : is_list (is_list is_string) (ScopeB::CtxB) -> RelAB : (forall X, mems X (ScopeA::CtxA) -> mems X (ScopeB::CtxB)) -> SNA : stmtNames (ScopeA::CtxA) S NA CtxA' -> SNB : stmtNames (ScopeB::CtxB) S NB CtxB' -> M : mem X NB -> mem X NA on SNA as IH_S, stmtNames_increaseCtxs_ctxs : forall ScopeA CtxA S NA CtxA' ScopeB CtxB NB CtxB' X, IsS : is_stmt S -> IsCtxA : is_list (is_list is_string) (ScopeA::CtxA) -> IsCtxB : is_list (is_list is_string) (ScopeB::CtxB) -> RelAB : (forall X, mems X (ScopeA::CtxA) -> mems X (ScopeB::CtxB)) -> SNA : stmtNames (ScopeA::CtxA) S NA CtxA' -> SNB : stmtNames (ScopeB::CtxB) S NB CtxB' -> M : mems X CtxA' -> mems X CtxB' on SNA as IH_S_C, exprNames_increaseCtxs : forall CtxA E NA CtxB NB X, IsE : is_expr E -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> ENA : exprNames CtxA E NA -> ENB : exprNames CtxB E NB -> M : mem X NB -> mem X NA on ENA as IH_E also argsNames_increaseCtxs : forall CtxA A NA CtxB NB X, IsA : is_args A -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> ANA : argsNames CtxA A NA -> ANB : argsNames CtxB A NB -> M : mem X NB -> mem X NA on ANA as IH_A, recFieldNames_increaseCtxs : forall CtxA RF NA CtxB NB X, IsRF : is_recFieldExprs RF -> IsCtxA : is_list (is_list is_string) CtxA -> IsCtxB : is_list (is_list is_string) CtxB -> RelAB : (forall X, mems X CtxA -> mems X CtxB) -> RFNA : recFieldNames CtxA RF NA -> RFNB : recFieldNames CtxB RF NB -> M : mem X NB -> mem X NA on RFNA as IH_RF. [Show Proof] /******************************************************************** Statement names are related across projection ********************************************************************/ /* These projection constraints ensure projections only use existing names and new names they introduce, not random new names. */ Projection_Constraint proj_exprNames : forall Names E E_P Ctx N N_P X, Pr : Names |{expr}- E ~~> E_P -> IsE : is_expr E -> IsNames : is_list is_string Names -> IsCtx : is_list (is_list is_string) Ctx -> EN : exprNames Ctx E N -> EN_P : exprNames Ctx E_P N_P -> M : mem X N_P -> mem X N. Projection_Constraint proj_stmtNames : forall Names S S_P Scope Ctx N Ctx' N_P Ctx'_P X, Pr : Names |{stmt}- S ~~> S_P -> IsS : is_stmt S -> IsNames : is_list is_string Names -> IsCtx : is_list (is_list is_string) (Scope::Ctx) -> SN : stmtNames (Scope::Ctx) S N Ctx' -> SN_P : stmtNames (Scope::Ctx) S_P N_P Ctx'_P -> M : mem X N_P -> mem X N. /* These two ensure projections only introduce the same new names as the originals, and all the same names. */ Projection_Constraint proj_stmtNames_names_forward : forall Names S S_P Scope Ctx N Ctx' N_P Ctx'_P X, Pr : Names |{stmt}- S ~~> S_P -> IsS : is_stmt S -> IsNames : is_list is_string Names -> IsCtx : is_list (is_list is_string) (Scope::Ctx) -> SN : stmtNames (Scope::Ctx) S N Ctx' -> SN_P : stmtNames (Scope::Ctx) S_P N_P Ctx'_P -> M : mems X Ctx' -> mems X Ctx'_P. Projection_Constraint proj_stmtNames_names_backward : forall Names S S_P Scope Ctx N Ctx' N_P Ctx'_P X, Pr : Names |{stmt}- S ~~> S_P -> IsS : is_stmt S -> IsNames : is_list is_string Names -> IsCtx : is_list (is_list is_string) (Scope::Ctx) -> SN : stmtNames (Scope::Ctx) S N Ctx' -> SN_P : stmtNames (Scope::Ctx) S_P N_P Ctx'_P -> M : mems X Ctx'_P -> mems X Ctx'. /******************************************************************** _____ _ |_ _| _ _ __ (_)_ __ __ _ | || | | | '_ \| | '_ \ / _` | | || |_| | |_) | | | | | (_| | |_| \__, | .__/|_|_| |_|\__, | |___/|_| |___/ 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, 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 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] /******************************************************************** 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, 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 as IH_S 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] /******************************************************************** 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 /\ is_string X. [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] 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_isCtx : forall FE EE 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 EE' O -> is_list (is_list (is_pair is_string is_value)) EE' on Ev as IH_C_E, evalExpr_isValue : forall FE EE 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 EE' 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_isCtx : forall FE EE 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 EE' O -> is_list (is_list (is_pair is_string is_value)) EE' on Ev as IH_C_A, evalArgs_isValue : forall FE EE 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 EE' O -> is_list is_value V on Ev as IH_V_A, evalRecFields_isCtx : forall FE EE 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 EE' O -> is_list (is_list (is_pair is_string is_value)) EE' on Ev as IH_C_RF, evalRecFields_isValue : forall FE EE 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 EE' 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 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 EE' 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 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 EE' O -> is_list is_value O on Ev as IH_A, evalRecFields_isOutput : forall FE EE 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 EE' 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 the context, or at % least older scopes for stmts %This will be important for extension evaluation and projection, % showing fresh_names still holds after evaluating one term Extensible_Theorem evalExpr_names_same : forall E FE EE V EE' 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 EE' O -> names_same EE EE' on Ev as IH_E, 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, evalArgs_names_same : forall A FE EE V EE' 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 EE' O -> names_same EE EE' on Ev as IH_A, evalRecFields_names_same : forall RF FE EE V EE' 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 EE' O -> names_same EE EE' on Ev as IH_RF. [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 evalExpr_keep_scopes : forall FE EE E EE' V O N, 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 V EE' O -> length EE N -> length EE' N. [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] Theorem evalArgs_keep_scopes : forall FE EE A EE' Vs O N, 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 Vs EE' O -> length EE N -> length EE' N. [Show Proof] Theorem evalRecFields_keep_scopes : forall FE EE RF EE' F O N, 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 F EE' O -> length EE N -> length EE' N. [Show Proof] /******************************************************************** Evaluation unique ********************************************************************/ 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, 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] Extensible_Theorem evalExpr_newNameScopes : forall FE EE_A EE_B E VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalExpr FE EE_B E VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> VA = VB on EvA as IH_V_E, evalExpr_newNameScopes_output : forall FE EE_A EE_B E VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalExpr FE EE_B E VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> O_A = O_B on EvA as IH_O_E, evalExpr_newNameScopes_ctx : forall FE EE_A EE_B E VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalExpr FE EE_B E VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> newNameScopes N Len EE_A' EE_B' on EvA as IH_C_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_newNameScopes : forall FE EE_A EE_B A VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalArgs FE EE_B A VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> VA = VB on EvA as IH_V_A, evalArgs_newNameScopes_output : forall FE EE_A EE_B A VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalArgs FE EE_B A VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> O_A = O_B on EvA as IH_O_A, evalArgs_newNameScopes_ctx : forall FE EE_A EE_B A VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalArgs FE EE_B A VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> newNameScopes N Len EE_A' EE_B' on EvA as IH_C_A, evalRecFields_newNameScopes : forall FE EE_A EE_B RF VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalRecFields FE EE_B RF VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> VA = VB on EvA as IH_V_RF, evalRecFields_newNameScopes_output : forall FE EE_A EE_B RF VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalRecFields FE EE_B RF VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> O_A = O_B on EvA as IH_O_RF, evalRecFields_newNameScopes_ctx : forall FE EE_A EE_B RF VA VB EE_A' EE_B' O_A O_B N Len, 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 EE_A' O_A -> EvB : evalRecFields FE EE_B RF VB EE_B' O_B -> NNS : newNameScopes N Len EE_A EE_B -> newNameScopes N Len EE_A' EE_B' on EvA as IH_C_RF. [Show Proof] /******************************************************************** Evaluation is Unique ********************************************************************/ Theorem evalExpr_unique : forall FE EE E VA EE_A OA VB EE_B 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 EE_A OA -> evalExpr FE EE E VB EE_B OB -> VA = VB /\ EE_A = EE_B /\ 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 EE_A OA VB EE_B 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 EE_A OA -> evalArgs FE EE A VB EE_B OB -> VA = VB /\ EE_A = EE_B /\ OA = OB. [Show Proof] Theorem evalRecFields_unique : forall FE EE RF VA EE_A OA VB EE_B 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 EE_A OA -> evalRecFields FE EE RF VB EE_B OB -> VA = VB /\ EE_A = EE_B /\ OA = OB. [Show Proof] /******************************************************************** Extension size versions of evaluation ********************************************************************/ Ext_Size evalExpr FE EE E V EE' O, evalArgs FE EE E V EE' O, evalRecFields FE EE E F EE' O, evalStmt FE EE S EE' O. Proj_Rel evalExpr FE EE E V EE' O, evalArgs FE EE E V EE' O, evalRecFields FE EE E F EE' 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_newNameScopes_exists_ES : forall FE EE_A EE_B E V EE_B' O N Len ES, 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 EE_B' O ES -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_A', <evalExpr {ES}> FE EE_A E V EE_A' 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_newNameScopes_exists_ES : forall FE EE_A EE_B A V EE_B' O N Len ES, 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 EE_B' O ES -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_A', <evalArgs {ES}> FE EE_A A V EE_A' O ES on EvB as IH_A, evalRecFields_newNameScopes_exists_ES : forall FE EE_A EE_B RF V EE_B' O N Len ES, 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 EE_B' O ES -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_A', <evalRecFields {ES}> FE EE_A RF V EE_A' O ES on EvB as IH_RF. [Show Proof] Theorem evalExpr_newNameScopes_exists : forall FE EE_A EE_B E V EE_B' O N Len, 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 EE_B' O -> newNameScopes N Len EE_A EE_B -> exists EE_A', evalExpr FE EE_A E V EE_A' 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_newNameScopes_exists : forall FE EE_A EE_B A V EE_B' O N Len, 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 EE_B' O -> newNameScopes N Len EE_A EE_B -> exists EE_A', evalArgs FE EE_A A V EE_A' O. [Show Proof] Theorem evalRecFields_newNameScopes_exists : forall FE EE_A EE_B RF V EE_B' O N Len, 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 EE_B' O -> newNameScopes N Len EE_A EE_B -> exists EE_A', evalRecFields FE EE_A RF V EE_A' O. [Show Proof] /******************************************************************** Evaluation back across newNameScopes ********************************************************************/ /* If we have A and B where we have `newNameScopes S Len A B` and a term evaluates under A, we also want to say it evaluates under B. However, this is not true in general as the term might use a variable introduced in the new scopes in A. To say this isn't possible, we specify all the names occurring in a term are in B using ctx_names and stmtNames (or the related relations for other types). We will use this for projection constraints requiring evaluation of originals when projections evaluate. */ Define ctx_names : list (list (pair K I)) -> list (list K) -> prop by ctx_names [] []; ctx_names (A::ARest) (B::BRest) := (forall K I, mem (K, I) A -> mem K B) /\ (forall K, mem K B -> exists I, mem (K, I) A) /\ ctx_names ARest BRest. Theorem ctx_names_add[K, I] : forall A B AS BS (K : K) (I : I), ctx_names (AS::A) (BS::B) -> ctx_names (((K, I)::AS)::A) ((K::BS)::B). [Show Proof] Theorem ctx_names_add_scope[K, I] : forall (A : list (list (pair K I))) B, ctx_names A B -> ctx_names ([]::A) ([]::B). [Show Proof] Theorem ctx_names_lookupScopes[K, I] : forall A B (K : K) (I : I), ctx_names A B -> lookupScopes K A I -> mems K B. [Show Proof] Theorem ctx_names_replaceScopes : forall A B X V A', is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list is_string) B -> ctx_names A B -> replaceScopes X V A A' -> ctx_names A' B. [Show Proof] Extensible_Theorem evalExpr_ctx_names : forall FE EE E V EE' O Ctx N, 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 -> IsCtx : is_list (is_list is_string) Ctx -> Ctxs : ctx_names EE Ctx -> EN : exprNames Ctx E N -> Ev : evalExpr FE EE E V EE' O -> ctx_names EE' Ctx on Ev as IH_E, evalStmt_ctx_names : forall FE EE S EE' O Ctx Ctx' N, 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 -> IsCtx : is_list (is_list is_string) Ctx -> Ctxs : ctx_names EE Ctx -> SN : stmtNames Ctx S N Ctx' -> Ev : evalStmt FE EE S EE' O -> ctx_names EE' Ctx' on Ev as IH_S, evalArgs_ctx_names : forall FE EE A V EE' O Ctx N, 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 -> IsCtx : is_list (is_list is_string) Ctx -> Ctxs : ctx_names EE Ctx -> AN : argsNames Ctx A N -> Ev : evalArgs FE EE A V EE' O -> ctx_names EE' Ctx on Ev as IH_A, evalRecFields_ctx_names : forall FE EE RF V EE' O Ctx N, 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 -> IsCtx : is_list (is_list is_string) Ctx -> Ctxs : ctx_names EE Ctx -> RFN : recFieldNames Ctx RF N -> Ev : evalRecFields FE EE RF V EE' O -> ctx_names EE' Ctx on Ev as IH_RF. [Show Proof] Theorem ctx_names_names[K, I] : forall (A : list (list (pair K I))) Names Ctx X, ctx_names A Ctx -> names A Names -> mems X Ctx -> mem X Names. [Show Proof] Theorem newNameScopes_ctx_names_lookupScopes [V] : forall N Len A B Ctx X (V : V), newNameScopes N Len A B -> ctx_names B Ctx -> mems X Ctx -> lookupScopes X A V -> lookupScopes X B V. [Show Proof] Theorem newNameScopes_replaceScopes_back : forall S Len A B X V RA Ctx, 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 -> ctx_names B Ctx -> mems X Ctx -> newNameScopes S Len A B -> replaceScopes X V A RA -> exists RB, replaceScopes X V B RB. [Show Proof] %ctx_names and empty names ensures all names are in EE_B or declared % in the term being evaluated %if we assume the term is well-typed under the scopes of EE_B, this is % a valid assumption Extensible_Theorem evalExpr_newNameScopes_exists_back : forall FE EE_A EE_B E V Ctx EE_A' O N Len, 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 -> IsCtx : is_list (is_list is_string) Ctx -> %---------- Ctxs : ctx_names EE_B Ctx -> EN : exprNames Ctx E [] -> %---------- EvA : evalExpr FE EE_A E V EE_A' O -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_B', evalExpr FE EE_B E V EE_B' O on EvA as IH_E, evalStmt_newNameScopes_exists_back : forall FE EE_A EE_B S Ctx Ctx' EE_A' O 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) -> IsCtx : is_list (is_list is_string) Ctx -> %---------- Ctxs : ctx_names (Scope::EE_B) Ctx -> SN : stmtNames Ctx S [] Ctx' -> %---------- EvA : evalStmt FE (Scope::EE_A) S EE_A' O -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_B', evalStmt FE (Scope::EE_B) S EE_B' O on EvA as IH_S, evalArgs_newNameScopes_exists_back : forall FE EE_A EE_B A V Ctx EE_A' O N Len, 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 -> IsCtx : is_list (is_list is_string) Ctx -> %---------- Ctxs : ctx_names EE_B Ctx -> AN : argsNames Ctx A [] -> %---------- EvA : evalArgs FE EE_A A V EE_A' O -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_B', evalArgs FE EE_B A V EE_B' O on EvA as IH_A, evalRecFields_newNameScopes_exists_back : forall FE EE_A EE_B RF V Ctx EE_A' O N Len, 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 -> IsCtx : is_list (is_list is_string) Ctx -> %---------- Ctxs : ctx_names EE_B Ctx -> RFN : recFieldNames Ctx RF [] -> %---------- EvA : evalRecFields FE EE_A RF V EE_A' O -> NNS : newNameScopes N Len EE_A EE_B -> exists EE_B', evalRecFields FE EE_B RF V EE_B' O on EvA as IH_RF. [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 EE_A' OA EE_B VB EE_B' 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 EE_A' OA -> EvB : evalExpr FE EE_B E VB EE_B' OB -> VA = VB /\ OA = OB on EvA as IH_E, evalExpr_scopes_same_ctx : forall E FE EE_A VA EE_A' OA EE_B VB EE_B' 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 EE_A' OA -> EvB : evalExpr FE EE_B E VB EE_B' OB -> scopes_same EE_A' EE_B' on EvA as IH_E_C, 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 EE_A' OA EE_B VB EE_B' 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 EE_A' OA -> EvB : evalArgs FE EE_B A VB EE_B' OB -> VA = VB /\ OA = OB on EvA as IH_A, evalArgs_scopes_same_ctx : forall A FE EE_A VA EE_A' OA EE_B VB EE_B' 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 EE_A' OA -> EvB : evalArgs FE EE_B A VB EE_B' OB -> scopes_same EE_A' EE_B' on EvA as IH_A_C, evalRecFields_scopes_same : forall RF FE EE_A VA EE_A' OA EE_B VB EE_B' 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 EE_A' OA -> EvB : evalRecFields FE EE_B RF VB EE_B' OB -> VA = VB /\ OA = OB on EvA as IH_RF, evalRecFields_scopes_same_ctx : forall RF FE EE_A VA EE_A' OA EE_B VB EE_B' 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 EE_A' OA -> EvB : evalRecFields FE EE_B RF VB EE_B' OB -> scopes_same EE_A' EE_B' on EvA as IH_RF_C. [Show Proof] Extensible_Theorem evalExpr_scopes_same_exists : forall E FE EE_A V EE_A' 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 EE_A' O -> exists EE_B', evalExpr FE EE_B E V EE_B' 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 EE_A' 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 EE_A' O -> exists EE_B', evalArgs FE EE_B A V EE_B' O on EvA as IH_A, evalRecFields_scopes_same_exists : forall RF FE EE_A V EE_A' 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 EE_A' O -> exists EE_B', evalRecFields FE EE_B RF V EE_B' O on EvA as IH_RF. [Show Proof] /******************************************************************** Projection Constraints for Evaluation ********************************************************************/ %projection evaluates to same value, related ctxs Projection_Constraint proj_evalExpr_forward : forall Names E E' FE EE V EE' O, Pr : Names |{expr}- E ~~> E' -> Names : names EE Names -> 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 EE' O -> exists EE'', evalExpr FE EE E' V EE'' O /\ scopes_same EE' EE''. %if proj evaluates, original evaluates to same value, related ctxs if %it only uses names occurring in the original Projection_Constraint proj_evalExpr_backward : forall Names E E' FE EE V EE' O Ctx, Pr : Names |{expr}- E ~~> E' -> Names : names EE Names -> 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 -> IsCtx : is_list (is_list is_string) Ctx -> Ctxs : ctx_names EE Ctx -> EN : exprNames Ctx E [] -> Ev : evalExpr FE EE E' V EE' O -> exists EE'', evalExpr FE EE E V EE'' O /\ scopes_same EE' EE''. %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''. %if proj evaluates, original evaluates to a related context if it %only uses names occurring in the original Projection_Constraint proj_evalStmt_backward : forall Names S S' FE EE EE' O Ctx Ctx', 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 -> IsCtx : is_list (is_list is_string) Ctx -> Ctxs : ctx_names EE Ctx -> SN : stmtNames Ctx S [] Ctx' -> 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 EE' O, evalExpr FE EE E V 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, IsE : is_expr E; forall FE EE A V EE' O, evalArgs FE EE A V 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, IsA : is_args A; forall FE EE RF V EE' O, evalRecFields FE EE RF V 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, 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] 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, nestedFieldTy Fs FTys Ty -> updateRecFields Fs V FVals Out -> valueType V Ty -> valFieldTys FVals FTys -> valFieldTys Out FTys. [Show Proof] Extensible_Theorem evalExpr_typePres_ctx : forall E FT ET Ty FE EE 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 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_C_E, evalExpr_typePres : forall E FT ET Ty FE EE 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 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 -> valueType V Ty on Ev as IH_T_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_C_S, evalArgs_typePres_Ctx : forall A FT ET Tys FE EE 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 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_C_A, evalArgs_typePres : forall A FT ET Tys FE EE 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 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 -> valueTypeList Vs Tys on Ev as IH_T_A, evalRecFields_typePres_Ctx : forall RF FT ET FTys FE EE 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 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_C_RF, evalRecFields_typePres : forall RF FT ET FTys FE EE 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 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 -> valFieldTys FVs FTys on Ev as IH_T_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 EE' 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 EE' 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 EE' 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 EE' O -> output_forms O on Ev as IH_A, evalRecFields_output_forms : forall RF FE EE Fields EE' 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 EE' 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]