SHARE
TWEET

Untitled

a guest May 19th, 2017 41 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. fmod TOP is
  2.   sort Top .
  3. endfm
  4.  
  5. fmod GENERIC-LIST is including NAT + TOP .
  6.   sorts BotList TopList .
  7.   subsort BotList < TopList < Top .
  8.   op nil : -> BotList .
  9.   op _,_ : BotList BotList -> BotList [assoc id: nil prec 121] .
  10.   op _,_ : TopList TopList -> TopList [ditto] .
  11.   op length_ : BotList -> Nat .
  12.   eq length(nil) = 0 .
  13. endfm
  14.  
  15. fmod KLIST{X :: TRIV} is including GENERIC-LIST .
  16.   sort List{X} NeList{X} .
  17.   subsort BotList < List{X} < TopList .
  18.   subsort X$Elt < NeList{X} < List{X} .
  19.   op _,_ : List{X} List{X} -> List{X} [ditto] .
  20.   op _,_ : NeList{X} List{X} -> NeList{X} [ditto] .
  21.   op _,_ : List{X} NeList{X} -> NeList{X} [ditto] .
  22.   op length_ : List{X} -> Nat [ditto] .
  23.   var x : X$Elt . var xl : List{X} .
  24.   eq length(x, xl) = length(xl) + 1 .
  25. endfm
  26.  
  27. fmod GENERIC-SET is including GENERIC-LIST .
  28.   sorts BotSet TopSet .
  29.   subsort BotSet < TopSet < Top .
  30.   op empty : -> BotSet .
  31.   op _&&_ : BotSet BotSet -> BotSet [assoc comm id: empty prec 121] .
  32.   op _&&_ : TopSet TopSet -> TopSet [ditto] .
  33.   op _in_ : BotList BotSet -> Bool .
  34.   eq nil in empty = false .
  35. endfm
  36.  
  37. fmod KSET{X :: TRIV} is
  38.   including GENERIC-SET .
  39.   including KLIST{X} .
  40.   sorts NeSet{X} Set{X} .
  41.   subsort BotSet < Set{X} < TopSet .
  42.   subsort X$Elt < NeSet{X} < Set{X} .
  43.   op _&&_ : Set{X} Set{X} -> Set{X} [ditto] .
  44.   op _&&_ : NeSet{X} Set{X} -> NeSet{X} [ditto] .
  45.   op _in_ : List{X} Set{X} -> Bool .
  46.   var x : X$Elt . var xs : Set{X} .
  47.   eq x in (x && xs) = true .
  48.   eq x in xs = false [owise] .
  49. endfm
  50.  
  51. fmod TUPLE is including TOP .
  52.   sort Tuple .
  53.   op `[_`] : [Top] -> Tuple .
  54. endfm
  55. view Tuple from TRIV to TUPLE is sort Elt to Tuple . endv
  56.  
  57. fmod GENERIC-MAP is
  58.   including GENERIC-LIST + GENERIC-SET .
  59.   op _[_] : BotSet BotList -> BotList .
  60.   op _[_<-_] : BotSet BotList BotList -> BotSet .
  61.   op _|->_ : BotList BotList -> BotSet .
  62.   eq empty[nil <- nil] = empty .
  63. endfm
  64.  
  65. fmod KMAP{X :: TRIV, Y :: TRIV} is including GENERIC-MAP .
  66.   including KLIST{X} .
  67.   including KLIST{Y} .
  68.   sort Map{X,Y} .
  69.   subsort BotSet < Map{X,Y} < TopSet .
  70.   op _&&_ : Map{X,Y} Map{X,Y} -> Map{X,Y} [ditto] .
  71.   op _[_] : Map{X,Y} List{X} -> List{Y} [ditto] .
  72.   op _[_<-_] : Map{X,Y} List{X} List{Y} -> Map{X, Y} [ditto] .
  73.   op _|->_ : List{X} List{Y} -> Map{X,Y} .
  74. ---  op get : Map{X,Y} X -> Y .
  75.   var x : X$Elt . var y y' : Y$Elt . var map : Map{X,Y} .
  76.   var xl : NeList{X} . var yl : NeList{Y} .
  77.  
  78.   eq ((x |-> y) && map)[x] = y .
  79.   eq map[nil <- nil] = map .
  80.   eq ((x |-> y') && map)[x <- y] = (x |-> y) && map .
  81.   eq map[x <- y] = (x |-> y) && map [owise] .
  82.   eq map[(x,xl) <- (y,yl)] = map[x <- y][xl <- yl] .
  83. ---  eq get(map,x) = map[x] .
  84. endfm
  85.  
  86. fmod K-SORTS is
  87.   sorts K KProper KResult .
  88.   subsorts KProper KResult < K .
  89. endfm
  90.  
  91. view K from TRIV to K-SORTS is sort Elt to K . endv
  92. view KProper from TRIV to K-SORTS is sort Elt to KProper . endv
  93. view KResult from TRIV to K-SORTS is sort Elt to KResult . endv
  94.  
  95. fmod K-PLAIN is including KLIST{K} + KLIST{KProper} * (sort NeList{KProper} to NeKProperList) + KLIST{KResult} .
  96.   subsorts List{KProper} List{KResult} < List{K} .
  97.   subsorts NeKProperList NeList{KResult} < NeList{K} .
  98.  
  99.   op .K : -> K .
  100.   op _->_ : K K -> K [prec 50 assoc id: .K] .
  101.   op _->_ : KProper K -> KProper [ditto] .
  102.  
  103.   var r : KResult . var kp : KProper . var kl1 kl2 : List{K} . ---KList .
  104.   var rl : List{KResult} . ---KResultList .
  105.   op strict_ : List{K} --- KList
  106.     -> K .
  107.   op result_ : List{KResult} ---  KResultList
  108.    -> KResult .
  109.   op strictfreeze : List{K} List{K} --- KList KList
  110.    -> K .
  111.   eq strict(kl1,kp,kl2) = kp -> strictfreeze(kl1,kl2) .
  112.   eq r -> strictfreeze(kl1,kl2) = strict(kl1,r,kl2) .
  113.   eq strict(rl) = result(rl) .
  114.  
  115.   op seqstrict_ : List{K} --- KList
  116.     -> K .
  117.   op seqstrictfreeze : List{KResult} List{K} --- KResultList KList
  118.     -> K .
  119.   eq strict(rl,kp,kl2) = kp -> seqstrictfreeze(rl, kl2) .
  120.   eq r -> seqstrictfreeze(rl, kl2) = seqstrict(rl, r, kl2) .
  121.   eq seqstrict(rl) = result(rl) .
  122. endfm
  123.  
  124. fmod NAME is sort Name . endfm
  125. view Name from TRIV to NAME is sort Elt to Name . endv
  126.  
  127. fmod VAL is sort Val . endfm
  128. view Val from TRIV to VAL is sort Elt to Val . endv
  129.  
  130. fmod LOC is
  131.   including INT .
  132.   sorts Loc .
  133.  
  134.   op loc : Nat -> Loc .
  135.   op _+Loc_ : Loc Int -> Loc .
  136.   vars N : Nat . var I : Int .
  137.   eq loc(N) +Loc I = loc(N + I) .
  138. endfm
  139.  
  140. view Loc from TRIV to LOC is sort Elt to Loc . endv
  141.  
  142. fmod LOC-COMPREHENSION is including KLIST{Loc} .
  143.   vars N N' : Nat .
  144.   op _..._ : Loc Loc -> List{Loc} [prec 10] .
  145.  ceq loc(N) ... loc(N') = nil if N' < N .
  146.   eq loc(N) ... loc(N') = loc(N), loc(N + 1) ... loc(N') .
  147. endfm
  148.  
  149. fmod ENV is including KMAP{Name, Loc} *
  150.            (sort Map{Name, Loc} to Env, op _`[_`] to get) . endfm
  151. view Env from TRIV to ENV is sort Elt to Env . endv
  152.  
  153. fmod TYPE is
  154.   sort Type .
  155.   op ? : -> Type .
  156. endfm
  157.  
  158. view Type from TRIV to TYPE is sort Elt to Type . endv
  159.  
  160. fmod TENV is including KMAP{Name, Type} *
  161.      (sort Map{Name, Type} to TEnv, op _`[_`] to get) . endfm
  162.  
  163. fmod TYPED-LOCATION-SORT is sort TypedLoc . endfm
  164. view TypedLoc from TRIV to TYPED-LOCATION-SORT is sort Elt to TypedLoc . endv
  165.  
  166.  
  167. fmod TYPED-LOCATION is
  168.   including KLIST{Type} .
  169.   including KLIST{Loc} .
  170.   including KLIST{TypedLoc} .
  171.   op _:_ : Loc Type -> TypedLoc .
  172.   op _:_ : List{Loc} List{Type} -> List{TypedLoc} [ditto] .
  173.   op type : TypedLoc -> Type .
  174.   op loc : TypedLoc -> Loc .
  175.   var l : Loc . var t : Type . var ll : NeList{Loc} . var tl : NeList{Type} .
  176.   eq type(l : t) = t .
  177.   eq loc(l : t) = l .
  178.   eq (l, ll) : (t, tl) = (l : t), (ll : tl) .
  179.   eq nil : nil = nil .
  180. endfm
  181.  
  182.  
  183. fmod TYPED-ENV is including KMAP{Name, TypedLoc} *
  184.   (sort Map{Name, TypedLoc} to Env) .
  185.   including TYPED-LOCATION . endfm
  186.  
  187. view TypedEnv from TRIV to TYPED-ENV is sort Elt to Env . endv
  188.  
  189. fmod STORE is including KMAP{Loc, Val} * (sort Map{Loc, Val} to Store, op _`[_`] to get) . endfm
  190.  
  191. fmod STACK is including KLIST{Tuple} * (sort List{Tuple} to Stack) . endfm
  192.  
  193. fmod CONFIG-ITEM is sort ConfigItem . endfm
  194. view ConfigItem from TRIV to CONFIG-ITEM is sort Elt to ConfigItem . endv
  195.  
  196. fmod CONFIG is including SET{ConfigItem} * (op _`,_ to __) .
  197.   sort Config .
  198.   op [[_]] : Set{ConfigItem} -> Config .
  199. endfm
  200.  
  201. ***( Types of List neeed:
  202. List{Tyvar}
  203. List{BType}
  204. List{Type}
  205. List{K}
  206.  
  207. KSET-MINUS{Tyvar}
  208. )***
  209. -----------------------Type Infrastructure ----------------------------
  210.  
  211. fmod BTYPE is
  212.   including TYPE .
  213.   sort BType .
  214.   subsort BType < Type .
  215. endfm
  216.  
  217. view BType from TRIV to BTYPE is sort Elt to BType . endv
  218.  
  219. fmod TYVAR is
  220.   including INT .
  221.   sort Tyvar .
  222.   op tyVar : Int -> Tyvar .
  223.   op incTyVar : Tyvar Int -> Tyvar .
  224.   vars N M : Int .
  225.   eq incTyVar(tyVar(N), M) = tyVar(N + M) .
  226. endfm
  227.  
  228. view Tyvar from TRIV to TYVAR is sort Elt to Tyvar . endv
  229.  
  230. fmod TYVAR-SEQ is
  231.   including KLIST{Tyvar} .
  232.   vars N : Nat .
  233.   vars tv : Tyvar .
  234.   op tyvarseq : Tyvar Nat -> List{Tyvar} .
  235.   eq tyvarseq(tv, 0) = tv .
  236.   eq tyvarseq(tv, N) = (tv, tyvarseq(incTyVar(tv,1),(N - 1))) .
  237. endfm
  238.  
  239. fmod TYPE-SUBST is
  240.   including KMAP {Tyvar, BType} *
  241.     (sort Map{Tyvar, BType} to TypeSubst, op _|->_ to _goesto_ ,
  242.      op _`[_<-_`] to _`[_gets_`], op _`[_`] to tysubstget , op _&&_ to _with_ ,
  243.      op _in_ to _eltof_ ) .
  244.   op appSubst : TypeSubst BType -> BType .
  245.   op compSubst : TypeSubst TypeSubst -> TypeSubst .
  246.   op compSubstAux : TypeSubst TypeSubst -> TypeSubst .
  247.   op compSubstThin : TypeSubst TypeSubst -> TypeSubst .
  248.  
  249.   vars tv tv' : Tyvar .
  250.   vars t t' : BType .
  251.   vars sigma sigma' : TypeSubst .
  252.  
  253.   eq appSubst (((tv goesto t) with sigma), tv) = t .
  254.   eq appSubst (sigma, tv) = tv [owise] .
  255.  
  256.   eq compSubstAux (sigma', ((tv goesto t) with sigma)) =
  257.      ((tv goesto appSubst(sigma', t)) with (compSubstAux(sigma', sigma))) .
  258.   eq compSubstAux (sigma', empty) = empty .
  259.   eq compSubstThin (((tv goesto t') with sigma'), ((tv goesto t) with sigma)) =
  260.      compSubstThin (sigma', ((tv goesto t) with sigma)) .
  261.   eq compSubstThin (sigma', sigma) = (sigma' with sigma) [owise] .
  262.   eq compSubst (sigma', sigma) =
  263.      compSubstThin(sigma', compSubstAux(sigma', sigma)) .
  264. endfm
  265.  
  266. fmod POLYFUN-BTYPE is
  267.   including QID .
  268.   including KLIST{BType} .
  269.   including TYPE-SUBST .
  270.   including KSET{Tyvar} .
  271.   including K-PLAIN .
  272.  
  273.   subsort Tyvar < BType .
  274.   subsort NeList{Tyvar} < NeList{BType} < NeList{K} .
  275.   subsort List{Tyvar} < List{BType} < List{K} .
  276.  
  277.   op tyConst : Qid List{BType} -> BType .
  278.   op tyConstK : Qid List{K} -> K .
  279.   op _-->_ : BType BType -> BType .
  280.   op _-->_ : K K -> K [ditto].
  281.   op occurs : Tyvar BType -> Bool .
  282.   op freeTyvars : List{BType} -> Set{Tyvar} .
  283.   op appSubstList : TypeSubst List{BType} -> List{BType} .
  284.  
  285.   vars tl tl' : List{BType} .
  286.   vars e e' : K .
  287.   vars t t' : BType .
  288.   vars sigma : TypeSubst .
  289.   vars N : Int .
  290.   vars tv tv' : Tyvar .
  291.   vars tyc : Qid .
  292.  
  293.   eq t --> t' = tyConst('fun,(t,t')) .
  294.   eq e --> e' = tyConstK('fun,(e,e')) .
  295.   eq tyConstK('fun,(t,t')) = tyConst('fun,(t,t')) .
  296.  
  297.   eq occurs(tv, (tv,tl)) = true .
  298.   eq occurs(tv, (tv',tl)) = occurs(tv, tl) [owise] .
  299.   eq occurs(tv, ((tyConst(tyc, tl)), tl')) = occurs(tv, (tl, tl')) .
  300.   eq occurs(tv, nil) = false .
  301.  
  302.   eq appSubst(sigma, tyConst(tyc,tl)) = tyConst(tyc,appSubstList(sigma, tl)) .
  303.  
  304.   eq appSubstList(sigma, nil) = nil .
  305.   eq appSubstList(sigma, (t, tl)) = (appSubst(sigma, t), appSubstList(sigma, tl)) .
  306.  
  307.   eq freeTyvars (tv) = (tv) .
  308.   eq freeTyvars (tyConst(tyc,tl)) = freeTyvars(tl) .
  309.   eq freeTyvars ((t,tl)) = (freeTyvars(t)) && (freeTyvars(tl)) .
  310.   eq freeTyvars (nil) = empty .
  311.  
  312. endfm
  313.  
  314. fmod KSET-MINUS{X :: TRIV} is
  315.   including KSET{X} .
  316.   including KLIST{X} .
  317.   op setminus : Set{X} Set{X} -> Set{X} .
  318.   op setlistminus : Set{X} List{X} -> Set{X} .
  319.   var x y : X$Elt .
  320.   vars xs ys : Set{X} .
  321.   vars xl : List{X} .
  322.   eq (x && x && xs) = (x && xs) .
  323.   eq setminus((x && xs), (x && ys)) = setminus(xs, ys) .
  324.   ceq setminus(xs, (y && ys)) = setminus (xs, ys) if not (y in xs) .
  325.   eq setminus(xs, empty) = xs .
  326.   eq setlistminus(xs, nil) = xs .
  327.   eq setlistminus((x && xs), (x, xl)) = setlistminus(xs, xl) .
  328.   ceq setlistminus(xs, (x, xl)) = setlistminus(xs, xl) if not (x in xs) .
  329. endfm
  330.  
  331. fmod CONSTRAINT is
  332.   including POLYFUN-BTYPE .
  333.   sort Constraint .
  334.   op _<->_ : BType BType -> Constraint .
  335. endfm
  336.  
  337. view Constraint from TRIV to CONSTRAINT is sort Elt to Constraint . endv
  338.  
  339. fmod MGU is
  340.   including KSET{Constraint} .
  341.   including KLIST{BType} .
  342.   including TYPE-SUBST .
  343.  
  344.   sort TypeSubstOrError SetConstOrError .
  345.   subsort TypeSubst < TypeSubstOrError .
  346.   subsort Set{Constraint} < SetConstOrError .
  347.  
  348.   op SCError : -> SetConstOrError .
  349.   op TSError : -> TypeSubstOrError .
  350.  
  351.   op appSubstConst : TypeSubst Set{Constraint} -> Set{Constraint} .
  352.   op zipConstraints : List{BType} List{BType} -> SetConstOrError .
  353.   op mgu : Set{Constraint} -> TypeSubstOrError .
  354.  
  355.   vars s t : BType .
  356.   vars sl tl tl' : List{BType} .
  357.   vars tv tv' : Tyvar .
  358.   vars S : Set{Constraint} .
  359.   vars tyc tyc' : Qid .
  360.   vars sigma phi psi : TypeSubst .
  361.  
  362.   eq appSubstConst(sigma, ((s <-> t) && S)) =
  363.      (((appSubst(sigma, s)) <-> (appSubst(sigma, t))) &&
  364.       appSubstConst(sigma, S)) .
  365.   eq appSubstConst(sigma, empty) = empty .
  366.  
  367.   eq zipConstraints ((s, sl), (t, tl)) = (s <-> t) && (zipConstraints(sl, tl)) .
  368.   eq zipConstraints (nil, nil) = empty .
  369.   eq zipConstraints (nil, (t, tl)) = SCError .
  370.   eq zipConstraints ((s, sl), nil) = SCError .
  371.  
  372.   eq mgu(empty) = empty .
  373.   eq mgu(((tv <-> tv) && S)) = mgu(S) .
  374.   eq mgu(((tyConst(tyc, sl) <-> tyConst(tyc, tl)) && S)) =
  375.      mgu(((zipConstraints(sl, tl)) && S)) .
  376.   ceq mgu(((tyConst(tyc, sl) <-> tyConst(tyc', tl)) && S)) = TSError
  377.       if not (tyc == tyc') .
  378.   eq mgu(((tyConst(tyc, tl) <-> tv) && S)) =
  379.      mgu(((tv <-> tyConst(tyc, tl)) && S)) .
  380.   ceq mgu(((tv <-> t) && S)) = compSubst((tv goesto appSubst(psi, t)), psi)
  381.    if (occurs(tv, t)) = false /\ psi := (mgu(appSubstConst((tv goesto t),S))) .
  382. endfm
  383.  
  384. fmod POLYFUN-GTYPE is
  385.   including KLIST{Type} .
  386.   including KLIST{Tyvar} .
  387.   including KSET-MINUS{Tyvar} .
  388.   including TYPE-SUBST .
  389.   including POLYFUN-BTYPE .
  390.   including BOOL .
  391.  
  392.   subsort NeList{BType} < NeList{Type} .
  393.   subsort List{BType} < List{Type} .
  394.  
  395.   op forall : List{Tyvar} BType -> Type .
  396.   op freeTyvars : List{Type} -> Set{Tyvar} [ditto] .
  397.   op appSubst : TypeSubst Type -> Type [ditto] .
  398.   op thinSubst : TypeSubst BType -> TypeSubst .
  399.   op cksubst : TypeSubst List{Tyvar} Type -> Type .
  400.   op cksubst : TypeSubst List{Tyvar} BType -> BType [ditto] .
  401.   op checkNoFreeVarCapture : TypeSubst List{Tyvar} -> Bool .
  402.   op listmem : Tyvar List{Tyvar} -> Bool .
  403.  
  404.   vars t t' : BType .
  405.   vars tv tv': Tyvar .
  406.   vars tvl tvl' : List{Tyvar} .
  407.   vars tl : List{BType} .
  408.   vars sigma : TypeSubst .
  409.  
  410.   eq forall((nil), t) = t .
  411.  
  412.   eq listmem(tv, (tvl, tv, tvl')) = true .
  413.   eq listmem(tv, tvl) = false [owise] .
  414.  
  415.   eq freeTyvars (forall(tl, t)) = setminus(freeTyvars (t), tl) .
  416.   eq appSubst(((tv goesto t) with sigma), (forall((tvl, tv, tvl'), t'))) =
  417.      appSubst(sigma, forall((tvl, tv, tvl'), t')) .
  418.  
  419.   eq appSubst(sigma, forall(tvl, t)) =
  420.      forall(tvl, cksubst((thinSubst(sigma, t)), tvl, t)) [owise] .
  421.  
  422.   eq thinSubst(empty, t) = empty .
  423.  
  424.   ceq thinSubst((tv goesto t) with sigma, t') =
  425.       thinSubst(sigma, t')
  426.    if not(occurs(tv, t')) .
  427.  
  428.   eq thinSubst((tv goesto t) with sigma, t') =
  429.      ((tv goesto t) with thinSubst(sigma, t')) [owise] .
  430.  
  431.   ceq cksubst(sigma, tvl, t) = appSubst(sigma, t) if
  432.       checkNoFreeVarCapture(sigma, tvl) .
  433.  
  434.   eq checkNoFreeVarCapture (((tv goesto t) with sigma), tvl) =
  435.      (setlistminus(freeTyvars(t), tvl) == freeTyvars(t)) and
  436.      checkNoFreeVarCapture (sigma, tvl) .
  437.   eq checkNoFreeVarCapture (empty, tvl) = true .
  438. endfm
  439.  
  440. fmod POLYFUN-TYENV is
  441.   including POLYFUN-GTYPE .
  442.   including TENV * (op empty to nul) .
  443.   including KLIST{Tyvar} .
  444.  
  445.   sort InstResult .
  446.  
  447.   op freeTyvars : TEnv -> Set{Tyvar} [ditto] .
  448.   op appSubstTEnv : TypeSubst TEnv -> TEnv .
  449.   op instResult : BType Tyvar -> InstResult .
  450.   op instantiate : Type Tyvar -> InstResult .
  451.   op instResultType : InstResult -> BType .
  452.   op instResultTyV : InstResult -> Tyvar .
  453.   op setToList : Set{Tyvar} -> List{Tyvar} .
  454.   op generalize : TEnv BType -> Type .
  455.   op setmem : Tyvar Set{Tyvar} -> Bool .
  456.  
  457.   vars n : Name .
  458.   vars Gamma : TEnv .
  459.   vars t : Type .
  460.   vars bt : BType .
  461.   vars sigma : TypeSubst .
  462.   vars tv tv' : Tyvar .
  463.   vars tvl tvl' : List{Tyvar} .
  464.   vars tvs : Set{Tyvar} .
  465.   vars tl : List{BType} .
  466.  
  467.   eq freeTyvars(((n |-> t) && Gamma)) = (freeTyvars(t) && freeTyvars(Gamma)) .
  468.   eq freeTyvars(nul) = empty .
  469.  
  470.   eq appSubstTEnv(sigma, ((n |-> t) && Gamma)) =
  471.      (n |-> (appSubst(sigma, t))) && appSubstTEnv(sigma, Gamma) .
  472.   eq appSubstTEnv(sigma, nul) = nul .
  473.  
  474.   eq instantiate ((forall((tv, tvl), t)), tv') =
  475.      instantiate ((forall(tvl, appSubst((tv goesto tv'), t))), incTyVar(tv', 1)) .
  476.  
  477.   eq instantiate (bt, tv') = instResult(bt, tv') .
  478.  
  479.   eq instResultType(instResult(bt, tv)) = bt .
  480.   eq instResultTyV(instResult(bt, tv)) = tv .
  481.  
  482.   eq setmem(tv, (tv && tvs)) = true .
  483.   eq setmem(tv, tvs) = false [owise] .
  484.  
  485.   eq setToList(empty) = nil .
  486.   ceq setToList((tv && tvs)) = (tv, setToList(tvs))
  487.    if not (setmem(tv, tvs)) .
  488.   eq setToList((tv && tvs)) = (setToList(tvs)) [owise] .
  489.  
  490.   eq generalize (Gamma, bt) =
  491.      (forall((setToList(setminus(freeTyvars(bt),freeTyvars(Gamma)))), bt)) .
  492.  
  493. endfm
  494.  
  495.  
  496. -------------------- Syntax, including strictness -----------------------
  497.  
  498.  
  499. fmod K-POLYFUN-BTYPE-STRICTNESS is
  500.   including POLYFUN-BTYPE .
  501.  
  502.   op tyConstArgBox : Qid List{K} List{K} -> K .
  503.  
  504.   vars tyc : Qid .
  505.   vars krl : List{KResult} .
  506.   vars kl : List{K} .
  507.   vars kp : KProper .
  508.   vars kr : KResult .
  509.  
  510.   eq (tyConstK(tyc, (krl, kp, kl))) = (kp -> tyConstArgBox(tyc, krl, kl)) .
  511.   eq (kr -> tyConstArgBox(tyc, krl, kl)) = tyConstK(tyc, (krl, kr, kl)) .
  512. endfm
  513.  
  514. fmod CONSTANT is
  515.   including INT .
  516.   including BOOL .
  517.   including VAL .
  518.   op #int_ : Int -> Val [prec 0] .
  519.   op #bool_ : Bool -> Val [prec 0] .
  520. endfm
  521.  
  522. fmod IDENTIFIER is
  523.   including NAME .
  524.   including QID .
  525.   including K-PLAIN .
  526.  
  527.   sort Identifier .
  528.  
  529.   subsort Qid < Identifier < Name < KProper .
  530.   ---Names may be looked up in Environments and Type Environments;
  531.  
  532.   endfm
  533.  
  534. view Identifier from TRIV to IDENTIFIER is sort Elt to Identifier . endv
  535.  
  536. fmod K-POLYFUN-ARITH-SYNTAX is
  537.   including K-SORTS .
  538.   op _++_ : K K -> KProper [prec 33 assoc] .
  539.   op _--_ : K K -> KProper [prec 33 gather(E e)] .
  540.   op _**_ : K K -> KProper [prec 31 assoc] .
  541. endfm
  542.  
  543.  
  544. fmod K-POLYFUN-ARITH-SYNTAX-DYNAMIC-STRICTNESS is
  545.   including K-POLYFUN-ARITH-SYNTAX .
  546.   including K-PLAIN .
  547.  
  548.   vars kp1 kp2 : KProper .
  549.   vars kr1 kr2 : KResult .
  550.   vars k2 : K .
  551.  
  552.   op []++_ : K -> K .
  553.   eq kp1 ++ k2 = kp1 -> []++ k2 .
  554.   eq kr1 -> []++ k2 = kr1 ++ k2 .
  555.   op _++[] : KResult -> K .
  556.   eq kr1 ++ kp2 = kp2 -> kr1 ++[] .
  557.   eq kr2 -> kr1 ++[] = kr1 ++ kr2 .
  558.  
  559.   op []--_ : K -> K .
  560.   eq kp1 -- k2 = kp1 -> []-- k2 .
  561.   eq kr1 -> []-- k2 = kr1 -- k2 .
  562.   op _--[] : KResult -> K .
  563.   eq kr1 -- kp2 = kp2 -> kr1 --[] .
  564.   eq kr2 -> kr1 --[] = kr1 -- kr2 .
  565.  
  566.   op []**_ : K -> K .
  567.   eq kp1 ** k2 = kp1 -> []** k2 .
  568.   eq kr1 -> []** k2 = kr1 ** k2 .
  569.   op _**[] : KResult -> K .
  570.   eq kr1 ** kp2 = kp2 -> kr1 **[] .
  571.   eq kr2 -> kr1 **[] = kr1 ** kr2 .
  572.  
  573. endfm
  574.  
  575. fmod K-POLYFUN-INT-REL-SYNTAX is
  576.   including K-SORTS .
  577.   op _<<<_ : K K -> KProper [prec 37] .
  578.   op _===_ : K K -> KProper  [prec 37] .
  579. endfm
  580.  
  581. fmod K-POLYFUN-INT-REL-SYNTAX-DYNAMIC-STRICTNESS is
  582.   including K-POLYFUN-INT-REL-SYNTAX .
  583.   including K-PLAIN .
  584.  
  585.   vars kp1 kp2 : KProper .
  586.   vars kr1 kr2 : KResult .
  587.   vars k2 : K .
  588.  
  589. --- Exp <<< Exp [strict, extends <:Int * Int -> Bool]
  590.   op []<<<_ : K -> K .
  591.   eq kp1 <<< k2 = kp1 -> []<<< k2 .
  592.   eq kr1 -> []<<< k2 = kr1 <<< k2 .
  593.   op _<<<[] : KResult -> K .
  594.   eq kr1 <<< kp2 = kp2 -> kr1 <<<[] .
  595.   eq kr2 -> kr1 <<<[] = kr1 <<< kr2 .
  596.  
  597. --- Exp === Exp [strict, extends =:Int * Int -> Bool]
  598.   op []===_ : K -> K .
  599.   eq kp1 === k2 = kp1 -> []=== k2 .
  600.   eq kr1 -> []=== k2 = kr1 === k2 .
  601.   op _===[] : KResult -> K .
  602.   eq kr1 === kp2 = kp2 -> kr1 ===[] .
  603.   eq kr2 -> kr1 ===[] = kr1 === kr2 .
  604.  
  605. endfm
  606.  
  607. fmod K-POLYFUN-LOGIC-SYNTAX is
  608.   including K-SORTS .
  609.   op not_ : K -> KProper .
  610.   op _And_ : K K -> KProper [prec 55 assoc] .
  611.   op _Or_ : K K -> KProper [prec 59 assoc] .
  612.   op if_then_else_fi : K K K -> KProper .
  613. endfm
  614.  
  615. fmod K-POLYFUN-LOGIC-SYNTAX-DYNAMIC-STRICTNESS is
  616.   including K-POLYFUN-LOGIC-SYNTAX .
  617.   including K-PLAIN .
  618.   vars kp1 kp2 : KProper .
  619.   vars kr1 kr2 : KResult .
  620.   vars k1 k2 : K .
  621.  
  622.   op not[] : -> K .
  623.   eq not kp1 = kp1 -> not[] .
  624.   eq kr1 -> not[] = not kr1 .
  625.  
  626. --- BExp And BExp [strict(1), ... ]
  627.   op []And_ : K -> K .
  628.   eq kp1 And k2 = kp1 -> []And k2 .
  629.   eq kr1 -> []And k2 = kr1 And k2 .
  630.  
  631. --- BExp Or BExp [strict(1), ... ]
  632.   op []Or_ : K -> K .
  633.   eq kp1 Or k2 = kp1 -> []Or k2 .
  634.   eq kr1 -> []Or k2 = kr1 Or k2 .
  635.  
  636.   op if[]then_else_fi : K K -> K .
  637.   eq if kp1 then k1 else k2 fi = kp1 -> (if[]then k1 else k2 fi) .
  638.   eq kr1 -> (if[]then k1 else k2 fi) = if kr1 then k1 else k2 fi .
  639.  
  640. endfm
  641.  
  642. fmod K-POLYFUN-LOGIC-SYNTAX-STATIC-STRICTNESS is
  643.   including K-POLYFUN-LOGIC-SYNTAX-DYNAMIC-STRICTNESS .
  644.   including K-PLAIN .
  645.   vars kp1 kp2 : KProper .
  646.   vars kr kr1 kr2 : KResult .
  647.   vars k2 : K .
  648.  
  649. --- BExp And BExp [strict, ... ]
  650.   op _And[] : KResult -> K .
  651.   eq kr1 And kp2 = kp2 -> kr1 And[] .
  652.   eq kr2 -> kr1 And[] = kr1 And kr2 .
  653.  
  654. --- BExp Or BExp [strict, ... ]
  655.   op _Or[] : KResult -> K .
  656.   eq kr1 Or kp2 = kp2 -> kr1 Or[] .
  657.   eq kr2 -> kr1 Or[] = kr1 Or kr2 .
  658.  
  659.   op if_then[]else_fi : KResult K -> K .
  660.   eq if kr1 then kp1 else k2 fi = kp1 -> if kr1 then[]else k2 fi .
  661.   eq kr2 -> if kr1 then[]else k2 fi = if kr1 then kr2 else k2 fi .
  662.  
  663.   op if_then_else[]fi : KResult KResult -> K .
  664.   eq if kr1 then kr2 else kp2 fi = kp2 -> if kr1 then kr2 else[]fi .
  665.   eq kr2 -> if kr then kr1 else[]fi = if kr then kr1 else kr2 fi .
  666. endfm
  667.  
  668. fmod K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX is
  669.   including K-PLAIN .
  670.   including IDENTIFIER .
  671.   including KLIST{Qid} .
  672.   including KLIST{Identifier} .
  673.   including KLIST{Name} .
  674.   subsort List{Qid} < List{Identifier} < List{Name} < List{KProper} .
  675.   subsort NeList{Qid} < NeList{Identifier} < NeList{Name} < NeKProperList .
  676.  
  677.   op fun_=>_ : Identifier K -> KProper .
  678.   op _(|_|) : K K -> KProper [prec 1 gather (E e)].
  679.   op let_=_in_end : Identifier K K -> KProper .
  680.   op letrec_=_in_end : Identifier K K -> KProper .
  681. endfm
  682.  
  683. fmod K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX-DYNAMIC-STRICTNESS is
  684.   including K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX .
  685.   op let_=[]in_end : Identifier K -> K .
  686.   op BoxApp : K -> K .
  687.   op AppBox : KResult -> K .
  688.   vars kp1 kp2 : KProper .
  689.   vars kr1 kr2 : KResult .
  690.   vars k2 : K .
  691.   vars x : Identifier .
  692.   eq let x = kp1 in k2 end = kp1 -> let x =[]in k2 end .
  693.   eq kr1 -> let x =[]in k2 end = let x = kr1 in k2 end .
  694.   eq kp1 (| k2 |) = kp1 -> BoxApp(k2) .
  695.   eq kr1 -> BoxApp(k2) = kr1 (| k2 |) .
  696.   eq kr1 (| kp2 |) = kp2 -> AppBox(kr1) .
  697.   eq kr2 -> AppBox(kr1) = kr1 (| kr2 |) .
  698. endfm
  699.  
  700. fmod K-POLYFUN-SYNTAX is
  701.   including CONSTANT .
  702.   including IDENTIFIER .
  703.   including K-POLYFUN-ARITH-SYNTAX .
  704.   including K-POLYFUN-INT-REL-SYNTAX .
  705.   including K-POLYFUN-LOGIC-SYNTAX .
  706.   including K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX .
  707.   subsorts Val < KResult .
  708. endfm
  709.  
  710. fmod K-POLYFUN-EXPRESSIONS-DYNAMIC-STRICTNESS is
  711.   including K-POLYFUN-ARITH-SYNTAX-DYNAMIC-STRICTNESS .
  712.   including K-POLYFUN-INT-REL-SYNTAX-DYNAMIC-STRICTNESS .
  713.   including K-POLYFUN-LOGIC-SYNTAX-DYNAMIC-STRICTNESS .
  714.   including K-POLYFUN-FUN-APP-LET-LETREC-SYNTAX-DYNAMIC-STRICTNESS .
  715. endfm
  716.  
  717. fmod K-POLYFUN-EXPRESSIONS-STATIC-STRICTNESS is
  718.   including K-POLYFUN-BTYPE-STRICTNESS .
  719.   including K-POLYFUN-EXPRESSIONS-DYNAMIC-STRICTNESS .
  720.   including K-POLYFUN-LOGIC-SYNTAX-STATIC-STRICTNESS .
  721. endfm
  722.  
  723. --------------------Config Items and Reduction Rules--------------------
  724.  
  725.  
  726. fmod K-POLYFUN-STATIC-CONFIGITEMS is
  727.   including K-PLAIN .
  728.   including CONFIG-ITEM .
  729.   including POLYFUN-GTYPE .
  730.   including KLIST{Type} .
  731.  
  732.   including POLYFUN-TYENV .
  733.   including KMAP{Tyvar, Type} *
  734.             (sort Map{Tyvar, Type} to TyEnv, op _|->_ to _goesto_ ,
  735.              op _`[_<-_`] to _`[_gets_`], op _`[_`] to get ,
  736.              op _&&_ to _with_ , op _in_ to _eltof_ ) .
  737.   including TYPE-SUBST .
  738.  
  739.  --- subsorts Type < KResult . --- I think I oly need BType < KResult .
  740.   subsorts BType < KResult .
  741.   subsorts List{BType} < List{KResult} .
  742.   subsorts NeList{BType} < NeList{KResult} .
  743.   subsorts TypeSubst < TyEnv .
  744.  
  745.   op kty : K -> ConfigItem .
  746.   op tenv : TEnv -> ConfigItem .
  747.   op freshTV : Tyvar -> ConfigItem .
  748.   op subst : TyEnv -> ConfigItem .
  749. endfm
  750.  
  751. fmod K-POLYFUN-NAME-STATIC-REDUCTIONS
  752.  is
  753.   including K-POLYFUN-STATIC-CONFIGITEMS .
  754.   including CONFIG .
  755.   including POLYFUN-TYENV .
  756.  
  757.   vars x : Name .
  758.   vars t : BType .
  759.   vars rest : K .
  760.   vars gamma : TEnv .
  761.   vars a a' : Tyvar .
  762.   vars i : InstResult .
  763.  
  764.   ceq kty(x -> rest) tenv(gamma) freshTV(a) =
  765.       kty(t -> rest) tenv(gamma) freshTV(a') if
  766.   i := instantiate((get(gamma, x)), a) /\
  767.   t := instResultType(i) /\
  768.   a' := instResultTyV(i) .
  769. endfm
  770.  
  771. fmod K-POLYFUN-CONSTANTS-STATIC-REDUCTIONS is
  772.   including K-POLYFUN-SYNTAX .
  773.   including POLYFUN-BTYPE .
  774.   including POLYFUN-TYENV .
  775.   including K-POLYFUN-STATIC-CONFIGITEMS .
  776.  
  777.   vars n : Int .
  778.   vars b : Bool .
  779.  
  780.   eq (#int n) = tyConst('int, nil) .
  781.   eq (#bool b) = tyConst('bool, nil) .
  782.  
  783. endfm
  784.  
  785. fmod K-POLYFUN-ARITH-INT-REL-LOGIC-STATIC-REDUCTIONS is
  786.   including K-POLYFUN-SYNTAX .
  787.   including K-POLYFUN-STATIC-CONFIGITEMS .
  788.   including CONFIG .
  789.   including MGU .
  790.  
  791.   vars t1 t2 t3 : BType .
  792.   vars rest : K .
  793.   vars Gamma : TEnv .
  794.   vars sigma sigma' : TypeSubst .
  795.  
  796.   ceq kty(t1 ++ t2 -> rest) tenv(Gamma) subst(sigma) =
  797.       kty((tyConst('int, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  798.       subst(sigma')
  799.    if sigma' := compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
  800.                     ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
  801.  
  802.   ceq kty(t1 -- t2 -> rest) tenv(Gamma) subst(sigma) =
  803.       kty((tyConst('int, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  804.       subst(sigma')
  805.    if sigma' := compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
  806.                     ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
  807.  
  808.   ceq kty(t1 ** t2 -> rest) tenv(Gamma) subst(sigma) =
  809.       kty((tyConst('int, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  810.       subst(sigma')
  811.    if sigma' := compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
  812.                     ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
  813.  
  814.   ceq kty(t1 <<< t2 -> rest) tenv(Gamma) subst(sigma) =
  815.       kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  816.       subst(sigma')
  817.    if sigma' :=
  818.       compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
  819.                     ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
  820.  
  821.   ceq kty(t1 === t2 -> rest) tenv(Gamma) subst(sigma) =
  822.       kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  823.       subst(sigma')
  824.    if sigma' :=
  825.       compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('int, nil))) &&
  826.                     ((appSubst(sigma, t2)) <-> (tyConst('int, nil)))))), sigma) .
  827.  
  828.   ceq kty(t1 And t2 -> rest) tenv(Gamma) subst(sigma) =
  829.       kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  830.       subst(sigma')
  831.    if sigma' :=
  832.       compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('bool, nil))) &&
  833.                     ((appSubst(sigma, t2)) <-> (tyConst('bool, nil)))))), sigma) .
  834.  
  835.   ceq kty(t1 Or t2 -> rest) tenv(Gamma) subst(sigma) =
  836.       kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  837.       subst(sigma')
  838.    if sigma' :=
  839.       compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('bool, nil))) &&
  840.                     ((appSubst(sigma, t2)) <-> (tyConst('bool, nil)))))), sigma) .
  841.  
  842.   ceq kty(not(t1) -> rest) tenv(Gamma) subst(sigma) =
  843.       kty((tyConst('bool, nil)) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  844.       subst(sigma')
  845.    if sigma' :=
  846.    compSubst((mgu(((appSubst(sigma, t1)) <-> (tyConst('bool, nil))))), sigma) .
  847.  
  848.   ceq kty((if t1 then t2 else t3 fi) -> rest) tenv(Gamma) subst(sigma) =
  849.       kty((appSubst(sigma',(appSubst(sigma, t2)))) -> rest)
  850.       tenv(appSubstTEnv(sigma', Gamma))
  851.       subst(sigma')
  852.    if sigma' :=
  853.       compSubst((mgu((((appSubst(sigma, t1)) <-> (tyConst('bool, nil))) &&
  854.                     ((appSubst(sigma, t2)) <-> (appSubst(sigma, t3)))))), sigma) .
  855.  
  856. endfm
  857.  
  858. fmod K-POLYFUN-TOP-REDUCTIONS is
  859.   including K-POLYFUN-SYNTAX .
  860.   including K-POLYFUN-STATIC-CONFIGITEMS .
  861.   including CONFIG .
  862.  
  863.   op [|_|] : K -> Config .
  864.   op done : -> Config .
  865.  
  866.   subsorts BType < Config .
  867.  
  868.   vars k1 : K .
  869.   vars t : BType .
  870.   vars beta : Tyvar .
  871.   vars Gamma : TEnv .
  872.   vars sigma : TypeSubst .
  873.  
  874.   eq [| k1 |] = [[ kty(k1) tenv(nul) subst(empty) freshTV(tyVar(0)) ]] .
  875. ---  eq [[kty(t) tenv(Gamma) subst(sigma) freshTV(beta) ]] = done .
  876.   eq [[kty(t) tenv(Gamma) subst(sigma) freshTV(beta) ]] = appSubst(sigma, t) .
  877.  
  878. endfm
  879.  
  880. fmod K-POLYFUN-NOFUN-REDUCTIONS is including
  881.  K-POLYFUN-EXPRESSIONS-STATIC-STRICTNESS +
  882. K-POLYFUN-NAME-STATIC-REDUCTIONS + K-POLYFUN-CONSTANTS-STATIC-REDUCTIONS +
  883. K-POLYFUN-ARITH-INT-REL-LOGIC-STATIC-REDUCTIONS + K-POLYFUN-TOP-REDUCTIONS .
  884. endfm
  885.  
  886. fmod K-POLYFUN is
  887.   including K-POLYFUN-NOFUN-REDUCTIONS .
  888.  
  889. --- some variables
  890.  
  891. var I : Identifier .
  892. vars e e' : KProper .
  893. var rest : K .
  894. var beta : Tyvar .
  895. vars Gamma Gamma' : TEnv .
  896. vars tau tau' : BType .
  897. vars sigma sigma' : TypeSubst .
  898.  
  899. --- PROBLEM 1
  900.  
  901. op restorety : TEnv -> K .
  902.  
  903. eq kty((fun I => e) -> rest) tenv(Gamma) freshTV(beta) =
  904.    kty(((beta --> e) -> restorety(Gamma)) -> rest) tenv(Gamma[I <- beta])
  905.       freshTV(incTyVar(beta, 1)) .
  906. eq kty((tau -> restorety(Gamma)) -> rest) tenv(Gamma') subst(sigma) =
  907.    kty(tau -> rest) tenv(appSubstTEnv(sigma, Gamma)) subst(sigma) .
  908.  
  909. --- PROBLEM 2
  910.  
  911. ceq kty((tau (| tau' |) ) -> rest) tenv(Gamma) subst(sigma) freshTV(beta) =
  912.     kty(appSubst(sigma',beta) -> rest) tenv(appSubstTEnv(sigma', Gamma))
  913.        subst(compSubst(sigma', sigma)) freshTV(incTyVar(beta, 1))
  914.     if sigma' := (mgu((appSubst(sigma,tau)) <->
  915.                       (appSubst(sigma, tau') --> beta))) .
  916.  
  917. --- PROBLEM 3
  918.  
  919. eq kty(let I = tau in e end -> rest) tenv(Gamma) subst(sigma) =
  920.    kty((e -> restorety(Gamma)) -> rest)
  921.       tenv(Gamma[I <- generalize(Gamma, appSubst(sigma, tau))]) subst(sigma) .
  922.  
  923. --- PROBLEM 4
  924.  
  925. op hasType : K -> K .
  926.  
  927. eq kty(letrec I = e in e' end -> rest) tenv(Gamma) freshTV(beta) =
  928.    kty(e -> hasType(I) -> e' -> restorety(Gamma) -> rest) tenv(Gamma[I <- beta])
  929.       freshTV(incTyVar(beta, 1)) .
  930.  
  931. ceq kty(tau -> hasType(I) -> rest) tenv(Gamma) subst(sigma) =
  932.     kty(rest)
  933.        tenv(appSubstTEnv(sigma',
  934.                          Gamma[I <- generalize(Gamma,
  935.                                                appSubst(sigma', tau))]))
  936.        subst(sigma')
  937.     if sigma' := compSubst(sigma,
  938.        mgu(appSubst(sigma, tau) <-> tyConst('int, nil)) .
  939. ---       mgu(appSubst(sigma, tau) <-> appSubst(sigma, Gamma[I]))) .
  940.  
  941. endfm
RAW Paste Data
Challenge yourself this year...
Learn something new in 2017
Top