API tools faq
paste
Advertisement
Guest User

Untitled

a guest
May 19th, 2017
61
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 29.08 KB | None | 0 0
raw download clone embed print report
  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
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!