mutated_ocaml / testsuite / tests / typing-gadts / term-conv.ml.reference

#                                                       module Typeable :
  sig
    type 'a ty =
        Int : int ty
      | String : string ty
      | List : 'a ty -> 'a list ty
      | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
      | Fun : ('a ty * 'b ty) -> ('a -> 'b) ty
    type (_, _) eq = Eq : ('a, 'a) eq
    exception CastFailure
    val check_eq : 't ty -> 't' ty -> ('t, 't') eq
    val gcast : 't ty -> 't' ty -> 't -> 't'
  end
#                               module HOAS :
  sig
    type _ term =
        Tag : 't Typeable.ty * int -> 't term
      | Con : 't -> 't term
      | Lam : 's Typeable.ty * ('s term -> 't term) -> ('s -> 't) term
      | App : ('s -> 't) term * 's term -> 't term
    val intp : 't term -> 't
  end
#                                                               module DeBruijn :
  sig
    type ('env, 't) ix =
        ZeroIx : ('env * 't, 't) ix
      | SuccIx : ('env, 't) ix -> ('env * 's, 't) ix
    val to_int : ('env, 't) ix -> int
    type ('env, 't) term =
        Var : ('env, 't) ix -> ('env, 't) term
      | Con : 't -> ('env, 't) term
      | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term
      | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term
    type _ stack =
        Empty : unit stack
      | Push : 'env stack * 't -> ('env * 't) stack
    val prj : ('env, 't) ix -> 'env stack -> 't
    val intp : ('env, 't) term -> 'env stack -> 't
  end
#                                                                             module Convert :
  sig
    type (_, _) layout =
        EmptyLayout : ('env, unit) layout
      | PushLayout : 't Typeable.ty * ('env, 'env') layout *
          ('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout
    val size : ('env, 'env') layout -> int
    val inc : ('env, 'env') layout -> ('env * 't, 'env') layout
    val prj :
      't Typeable.ty -> int -> ('env, 'env') layout -> ('env, 't) DeBruijn.ix
    val cvt : ('env, 'env) layout -> 't HOAS.term -> ('env, 't) DeBruijn.term
    val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term
  end
#                                               module Main :
  sig
    val i : 'a Typeable.ty -> ('a -> 'a) HOAS.term
    val zero : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
    val one : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
    val two : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
    val three : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
    val plus :
      'a Typeable.ty ->
      ((('a -> 'a) -> 'a -> 'a) ->
       (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a)
      HOAS.term
    val plus_2_3 : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term
    val i' : (unit, int -> int) DeBruijn.term
    val plus_2_3' : (unit, (int -> int) -> int -> int) DeBruijn.term
    val eval_plus_2_3' : int
  end
# 
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.