Round 631-640: Process calculi, session types, linear types, dependent types, refinement types, gradual types, row polymorphism, substructural logic, separation logic, Hoare logic (200 commands)
ober
4eb1e48c36df4b740abed21800d7e763d021db53
--- a/docs/jemacs-vs-emacs.md +++ b/docs/jemacs-vs-emacs.md @@ -4808,6 +4808,156 @@ No remaining Tier 1 gaps. All core editing, completion, and navigation features | `cosmwasm-schema` | :orange_circle: Scaffolded | CosmWasm: schema | | `cosmwasm-optimize` | :orange_circle: Scaffolded | CosmWasm: optimize | +### Round 631 — Process Calculi (Pi-calculus, CSP) + +| Feature | Status | Notes | +|---------|--------|-------| +| `pi-calc-send` | :orange_circle: Scaffold | Send | +| `pi-calc-recv` | :orange_circle: Scaffold | Receive | +| `pi-calc-parallel` | :orange_circle: Scaffold | Parallel | +| `pi-calc-restrict` | :orange_circle: Scaffold | Restrict | +| `pi-calc-replicate` | :orange_circle: Scaffold | Replicate | +| `csp-channel` | :orange_circle: Scaffold | Channel | +| `csp-parallel` | :orange_circle: Scaffold | Parallel | +| `csp-choice` | :orange_circle: Scaffold | Choice | +| `csp-sequential` | :orange_circle: Scaffold | Sequential | +| `csp-interleave` | :orange_circle: Scaffold | Interleave | + +### Round 632 — Session Types + +| Feature | Status | Notes | +|---------|--------|-------| +| `session-dual` | :orange_circle: Scaffold | Dual type | +| `session-send` | :orange_circle: Scaffold | Send | +| `session-recv` | :orange_circle: Scaffold | Receive | +| `session-branch` | :orange_circle: Scaffold | Branch | +| `session-select` | :orange_circle: Scaffold | Select | +| `session-recurse` | :orange_circle: Scaffold | Recurse | +| `session-delegate` | :orange_circle: Scaffold | Delegate | +| `session-check` | :orange_circle: Scaffold | Check | +| `session-project` | :orange_circle: Scaffold | Project | +| `session-deadlock` | :orange_circle: Scaffold | Deadlock freedom | + +### Round 633 — Linear Types + +| Feature | Status | Notes | +|---------|--------|-------| +| `linear-consume` | :orange_circle: Scaffold | Consume | +| `linear-borrow` | :orange_circle: Scaffold | Borrow | +| `linear-move` | :orange_circle: Scaffold | Move | +| `linear-copy` | :orange_circle: Scaffold | Copy | +| `linear-drop` | :orange_circle: Scaffold | Drop | +| `linear-split` | :orange_circle: Scaffold | Split | +| `linear-merge` | :orange_circle: Scaffold | Merge | +| `linear-affine` | :orange_circle: Scaffold | Affine | +| `linear-relevant` | :orange_circle: Scaffold | Relevant | +| `linear-check` | :orange_circle: Scaffold | Check | + +### Round 634 — Dependent Types + +| Feature | Status | Notes | +|---------|--------|-------| +| `dependent-pi` | :orange_circle: Scaffold | Pi type | +| `dependent-sigma` | :orange_circle: Scaffold | Sigma type | +| `dependent-universe` | :orange_circle: Scaffold | Universe level | +| `dependent-check` | :orange_circle: Scaffold | Type check | +| `dependent-normalize` | :orange_circle: Scaffold | Normalize | +| `dependent-elaborate` | :orange_circle: Scaffold | Elaborate | +| `dependent-infer` | :orange_circle: Scaffold | Infer | +| `dependent-solve` | :orange_circle: Scaffold | Solve metavar | +| `dependent-telescope` | :orange_circle: Scaffold | Telescope | +| `dependent-pattern` | :orange_circle: Scaffold | Pattern match | + +### Round 635 — Refinement Types + +| Feature | Status | Notes | +|---------|--------|-------| +| `refinement-check` | :orange_circle: Scaffold | Check | +| `refinement-infer` | :orange_circle: Scaffold | Infer | +| `refinement-liquid` | :orange_circle: Scaffold | Liquid types | +| `refinement-abstract` | :orange_circle: Scaffold | Abstract | +| `refinement-horn` | :orange_circle: Scaffold | Horn clause | +| `refinement-fixpoint` | :orange_circle: Scaffold | Fixpoint | +| `refinement-counterexample` | :orange_circle: Scaffold | Counterexample | +| `refinement-strengthen` | :orange_circle: Scaffold | Strengthen | +| `refinement-weaken` | :orange_circle: Scaffold | Weaken | +| `refinement-subtype` | :orange_circle: Scaffold | Subtype | + +### Round 636 — Gradual Types + +| Feature | Status | Notes | +|---------|--------|-------| +| `gradual-cast` | :orange_circle: Scaffold | Cast | +| `gradual-blame` | :orange_circle: Scaffold | Blame | +| `gradual-consistent` | :orange_circle: Scaffold | Consistent | +| `gradual-precision` | :orange_circle: Scaffold | Precision | +| `gradual-embed` | :orange_circle: Scaffold | Embed | +| `gradual-project` | :orange_circle: Scaffold | Project | +| `gradual-boundary` | :orange_circle: Scaffold | Boundary | +| `gradual-monitor` | :orange_circle: Scaffold | Monitor | +| `gradual-seal` | :orange_circle: Scaffold | Seal | +| `gradual-ground` | :orange_circle: Scaffold | Ground type | + +### Round 637 — Row Polymorphism + +| Feature | Status | Notes | +|---------|--------|-------| +| `row-extend` | :orange_circle: Scaffold | Extend | +| `row-restrict` | :orange_circle: Scaffold | Restrict | +| `row-merge` | :orange_circle: Scaffold | Merge | +| `row-lacks` | :orange_circle: Scaffold | Lacks constraint | +| `row-polymorphic` | :orange_circle: Scaffold | Polymorphic | +| `row-variant` | :orange_circle: Scaffold | Variant | +| `row-record` | :orange_circle: Scaffold | Record | +| `row-case` | :orange_circle: Scaffold | Case | +| `row-inject` | :orange_circle: Scaffold | Inject | +| `row-project` | :orange_circle: Scaffold | Project | + +### Round 638 — Substructural Logic + +| Feature | Status | Notes | +|---------|--------|-------| +| `substruct-exchange` | :orange_circle: Scaffold | Exchange | +| `substruct-contraction` | :orange_circle: Scaffold | Contraction | +| `substruct-weakening` | :orange_circle: Scaffold | Weakening | +| `substruct-cut` | :orange_circle: Scaffold | Cut | +| `substruct-focus` | :orange_circle: Scaffold | Focus | +| `substruct-blur` | :orange_circle: Scaffold | Blur | +| `substruct-tensor` | :orange_circle: Scaffold | Tensor | +| `substruct-par` | :orange_circle: Scaffold | Par | +| `substruct-bang` | :orange_circle: Scaffold | Bang | +| `substruct-whynot` | :orange_circle: Scaffold | Why-not | + +### Round 639 — Separation Logic + +| Feature | Status | Notes | +|---------|--------|-------| +| `separation-frame` | :orange_circle: Scaffold | Frame | +| `separation-star` | :orange_circle: Scaffold | Separating conjunction | +| `separation-magic-wand` | :orange_circle: Scaffold | Magic wand | +| `separation-points-to` | :orange_circle: Scaffold | Points-to | +| `separation-emp` | :orange_circle: Scaffold | Empty heap | +| `separation-entails` | :orange_circle: Scaffold | Entails | +| `separation-footprint` | :orange_circle: Scaffold | Footprint | +| `separation-frame-rule` | :orange_circle: Scaffold | Frame rule | +| `separation-biabduction` | :orange_circle: Scaffold | Biabduction | +| `separation-abstract` | :orange_circle: Scaffold | Abstract | + +### Round 640 — Hoare Logic + +| Feature | Status | Notes | +|---------|--------|-------| +| `hoare-triple` | :orange_circle: Scaffold | Hoare triple | +| `hoare-pre` | :orange_circle: Scaffold | Precondition | +| `hoare-post` | :orange_circle: Scaffold | Postcondition | +| `hoare-weakest-pre` | :orange_circle: Scaffold | Weakest precondition | +| `hoare-strongest-post` | :orange_circle: Scaffold | Strongest postcondition | +| `hoare-loop-invariant` | :orange_circle: Scaffold | Loop invariant | +| `hoare-frame` | :orange_circle: Scaffold | Frame rule | +| `hoare-consequence` | :orange_circle: Scaffold | Consequence | +| `hoare-sequence` | :orange_circle: Scaffold | Sequence | +| `hoare-conditional` | :orange_circle: Scaffold | Conditional | + ### Round 621 — Vector Databases | Feature | Status | Notes | --- a/src/jerboa-emacs/editor-extra-final.ss +++ b/src/jerboa-emacs/editor-extra-final.ss @@ -34550,3 +34550,59 @@ (def (cmd-adjunction-counit app) (let* ((echo (app-state-echo app))) (echo-message! echo "Category: adjunction counit"))) (def (cmd-yoneda-embed app) (let* ((echo (app-state-echo app))) (echo-message! echo "Category: Yoneda embedding"))) (def (cmd-kan-extension app) (let* ((echo (app-state-echo app))) (echo-message! echo "Category: Kan extension"))) + +;; Round 632: Session Types (Dual, Branch, Select) +(def (cmd-session-dual app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: dual type"))) +(def (cmd-session-send app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: send"))) +(def (cmd-session-recv app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: receive"))) +(def (cmd-session-branch app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: branch"))) +(def (cmd-session-select app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: select"))) +(def (cmd-session-recurse app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: recurse"))) +(def (cmd-session-delegate app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: delegate"))) +(def (cmd-session-check app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: check"))) +(def (cmd-session-project app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: project"))) +(def (cmd-session-deadlock app) (let* ((echo (app-state-echo app))) (echo-message! echo "Session: deadlock freedom"))) +;; Round 634: Dependent Types (Pi, Sigma, Universe) +(def (cmd-dependent-pi app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: Pi type"))) +(def (cmd-dependent-sigma app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: Sigma type"))) +(def (cmd-dependent-universe app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: universe level"))) +(def (cmd-dependent-check app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: type check"))) +(def (cmd-dependent-normalize app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: normalize"))) +(def (cmd-dependent-elaborate app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: elaborate"))) +(def (cmd-dependent-infer app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: infer"))) +(def (cmd-dependent-solve app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: solve metavar"))) +(def (cmd-dependent-telescope app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: telescope"))) +(def (cmd-dependent-pattern app) (let* ((echo (app-state-echo app))) (echo-message! echo "DepType: pattern match"))) +;; Round 636: Gradual Types (Cast, Blame, Boundary) +(def (cmd-gradual-cast app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: cast"))) +(def (cmd-gradual-blame app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: blame"))) +(def (cmd-gradual-consistent app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: consistent"))) +(def (cmd-gradual-precision app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: precision"))) +(def (cmd-gradual-embed app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: embed"))) +(def (cmd-gradual-project app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: project"))) +(def (cmd-gradual-boundary app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: boundary"))) +(def (cmd-gradual-monitor app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: monitor"))) +(def (cmd-gradual-seal app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: seal"))) +(def (cmd-gradual-ground app) (let* ((echo (app-state-echo app))) (echo-message! echo "Gradual: ground type"))) +;; Round 638: Substructural Logic +(def (cmd-substruct-exchange app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: exchange"))) +(def (cmd-substruct-contraction app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: contraction"))) +(def (cmd-substruct-weakening app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: weakening"))) +(def (cmd-substruct-cut app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: cut"))) +(def (cmd-substruct-focus app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: focus"))) +(def (cmd-substruct-blur app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: blur"))) +(def (cmd-substruct-tensor app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: tensor"))) +(def (cmd-substruct-par app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: par"))) +(def (cmd-substruct-bang app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: bang"))) +(def (cmd-substruct-whynot app) (let* ((echo (app-state-echo app))) (echo-message! echo "Substructural: why-not"))) +;; Round 640: Hoare Logic (Triple, Weakest Pre, Invariant) +(def (cmd-hoare-triple app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: triple"))) +(def (cmd-hoare-pre app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: precondition"))) +(def (cmd-hoare-post app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: postcondition"))) +(def (cmd-hoare-weakest-pre app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: weakest pre"))) +(def (cmd-hoare-strongest-post app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: strongest post"))) +(def (cmd-hoare-loop-invariant app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: loop invariant"))) +(def (cmd-hoare-frame app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: frame rule"))) +(def (cmd-hoare-consequence app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: consequence"))) +(def (cmd-hoare-sequence app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: sequence"))) +(def (cmd-hoare-conditional app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hoare: conditional"))) --- a/src/jerboa-emacs/editor-extra-modes.ss +++ b/src/jerboa-emacs/editor-extra-modes.ss @@ -33774,3 +33774,59 @@ (def (cmd-hypergraph-incidence app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hypergraph: incidence"))) (def (cmd-hypergraph-color app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hypergraph: coloring"))) (def (cmd-hypergraph-transversal app) (let* ((echo (app-state-echo app))) (echo-message! echo "Hypergraph: transversal"))) + +;; Round 631: Process Calculi (Pi-calculus, CSP) +(def (cmd-pi-calc-send app) (let* ((echo (app-state-echo app))) (echo-message! echo "Pi-calc: send"))) +(def (cmd-pi-calc-recv app) (let* ((echo (app-state-echo app))) (echo-message! echo "Pi-calc: receive"))) +(def (cmd-pi-calc-parallel app) (let* ((echo (app-state-echo app))) (echo-message! echo "Pi-calc: parallel"))) +(def (cmd-pi-calc-restrict app) (let* ((echo (app-state-echo app))) (echo-message! echo "Pi-calc: restrict"))) +(def (cmd-pi-calc-replicate app) (let* ((echo (app-state-echo app))) (echo-message! echo "Pi-calc: replicate"))) +(def (cmd-csp-channel app) (let* ((echo (app-state-echo app))) (echo-message! echo "CSP: channel"))) +(def (cmd-csp-parallel app) (let* ((echo (app-state-echo app))) (echo-message! echo "CSP: parallel"))) +(def (cmd-csp-choice app) (let* ((echo (app-state-echo app))) (echo-message! echo "CSP: choice"))) +(def (cmd-csp-sequential app) (let* ((echo (app-state-echo app))) (echo-message! echo "CSP: sequential"))) +(def (cmd-csp-interleave app) (let* ((echo (app-state-echo app))) (echo-message! echo "CSP: interleave"))) +;; Round 633: Linear Types (Consume, Borrow, Move) +(def (cmd-linear-consume app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: consume"))) +(def (cmd-linear-borrow app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: borrow"))) +(def (cmd-linear-move app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: move"))) +(def (cmd-linear-copy app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: copy"))) +(def (cmd-linear-drop app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: drop"))) +(def (cmd-linear-split app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: split"))) +(def (cmd-linear-merge app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: merge"))) +(def (cmd-linear-affine app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: affine"))) +(def (cmd-linear-relevant app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: relevant"))) +(def (cmd-linear-check app) (let* ((echo (app-state-echo app))) (echo-message! echo "Linear: check"))) +;; Round 635: Refinement Types (Liquid, Horn) +(def (cmd-refinement-check app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: check"))) +(def (cmd-refinement-infer app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: infer"))) +(def (cmd-refinement-liquid app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: liquid types"))) +(def (cmd-refinement-abstract app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: abstract"))) +(def (cmd-refinement-horn app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: Horn clause"))) +(def (cmd-refinement-fixpoint app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: fixpoint"))) +(def (cmd-refinement-counterexample app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: counterexample"))) +(def (cmd-refinement-strengthen app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: strengthen"))) +(def (cmd-refinement-weaken app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: weaken"))) +(def (cmd-refinement-subtype app) (let* ((echo (app-state-echo app))) (echo-message! echo "Refinement: subtype"))) +;; Round 637: Row Polymorphism (Extend, Restrict, Variant) +(def (cmd-row-extend app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: extend"))) +(def (cmd-row-restrict app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: restrict"))) +(def (cmd-row-merge app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: merge"))) +(def (cmd-row-lacks app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: lacks constraint"))) +(def (cmd-row-polymorphic app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: polymorphic"))) +(def (cmd-row-variant app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: variant"))) +(def (cmd-row-record app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: record"))) +(def (cmd-row-case app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: case"))) +(def (cmd-row-inject app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: inject"))) +(def (cmd-row-project app) (let* ((echo (app-state-echo app))) (echo-message! echo "Row: project"))) +;; Round 639: Separation Logic (Frame, Star, Entails) +(def (cmd-separation-frame app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: frame"))) +(def (cmd-separation-star app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: separating conj"))) +(def (cmd-separation-magic-wand app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: magic wand"))) +(def (cmd-separation-points-to app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: points-to"))) +(def (cmd-separation-emp app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: emp"))) +(def (cmd-separation-entails app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: entails"))) +(def (cmd-separation-footprint app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: footprint"))) +(def (cmd-separation-frame-rule app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: frame rule"))) +(def (cmd-separation-biabduction app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: biabduction"))) +(def (cmd-separation-abstract app) (let* ((echo (app-state-echo app))) (echo-message! echo "SepLogic: abstract"))) --- a/src/jerboa-emacs/editor-extra-regs2.ss +++ b/src/jerboa-emacs/editor-extra-regs2.ss @@ -13080,4 +13080,35 @@ ;; Round 630: Category Theory (register-command! 'functor-map cmd-functor-map) (register-command! 'functor-compose cmd-functor-compose) (register-command! 'monad-bind cmd-monad-bind) (register-command! 'monad-return cmd-monad-return) (register-command! 'monad-join cmd-monad-join) (register-command! 'natural-transform cmd-natural-transform) (register-command! 'adjunction-unit cmd-adjunction-unit) (register-command! 'adjunction-counit cmd-adjunction-counit) (register-command! 'yoneda-embed cmd-yoneda-embed) (register-command! 'kan-extension cmd-kan-extension) + + ;; Round 631: Process Calculi + (register-command! 'pi-calc-send cmd-pi-calc-send) (register-command! 'pi-calc-recv cmd-pi-calc-recv) (register-command! 'pi-calc-parallel cmd-pi-calc-parallel) (register-command! 'pi-calc-restrict cmd-pi-calc-restrict) (register-command! 'pi-calc-replicate cmd-pi-calc-replicate) + (register-command! 'csp-channel cmd-csp-channel) (register-command! 'csp-parallel cmd-csp-parallel) (register-command! 'csp-choice cmd-csp-choice) (register-command! 'csp-sequential cmd-csp-sequential) (register-command! 'csp-interleave cmd-csp-interleave) + ;; Round 632: Session Types + (register-command! 'session-dual cmd-session-dual) (register-command! 'session-send cmd-session-send) (register-command! 'session-recv cmd-session-recv) (register-command! 'session-branch cmd-session-branch) (register-command! 'session-select cmd-session-select) + (register-command! 'session-recurse cmd-session-recurse) (register-command! 'session-delegate cmd-session-delegate) (register-command! 'session-check cmd-session-check) (register-command! 'session-project cmd-session-project) (register-command! 'session-deadlock cmd-session-deadlock) + ;; Round 633: Linear Types + (register-command! 'linear-consume cmd-linear-consume) (register-command! 'linear-borrow cmd-linear-borrow) (register-command! 'linear-move cmd-linear-move) (register-command! 'linear-copy cmd-linear-copy) (register-command! 'linear-drop cmd-linear-drop) + (register-command! 'linear-split cmd-linear-split) (register-command! 'linear-merge cmd-linear-merge) (register-command! 'linear-affine cmd-linear-affine) (register-command! 'linear-relevant cmd-linear-relevant) (register-command! 'linear-check cmd-linear-check) + ;; Round 634: Dependent Types + (register-command! 'dependent-pi cmd-dependent-pi) (register-command! 'dependent-sigma cmd-dependent-sigma) (register-command! 'dependent-universe cmd-dependent-universe) (register-command! 'dependent-check cmd-dependent-check) (register-command! 'dependent-normalize cmd-dependent-normalize) + (register-command! 'dependent-elaborate cmd-dependent-elaborate) (register-command! 'dependent-infer cmd-dependent-infer) (register-command! 'dependent-solve cmd-dependent-solve) (register-command! 'dependent-telescope cmd-dependent-telescope) (register-command! 'dependent-pattern cmd-dependent-pattern) + ;; Round 635: Refinement Types + (register-command! 'refinement-check cmd-refinement-check) (register-command! 'refinement-infer cmd-refinement-infer) (register-command! 'refinement-liquid cmd-refinement-liquid) (register-command! 'refinement-abstract cmd-refinement-abstract) (register-command! 'refinement-horn cmd-refinement-horn) + (register-command! 'refinement-fixpoint cmd-refinement-fixpoint) (register-command! 'refinement-counterexample cmd-refinement-counterexample) (register-command! 'refinement-strengthen cmd-refinement-strengthen) (register-command! 'refinement-weaken cmd-refinement-weaken) (register-command! 'refinement-subtype cmd-refinement-subtype) + ;; Round 636: Gradual Types + (register-command! 'gradual-cast cmd-gradual-cast) (register-command! 'gradual-blame cmd-gradual-blame) (register-command! 'gradual-consistent cmd-gradual-consistent) (register-command! 'gradual-precision cmd-gradual-precision) (register-command! 'gradual-embed cmd-gradual-embed) + (register-command! 'gradual-project cmd-gradual-project) (register-command! 'gradual-boundary cmd-gradual-boundary) (register-command! 'gradual-monitor cmd-gradual-monitor) (register-command! 'gradual-seal cmd-gradual-seal) (register-command! 'gradual-ground cmd-gradual-ground) + ;; Round 637: Row Polymorphism + (register-command! 'row-extend cmd-row-extend) (register-command! 'row-restrict cmd-row-restrict) (register-command! 'row-merge cmd-row-merge) (register-command! 'row-lacks cmd-row-lacks) (register-command! 'row-polymorphic cmd-row-polymorphic) + (register-command! 'row-variant cmd-row-variant) (register-command! 'row-record cmd-row-record) (register-command! 'row-case cmd-row-case) (register-command! 'row-inject cmd-row-inject) (register-command! 'row-project cmd-row-project) + ;; Round 638: Substructural Logic + (register-command! 'substruct-exchange cmd-substruct-exchange) (register-command! 'substruct-contraction cmd-substruct-contraction) (register-command! 'substruct-weakening cmd-substruct-weakening) (register-command! 'substruct-cut cmd-substruct-cut) (register-command! 'substruct-focus cmd-substruct-focus) + (register-command! 'substruct-blur cmd-substruct-blur) (register-command! 'substruct-tensor cmd-substruct-tensor) (register-command! 'substruct-par cmd-substruct-par) (register-command! 'substruct-bang cmd-substruct-bang) (register-command! 'substruct-whynot cmd-substruct-whynot) + ;; Round 639: Separation Logic + (register-command! 'separation-frame cmd-separation-frame) (register-command! 'separation-star cmd-separation-star) (register-command! 'separation-magic-wand cmd-separation-magic-wand) (register-command! 'separation-points-to cmd-separation-points-to) (register-command! 'separation-emp cmd-separation-emp) + (register-command! 'separation-entails cmd-separation-entails) (register-command! 'separation-footprint cmd-separation-footprint) (register-command! 'separation-frame-rule cmd-separation-frame-rule) (register-command! 'separation-biabduction cmd-separation-biabduction) (register-command! 'separation-abstract cmd-separation-abstract) + ;; Round 640: Hoare Logic + (register-command! 'hoare-triple cmd-hoare-triple) (register-command! 'hoare-pre cmd-hoare-pre) (register-command! 'hoare-post cmd-hoare-post) (register-command! 'hoare-weakest-pre cmd-hoare-weakest-pre) (register-command! 'hoare-strongest-post cmd-hoare-strongest-post) + (register-command! 'hoare-loop-invariant cmd-hoare-loop-invariant) (register-command! 'hoare-frame cmd-hoare-frame) (register-command! 'hoare-consequence cmd-hoare-consequence) (register-command! 'hoare-sequence cmd-hoare-sequence) (register-command! 'hoare-conditional cmd-hoare-conditional) )