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.

datatype oper
  = IsNil
  | IsInt
  | IsNeg
  | IsZero
  | IsPos
  | IsSym
  | IsStr
  | IsPair
  | IsLam
  | Plus
  | Minus
  | Compare
  | Fst
  | Snd
  | ConsSym
  | DeconsSym
  | SymListToStr
  | StrToSymList
The datatype of program operators.

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
The concrete datatype of programs:

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
is a low-level function used by JForlan. See the code for more information.


[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.12
Copyright © 2019 Alley Stoughton