Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- fmod TOP is
- sort Top .
- endfm
- fmod GENERIC-LIST is including NAT + TOP .
- sorts BotList TopList .
- subsort BotList < TopList < Top .
- op nil : -> BotList .
- op _,_ : BotList BotList -> BotList [assoc id: nil prec 121] .
- op _,_ : TopList TopList -> TopList [ditto] .
- op length_ : BotList -> Nat .
- eq length(nil) = 0 .
- endfm
- fmod KLIST{X :: TRIV} is including GENERIC-LIST .
- sort List{X} NeList{X} .
- subsort BotList < List{X} < TopList .
- subsort X$Elt < NeList{X} < List{X} .
- op _,_ : List{X} List{X} -> List{X} [ditto] .
- op _,_ : NeList{X} List{X} -> NeList{X} [ditto] .
- op _,_ : List{X} NeList{X} -> NeList{X} [ditto] .
- op length_ : List{X} -> Nat [ditto] .
- var x : X$Elt . var xl : List{X} .
- eq length(x, xl) = length(xl) + 1 .
- endfm
- fmod GENERIC-SET is including GENERIC-LIST .
- sorts BotSet TopSet .
- subsort BotSet < TopSet < Top .
- op empty : -> BotSet .
- op _&&_ : BotSet BotSet -> BotSet [assoc comm id: empty prec 121] .
- op _&&_ : TopSet TopSet -> TopSet [ditto] .
- op _in_ : BotList BotSet -> Bool .
- eq nil in empty = false .
- endfm
- fmod KSET{X :: TRIV} is
- including GENERIC-SET .
- including KLIST{X} .
- sorts NeSet{X} Set{X} .
- subsort BotSet < Set{X} < TopSet .
- subsort X$Elt < NeSet{X} < Set{X} .
- op _&&_ : Set{X} Set{X} -> Set{X} [ditto] .
- op _&&_ : NeSet{X} Set{X} -> NeSet{X} [ditto] .
- op _in_ : List{X} Set{X} -> Bool .
- var x : X$Elt . var xs : Set{X} .
- eq x in (x && xs) = true .
- eq x in xs = false [owise] .
- endfm
- fmod TUPLE is including TOP .
- sort Tuple .
- op `[_`] : [Top] -> Tuple .
- endfm
- view Tuple from TRIV to TUPLE is sort Elt to Tuple . endv
- fmod GENERIC-MAP is
- including GENERIC-LIST + GENERIC-SET .
- op _[_] : BotSet BotList -> BotList .
- op _[_<-_] : BotSet BotList BotList -> BotSet .
- op _|->_ : BotList BotList -> BotSet .
- eq empty[nil <- nil] = empty .
- endfm
- fmod KMAP{X :: TRIV, Y :: TRIV} is including GENERIC-MAP .
- including KLIST{X} .
- including KLIST{Y} .
- sort Map{X,Y} .
- subsort BotSet < Map{X,Y} < TopSet .
- op _&&_ : Map{X,Y} Map{X,Y} -> Map{X,Y} [ditto] .
- op _[_] : Map{X,Y} List{X} -> List{Y} [ditto] .
- op _[_<-_] : Map{X,Y} List{X} List{Y} -> Map{X, Y} [ditto] .
- op _|->_ : List{X} List{Y} -> Map{X,Y} .
- --- op get : Map{X,Y} X -> Y .
- var x : X$Elt . var y y' : Y$Elt . var map : Map{X,Y} .
- var xl : NeList{X} . var yl : NeList{Y} .
- eq ((x |-> y) && map)[x] = y .
- eq map[nil <- nil] = map .
- eq ((x |-> y') && map)[x <- y] = (x |-> y) && map .
- eq map[x <- y] = (x |-> y) && map [owise] .
- eq map[(x,xl) <- (y,yl)] = map[x <- y][xl <- yl] .
- --- eq get(map,x) = map[x] .
- endfm
- fmod K-SORTS is
- sorts K KProper KResult .
- subsorts KProper KResult < K .
- endfm
- view K from TRIV to K-SORTS is sort Elt to K . endv
- view KProper from TRIV to K-SORTS is sort Elt to KProper . endv
- view KResult from TRIV to K-SORTS is sort Elt to KResult . endv
- fmod K-PLAIN is including KLIST{K} + KLIST{KProper} * (sort NeList{KProper} to NeKProperList) + KLIST{KResult} .
- subsorts List{KProper} List{KResult} < List{K} .
- subsorts NeKProperList NeList{KResult} < NeList{K} .
- op .K : -> K .
- op _->_ : K K -> K [prec 50 assoc id: .K] .
- op _->_ : KProper K -> KProper [ditto] .
- var r : KResult . var kp : KProper . var kl1 kl2 : List{K} . ---KList .
- var rl : List{KResult} . ---KResultList .
- op strict_ : List{K} --- KList
- -> K .
- op result_ : List{KResult} --- KResultList
- -> KResult .
- op strictfreeze : List{K} List{K} --- KList KList
- -> K .
- eq strict(kl1,kp,kl2) = kp -> strictfreeze(kl1,kl2) .
- eq r -> strictfreeze(kl1,kl2) = strict(kl1,r,kl2) .
- eq strict(rl) = result(rl) .
- op seqstrict_ : List{K} --- KList
- -> K .
- op seqstrictfreeze : List{KResult} List{K} --- KResultList KList
- -> K .
- eq strict(rl,kp,kl2) = kp -> seqstrictfreeze(rl, kl2) .
- eq r -> seqstrictfreeze(rl, kl2) = seqstrict(rl, r, kl2) .
- eq seqstrict(rl) = result(rl) .
- endfm
- fmod NAME is sort Name . endfm
- view Name from TRIV to NAME is sort Elt to Name . endv
- fmod VAL is sort Val . endfm
- view Val from TRIV to VAL is sort Elt to Val . endv
- fmod LOC is
- including INT .
- sorts Loc .
- op loc : Nat -> Loc .
- op _+Loc_ : Loc Int -> Loc .
- vars N : Nat . var I : Int .
- eq loc(N) +Loc I = loc(N + I) .
- endfm
- view Loc from TRIV to LOC is sort Elt to Loc . endv
- fmod LOC-COMPREHENSION is including KLIST{Loc} .
- vars N N' : Nat .
- op _..._ : Loc Loc -> List{Loc} [prec 10] .
- ceq loc(N) ... loc(N') = nil if N' < N .
- eq loc(N) ... loc(N') = loc(N), loc(N + 1) ... loc(N') .
- endfm
- fmod ENV is including KMAP{Name, Loc} *
- (sort Map{Name, Loc} to Env, op _`[_`] to get) . endfm
- view Env from TRIV to ENV is sort Elt to Env . endv
- fmod TYPE is
- sort Type .
- op ? : -> Type .
- endfm
- view Type from TRIV to TYPE is sort Elt to Type . endv
- fmod TENV is including KMAP{Name, Type} *
- (sort Map{Name, Type} to TEnv, op _`[_`] to get) . endfm
- fmod TYPED-LOCATION-SORT is sort TypedLoc . endfm
- view TypedLoc from TRIV to TYPED-LOCATION-SORT is sort Elt to TypedLoc . endv
- fmod TYPED-LOCATION is
- including KLIST{Type} .
- including KLIST{Loc} .
- including KLIST{TypedLoc} .
- op _:_ : Loc Type -> TypedLoc .
- op _:_ : List{Loc} List{Type} -> List{TypedLoc} [ditto] .
- op type : TypedLoc -> Type .
- op loc : TypedLoc -> Loc .
- var l : Loc . var t : Type . var ll : NeList{Loc} . var tl : NeList{Type} .
- eq type(l : t) = t .
- eq loc(l : t) = l .
- eq (l, ll) : (t, tl) = (l : t), (ll : tl) .
- eq nil : nil = nil .
- endfm
- fmod TYPED-ENV is including KMAP{Name, TypedLoc} *
- (sort Map{Name, TypedLoc} to Env) .
- including TYPED-LOCATION . endfm
- view TypedEnv from TRIV to TYPED-ENV is sort Elt to Env . endv
- fmod STORE is including KMAP{Loc, Val} * (sort Map{Loc, Val} to Store, op _`[_`] to get) . endfm
- fmod STACK is including KLIST{Tuple} * (sort List{Tuple} to Stack) . endfm
- fmod CONFIG-ITEM is sort ConfigItem . endfm
- view ConfigItem from TRIV to CONFIG-ITEM is sort Elt to ConfigItem . endv
- fmod CONFIG is including SET{ConfigItem} * (op _`,_ to __) .
- sort Config .
- op [[_]] : Set{ConfigItem} -> Config .
- endfm
- ***( Types of List neeed:
- List{Tyvar}
- List{BType}
- List{Type}
- List{K}
- KSET-MINUS{Tyvar}
- )***
- -----------------------Type Infrastructure ----------------------------
- fmod BTYPE is
- including TYPE .
- sort BType .
- subsort BType < Type .
- endfm
- view BType from TRIV to BTYPE is sort Elt to BType . endv
- fmod TYVAR is
- including INT .
- sort Tyvar .
- op tyVar : Int -> Tyvar .
- op incTyVar : Tyvar Int -> Tyvar .
- vars N M : Int .
- eq incTyVar(tyVar(N), M) = tyVar(N + M) .
- endfm
- view Tyvar from TRIV to TYVAR is sort Elt to Tyvar . endv
- fmod TYVAR-SEQ is
- including KLIST{Tyvar} .
- vars N : Nat .
- vars tv : Tyvar .
- op tyvarseq : Tyvar Nat -> List{Tyvar} .
- eq tyvarseq(tv, 0) = tv .
- eq tyvarseq(tv, N) = (tv, tyvarseq(incTyVar(tv,1),(N - 1))) .
- endfm
- fmod TYPE-SUBST is
- including KMAP {Tyvar, BType} *
- (sort Map{Tyvar, BType} to TypeSubst, op _|->_ to _goesto_ ,
- op _`[_<-_`] to _`[_gets_`], op _`[_`] to tysubstget , op _&&_ to _with_ ,
- op _in_ to _eltof_ ) .
- op appSubst : TypeSubst BType -> BType .
- op compSubst : TypeSubst TypeSubst -> TypeSubst .
- op compSubstAux : TypeSubst TypeSubst -> TypeSubst .
- op compSubstThin : TypeSubst TypeSubst -> TypeSubst .
- vars tv tv' : Tyvar .
- vars t t' : BType .
- vars sigma sigma' : TypeSubst .
- eq appSubst (((tv goesto t) with sigma), tv) = t .
- eq appSubst (sigma, tv) = tv [owise] .
- eq compSubstAux (sigma', ((tv goesto t) with sigma)) =
- ((tv goesto appSubst(sigma', t)) with (compSubstAux(sigma', sigma))) .
- eq compSubstAux (sigma', empty) = empty .
- eq compSubstThin (((tv goesto t') with sigma'), ((tv goesto t) with sigma)) =
- compSubstThin (sigma', ((tv goesto t) with sigma)) .
- eq compSubstThin (sigma', sigma) = (sigma' with sigma) [owise] .
- eq compSubst (sigma', sigma) =
- compSubstThin(sigma', compSubstAux(sigma', sigma)) .
- endfm
- fmod POLYFUN-BTYPE is
- including QID .
- including KLIST{BType} .
- including TYPE-SUBST .
- including KSET{Tyvar} .
- including K-PLAIN .
- subsort Tyvar < BType .
- subsort NeList{Tyvar} < NeList{BType} < NeList{K} .
- subsort List{Tyvar} < List{BType} < List{K} .
- op tyConst : Qid List{BType} -> BType .
- op tyConstK : Qid List{K} -> K .
- op _-->_ : BType BType -> BType .
- op _-->_ : K K -> K [ditto].
- op occurs : Tyvar BType -> Bool .
- op freeTyvars : List{BType} -> Set{Tyvar} .
- op appSubstList : TypeSubst List{BType} -> List{BType} .
- vars tl tl' : List{BType} .
- vars e e' : K .
- vars t t' : BType .
- vars sigma : TypeSubst .
- vars N : Int .
- vars tv tv' : Tyvar .
- vars tyc : Qid .
- eq t --> t' = tyConst('fun,(t,t')) .
- eq e --> e' = tyConstK('fun,(e,e')) .
- eq tyConstK('fun,(t,t')) = tyConst('fun,(t,t')) .
- eq occurs(tv, (tv,tl)) = true .
- eq occurs(tv, (tv',tl)) = occurs(tv, tl) [owise] .
- eq occurs(tv, ((tyConst(tyc, tl)), tl')) = occurs(tv, (tl, tl')) .
- eq occurs(tv, nil) = false .
- eq appSubst(sigma, tyConst(tyc,tl)) = tyConst(tyc,appSubstList(sigma, tl)) .
- eq appSubstList(sigma, nil) = nil .
- eq appSubstList(sigma, (t, tl)) = (appSubst(sigma, t), appSubstList(sigma, tl)) .
- eq freeTyvars (tv) = (tv) .
- eq freeTyvars (tyConst(tyc,tl)) = freeTyvars(tl) .
- eq freeTyvars ((t,tl)) = (freeTyvars(t)) && (freeTyvars(tl)) .
- eq freeTyvars (nil) = empty .
- endfm
- fmod KSET-MINUS{X :: TRIV} is
- including KSET{X} .
- including KLIST{X} .
- op setminus : Set{X} Set{X} -> Set{X} .
- op setlistminus : Set{X} List{X} -> Set{X} .
- var x y : X$Elt .
- vars xs ys : Set{X} .
- vars xl : List{X} .
- eq (x && x && xs) = (x && xs) .
- eq setminus((x && xs), (x && ys)) = setminus(xs, ys) .
- ceq setminus(xs, (y && ys)) = setminus (xs, ys) if not (y in xs) .
- eq setminus(xs, empty) = xs .
- eq setlistminus(xs, nil) = xs .
- eq setlistminus((x && xs), (x, xl)) = setlistminus(xs, xl) .
- ceq setlistminus(xs, (x, xl)) = setlistminus(xs, xl) if not (x in xs) .
- endfm
- fmod CONSTRAINT is
- including POLYFUN-BTYPE .
- sort Constraint .
- op _<->_ : BType BType -> Constraint .
- endfm
- view Constraint from TRIV to CONSTRAINT is sort Elt to Constraint . endv
- fmod MGU is
- including KSET{Constraint} .
- including KLIST{BType} .
- including TYPE-SUBST .
- sort TypeSubstOrError SetConstOrError .
- subsort TypeSubst < TypeSubstOrError .
- subsort Set{Constraint} < SetConstOrError .
- op SCError : -> SetConstOrError .
- op TSError : -> TypeSubstOrError .
- op appSubstConst : TypeSubst Set{Constraint} -> Set{Constraint} .
- op zipConstraints : List{BType} List{BType} -> SetConstOrError .
- op mgu : Set{Constraint} -> TypeSubstOrError .
- vars s t : BType .
- vars sl tl tl' : List{BType} .
- vars tv tv' : Tyvar .
- vars S : Set{Constraint} .
- vars tyc tyc' : Qid .
- vars sigma phi psi : TypeSubst .
- eq appSubstConst(sigma, ((s <-> t) && S)) =
- (((appSubst(sigma, s)) <-> (appSubst(sigma, t))) &&
- appSubstConst(sigma, S)) .
- eq appSubstConst(sigma, empty) = empty .
- eq zipConstraints ((s, sl), (t, tl)) = (s <-> t) && (zipConstraints(sl, tl)) .
- eq zipConstraints (nil, nil) = empty .
- eq zipConstraints (nil, (t, tl)) = SCError .
- eq zipConstraints ((s, sl), nil) = SCError .
- eq mgu(empty) = empty .
- eq mgu(((tv <-> tv) && S)) = mgu(S) .
- eq mgu(((tyConst(tyc, sl) <-> tyConst(tyc, tl)) && S)) =
- mgu(((zipConstraints(sl, tl)) && S)) .
- ceq mgu(((tyConst(tyc, sl) <-> tyConst(tyc', tl)) && S)) = TSError
- if not (tyc == tyc') .
- eq mgu(((tyConst(tyc, tl) <-> tv) && S)) =
- mgu(((tv <-> tyConst(tyc, tl)) && S)) .
- ceq mgu(((tv <-> t) && S)) = compSubst((tv goesto appSubst(psi, t)), psi)
- if (occurs(tv, t)) = false /\ psi := (mgu(appSubstConst((tv goesto t),S))) .
- endfm
- fmod POLYFUN-GTYPE is
- including KLIST{Type} .
- including KLIST{Tyvar} .
- including KSET-MINUS{Tyvar} .
- including TYPE-SUBST .
- including POLYFUN-BTYPE .
- including BOOL .
- subsort NeList{BType} < NeList{Type} .
- subsort List{BType} < List{Type} .
- op forall : List{Tyvar} BType -> Type .
- op freeTyvars : List{Type} -> Set{Tyvar} [ditto] .
- op appSubst : TypeSubst Type -> Type [ditto] .
- op thinSubst : TypeSubst BType -> TypeSubst .
- op cksubst : TypeSubst List{Tyvar} Type -> Type .
- op cksubst : TypeSubst List{Tyvar} BType -> BType [ditto] .
- op checkNoFreeVarCapture : TypeSubst List{Tyvar} -> Bool .
- op listmem : Tyvar List{Tyvar} -> Bool .
- vars t t' : BType .
- vars tv tv': Tyvar .
- vars tvl tvl' : List{Tyvar} .
- vars tl : List{BType} .
- vars sigma : TypeSubst .
- eq forall((nil), t) = t .
- eq listmem(tv, (tvl, tv, tvl')) = true .
- eq listmem(tv, tvl) = false [owise] .
- eq freeTyvars (forall(tl, t)) = setminus(freeTyvars (t), tl) .
- eq appSubst(((tv goesto t) with sigma), (forall((tvl, tv, tvl'), t'))) =
- appSubst(sigma, forall((tvl, tv, tvl'), t')) .
- eq appSubst(sigma, forall(tvl, t)) =
- forall(tvl, cksubst((thinSubst(sigma, t)), tvl, t)) [owise] .
- eq thinSubst(empty, t) = empty .
- ceq thinSubst((tv goesto t) with sigma, t') =
- thinSubst(sigma, t')
- if not(occurs(tv, t')) .
- eq thinSubst((tv goesto t) with sigma, t') =
- ((tv goesto t) with thinSubst(sigma, t')) [owise] .
- ceq cksubst(sigma, tvl, t) = appSubst(sigma, t) if
- checkNoFreeVarCapture(sigma, tvl) .
- eq checkNoFreeVarCapture (((tv goesto t) with sigma), tvl) =
- (setlistminus(freeTyvars(t), tvl) == freeTyvars(t)) and
- checkNoFreeVarCapture (sigma, tvl) .
- eq checkNoFreeVarCapture (empty, tvl) = true .
- endfm
- fmod POLYFUN-TYENV is
- including POLYFUN-GTYPE .
- including TENV * (op empty to nul) .
- including KLIST{Tyvar} .
- sort InstResult .
- op freeTyvars : TEnv -> Set{Tyvar} [ditto] .
- op appSubstTEnv : TypeSubst TEnv -> TEnv .
- op instResult : BType Tyvar -> InstResult .
- op instantiate : Type Tyvar -> InstResult .
- op instResultType : InstResult -> BType .
- op instResultTyV : InstResult -> Tyvar .
- op setToList : Set{Tyvar} -> List{Tyvar} .
- op generalize : TEnv BType -> Type .
- op setmem : Tyvar Set{Tyvar} -> Bool .
- vars n : Name .
- vars Gamma : TEnv .
- vars t : Type .
- vars bt : BType .
- vars sigma : TypeSubst .
- vars tv tv' : Tyvar .
- vars tvl tvl' : List{Tyvar} .
- vars tvs : Set{Tyvar} .
- vars tl : List{BType} .
- eq freeTyvars(((n |-> t) && Gamma)) = (freeTyvars(t) && freeTyvars(Gamma)) .
- eq freeTyvars(nul) = empty .
- eq appSubstTEnv(sigma, ((n |-> t) && Gamma)) =
- (n |-> (appSubst(sigma, t))) && appSubstTEnv(sigma, Gamma) .
- eq appSubstTEnv(sigma, nul) = nul .
- eq instantiate ((forall((tv, tvl), t)), tv') =
- instantiate ((forall(tvl, appSubst((tv goesto tv'), t))), incTyVar(tv', 1)) .
- eq instantiate (bt, tv') = instResult(bt, tv') .
- eq instResultType(instResult(bt, tv)) = bt .
- eq instResultTyV(instResult(bt, tv)) = tv .
- eq setmem(tv, (tv && tvs)) = true .
- eq setmem(tv, tvs) = false [owise] .
- eq setToList(empty) = nil .
- ceq setToList((tv && tvs)) = (tv, setToList(tvs))
- if not (setmem(tv, tvs)) .
- eq setToList((tv && tvs)) = (setToList(tvs)) [owise] .
- eq generalize (Gamma, bt) =
- (forall((setToList(setminus(freeTyvars(bt),freeTyvars(Gamma)))), bt)) .
- endfm
- -------------------- Syntax, including strictness -----------------------
- fmod K-POLYFUN-BTYPE-STRICTNESS is
- including POLYFUN-BTYPE .
- op tyConstArgBox : Qid List{K} List{K} -> K .
- vars tyc : Qid .
- vars krl : List{KResult} .
- vars kl : List{K} .
- vars kp : KProper .
- vars kr : KResult .
- eq (tyConstK(tyc, (krl, kp, kl))) = (kp -> tyConstArgBox(tyc, krl, kl)) .
- eq (kr -> tyConstArgBox(tyc, krl, kl)) = tyConstK(tyc, (krl, kr, kl)) .
- endfm
- fmod CONSTANT is
- including INT .
- including BOOL .
- including VAL .
- op #int_ : Int -> Val [prec 0] .
- op #bool_ : Bool -> Val [prec 0] .
- endfm
- fmod IDENTIFIER is
- including NAME .
- including QID .
- including K-PLAIN .
- sort Identifier .
- subsort Qid < Identifier < Name < KProper .
- ---Names may be looked up in Environments and Type Environments;
- endfm
- view Identifier from TRIV to IDENTIFIER is sort Elt to Identifier . endv
- fmod K-POLYFUN-ARITH-SYNTAX is
- including K-SORTS .
- op _++_ : K K -> KProper [prec 33 assoc] .
- op _--_ : K K -> KProper [prec 33 gather(E e)] .
- op _**_ : K K -> KProper [prec 31 assoc] .
- endfm
- fmod K-POLYFUN-ARITH-SYNTAX-DYNAMIC-STRICTNESS is
- including K-POLYFUN-ARITH-SYNTAX .
- including K-PLAIN .
- vars kp1 kp2 : KProper .
- vars kr1 kr2 : KResult .
- vars k2 : K .
- op []++_ : K -> K .
- eq kp1 ++ k2 = kp1 -> []++ k2 .
- eq kr1 -> []++ k2 = kr1 ++ k2 .
- op _++[] : KResult -> K .
- eq kr1 ++ kp2 = kp2 -> kr1 ++[] .
- eq kr2 -> kr1 ++[] = kr1 ++ kr2 .
- op []--_ : K -> K .
- eq kp1 -- k2 = kp1 -> []-- k2 .
- eq kr1 -> []-- k2 = kr1 -- k2 .
- op _--[] : KResult -> K .
- eq kr1 -- kp2 = kp2 -> kr1 --[] .
- eq kr2 -> kr1 --[] = kr1 -- kr2 .
- op []**_ : K -> K .
- eq kp1 ** k2 = kp1 -> []** k2 .
- eq kr1 -> []** k2 = kr1 ** k2 .
- op _**[] : KResult -> K .
- eq kr1 ** kp2 = kp2 -> kr1 **[] .
- eq kr2 -> kr1 **[] = kr1 ** kr2 .
- endfm
- fmod K-POLYFUN-INT-REL-SYNTAX is
- including K-SORTS .
- op _<<<_ : K K -> KProper [prec 37] .
- op _===_ : K K -> KProper [prec 37] .
- endfm
- fmod K-POLYFUN-INT-REL-SYNTAX-DYNAMIC-STRICTNESS is
- including K-POLYFUN-INT-REL-SYNTAX .
- including K-PLAIN .
- vars kp1 kp2 : KProper .
- vars kr1 kr2 : KResult .
- vars k2 : K .
- --- Exp <<< Exp [strict, extends <:Int * Int -> Bool]
- op []<<<_ : K -> K .
- eq kp1 <<< k2 = kp1 -> []<<< k2 .
- eq kr1 -> []<<< k2 = kr1 <<< k2 .
- op _<<<[] : KResult -> K .
- eq kr1 <<< kp2 = kp2 -> kr1 <<<[] .
- eq kr2 -> kr1 <<<[] = kr1 <<< kr2 .
- --- Exp === Exp [strict, extends =:Int * Int -> Bool]
- op []===_ : K -> K .
- eq kp1 === k2 = kp1 -> []=== k2 .
- eq kr1 -> []=== k2 = kr1 === k2 .
- op _===[] : KResult -> K .
- eq kr1 === kp2 = kp2 -> kr1 ===[] .
- eq kr2 -> kr1 ===[] = kr1 === kr2 .
- endfm
- fmod K-POLYFUN-LOGIC-SYNTAX is
- including K-SORTS .
- op not_ : K -> KProper .
- op _And_ : K K -> KProper [prec 55 assoc] .
- op _Or_ : K K -> KProper [prec 59 assoc] .
- op if_then_else_fi : K K K -> KProper .
- endfm
- fmod K-POLYFUN-LOGIC-SYNTAX-DYNAMIC-STRICTNESS is
- including K-POLYFUN-LOGIC-SYNTAX .
- including K-PLAIN .
- vars kp1 kp2 : KProper .
- vars kr1 kr2 : KResult .
- vars k1 k2 : K .
- op not[] : -> K .
- eq not kp1 = kp1 -> not[] .
- eq kr1 -> not[] = not kr1 .
- --- BExp And BExp [strict(1), ... ]
- op []And_ : K -> K .
- eq kp1 And k2 = kp1 -> []And k2 .
- eq kr1 -> []And k2 = kr1 And k2 .
- --- BExp Or BExp [strict(1), ... ]
- op []Or_ : K -> K .
- eq kp1 Or k2 = kp1 -> []Or k2 .
- eq kr1 -> []Or k2 = kr1 Or k2 .
- op if[]then_else_fi : K K -> K .
- eq if kp1 then k1 else k2 fi = kp1 -> (if[]then k1 else k2 fi) .
- eq kr1 -> (if[]then k1 else k2 fi) = if kr1 then k1 else k2 fi .
- endfm
- fmod K-POLYFUN-LOGIC-SYNTAX-STATIC-STRICTNESS is
- including K-POLYFUN-LOGIC-SYNTAX-DYNAMIC-STRICTNESS .
- including K-PLAIN .
- vars kp1 kp2 : KProper .
- vars kr kr1 kr2 : KResult .
- vars k2 : K .
- --- BExp And BExp [strict, ... ]
- op _And[] : KResult -> K .
- eq kr1 And kp2 = kp2 -> kr1 And[] .
- eq kr2 -> kr1 And[] = kr1 And kr2 .
- --- BExp Or BExp [strict, ... ]
- op _Or[] : KResult -> K .
- eq kr1 Or kp2 = kp2 -> kr1 Or[] .
- eq kr2 -> kr1 Or[] = kr1 Or kr2 .
- op if_then[]else_fi : KResult K -> K .
- eq if kr1 then kp1 else k2 fi = kp1 -> if kr1 then[]else k2 fi .
- eq kr2 -> if kr1 then[]else k2 fi = if kr1 then kr2 else k2 fi .
- op if_then_else[]fi : KResult KResult -> K .
- eq if kr1 then kr2 else kp2 fi = kp2 -> if kr1 then kr2 else[]fi .
- eq kr2 -> if kr then kr1 else[]fi = if kr then kr1 else kr2 fi .
- endfm
- fmod K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX is
- including K-PLAIN .
- including IDENTIFIER .
- including KLIST{Qid} .
- including KLIST{Identifier} .
- including KLIST{Name} .
- subsort List{Qid} < List{Identifier} < List{Name} < List{KProper} .
- subsort NeList{Qid} < NeList{Identifier} < NeList{Name} < NeKProperList .
- op fun_=>_ : Identifier K -> KProper .
- op _(|_|) : K K -> KProper [prec 1 gather (E e)].
- op let_=_in_end : Identifier K K -> KProper .
- op letrec_=_in_end : Identifier K K -> KProper .
- endfm
- fmod K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX-DYNAMIC-STRICTNESS is
- including K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX .
- op let_=[]in_end : Identifier K -> K .
- op BoxApp : K -> K .
- op AppBox : KResult -> K .
- vars kp1 kp2 : KProper .
- vars kr1 kr2 : KResult .
- vars k2 : K .
- vars x : Identifier .
- eq let x = kp1 in k2 end = kp1 -> let x =[]in k2 end .
- eq kr1 -> let x =[]in k2 end = let x = kr1 in k2 end .
- eq kp1 (| k2 |) = kp1 -> BoxApp(k2) .
- eq kr1 -> BoxApp(k2) = kr1 (| k2 |) .
- eq kr1 (| kp2 |) = kp2 -> AppBox(kr1) .
- eq kr2 -> AppBox(kr1) = kr1 (| kr2 |) .
- endfm
- fmod K-POLYFUN-SYNTAX is
- including CONSTANT .
- including IDENTIFIER .
- including K-POLYFUN-ARITH-SYNTAX .
- including K-POLYFUN-INT-REL-SYNTAX .
- including K-POLYFUN-LOGIC-SYNTAX .
- including K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX .
- subsorts Val < KResult .
- endfm
- fmod K-POLYFUN-EXPRESSIONS-DYNAMIC-STRICTNESS is
- including K-POLYFUN-ARITH-SYNTAX-DYNAMIC-STRICTNESS .
- including K-POLYFUN-INT-REL-SYNTAX-DYNAMIC-STRICTNESS .
- including K-POLYFUN-LOGIC-SYNTAX-DYNAMIC-STRICTNESS .
- including K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX-DYNAMIC-STRICTNESS .
- endfm
- fmod K-POLYFUN-EXPRESSIONS-STATIC-STRICTNESS is
- including K-POLYFUN-BTYPE-STRICTNESS .
- including K-POLYFUN-EXPRESSIONS-DYNAMIC-STRICTNESS .
- including K-POLYFUN-LOGIC-SYNTAX-STATIC-STRICTNESS .
- endfm
- --------------------Config Items and Reduction Rules--------------------
- fmod K-POLYFUN-STATIC-CONFIGITEMS is
- including K-PLAIN .
- including CONFIG-ITEM .
- including POLYFUN-GTYPE .
- including KLIST{Type} .
- including POLYFUN-TYENV .
- including KMAP{Tyvar, Type} *
- (sort Map{Tyvar, Type} to TyEnv, op _|->_ to _goesto_ ,
- op _`[_<-_`] to _`[_gets_`], op _`[_`] to get ,
- op _&&_ to _with_ , op _in_ to _eltof_ ) .
- including TYPE-SUBST .
- --- subsorts Type < KResult . --- I think I oly need BType < KResult .
- subsorts BType < KResult .
- subsorts List{BType} < List{KResult} .
- subsorts NeList{BType} < NeList{KResult} .
- subsorts TypeSubst < TyEnv .
- op kty : K -> ConfigItem .
- op tenv : TEnv -> ConfigItem .
- op freshTV : Tyvar -> ConfigItem .
- op subst : TyEnv -> ConfigItem .
- endfm
- fmod K-POLYFUN-NAME-STATIC-REDUCTIONS
- is
- including K-POLYFUN-STATIC-CONFIGITEMS .
- including CONFIG .
- including POLYFUN-TYENV .
- vars x : Name .
- vars t : BType .
- vars rest : K .
- vars gamma : TEnv .
- vars a a' : Tyvar .
- vars i : InstResult .
- ceq kty(x -> rest) tenv(gamma) freshTV(a) =
- kty(t -> rest) tenv(gamma) freshTV(a') if
- i := instantiate((get(gamma, x)), a) /\
- t := instResultType(i) /\
- a' := instResultTyV(i) .
- endfm
- fmod K-POLYFUN-CONSTANTS-STATIC-REDUCTIONS is
- including K-POLYFUN-SYNTAX .
- including POLYFUN-BTYPE .
- including POLYFUN-TYENV .
- including K-POLYFUN-STATIC-CONFIGITEMS .
- vars n : Int .
- vars b : Bool .
- eq (#int n) = tyConst('int, nil) .
- eq (#bool b) = tyConst('bool, nil) .
- endfm
- fmod K-POLYFUN-ARITH-INT-REL-LOGIC-STATIC-REDUCTIONS is
- including K-POLYFUN-SYNTAX .
- including K-POLYFUN-STATIC-CONFIGITEMS .
- including CONFIG .
- including MGU .
- vars t1 t2 t3 : BType .
- vars rest : K .
- vars Gamma : TEnv .
- vars sigma sigma' : TypeSubst .
- ceq kty(t1 ++ t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('int, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' := compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
- ceq kty(t1 -- t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('int, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' := compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
- ceq kty(t1 ** t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('int, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' := compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
- ceq kty(t1 <<< t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' :=
- compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
- ceq kty(t1 === t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' :=
- compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
- ceq kty(t1 And t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' :=
- compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('bool, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('bool, nil)))))), sigma) .
- ceq kty(t1 Or t2 -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' :=
- compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('bool, nil))) &&
- ((appSubst(sigma, t2)) <-> (tyConst('bool, nil)))))), sigma) .
- ceq kty(not(t1) -> rest) tenv(Gamma) subst(sigma) =
- kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' :=
- compSubst((mgu(((appSubst(sigma, t1)) <-> (tyConst('bool, nil))))), sigma) .
- ceq kty((if t1 then t2 else t3 fi) -> rest) tenv(Gamma) subst(sigma) =
- kty((appSubst(sigma',(appSubst(sigma, t2)))) -> rest)
- tenv(appSubstTEnv(sigma', Gamma))
- subst(sigma')
- if sigma' :=
- compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('bool, nil))) &&
- ((appSubst(sigma, t2)) <-> (appSubst(sigma, t3)))))), sigma) .
- endfm
- fmod K-POLYFUN-TOP-REDUCTIONS is
- including K-POLYFUN-SYNTAX .
- including K-POLYFUN-STATIC-CONFIGITEMS .
- including CONFIG .
- op [|_|] : K -> Config .
- op done : -> Config .
- subsorts BType < Config .
- vars k1 : K .
- vars t : BType .
- vars beta : Tyvar .
- vars Gamma : TEnv .
- vars sigma : TypeSubst .
- eq [| k1 |] = [[ kty(k1) tenv(nul) subst(empty) freshTV(tyVar(0)) ]] .
- --- eq [[kty(t) tenv(Gamma) subst(sigma) freshTV(beta) ]] = done .
- eq [[kty(t) tenv(Gamma) subst(sigma) freshTV(beta) ]] = appSubst(sigma, t) .
- endfm
- fmod K-POLYFUN-NOFUN-REDUCTIONS is including
- K-POLYFUN-EXPRESSIONS-STATIC-STRICTNESS +
- K-POLYFUN-NAME-STATIC-REDUCTIONS + K-POLYFUN-CONSTANTS-STATIC-REDUCTIONS +
- K-POLYFUN-ARITH-INT-REL-LOGIC-STATIC-REDUCTIONS + K-POLYFUN-TOP-REDUCTIONS .
- endfm
- fmod K-POLYFUN is
- including K-POLYFUN-NOFUN-REDUCTIONS .
- --- some variables
- var I : Identifier .
- vars e e' : KProper .
- var rest : K .
- var beta : Tyvar .
- vars Gamma Gamma' : TEnv .
- vars tau tau' : BType .
- vars sigma sigma' : TypeSubst .
- --- PROBLEM 1
- op restorety : TEnv -> K .
- eq kty((fun I => e) -> rest) tenv(Gamma) freshTV(beta) =
- kty(((beta --> e) -> restorety(Gamma)) -> rest) tenv(Gamma[I <- beta])
- freshTV(incTyVar(beta, 1)) .
- eq kty((tau -> restorety(Gamma)) -> rest) tenv(Gamma') subst(sigma) =
- kty(tau -> rest) tenv(appSubstTEnv(sigma, Gamma)) subst(sigma) .
- --- PROBLEM 2
- ceq kty((tau (| tau' |) ) -> rest) tenv(Gamma) subst(sigma) freshTV(beta) =
- kty(appSubst(sigma',beta) -> rest) tenv(appSubstTEnv(sigma', Gamma))
- subst(compSubst(sigma', sigma)) freshTV(incTyVar(beta, 1))
- if sigma' := (mgu((appSubst(sigma,tau)) <->
- (appSubst(sigma, tau') --> beta))) .
- --- PROBLEM 3
- eq kty(let I = tau in e end -> rest) tenv(Gamma) subst(sigma) =
- kty((e -> restorety(Gamma)) -> rest)
- tenv(Gamma[I <- generalize(Gamma, appSubst(sigma, tau))]) subst(sigma) .
- --- PROBLEM 4
- op hasType : K -> K .
- eq kty(letrec I = e in e' end -> rest) tenv(Gamma) freshTV(beta) =
- kty(e -> hasType(I) -> e' -> restorety(Gamma) -> rest) tenv(Gamma[I <- beta])
- freshTV(incTyVar(beta, 1)) .
- ceq kty(tau -> hasType(I) -> rest) tenv(Gamma) subst(sigma) =
- kty(rest)
- tenv(appSubstTEnv(sigma',
- Gamma[I <- generalize(Gamma,
- appSubst(sigma', tau))]))
- subst(sigma')
- if sigma' := compSubst(sigma,
- mgu(appSubst(sigma, tau) <-> tyConst('int, nil)) .
- --- mgu(appSubst(sigma, tau) <-> appSubst(sigma, Gamma[I]))) .
- endfm
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement