~thon/thon

cf08c4705ad8b2eab88c6c9d4a81b828f5cfe869 — Evan Bergeron 4 months ago 99dcfcf
Build map over types and use it to erase names for type equality
3 files changed, 51 insertions(+), 21 deletions(-)

A examples/typnames.thon
M parse/ast.sml
M thon.sml
A examples/typnames.thon => examples/typnames.thon +3 -0
@@ 0,0 1,3 @@
ifz Z of
  Z -> poly t -> (Z)
| S p -> poly s -> (Z)

M parse/ast.sml => parse/ast.sml +33 -18
@@ 45,6 45,7 @@ sig
      | TmUnit

    val expMap : (exp -> exp) -> exp -> exp
    val typMap : (typ -> typ) -> typ -> typ

  structure Print :
  sig


@@ 98,34 99,48 @@ struct
      | Unfold of exp
      | TmUnit

    (* DEVNOTE this only applies f at the leaves *)
    fun expMap f e =
        case e
         of  Zero => f Zero
           | TmUnit => f TmUnit
           | Var (name, n)  => f (Var(name, n))
           | Succ e' => Succ (f e')
           | ProdLeft e' => ProdLeft(f e')
           | ProdRight e' => ProdRight(f e')
           | PlusLeft(t, e') => PlusLeft(t, f e')
           | Succ e' => Succ (expMap f e')
           | ProdLeft e' => ProdLeft(expMap f e')
           | ProdRight e' => ProdRight(expMap f e')
           | PlusLeft(t, e') => PlusLeft(t, expMap f e')
           | PlusRight(t, e') => PlusRight(t, e')
           | Case(c, lname, l, rname, r) =>
             Case(f c, lname, f l, rname, f r)
           | Fn(argName, t, f') => Fn(argName, t, (f f'))
             Case(expMap f c, lname, expMap f l, rname, expMap f r)
           | Fn(argName, t, f') => Fn(argName, t, (expMap f f'))
           | Let(varname, vartype, varval, varscope) =>
             Let(varname, vartype, (f varval), (f varscope))
           | App(f', n) => App((f f'), f n)
           | Ifz(i, t, prev, e) => Ifz(f i, f t, prev, f e)
             Let(varname, vartype, (expMap f varval), (expMap f varscope))
           | App(f', n) => App((expMap f f'), expMap f n)
           | Ifz(i, t, prev, e) => Ifz(expMap f i, expMap f t, prev, expMap f e)
           | Rec(i, baseCase, prevCaseName, recCase) =>
             Rec(f i, f baseCase, prevCaseName, f recCase)
           | Fix(name, t, e') => Fix(name, t, f e')
           | TypFn (name, e') => TypFn (name, f e')
           | TypApp (appType, e') => TypApp(appType, f e')
           | Impl(reprType, pkgImpl, t) => Impl(reprType, f pkgImpl, t)
             Rec(expMap f i, expMap f baseCase, prevCaseName, expMap f recCase)
           | Fix(name, t, e') => Fix(name, t, expMap f e')
           | TypFn (name, e') => TypFn (name, expMap f e')
           | TypApp (appType, e') => TypApp(appType, expMap f e')
           | Impl(reprType, pkgImpl, t) => Impl(reprType, expMap f pkgImpl, t)
           | Use(pkg, clientName, typeName, client) =>
             Use(f pkg, clientName, typeName, f client)
           | Pair(l, r) => Pair(f l, f r)
           | Fold(t, e') => Fold(t, (f e'))
           | Unfold(e') => Unfold(f e')
             Use(expMap f pkg, clientName, typeName, expMap f client)
           | Pair(l, r) => Pair(expMap f l, expMap f r)
           | Fold(t, e') => Fold(t, (expMap f e'))
           | Unfold(e') => Unfold(expMap f e')

    (* DEVNOTE this applies f at every node *)
    fun typMap f t =
        case t of
            Nat => f t
          | Unit => f t
          | TypVar (name, i) => f t
          | Arr(d, c) => f (Arr(typMap f d, typMap f c))
          | Prod(l, r) => f (Prod(typMap f l, typMap f r))
          | Plus(l, r) => f (Plus(typMap f l, typMap f r))
          | All (name, t') => f (All(name, typMap f t'))
          | Some (name, t') => f (Some(name, typMap f t'))
          | TyRec (name, t') => f (TyRec(name, typMap f t'))


  structure Print =

M thon.sml => thon.sml +15 -3
@@ 9,6 9,7 @@ structure Thon : sig
                   val step : A.exp -> A.exp
                   val subst : A.exp -> A.exp -> A.exp
                   val run : string -> A.exp
                   val eraseNamesInTyp : A.typ -> A.typ
                   val runFile : string -> A.exp
                   val findParseErrors : string -> unit
                 end =


@@ 277,8 278,18 @@ end
fun substTypeInExp srcType dstExp = substTypeInExp' srcType dstExp 0


(* BUG this doesn't respect alpha equivalence (shouldn't care about type var names) *)
fun typeEq (t : A.typ) (t' : A.typ) = (t = t')
fun eraseNamesInTyp t =
    let fun erase t =
            (case t of
                 A.TypVar(_, i) => A.TypVar("", i)
               | A.All(_, t') => A.All("", t')
               | A.Some(_, t') => A.Some("", t')
               | A.TyRec(_, t') => A.TyRec("", t')
               | _ => t
            )
    in A.typMap erase t end

fun typeEq (t : A.typ) (t' : A.typ) = ((eraseNamesInTyp t) = (eraseNamesInTyp t'))

fun typeof' ctx typCtx e =
    case e


@@ 348,7 359,6 @@ fun typeof' ctx typCtx e =
             if not (typeEq t t2) then raise IllTyped else t
         end
       | A.Fix (name, typ, e) => typeof' (typ::ctx) typCtx e
       (* BUG need to build a type equality func that ignores names *)
       | A.TypFn (name, e) => A.All(name, typeof' ctx (NONE::typCtx) e)
       | A.TypApp (appType, e) =>
         if not (istype typCtx appType) then raise IllTyped else


@@ 1080,6 1090,8 @@ val true = (zerobst = appbst);

val Succ (Succ Zero) = runFile "/home/evan/thon/examples/setget.thon";

val TypFn ("t", Zero) = runFile "/home/evan/thon/examples/typnames.thon";

in
()
end