Forlan Manual

The `Prog` Module

Synopsis

signature PROG structure Prog :> PROG

The module defines the abstract type of programs.

Interface

datatype const = True | False | Nil datatype oper = IsNil | IsInt | IsNeg | IsZero | IsPos | IsSym | IsStr | IsPair | IsLam | Plus | Minus | Compare | Fst | Snd | ConsSym | DeconsSym | SymListToStr | StrToSymList datatype concr = Var of Var.var | Const of const | Int of IntInf.int | Sym of Sym.sym | Str of Str.str | Pair of concr * concr | Calc of oper * concr | Cond of concr * concr * concr | App of concr * concr | Lam of Var.var * concr | LetSimp of Var.var * concr * concr | LetRec of Var.var * Var.var * concr * concr type prog val fromConcr : concr -> prog val toConcr : prog -> concr val var : Var.var -> prog val const : const -> prog val int : IntInf.int -> prog val sym : Sym.sym -> prog val str : Str.str -> prog val pair : prog * prog -> prog val calc : oper * prog -> prog val cond : prog * prog * prog -> prog val app : prog * prog -> prog val lam : Var.var * prog -> prog val letSimp : Var.var * prog * prog -> prog val letRec : Var.var * Var.var * prog * prog -> prog val fromString : string -> prog val input : string -> prog val toPP : prog -> PP.pp val toString : prog -> string val output : string * prog -> unit val compare : prog Sort.total_ordering val equal : prog * prog -> bool val toStr : prog -> Str.str val fromStr : Str.str -> prog val validPath : prog * int list -> bool val height : prog -> int val size : prog -> int val numLeaves : prog -> int val select : prog * int list -> prog val update : prog * int list * prog -> prog val maximumLengthPath : prog -> int list val validLeafPath : prog * int list -> bool val free : prog -> Var.var Set.set type cp val toClosed : prog -> cp val fromClosed : cp -> prog val subst : cp * Var.var * prog -> prog val isValue : cp -> bool datatype step = Value | Error | Next of cp val step : cp -> step datatype run = Ans of cp | Fail of cp | Intermed of cp val run : cp * int -> run val evaluate : prog * int -> unit datatype accept = Accept | RejectWithFalse | RejectOtherwise | Unknown of cp val accept : cp -> Str.str * int -> accept val accepted : prog -> Str.str * int -> unit val toRep : prog -> prog val fromRep : prog -> prog val isRep : prog -> bool val jforlanNew : unit -> prog val jforlanEdit : prog -> prog val jforlanValidate : string -> unit val jforlanPretty : string -> unit

Description

datatype const = True | False | Nil

The datatype of program constants.

The datatype of program operators.

The concrete datatype of programs:

For all program variables v, Var v is the one-node tree labeled by var(v).
For all program constants con, Const con is the one-node tree labeled by const(con).
For all integers n, Int n is the one-node tree labeled by int(n).
For all symbols a, Sym a is the one-node tree labeled by sym(a).
For all strings x, Str x is the one-node tree labeled by str(x).
For all programs pr1 and pr2, Pair(pr1, pr2) is the tree whose root node is labeled by pair, with two children, a left child pr1, and a right child pr2.
For all program operators oper and programs pr, Calc(oper, pr) is the tree whose root node is labeled by calc(oper), with one child pr.
For all programs pr1, pr2 and pr3, Cond(pr1, pr2, pr3) is the tree whose root node is labeled by cond, with three children, a left child pr1, a middle child pr2, and a right child pr3.
For all programs pr1 and pr2, App(pr1, pr2) is the tree whose root node is labeled by app, with two children, a left child pr1, and a right child pr2.
For all program variables v and programs pr, Lam(v, pr) is the tree whose root node is labeled lam(v), with one child pr.
For all program variables v and programs pr1 and pr2, LetSimp(v, pr1, pr2) is the tree whose root node is labeled letSimp(v), with two children, a left child pr1, and a right child pr2.
For all program variables v1 and v2, and programs pr1 and pr2, LetRec(v1, v2, pr1, pr2) is the tree whose root node is labeled letRec(v1, v2), with two children, a left child pr1, and a right child pr2.

type prog

The abstract type of programs, consisting of the values of type concr.

fromConcr concr

returns concr.

toConcr pr

returns pr.

var v

returns Var v.

const con

returns Const con.

int n

returns Int n.

sym a

returns Sym a.

str x

returns Str x.

pair(pr1, pr2)

returns Pair(pr1, pr2).

calc(oper, pr)

returns Calc(oper, pr).

cond(pr1, pr2, pr3)

returns Cond(pr1, pr2, pr2).

App(pr1, pr2)

returns app(pr1, pr2).

lam(v, pr)

returns Lam(v, pr).

letSimp(v, pr1, pr2)

returns LetSimp(v, pr1, pr2).

letRec(v1, v2, pr1, pr2)

returns LetRec(v1, v2, pr1, pr2).

fromString s

inputs a program from s.

input fil

inputs a program from the file named fil.

toPP pr

returns a pretty-printing expression for pr.

toString pr

pretty-prints pr to a string.

output(fil, pr)

pretty-prints pr to the file named by fil.

compare(pr1, pr2)

is defined by:

  local
    fun constKind Nil   = 1
      | constKind True  = 2
      | constKind False = 3

    fun compareConst(con, con') = Int.compare(constKind con, constKind con')

    fun operKind IsNil        = 1
      | operKind IsInt        = 2
      | operKind IsNeg        = 3
      | operKind IsZero       = 4
      | operKind IsPos        = 5
      | operKind IsSym        = 6
      | operKind IsStr        = 7
      | operKind IsPair       = 8
      | operKind IsLam        = 9
      | operKind Plus         = 10
      | operKind Minus        = 11
      | operKind Compare      = 12
      | operKind Fst          = 13
      | operKind Snd          = 14
      | operKind ConsSym      = 15
      | operKind DeconsSym    = 16
      | operKind SymListToStr = 17
      | operKind StrToSymList = 18

    fun compareOperat(oper, oper') = Int.compare(operKind oper, operKind oper')

    fun kind(Var _)     = 1
      | kind(Const _)   = 2
      | kind(Int _)     = 3
      | kind(Sym _)     = 4
      | kind(Str _)     = 5
      | kind(Pair _)    = 6
      | kind(Calc _)    = 7
      | kind(Cond _)    = 9
      | kind(App _)     = 8
      | kind(Lam _)     = 10
      | kind(LetSimp _) = 11
      | kind(LetRec _)  = 12
  in
    fun compare(pr, pr') =
          case Int.compare(kind pr, kind pr') of
               LESS    => LESS
             | EQUAL   =>
                 (case (pr, pr') of
                       (Var v,                    Var v')                       =>
                         Var.compare(v, v')
                     | (Const con,                Const con')                   =>
                         compareConst(con, con')
                     | (Int n,                    Int n')                       =>
                         IntInf.compare(n, n')
                     | (Sym a,                    Sym a')                       =>
                         Sym.compare(a, a')
                     | (Str x,                    Str x')                       =>
                         Str.compare(x, x')
                     | (Pair(pr1, pr2),           Pair(pr1', pr2'))             =>
                         (case compare(pr1, pr1') of
                               LESS    => LESS
                             | EQUAL   => compare(pr2, pr2')
                             | GREATER => GREATER)
                     | (Calc(oper, pr),           Calc(oper', pr'))             =>
                         (case compareOperat(oper, oper') of
                               LESS    => LESS
                             | EQUAL   => compare(pr, pr')
                             | GREATER => GREATER)
                     | (Cond(pr1, pr2, pr3),      Cond(pr1', pr2', pr3'))       =>
                         (case compare(pr1, pr1') of
                               LESS    => LESS
                             | EQUAL   =>
                                 (case compare(pr2, pr2') of
                                       LESS    => LESS
                                     | EQUAL   => compare(pr3, pr3')
                                     | GREATER => GREATER)
                             | GREATER => GREATER)
                     | (App(pr1, pr2),            App(pr1', pr2'))              =>
                         (case compare(pr1, pr1') of
                               LESS    => LESS
                             | EQUAL   => compare(pr2, pr2')
                             | GREATER => GREATER)
                     | (Lam(v, pr),               Lam(v', pr'))                 =>
                         (case Var.compare(v, v') of
                               LESS    => LESS
                             | EQUAL   => compare(pr, pr')
                             | GREATER => GREATER)
                     | (LetSimp(v, pr1, pr2),     LetSimp(v', pr1', pr2'))      =>
                         (case Var.compare(v, v') of
                               LESS    => LESS
                             | EQUAL   =>
                                 (case compare(pr1, pr1') of
                                       LESS    => LESS
                                     | EQUAL   => compare(pr2, pr2')
                                     | GREATER => GREATER)
                             | GREATER => GREATER)
                     | (LetRec(v1, v2, pr1, pr2), LetRec(v1', v2', pr1', pr2')) =>
                         (case Var.compare(v1, v1') of
                               LESS    => LESS
                             | EQUAL   =>
                                 (case Var.compare(v2, v2') of
                                       LESS    => LESS
                                     | EQUAL   =>
                                         (case compare(pr1, pr1') of
                                               LESS    => LESS
                                             | EQUAL   => compare(pr2, pr2')
                                             | GREATER => GREATER)
                                     | GREATER => GREATER)
                             | GREATER => GREATER)
                     | _                                                        =>
                         M.cannotHappen())
             | GREATER => GREATER
  end

equal(pr1, pr2)

tests whether pr1 and pr2 are equal.

toStr pr

returns the encoding of pr as a Forlan string, over the alphabet consisting of the symbols <comma>, <perc>, <tilde>, <openPar>, <closPar>, <less> and <great>.

fromStr x

returns the unique program that x encodes. Issues an error message if x isn't the code of a program.

validPath(pr, ns)

tests whether ns is a valid path for pr.

height pr

returns the height of pr.

size pr

returns the size of pr.

numLeaves pr

returns the number of leaves of pr.

select(pr, ns)

returns the subtree of pr pointed to by ns. Issues an error message if ns isn't a valid path for pr.

update(pr, ns, pr')

replaces the subtree of pr pointed to by ns with pr'. Issues an error message if ns isn't valid for pr.

maximumLengthPath pr

returns a leftmost, maximum length path for pr.

validLeafPath(pr, ns)

tests whether ns is a valid path for pr that points to a leaf of pr, i.e., to a subtree with no children.

free pr

returns the set of free program variables of pr.

type cp

The abstract type of closed programs.

toClosed pr

returns pr. Issues an error message if pr is not closed.

fromClosed pr

returns pr.

subst(pr, v, pr')

substitutes pr for all the free occurrences of v in pr'.

isValue pr

tests whether pr is a value.

datatype step = Value | Error | Next of cp

Datatype used by the function step.

step pr

The next step function, for trying to run a closed program pr one step. (See the textbook for its specification.) If the result is Value, this means that pr is a value. If the result is Error, this means that pr is an error. And, if the result is

Next
pr'

, this means that running pr one step resulted in pr'.

datatype run = Ans of cp | Fail of cp | Intermed of cp

Datatype used by the function run.

run(pr, n)

Tries to run pr n steps. A result of Ans pr' means that pr terminated with a value pr'. A result of Fail pr' means that pr terminated with an error pr'. And a result of Intermed pr' means that an intermediate result pr' was produced. Issues an error message if n is negative.

evaluate(pr, n)

explains the significance of the value of type run produced by evaluating run(pr, n). Issues an error message if pr is not closed, or if n is negative.

datatype accept = Accept | RejectWithFalse | RejectOtherwise | Unknown of cp

Datatype used by the accept function.

accept pr (x, n)

gives a partial answer to the question of whether pr accepts x, based on running App(pr, Str x) for n steps (or less, if fewer steps suffice to give a definitive answer). A result of Accept means that pr accepted x by terminating with Const True. A result of RejectWithFalse means that pr rejected x by yielding

Const
False

. A result of RejectOtherwise means that pr rejected x by terminating with a value other than Const True or Const False, or with an error. And a result of Unknown cp means that n steps of evaluation produced an intermediate program pr' that is neither a value nor an error.

accepted pr

issues an error message if pr isn't closed. Otherwise, returns a function f that behaves as follows, when called with argument (x, n). If n is negative, then an error message is issued. Otherwise, it explains the significance of the value of type accept produced by evaluating accept pr (x, n).

toRep pr

returns the program representation representing pr.

toRep pr

If pr is a program representation, then toRep returns the program represented by pr; otherwise, it issues an error message.

isRep pr

tests whether pr is a program representation.

jforlanNew()

invokes JForlan, and returns the program that the user creates and commits. Issues an error message if the user aborts, instead.

jforlanEdit prog

invokes JForlan, letting the user edit prog, and returning the resulting program that the user commits. Issues an error message if the user aborts, instead.

jforlanValidate

is a low-level function used by JForlan. See the code for more information.

jforlanPretty