From cb5eb6f1202a60545580f14ba30865624b48635b Mon Sep 17 00:00:00 2001 From: Ruslan Shevchenko Date: Sun, 22 Oct 2023 17:58:29 +0300 Subject: [PATCH] slow advance in proof model --- docs/formalization/ismodel/CoreCps.thy | 139 +++++++++++++++++-------- 1 file changed, 94 insertions(+), 45 deletions(-) diff --git a/docs/formalization/ismodel/CoreCps.thy b/docs/formalization/ismodel/CoreCps.thy index a7162065..7d3c3a11 100644 --- a/docs/formalization/ismodel/CoreCps.thy +++ b/docs/formalization/ismodel/CoreCps.thy @@ -82,7 +82,7 @@ type_synonym varIndex = int type_synonym typeVarState = "varIndex \ typeexpr" definition isCorrectVarType::" int \ typeVarState \ bool" where - "isCorrectVarType x s = (s(x) \ ErrorTp)" + "isCorrectVarType x s = ((s(x)) \ ErrorTp)" fun maxVarIndex:: "expr \ int \ int" where @@ -104,10 +104,19 @@ fun typeExpr :: "expr \ typeVarState \ typeexpr" where "typeExpr (ConstantExpr x) s = ConstTp" | "typeExpr (Let v vt vv body) s = ( - if (vt = ErrorTp) then ErrorTp else (typeExpr body (s(v:=vt)) ) + if \ (isCorrectTp vt) then ErrorTp else + (case (typeExpr vv s) of + ErrorTp \ ErrorTp + | vvt \ if (vvt \ vt) then ErrorTp else + (typeExpr body (s(v:=vt)) ) + ) )" | - "typeExpr (Ref i it) s = (if (it = s(i))\(it \ ErrorTp) then it else ErrorTp)" + "typeExpr (Ref i it) s = ( + if \(isCorrectTp it) then ErrorTp + else + if ((s(i)) = it) then it else ErrorTp + )" | "typeExpr (If cond ifTrue ifFalse) s = ( case (typeExpr cond s) of @@ -117,40 +126,52 @@ fun typeExpr :: "expr \ typeVarState \ typeexpr" where | "typeExpr (While e1 e2) s = ConstTp" | - "typeExpr (Lambda i tp body) s = (ArrowTp tp (typeExpr body (s(i:=tp))))" + "typeExpr (Lambda i tp body) s = ( + if \(isCorrectTp tp) then + ErrorTp + else (case (typeExpr body (s(i:=tp))) of + ErrorTp \ ErrorTp + | + tb \ ArrowTp tp tb + ) + )" | "typeExpr (App x arg) s = - (case (typeExpr x s) of - ErrorTp \ ErrorTp - | - (ArrowTp xi xo) \ if ((typeExpr arg s) = xi)\(xi \ ErrorTp) then xo else ErrorTp + ( + case (typeExpr x s) of + (ArrowTp xi xo) \ ( + if (isCorrectTp xi)\((typeExpr arg s) = xi) then + xo + else ErrorTp + ) | other \ ErrorTp ) " | - "typeExpr (Mpure x) s = ( case (typeExpr x s) of - ErrorTp \ ErrorTp - | tx \ MonadTp tx + "typeExpr (Mpure x) s = ( let tx = (typeExpr x s) in + if (isCorrectTp tx) then tx else ErrorTp )" | "typeExpr (MflatMap fa f) s = ( - case (typeExpr fa s) of - MonadTp ErrorTp \ ErrorTp - | MonadTp a \ (case (typeExpr f s) of - ArrowTp a1 (MonadTp ErrorTp) \ ErrorTp - | ArrowTp a1 (MonadTp a2) \ a2 - | other \ ErrorTp) - | other \ ErrorTp - )" + let at = (typeExpr fa s); ft = (typeExpr f s) in + if (isCorrectTp at)\(isCorrectTp ft) then + (case at of + MonadTp a \ (case ft of + ArrowTp a1 (MonadTp a2) \ a2 + | other \ ErrorTp) + | other \ ErrorTp + ) + else ErrorTp + )" | "typeExpr (Await e) s = ( case (typeExpr e s) of - MonadTp te \ te + MonadTp te \ if (isCorrectTp te) then te else ErrorTp | other \ ErrorTp )" | - "typeExpr (ExternalFun fi ft) s = ft" + "typeExpr (ExternalFun fi ft) s = (if (isCorrectTp ft) then ft else ErrorTp)" | "typeExpr (Error e) s = ErrorTp" @@ -195,7 +216,7 @@ fun isCompatibleAk :: "AsyncKind \ AsyncKind \ bool" whe datatype CpsTree = CpsTreePure expr | - CpsTreeFlatMap CpsTree int typeexpr CpsTree + CpsTreeFlatMap CpsTree int CpsTree | CpsTreeAsync expr AsyncKind | @@ -207,19 +228,24 @@ datatype CpsTree = ErrorCpsTree fun typeCpsTree:: "CpsTree \ typeVarState \ typeexpr" where - "typeCpsTree (CpsTreePure expr) s = MonadTp (typeExpr expr s)" + "typeCpsTree (CpsTreePure expr) s = (case (typeExpr expr s) of + ErrorTp \ ErrorTp + | t \ MonadTp t + )" | - "typeCpsTree (CpsTreeFlatMap src i tb fbody) s = ( + "typeCpsTree (CpsTreeFlatMap src i fbody) s = ( case (typeCpsTree src s) of - MonadTp srct \ + MonadTp srct \ (case (typeCpsTree fbody (s(i:=srct))) of - ArrowTp fx fy \ if (fx = srct) then fy else ErrorTp + MonadTp bt \ if (bt = ErrorTp) then ErrorTp else MonadTp bt | other \ ErrorTp) |other \ ErrorTp )" | "typeCpsTree (CpsTreeAsync e k) s = ( - (typeExpr e s) + case (typeExpr e s) of + MonadTp t \ if (t = ErrorTp) then ErrorTp else MonadTp t + |other \ ErrorTp )" | "typeCpsTree (CpsTreeLambda v vt body) s = ( @@ -235,13 +261,42 @@ fun typeCpsTree:: "CpsTree \ typeVarState \ typeexpr" wh "typeCpsTree ErrorCpsTree s = ErrorTp" -fun isCorrectExpr::"expr \ typeVarState \ bool" where - "isCorrectExpr e s = ((typeExpr e s) \ ErrorTp)" +definition isCorrectExpr::"expr \ typeVarState \ bool" where + "isCorrectExpr e s \ ((typeExpr e s) \ ErrorTp)" fun isCorrectCps :: "CpsTree \ typeVarState \ bool" where "isCorrectCps t s = ((typeCpsTree t s) \ ErrorTp)" +lemma noMonadTpErrprExpr: "isCorrectExpr t s \ (typeExpr t s \ MonadTp ErrorTp)" + nitpick + apply(induct t) + subgoal + apply(simp) + done + subgoal + apply() + + +lemma noMonadTpErrorCps: "isCorrectCps tree s \ (typeCpsTree tree s) \ (MonadTp ErrorTp)" + apply(auto) + apply(induct tree) + subgoal + sorry + + +lemma correctFlatMapNoErrorKind: " + (isCorrectCps (source::CpsTree) s) + \ ((typeCpsTree source s) = MonadTp ts) + \ (isCorrectCps (body::CpsTree) (s(v:=ts)) ) + \ ((typeCpsTree body (s(v:=ts))) = MonadTp tb) + \ isCorrectCps (CpsTreeFlatMap source v body) s" + nitpick + apply(auto) + done + + + fun asyncKind :: "CpsTree \ AsyncKind" where @@ -274,7 +329,7 @@ definition isRedusableCps::"CpsTree \ typeVarState \ boo (* analog of CpsTree.transformed *) -fun cpsTreeToExpr :: "CpsTree \ typeVarState \ expr" where +function cpsTreeToExpr :: "CpsTree \ typeVarState \ expr" where "cpsTreeToExpr (CpsTreePure e) s = Mpure e" | "cpsTreeToExpr (CpsTreeFlatMap arg v vt vbody) s = @@ -299,9 +354,10 @@ fun cpsTreeToExpr :: "CpsTree \ typeVarState \ expr" whe "cpsTreeToExpr (CpsTreeLet v vt vv cpsBody) s = (Let v vt vv (cpsTreeToExpr cpsBody (s(v:=vt))))" | "cpsTreeToExpr ErrorCpsTree s = Error ''ErrorCpsTree'' " + apply(auto) + sorry - fun unpureCpsTree :: "CpsTree \ (expr option)" where "unpureCpsTree (CpsTreePure e) = (Some e)" | @@ -339,23 +395,16 @@ lemma correctNotError: "isCorrectCps (t::CpsTree) s \ t \ by auto -lemma correctFlatMapNoErrorKind: " - (isCorrectCps (source::CpsTree) s) \ (isCorrectCps (body::CpsTree) s) \ (vt \ ErrorTp) - \ isCorrectCps (CpsTreeFlatMap source v vt body) s" - nitpick - oops -lemma correctNoErrorKind: "(isCorrectCpsTree (t::CpsTree) (s::typeVarState)) \ ((asyncKind t) \ AKError)" - (*nitpick*) - apply(simp) - apply(induct_tac t) - subgoal apply(auto) - done - subgoal - - +lemma correctNoErrorKind: "(isCorrectCps (t::CpsTree) (s::typeVarState)) \ ((asyncKind t) \ AKError)" + nitpick + apply(induct_tac t, auto) + subgoal + apply(split asyncKind.split) + + oops