Skip to content

Instantly share code, notes, and snippets.

@ClarkeRemy

ClarkeRemy/grokking_the _sequent_calculus.sml

Last active March 25, 2025 15:47
Show Gist options
  • Save ClarkeRemy/89950343b85f19bc198c9de8e8fc0f57 to your computer and use it in GitHub Desktop.
Save ClarkeRemy/89950343b85f19bc198c9de8e8fc0f57 to your computer and use it in GitHub Desktop.
Download ZIP
Grokking the Sequent Calculus
Raw
grokking_the _sequent_calculus.sml
fun y f x = f (y f) x
functor Fix(type 'a f )
= struct
type 'a f = 'a f
datatype fix = FIX of fix f
fun inj v = FIX v
fun prj (FIX v) = v
end
functor Schemes
( structure S
: sig
type 'a f
type fix
val fmap : ('a -> 'b) -> 'a f -> 'b f
val prj : fix -> fix f
val inj : fix f -> fix
end
)
= struct
open S
(*
fun cata alg x = (alg o fmap (cata alg ) o prj ) x
*)
fun ana coalg x = (inj o fmap (ana coalg) o coalg) x
fun hylo alg coalg x = (alg o fmap (hylo alg coalg) o coalg) x
fun apo coalg x = (inj o fmap (Either.proj o Either.map (fn a => a, apo coalg) ) o coalg) x
(*
datatype 'a free = RET of 'a
| OP_ of 'a free f
fun free' coalg = fn RET a => coalg a
| OP_ k => k
*)
datatype 'a cofree = COFREE of 'a * ('a cofree) f
fun extract (COFREE (x, _)) = x
fun cofree' alg x = COFREE (alg x, x)
(* fun cofree_cata alg x = (alg o (fn (a, p) => (a, fmap (cofree_cata alg ) p)) o (fn COFREE c => c)) x *)
(* fun cofree_ana coalg x = (COFREE o (fn (a, p) => (a, fmap (cofree_ana coalg) p)) o coalg ) x *)
fun cofree_hylo alg coalg x = (alg o (fn (a, p) => (a, fmap (cofree_hylo alg coalg) p)) o coalg ) x
end
structure Compiler =
struct
structure Utils
= struct
fun zip (x::xs) (y_::ys) acc error = zip xs ys ((x,y_)::acc) error
| zip [] [] acc _ = acc
| zip _ _ _ error = raise error
end
structure Op = struct
datatype ('args)
binop = +` of 'args
| -` of 'args
| *` of 'args
fun destructor ( +` a) = ( +` , a)
| destructor ( -` a) = ( -` , a)
| destructor ( *` a) = ( *` , a)
fun primop ( +` _) = Word.+
| primop ( -` _) = Word.-
| primop ( *` _) = Word.*
end
type number = Word.word
datatype name = $ of string
datatype var = +$ of string
datatype coVar = -$ of string
fun eq_name ( $ x) ( $ y) = case String.compare (x, y) of EQUAL => true | _ => false
fun eq_var (+$ x) (+$ y) = case String.compare (x, y) of EQUAL => true | _ => false
fun eq_coVar (-$ x) (-$ y) = case String.compare (x, y) of EQUAL => true | _ => false
fun pretty_var (+$v) = "+$" ^ v ^ " "
fun pretty_coVar (-$v) = "-$" ^ v ^ " "
fun pretty_num n = "#" ^ Word.toString n ^ " "
fun pretty_ifz ws nli {if_zero,then_,else_} = "ifz " ^ nli
^ ws ^ if_zero ^ nli
^ "then " ^ nli
^ ws ^ then_ ^ nli
^ "else " ^ nli
^ ws ^ else_ ^ nli
^ "end "
fun pretty_print_def_ pp indent {def= $ d, args=(vs,cvs), body}
= ( "def $" ^ d
^ ( if List.null vs andalso List.null cvs
then "(;)"
else "("
^ ( case vs of [] => ""
| (+$ x :: xs) => List.foldl (fn (+$ v, acc) => acc ^ ", +$" ^ v)
("+$" ^ x)
xs
^ ""
)
^ ";"
^ ( case cvs of [] => ""
| (-$ x :: xs) => " "
^ List.foldl (fn (-$ v, acc) => acc ^ ", -$" ^ v)
("-$" ^ x)
xs
)
^ ") :=\n"
^ (if Option.isNone indent then " " else "") ^ pp indent body
)
^ "\n\n"
)
structure Fun
= struct
datatype 'term definition = DEF of { def : name
, args : var list * coVar list
, body : 'term
}
type 'term programs = 'term definition list
type 'term k_or_d = { tag : name, fields : 'term list }
type 'term case_cocase = { tag : name, fields : var list, body : 'term } list
datatype 'term lambda = \ of var * 'term
datatype 'term term = VAR of var
| NUM of number
| OP of ('term * 'term) Op.binop
| IFZ of { if_zero : 'term
, then_: 'term
, else_: 'term
}
| LET of { let_ : (var * 'term), in_ : 'term }
| CALL of { name : name
, args : 'term list * coVar list
}
| K of 'term k_or_d
| CASE_OF of 'term * 'term case_cocase
| DO_D of 'term * 'term k_or_d
| COCASE of 'term case_cocase
| LAMBDA of 'term lambda
| AP of 'term * 'term
| LABEL of { label : coVar, in_ : 'term }
| GOTO of { bind : 'term, label : coVar}
fun fmap_ m f
= case f (* base cases *)
of VAR v => VAR v
| NUM n => NUM n
(* recursive cases *)
| OP oper => let fun m_ (oper_, (left, right)) = (OP o oper_) (m left, m right) in m_ (Op.destructor oper) end
| IFZ {if_zero,then_,else_} => IFZ {if_zero= m if_zero, then_= m then_, else_= m else_}
| LET {let_ = (v, bound), in_ = body} => LET {let_= (v, m bound), in_ = m body}
| CALL {name,args=(ts,cvs)} => CALL {name=name,args=(List.map m ts,cvs)}
| K {tag,fields} => K {tag=tag,fields= List.map m fields}
| CASE_OF(val_,cases) => CASE_OF ( m val_
, ( List.map ( fn case_ => { tag = #tag case_
, fields = #fields case_
, body = (m o #body) case_}
)
) cases
)
| DO_D (t, {tag,fields}) => DO_D (m t, {tag=tag, fields=List.map m fields})
| COCASE cocases => ( COCASE
o List.map ( fn cocase => { tag = #tag cocase
, fields = #fields cocase
, body = (m o #body) cocase
}
)
) cocases
| LAMBDA (\(x,t)) => (LAMBDA o \) (x,m t)
| AP (func, term) => AP (m func, m term)
| LABEL {label,in_} => LABEL {label=label, in_=m in_}
| GOTO {bind,label} => GOTO {bind=m bind, label=label}
local structure F = Fix(type 'term f = 'term term)
in open F end
local structure Scheme = Schemes(
structure S
= struct
type 'a f = 'a term
type fix = fix
val fmap = fmap_
val prj = prj
val inj = inj
end
)
in open Scheme
end
fun is_term_value (FIX t : fix) = case t
of VAR _ => true (* when bound, it will be a value, not an unevaluated expression *)
| NUM _ => true
| K k => List.foldl (fn (t_, acc) => acc andalso is_term_value t_) true (#fields k)
| COCASE _ => true
| LAMBDA _ => true
| _ => false
fun pretty_print indentation f : string
= let fun indent_ f acc n = if n = 0 then acc else f (" " ^ acc) (n - 1)
val indent = y indent_ ""
in
(case indentation of SOME {limit=_,indent=d} => indent d
| NONE => ""
) ^
cofree_hylo
(fn (d, t) =>
let val (nl, nli) = case d of SOME {limit=_,indent=d_} => ("\n","\n" ^ indent d_)
| NONE => ("","")
val ws = if Option.isSome d then " " else ""
in
case t
of VAR v => pretty_var v
| NUM n => pretty_num n
| OP oper => let val (o_,l,r) = case oper of Op.+`(l,r) => ("+ ",l,r)
| Op.-`(l,r) => ("- ",l,r)
| Op.*`(l,r) => ("* ",l,r)
in "( " ^ l ^ nli
^ o_ ^ r ^ nli
^ ") "
end
| IFZ ifz_ => pretty_ifz ws nli ifz_
| LET {let_=(+$ v,bound),in_} => "(let +$" ^ v ^ " := " ^ nli
^ ws ^ bound ^ nli
^ "in " ^ nli
^ ws ^ in_ ^ nli
^ "end)"
| CALL {name= $ n,args=(ts,cvs)} => "call[$" ^ n ^ "]"
^
( if List.null ts andalso List.null cvs
then "(;)"
else
nli
^ "("
^ (case ts
of [] => ""
| (x :: xs) => " "
^ List.foldl (fn (s,acc) => acc ^ nli ^ ", " ^ s )
x
xs
)
^ nli
^ ";"
^ (case cvs
of [] => ""
| (-$ x :: xs) => " "
^ List.foldl (fn (-$ s,acc) => acc ^ nli ^ ", -$" ^ s )
("-$" ^ x)
xs
)
^ nli
^ ") "
)
| K {tag= $ t,fields} => "K[$" ^ t ^ "]"
^ (case fields
of [] => " "
| (x :: xs) => ( nli
^ "( "
^ List.foldl (fn (s,acc) => acc ^ nli ^ ", " ^ s )
x
xs
^ nli
^ ") "
)
)
| CASE_OF (t,cases) => "case " ^ nli
^ ws ^ t ^ nli
^ "of " ^
( case cases
of [] => "{} " ^ nl
| (c :: cs) =>
let fun case_string {tag= $ tag,fields,body}
= "K[$" ^ tag ^ "]"
^ (case fields
of [] => ""
| (+$ x :: xs) => nli ^ ws ^ "( "
^ List.foldl (fn (+$ s,acc) => acc ^ ", +$" ^ s )
("+$" ^ x)
xs
^ ")"
)
^ nli
^ ws ^ "=>" ^ nli
^ ws ^ body
in
nli
^ "{ " ^ List.foldl (fn (case_,acc) => acc ^ nl ^ nli ^ "| " ^ case_string case_ )
(case_string c)
cs
^ nli
^ "} "
end
)
| DO_D (t,{tag= $ tag,fields}) => t ^ ".D[$" ^ tag ^ "]" ^
(case fields
of [] => " "
| (x :: xs) => nli ^ "( "
^ List.foldl (fn (s,acc) => acc ^ nli ^ ", " ^ s )
x
xs
^ nli
^ ") "
)
| COCASE cocases => "cocase"
^ (case cocases
of [] => "{} " ^ nl
| (c :: cs) =>
let fun cocase_string {tag= $ tag,fields,body}
= ( "D[$" ^ tag ^ "]"
^ (case fields
of [] => ""
| (+$ x :: xs) => nli ^ "( "
^ List.foldl (fn (+$ s,acc) => acc ^ nli ^ ", +$" ^ s )
x
xs
^ nli
^ ")"
)
^ nli
^ "=>" ^ nli
^ body
)
in
( nli
^ "{ " ^ List.foldl (fn (cocase_,acc) => acc ^ nl ^ nli ^ "| " ^ cocase_string cocase_ )
(cocase_string c)
cs
^ nli
^ "} "
)
end
)
| LAMBDA (\(+$ v, body)) => ( "\\[+$" ^ v ^ "]." ^ nli
^ "( "
^ body ^ nli
^ ")"
)
| AP (f,a) => ( "ap" ^ nli
^ "( " ^ f ^ nli
^ ", " ^ a ^ nli
^ ") "
)
| LABEL {label= -$ l,in_} => ( "label[-$" ^ l ^ "]"^ nli
^ "{ " ^ in_ ^ nli
^ "} "
)
| GOTO {bind, label= -$ l} => ( "goto" ^ nli
^ "( " ^ bind ^ nli
^ "; -$" ^ l ^ nli ^ ") "
)
end
)
( fn (d, FIX t) => (d, fmap (fn slot => (case d of SOME{limit=l,indent=i} => if l < 0 then NONE else SOME {limit=l-1,indent=i+1} | NONE => NONE,slot)) t))
(indentation, f)
end
fun pretty_print_def setting (DEF f) = pretty_print_def_ pretty_print setting f
end
structure Core
= struct
datatype 'statement definition = DEF of { def : name
, args : var list * coVar list
, body : 'statement
}
type 'statement programs = 'statement definition list
type 'statement case_cocase = { tag : name, fields : var list * coVar list, body : 'statement } list
datatype 'statement proof = VAR of var
| NUM of number
| \+ of coVar * 'statement
| K of { tag : name, fields : 'statement proof list * 'statement continuation list }
| COCASE of 'statement case_cocase
and 'statement continuation = CO_VAR of coVar
| \- of var * 'statement
| CASE of 'statement case_cocase
| D of { tag : name, fields : 'statement proof list * 'statement continuation list }
type 'statement k_or_d = { tag : name, fields : 'statement proof list * 'statement continuation list }
datatype 'statement cut = <+/-> of 'statement proof * 'statement continuation
type 'statement ifz = { if_zero : 'statement proof
, then_ : 'statement
, else_ : 'statement
}
datatype 'statement statement = OP of ( 'statement proof
* 'statement proof
* 'statement continuation
) Op.binop
| IFZ of 'statement ifz
| CUT of 'statement cut
| CALL of { name : name
, args : 'statement proof list
* 'statement continuation list
}
fun fmap_proof m f
= case f of VAR v => VAR v
| NUM n => NUM n
| \+(cv, s) => \+(cv, m s)
| K {tag, fields=(vs,cvs)} => K { tag = tag
, fields = ( List.map (fmap_proof m) vs
, List.map (fmap_cont m) cvs
)
}
| COCASE cocases => ( COCASE
o List.map (fn {tag,fields,body} => {tag=tag,fields=fields, body=m body } )
) cocases
and fmap_cont m f
= case f of CO_VAR cv => CO_VAR cv
| \-(c, s) => \-(c, m s)
| D {tag, fields=(vs,cvs)} => D { tag = tag
, fields = ( List.map (fmap_proof m) vs
, List.map (fmap_cont m) cvs
)
}
| CASE cases => ( CASE
o List.map (fn {tag,fields,body} => {tag=tag,fields=fields, body=m body } )
) cases
fun fmap_ m f
= case f of OP oper => let fun m_ (oper_, (left,right,cont)) = (OP o oper_) (fmap_proof m left, fmap_proof m right, fmap_cont m cont) in m_ (Op.destructor oper) end
| IFZ{if_zero,then_,else_} => IFZ {if_zero=fmap_proof m if_zero, then_=m then_, else_=m else_}
| CUT(<+/->(p,c)) => (CUT o <+/->)(fmap_proof m p, fmap_cont m c)
| CALL{name, args=(proofs,conts)} => CALL{ name = name
, args = ( List.map (fmap_proof m) proofs
, List.map (fmap_cont m) conts
)
}
(* proof and cont fmap as a priority *)
fun fmap_proof_cont_statement p c s f
= case f of OP oper => let fun m_ (oper_, (left,right,cont)) = (OP o oper_) (p left, p right, c cont) in m_ (Op.destructor oper) end
| IFZ{if_zero,then_,else_} => IFZ{if_zero=p if_zero, then_=s then_, else_=s else_}
| CUT(<+/->(proof,cont)) => (CUT o <+/->)(p proof, c cont)
| CALL{name, args=(proofs,conts)} => CALL{ name = name
, args = ( List.map p proofs
, List.map c conts
)
}
local
structure F = Fix(type 'statement f = 'statement statement)
structure Scheme = Schemes(
structure S
= struct
open F
val fmap = fmap_
end
)
in
open F
open Scheme
end
fun is_proof_val p
= case p
of K k => List.foldl (fn (t_, acc) => acc andalso is_proof_val t_) true ((#1 o #fields) k)
| COCASE _ => true
| NUM _ => true
| VAR _ => true (* when bound, it will be a value, not an unevaluated expression *)
| \+ _ => false
fun is_cont_val c
= case c
of D _ => true
| CASE _ => true
| \- _ => true
| CO_VAR _ => true
local
fun indent_ f acc n = if n = 0 then acc else f (" " ^ acc) (n - 1)
val indent = y indent_ ""
fun get_ws_nl_nli setting = case setting of SOME {limit=_,indent=d_} => (" ","\n","\n" ^ indent d_)
| NONE => ("","","")
fun pretty_print_statement indentation fix_ : string
= (case indentation of SOME {limit=_,indent=d} => indent d
| NONE => ""
)
^
cofree_hylo
(fn (setting, t) =>
let val (ws, _, nli) = get_ws_nl_nli setting
val pretty_p = pretty_proof ws nli
val pretty_c = pretty_cont ws nli
in
case t
of
OP oper => let val (o_,l,r,c) = case oper of Op.+`(l,r,c) => ("+ ",l,r,c)
| Op.-`(l,r,c) => ("- ",l,r,c)
| Op.*`(l,r,c) => ("* ",l,r,c)
in "( " ^ pretty_p l ^ nli
^ o_ ^ pretty_p r ^ nli
^ "; " ^ pretty_c c ^ nli
^ ") "
end
| IFZ {if_zero,then_,else_} => pretty_ifz ws nli {if_zero = pretty_p if_zero, then_=then_, else_=else_ }
| CUT (<+/-> (p,c)) => "< " ^ pretty_p p ^ nli ^ "| " ^ pretty_c c ^ nli ^ "> "
| CALL {name= $ n,args=(ps,cs)} => ( "call[$" ^ n ^ "]"
^ ( if List.null ps andalso List.null cs
then "(;)"
else
nli
^ "("
^ (case ps
of [] => ""
| (x :: xs) => " "
^ List.foldl (fn (p,acc) => acc ^ nli ^ ", " ^ pretty_p p )
(pretty_p x)
xs
)
^ nli
^ ";"
^ (case cs
of [] => ""
| (x :: xs) => " "
^ List.foldl (fn (c,acc) => acc ^ nli ^ ", " ^ pretty_c c )
(pretty_c x)
xs
)
^ nli
^ ") "
)
)
end
)
( fn (d, FIX t) => (d, let
val s = (fn slot => (case d of SOME{limit=l,indent=i} => if l < 0 then NONE else SOME {limit=l-1,indent=i+1} | NONE => NONE,slot))
val s_ = (fn slot => (case d of SOME{limit=l,indent=i} => if l < 0 then NONE else SOME {limit=l-1,indent=i+2} | NONE => NONE,slot))
in
fmap_proof_cont_statement (fn (v as COCASE _) => fmap_proof s_ v
| v => fmap_proof s v
)
(fn (v as CASE _) => fmap_cont s_ v
| v => fmap_cont s v
)
s
t
end
)
)
(indentation, fix_)
and pretty_proof ws nli
= (fn VAR v => pretty_var v
| NUM n => pretty_num n
| \+(-$cv,s) => "\\+[-$" ^ cv ^ "]." ^ nli ^ ws ^ s
| COCASE cases => pretty_case_cocase ws nli cases "cocase" "D"
| K (k as {tag= $ tag, fields = (_,_)}) => ( "K[$" ^ tag ^ "]" ^ nli
^ pretty_k_or_d ws nli k
)
)
and pretty_cont ws nli
= (fn CO_VAR cv => pretty_coVar cv
| \-(+$v,s) => "\\-[+$" ^ v ^ "]." ^ nli ^ ws ^ s
| D (d as {tag= $ tag, fields = (_,_)}) => ( "D[$" ^ tag ^ "]" ^ nli
^ pretty_k_or_d ws nli d
)
| CASE cases => pretty_case_cocase ws nli cases "case" "K"
)
and pretty_k_or_d ws nli {tag= _, fields = (ps,cs)}
= if List.null ps andalso List.null cs
then ""
else ( ws ^ "( "
^ ( case ps
of [] => ""
| (x :: xs) => ( " "
^ List.foldl (fn (p,acc) => acc ^ nli ^ ws ^ ", " ^ pretty_proof ws nli p)
(pretty_proof ws nli x)
xs
)
) ^ nli
^ ws ^ ";"
^ ( case cs
of [] => ""
| (x :: xs) => ( " "
^ List.foldl (fn (c,acc) => acc ^ nli ^ ws ^ ", " ^ pretty_cont ws nli c)
(pretty_cont ws nli x)
xs
)
) ^ nli
^ ws ^ ") "
)
and pretty_case_cocase ws nli case_cocase_ case_cocase_string k_or_d_string
= ( case_cocase_string ^ " " ^ nli
^ (case case_cocase_
of [] => "{}"
| (x :: xs)
=> let fun case_ {tag= $tag, fields, body}
= ( k_or_d_string ^ "[$" ^ tag ^ "]"
^ (case fields
of ([],[]) => " "
| (vs,cvs)
=> ( "( "
^ (case vs
of [] => ""
| (+$x :: xs) => List.foldl (fn (+$v,acc) => acc ^ ", +$" ^ v ^ " ")
("+$" ^ x)
xs
)
^ ";"
^ (case cvs
of [] => ""
| (-$x :: xs) => " " ^ List.foldl (fn (-$v,acc) => acc ^ ", -$" ^ v ^ " ")
("-$" ^ x)
xs
)
^ " )"
)
)
^ nli
^ ws ^ ws ^ "=>" ^ nli
^ ws ^ ws ^ body
)
in
( ws ^ "{ " ^ List.foldl (fn (s,acc) => acc ^ nli ^ ws ^ "| " ^ case_ s ^ " ")
(case_ x)
xs
^ ws ^ nli ^ ws ^ "} "
)
end
)
)
in
val pretty_print_statement = pretty_print_statement
fun pretty_print_proof indentation = pretty_proof "" (if Option.isSome indentation then "\n" else "") o fmap_proof (pretty_print_statement indentation)
fun pretty_print_cont indentation = pretty_cont "" (if Option.isSome indentation then "\n" else "") o fmap_cont (pretty_print_statement indentation)
end
fun pretty_print_def setting (DEF f) = pretty_print_def_ pretty_print_statement setting f
end
local val fresh_var_count = ref 0
in
fun fresh () = ( fresh_var_count := (!fresh_var_count) + 1
; "_" ^ Int.toString (!fresh_var_count)
)
fun unsafe_refresh_fresh () = fresh_var_count := 0
val fresh_var = +$ o fresh
val fresh_coVar = -$ o fresh
end
structure Convert
= struct
(* open Fun *)
open Core
val fix_cut = (FIX o CUT o <+/->)
(* [|x|] := x *)
val variable : var -> fix proof = VAR
(* [|#n|] := #n *)
val number : number -> fix proof = NUM
(* [|t1 (op) t2|] := mu a.(op)([|t1|], [|t2|]; a) (a fresh) *)
fun binop f bop : fix proof = let val -? = fresh_coVar()
val (oper, (l,r)) = Op.destructor bop
in \+ ( -?, (FIX o OP o oper) (f l, f r, CO_VAR -?) )
end
(* [|ifz(t1,t2,t3|] := mu a.ifz([|t1|], <[|t2|] | a>, <[|t3|] | a>) *)
fun if_zero f {if_zero,then_,else_} : fix proof = let val -? = fresh_coVar()
fun perform x = fix_cut(f x, CO_VAR -?)
in \+ (-?, (FIX o IFZ) {if_zero = f if_zero, then_ = perform then_, else_ = perform else_})
end
(* [|let x = t1 in t2|] := mu a.<[|t1|] | ~mu x.<[|t2|] | a>> (a fresh)*)
fun let_ f {let_=(binding,bound), in_} : fix proof = let val -? = fresh_coVar()
fun cut p c = fix_cut (f p, c)
in \+ (-?, cut bound (\-(binding, cut in_ (CO_VAR -?))))
end
(* [|f(t..;a..|] := mu a_.f([|t|]..;a..,a_) (a_ fresh) *)
fun call f {name, args=(vs,cvs)} : fix proof = let val -? = fresh_coVar()
in \+ ( -?
, (FIX o CALL)
{ name = name
, args = ( List.map f vs
, List.map CO_VAR (List.@(cvs, [-?]))
)
}
)
end
(* [|def f(x..;a..) := t|] := def f(x..;(a..),a_) := <[|t|] | a_> (a_ fresh) *)
fun def (f : Fun.fix -> fix proof) {def=def_,args=(vs,cvs),body} : fix definition
= let val -? = fresh_coVar()
in DEF { def = def_
, args = ( vs , List.@(cvs, [-?]) )
, body = fix_cut (f body, CO_VAR -?)
}
end
(* [|K(t_1,...,t_n)|] := K([|t_1|],...,[|t_n|]) *)
fun constructor f ({tag,fields}: Fun.fix Fun.k_or_d) : fix proof = K {tag = tag, fields=(List.map f fields,[])}
(* [|case t of {K_i(x_ij..) => t_i, ..}|] := mu a.<[|t|] | case {K_i(x_ij..;) => <[|t_i|] | a>}> (a fresh)*)
fun case_of f ((t,c) : Fun.fix * Fun.fix Fun.case_cocase) : fix proof
= let val -? = fresh_coVar()
in \+( -?
, ( FIX o CUT
o (fn x => <+/->(f t, CASE x))
o List.map (fn {tag,fields,body} => { tag = tag,
fields = (fields,[]),
body = fix_cut(f body, CO_VAR -?)
}
)
) c
)
end
(* [|t.D(t_1,...,t_n)|] := mu a.<[|t|] | D([|t_1|],...,[|t_n|]; a)> (a frash) *)
fun do_d f ((t,{tag,fields}) : Fun.fix * Fun.fix Fun.k_or_d) : fix proof
= let val -? = fresh_coVar()
in \+( -?
, fix_cut(f t, D {tag=tag, fields=(List.map f fields,[CO_VAR -?])})
)
end
(* [|cocase {D_i(x_ij..), ..}|] := cocase {D_i(x_ij;a_i) => <[|t_i|] | a_i>, ..} ((a_i..) fresh) *)
fun cocase_ f : Fun.fix Fun.case_cocase -> fix proof
= COCASE
o List.map ( fn {tag,fields,body} =>
let val -? = fresh_coVar()
in { tag = tag
, fields = (fields,[-?])
, body = fix_cut(f body, CO_VAR -?)
}
end
)
val ap_tag = $"ap"
(* [|\x.t|] := cocase { ap(x;a) => <[|t|] | a> } (a fresh) *)
fun lambda f (Fun.\(x,t) : 'body Fun.lambda) = let val -? = fresh_coVar()
in COCASE [{ tag = ap_tag
, fields = ([x],[-?])
, body = fix_cut (f t,CO_VAR -?)
}]
end
(* [|t1 t2|] := mu a.<[|t1|] | ap([|t2|];a)> (a fresh) *)
fun apply f (func, arg) = let val -? = fresh_coVar()
in \+( -?
, fix_cut (f func, D { tag = ap_tag, fields = ([f arg], [CO_VAR -?]) })
)
end
(* [|label a {t}|] := mu a.<[|t|] | a> (a fresh) *)
fun label_ f {label,in_} = \+(label, fix_cut(f in_, CO_VAR label))
(* [|goto(t;a)|] := mu b.<[|t|] | a> (b fresh) *)
fun goto_ f {bind,label} = let val -? = fresh_coVar()
in \+(-?, fix_cut(f bind, CO_VAR label))
end
fun translate (Fun.FIX fun_term)
= let val f = translate
in
(case fun_term of Fun.VAR v => variable v
| Fun.NUM n => number n
| Fun.OP o_ => binop f o_
| Fun.IFZ i => if_zero f i
| Fun.LET l => let_ f l
| Fun.CALL c => call f c
| Fun.K k => constructor f k
| Fun.CASE_OF c => case_of f c
| Fun.DO_D d => do_d f d
| Fun.COCASE c => cocase_ f c
| Fun.LAMBDA l => lambda f l
| Fun.AP a => apply f a
| Fun.LABEL l => label_ f l
| Fun.GOTO g => goto_ f g
)
end
fun definition_translation (Fun.DEF d) = def translate d
val program_translation = List.map definition_translation
end
structure PartialEvalFun
= struct
open Fun
(* ifz(#0, t1, t2) ==> t1
ifz(#n, t1, t2) ==> t2 (if n =/= 0)
*)
fun p_eval_ifz {if_zero=FIX(NUM n), then_, else_} = if Word.fromInt 0 = n then then_ else else_
| p_eval_ifz ifz_ = (FIX o IFZ) ifz_
(* x:=y in t ==> t[y/x] *)
fun p_eval_substitute_var_term ((from, to) : var * fix) : fix -> fix
= apo ( fn FIX(VAR v) => if eq_var from v then (fmap Either.INL o prj) to else VAR v
| FIX(LET{let_ = (binding,bound), in_ =body}) => LET{ let_ = (binding,Either.INR bound)
, in_ = if eq_var from binding then Either.INL body else Either.INR body
}
| FIX(l as LAMBDA(\(v,_))) => fmap (if eq_var from v then Either.INL else Either.INR) l
| otherwise => (fmap Either.INR o prj) otherwise
)
(* ((x:=y)..) in t ==> t[(y..)/(x..)] *)
fun p_eval_substitute_varList_term (subs' : (var * fix) list) fix_ : fix
= apo ( fn ([] , rest) => (fmap Either.INL o prj) rest
| (subs, FIX(VAR v)) => (case List.find (fn (s,_) => eq_var s v) subs
of SOME (_,to) => (fmap Either.INL o prj) to
| NONE => VAR v
)
| (subs, FIX(LET{let_= (binding,bound), in_})) => LET{ let_ = (binding,Either.INR (subs, bound))
, in_ = Either.INR (List.filter (fn (s,_) => not(eq_var s binding)) subs ,in_)
}
| (subs, FIX(l as LAMBDA(\(v,_)))) => let val filtered = List.filter (fn (s,_) => not(eq_var s v)) subs
in
fmap (if List.exists (fn (from,_) => eq_var from v) subs
then Either.INL
else (fn x => Either.INR (filtered, x))
)
l
end
| (subs, otherwise) => (fmap (Either.INR o (fn t => (subs, t))) o prj) otherwise
)
(subs', fix_)
(* a:=b in t ==> t[b/a] *)
fun p_eval_substitute_coVar_term ((from, to) : coVar * coVar) : fix -> fix
= apo ( fn FIX(CALL {name,args=(args_,cvs)}) => CALL { name = name
, args = ( List.map Either.INR args_
, List.map (fn cv => if eq_coVar from cv then to else cv) cvs
)
}
| otherwise => (fmap Either.INR o prj) otherwise
)
(* ((a:=b)..) in t ==> t[(b..)/(a..)] *)
fun p_eval_substitute_coVarList_term (subs' : (coVar * coVar) list) fix_ : fix
= apo ( fn (subs, FIX(CALL {name,args=(args_,cvs)})) => CALL { name = name
, args = ( List.map (Either.INR o (fn t => (subs,t))) args_
, List.map (fn cv => case List.find (fn (from,_) => eq_coVar from cv) subs
of SOME (_,to) => to
| NONE => cv
)
cvs
)
}
| (subs, otherwise) => (fmap (Either.INR o (fn t => (subs,t))) o prj) otherwise
)
(subs', fix_)
(* #n (op) #m ==> #(n (op) m) *)
fun p_eval_op op_ l r = (Op.primop op_)(l,r)
(* let x = t1 in t2 = t2[t1/x] *)
fun p_eval_let (t as {let_=l as (_,expr), in_}) = if is_term_value expr
then p_eval_substitute_var_term l in_
else (FIX o LET) t
(* f(t..;a..) ==> t_[(t..)/(x..), (a..)/(b..)] (if f(x..;b..) := t_ in P) *)
exception PARTIAL_EVAL_CALL of {name : name, args : fix list * coVar list} * fix programs
fun p_eval_call (f as {name, args = (vs, cs)}) progs
= let val error = PARTIAL_EVAL_CALL(f,progs)
val DEF {def=_, args=(def_vars,def_coVars), body}
= case List.find (fn DEF def_ => eq_name (#def def_) name) progs
of SOME p => p
| NONE => raise error
in
(p_eval_substitute_varList_term (Utils.zip def_vars vs [] error) o p_eval_substitute_coVarList_term (Utils.zip def_coVars cs [] error))
body
end
local
fun p_eval_case_cocase error_type (cases : fix case_cocase) (kd : fix k_or_d)
= let val error = error_type(cases, kd)
in case List.find (fn case_ => eq_name (#tag case_) (#tag kd) ) cases
of NONE => raise error
| SOME case_ => p_eval_substitute_varList_term (Utils.zip (#fields case_) (#fields kd) [] error) (#body case_)
end
in
(* case K(t..) of {K(x..) => t_, ...} ==> t_[(t..)/(x..)] *)
exception PARTIAL_EVAL_CASE_OF_K of (fix case_cocase * fix k_or_d)
fun p_eval_case_of_k_cases k c = p_eval_case_cocase PARTIAL_EVAL_CASE_OF_K c k
(* cocase {D(x..) => t_, ...}.D(t..) ==> t_[(t..)/(x..)]*)
exception PARTIAL_EVAL_COCASE_WITH_D of (fix case_cocase * fix k_or_d)
fun p_eval_d_cocases d cocases = p_eval_case_cocase PARTIAL_EVAL_COCASE_WITH_D cocases d
end
(* (\x.t) t_ ==> t[t_/x] *)
fun p_eval_ap (l as \(v,b)) (arg : fix) = if is_term_value arg
then p_eval_substitute_var_term (v,arg) b
else (FIX o AP) ((FIX o LAMBDA) l, arg)
fun partial_eval_noInline_pass (fix_ : fix)
= let
fun do_op oper = (case Op.destructor oper
of (_, (FIX (NUM l), FIX (NUM r))) => (FIX o NUM) (p_eval_op oper l r)
| _ => (FIX o OP) oper
)
val traverse_labels
= let fun left_to_right_vals r fields = (case List.mapPartial r fields
of [] => NONE
| (x :: _) => SOME x
)
fun pattern r return_label (FIX t : fix) =
let val f = r return_label
in
case t
of LABEL {label,in_} => if eq_coVar label return_label
then NONE
else f in_
| GOTO { bind, label} => if eq_coVar label return_label andalso is_term_value bind
then SOME bind
else f bind
| K k => left_to_right_vals f (#fields k)
| CASE_OF case_of => f (#1 case_of)
| IFZ ifz_ => f (#if_zero ifz_)
| OP oper => let val (_, (left, right)) = Op.destructor oper
in case (f left)
of NONE => f right
| x => x
end
| DO_D ( FIX (COCASE _), d) => left_to_right_vals f (#fields d)
| LET let_ => f ((#2 o #let_) let_)
| AP ap => f (#1 ap)
| CALL c => left_to_right_vals f ((#1 o #args) c)
| NUM _ => NONE
| VAR _ => NONE
| LAMBDA _ => NONE
| COCASE _ => NONE
| DO_D _ => NONE
end
in
y pattern
end
fun apply_reduction (FIX e) = (case e
of OP oper => do_op oper
| IFZ ifz_ => p_eval_ifz ifz_
| LET {let_=l as (_,expr), in_} => if is_term_value expr
then p_eval_substitute_var_term l in_
else FIX e
| CASE_OF (FIX (K k), cases) => p_eval_case_of_k_cases k cases
| DO_D (FIX (COCASE c), d) => p_eval_d_cocases d c
| AP (FIX (LAMBDA l), arg) => p_eval_ap l arg
| l as LABEL {label, in_} => (case traverse_labels label in_
of SOME x => x
| NONE => FIX l
)
| _ => FIX e)
in
hylo (apply_reduction o inj o fmap apply_reduction )
(fmap apply_reduction o prj o apply_reduction )
fix_
end
end
structure PartialEvalCore
= struct
open Core
(*--Var Sub--*)
(* x:=p in s ==> s[p/x] *)
fun p_eval_substitute_var_statement ((from,to) : var * fix proof) : fix -> fix
= let fun svp p = case p of VAR v => if eq_var v from then fmap_proof Either.INL to else VAR v
| _ => fmap_proof Either.INR p
fun svc c = case c of \-(binding, s) => \-(binding, (if eq_var from binding then Either.INL else Either.INR) s )
| _ => fmap_cont Either.INR c
in
apo (fmap_proof_cont_statement svp svc Either.INR o prj)
end
(* ((x:=p)..) in s ==> s[(p..)/(x..)] *)
fun p_eval_substitute_varList_statement (subs' : (var * fix proof) list) (fix_ : fix) : fix
= let fun svp subs p' = case p' of VAR v => ( case List.find (fn (from,_) => eq_var from v) subs
of SOME (_,to) => fmap_proof Either.INL to
| NONE => VAR v
)
| p => fmap_proof (Either.INR o (fn s => (subs, s))) p
fun svc subs c' = case c' of \-(binding, s) => \-( binding
, Either.INR ( List.filter (fn (from,_) => not(eq_var from binding)) subs
, s
)
)
| c => fmap_cont (Either.INR o (fn s => (subs, s))) c
in
apo (fn ([] , FIX s) => fmap Either.INL s
| (subs, FIX s) => fmap_proof_cont_statement (svp subs)
(svc subs)
(Either.INR o (fn s_ => (subs,s_)))
s
)
(subs',fix_)
end
(*--CoVar Sub--*)
(* a:=c in s ==> s[c/a] *)
fun p_eval_substitute_coVar_statement ((from,to) : coVar * fix continuation) : fix -> fix
= let fun svp p = case p of \+(cv,s) => \+(cv, (if eq_coVar from cv then Either.INL else Either.INR) s )
| _ => fmap_proof Either.INR p
fun svc c = case c of CO_VAR cv => if eq_coVar from cv then fmap_cont Either.INL to else CO_VAR cv
| _ => fmap_cont Either.INR c
in
apo (fmap_proof_cont_statement svp svc Either.INR o prj)
end
(* ((a:=c)..) in s ==> s[(c..)/(a..)] *)
fun p_eval_substitute_coVarList_statement (subs' : (coVar * fix continuation) list) fix_ : fix
= let fun svp subs p' = case p' of \+(cv,s) => \+( cv
, Either.INR ( List.filter (fn (from,_) => not(eq_coVar from cv)) subs, s )
)
| p => fmap_proof (Either.INR o (fn s => (subs, s))) p
fun svc subs c = case c of CO_VAR cv => ( case List.find (fn (from,_) => eq_coVar from cv) subs
of SOME (_,to) => fmap_cont Either.INL to
| NONE => CO_VAR cv
)
| _ => fmap_cont (Either.INR o (fn s => (subs, s))) c
in
apo (fn ([] , FIX s) => fmap Either.INL s
| (subs, FIX s) => fmap_proof_cont_statement (svp subs)
(svc subs)
(Either.INR o (fn s_ => (subs,s_)))
s
)
(subs', fix_)
end
(* ifz(#0,s1,s2) ==> s1
ifz(#n,s1,s2) ==> s2 (if n =/= 0)
*)
fun p_eval_ifz {if_zero=NUM n, then_=FIX s1, else_=FIX s2} = if Word.fromInt 0 = n then s1 else s2
| p_eval_ifz ifz = IFZ ifz
(* (op)(#n,#m;c) ==> <#(n (op) m) | c> *)
fun p_eval_op op_ l r c = ((NUM o op_)(l,r), c)
(* <mu a.s | c> ==> s[c/a] *)
fun p_eval_apply_mu (a,s) c = p_eval_substitute_coVar_statement (a,c) s
(* <p | ~mu x.s> ==> s[p/x] *)
fun p_eval_apply_tmu p (x,s) = p_eval_substitute_var_statement (x,p) s
(* f(p.. ; c..) ==> s[(p..)/(x..), (c..)/(a..)] (if f(x..;a..) := s in P) *)
exception PARTIAL_EVAL_CALL of {name : name, args : fix proof list * fix continuation list} * fix programs
fun p_eval_call (func as {name, args=(proofs,conts)}) (progs : fix programs) =
let val error = PARTIAL_EVAL_CALL(func, progs)
val DEF {def=_ ,args=(formalParams,formalCoParams), body}
= case List.find (fn DEF def_ => eq_name (#def def_) name ) progs
of SOME d => d
| NONE => raise error
in
( p_eval_substitute_coVarList_statement (Utils.zip formalCoParams conts [] error)
o p_eval_substitute_varList_statement (Utils.zip formalParams proofs [] error)
) body
end
local
fun p_eval_pattern_match { tag, fields = (proofs , conts) } cases_ error
= let val {body,fields=(formalParams,formalCoParams),tag=_}
= case List.find (fn {tag=case_tag, fields=_, body=_} => eq_name case_tag tag) cases_
of SOME c => c
| NONE => raise error
in
( p_eval_substitute_coVarList_statement (Utils.zip formalCoParams conts [] error)
o p_eval_substitute_varList_statement (Utils.zip formalParams proofs [] error)
) body
end
in
(* <K(p..;c..) | case {K(x..;a..) => s, ...}> ==> s[(p..)/(x..) ; (c..)/(a..)] *)
exception PARTIAL_EVAL_CUT_K_CASE of fix cut
fun p_eval_cut_k_case k cases = p_eval_pattern_match k cases ((PARTIAL_EVAL_CUT_K_CASE o <+/->) (K k, CASE cases) )
(* <cocase {D(x..;a..) => s, ...} | D(p..;c..)> ==> s[(p..)/(x..) ; (c..)/(a..)] *)
exception PARTIAL_EVAL_CUT_COCASE_D of fix cut
fun p_eval_cut_cocase_d cocases d = p_eval_pattern_match d cocases ((PARTIAL_EVAL_CUT_COCASE_D o <+/->) (COCASE cocases, D d))
end
val static_focus_layer
(* ana will recurse into the statement bodys *)
(* We need to remember that nested proof and continuation focussing needs to be done manualy *)
= let fun proof_focusing (p : fix proof) : fix proof
= case p
of K{tag, fields} => let fun loop rev_front (fp :: fps)
= (if is_proof_val fp
then loop (fp :: rev_front) fps
else let val a = fresh_coVar()
val x = fresh_var()
val fix_cut = FIX o CUT o <+/->
in \+(a, fix_cut (fp, \-(x, fix_cut (K{ tag=tag
, fields=(List.revAppend (rev_front, VAR x :: fps), #2 fields)
}
, CO_VAR a
))))
end
)
| loop _ []
= K{tag=tag, fields=( List.map proof_focusing (#1 fields)
, List.map cont_focusing (#2 fields)
)
}
in
loop [] (#1 fields)
end
| NUM _ => p
| VAR _ => p
| \+ _ => p
| COCASE _ => p
(* ana will recurse into the statement bodys *)
(* We need to remember that nested proof and continuation focussing needs to be done manualy *)
and cont_focusing (c : fix continuation) : fix continuation
= case c
of D{tag, fields} => let fun loop rev_front (fp :: fps)
= (if is_proof_val fp
then loop (fp :: rev_front) fps
else let val y = fresh_var()
val x = fresh_var()
val fix_cut = FIX o CUT o <+/->
in \-(y, fix_cut (fp, \-(x, fix_cut ( VAR y
, D{ tag=tag
, fields=(List.revAppend (rev_front, VAR x :: fps), #2 fields)
}
))))
end
)
| loop _ []
= D{tag=tag, fields=( List.map proof_focusing (#1 fields)
, List.map cont_focusing (#2 fields)
)
}
in
loop [] (#1 fields)
end
| CO_VAR _ => c
| \- _ => c
| CASE _ => c
(* ana will recurse into the statement bodys *)
(* We need to remember that nested proof and continuation focussing needs to be done manualy *)
and statement_focusing (FIX s : fix) : fix
= FIX (case s
of CUT _ => s
| OP oper => let val x = fresh_var()
type arg = fix proof * fix proof * fix continuation
val (op_ : arg -> arg Op.binop, (l,r,c)) = Op.destructor oper
in case (is_proof_val l, is_proof_val r)
of (false, _) => (CUT o <+/->) (l, \-(x, (FIX o OP o op_)(VAR x,r,c)))
| ( _, false) => (CUT o <+/->) (r, \-(x, (FIX o OP o op_)(l,VAR x,c)))
| ( true, true) => (OP o op_)(proof_focusing l, proof_focusing r, cont_focusing c)
end
| IFZ ifz_ => let val {if_zero, then_, else_} = ifz_
in if is_proof_val if_zero
then IFZ { if_zero = proof_focusing if_zero
, then_=then_
, else_=else_
}
else let val x = fresh_var()
in (CUT o <+/->)
( proof_focusing if_zero
, \-( x
, (FIX o IFZ)
{ if_zero = VAR x
, then_ = then_
, else_ = else_
}
)
)
end
end
| CALL call => let val {name, args=(proofs, conts)} = call
fun loop rev_front (p :: ps)
= (if is_proof_val p
then loop (p :: rev_front) ps
else let val x = fresh_var()
val c = \-(x
, (FIX o CALL)
{ name=name
, args=( List.revAppend (rev_front, VAR x :: ps), conts)
}
)
in (CUT o <+/->)(p, c)
end
)
| loop _ [] = CALL { name=name
, args = ( List.map proof_focusing proofs
, List.map cont_focusing conts
)
}
in loop [] proofs
end
)
in (fmap_proof_cont_statement proof_focusing cont_focusing statement_focusing)
end
fun p_eval_clear_mu_then f p0 = case fmap_proof f p0 of \+ (cv0, (FIX (CUT (<+/-> (p1 ,CO_VAR cv1))))) => if eq_coVar cv0 cv1 then p1 else p0
| p2 => p2
fun p_eval_clear_tmu_then f c0 = case fmap_cont f c0 of \- (v0, (FIX ( CUT ( <+/-> (VAR v1, c1))))) => if eq_var v0 v1 then c1 else c0
| c2 => c2
fun partial_eval_noInline_pass (fix_ : fix)
= let
fun do_cut cut = case cut of (\+ mu, c) => p_eval_apply_mu mu c
| (p, \- tmu) => p_eval_apply_tmu p tmu
| (K k, CASE c) => p_eval_cut_k_case k c
| (COCASE c, D d) => p_eval_cut_cocase_d c d
| _ => (FIX o CUT o <+/->) cut
fun do_op oper = case Op.destructor oper
of (_, (NUM l, NUM r, c)) => do_cut (p_eval_op (Op.primop oper) l r c)
| _ => (FIX o OP) oper
fun apply_reduction (FIX e) = case e
of OP oper => do_op oper
| CUT (<+/-> cut) => do_cut cut
| IFZ ifz_ => FIX (p_eval_ifz ifz_)
| _ => FIX e
val apply_reduction__ = fmap_proof_cont_statement (p_eval_clear_mu_then apply_reduction )
(p_eval_clear_tmu_then apply_reduction )
apply_reduction
(* fun static_focus_layer x = x *)
in
hylo ( apply_reduction o inj o apply_reduction__ o static_focus_layer )
( static_focus_layer o apply_reduction__ o prj o apply_reduction )
fix_
end
val partial_eval_noInline_pass_proof = p_eval_clear_mu_then partial_eval_noInline_pass
val partial_eval_noInline_pass_cont = p_eval_clear_tmu_then partial_eval_noInline_pass
end
structure Typing
= struct
datatype k = NIL | CONS | TUP
datatype d = HEAD | TAIL | FIRST | SND | AP
datatype 'tau tau = INT
| LIST of 'tau
| PAIR of 'tau * 'tau
| STREAM of 'tau
| LPAIR of 'tau * 'tau
| --> of 'tau * 'tau
infixr 3 -->
fun fmap_tau m f
= case f
of INT => INT
| LIST l => LIST (m l)
| PAIR (l,r) => PAIR (m l, m r)
| STREAM s => STREAM (m s)
| LPAIR (l,r) => PAIR (m l, m r)
| l --> r => m l --> m r
structure TauF = Fix(type 'tau f = 'tau tau)
local open TauF
in
structure TauS = Schemes(
structure S
= struct
open TauF
val fmap = fmap_tau
end
)
end
val eq_type = let fun eq_ r (TauF.FIX t0_) (TauF.FIX t1_) =
case (t0_, t1_)
of ( INT , INT ) => true
| ( LIST l0, LIST l1) => r l0 l1
| ( PAIR (l0, r0), PAIR (l1, r1)) => r l0 l1 andalso r r0 r1
| (STREAM s0, STREAM s1) => r s0 s1
| ( LPAIR (l0, r0), LPAIR (l1, r1)) => r l0 l1 andalso r r0 r1
| ( in0 --> out0, in1 --> out1) => r in0 in1 andalso r out0 out1
| _ => false
in y eq_
end
infix 2 `:
datatype val_of_type = `: of (string * TauF.fix)
datatype 'context context = CTX_0
| PRD of 'context * val_of_type
| CNS of 'context * val_of_type
infix PRD CNS
fun fmap_ctx m f
= case f
of CTX_0 => CTX_0
| c PRD vt => m c PRD vt
| c CNS vt => m c CNS vt
structure CtxF = Fix(type 'tau f = 'tau context)
local open CtxF
in
structure CtxS = Schemes(
structure S
= struct
open CtxF
val fmap = fmap_ctx
end
)
end
(*
%% cut
'|-'(Gamma, <P|C>) :-
'|-'(Gamma, +P), tau(P),
'|-'(Gamma, -C), tau(C).
*)
end
end
structure Examples
= struct
open Compiler
local open Fun
in
val num_ = (FIX o NUM o Word.fromInt)
val var_ = (FIX o VAR o +$)
datatype of_ = of_
fun case_ c of_ cs = (FIX o CASE_OF)(c,cs)
datatype ==> = ==>
fun -- tag fields ==> body = {tag= $ tag, fields= List.map +$ fields, body=body}
fun call_ name vargs cargs = (FIX o CALL) {name= $ name, args=(vargs, List.map -$ cargs)}
fun op_ o_ l r = (FIX o OP o o_) (l, r)
datatype equals = ::=
fun def_ d vargs cargs ::= body = DEF {def= $ d, args=(List.map +$ vargs, List.map -$ cargs), body=body}
fun label_ l i = (FIX o LABEL) {label= -$l, in_=i}
datatype then_ = then_
datatype else_ = else_
fun ifz_ cond then_ t else_ e = (FIX o IFZ) {if_zero=cond, then_=t, else_=e}
fun goto_ v l = (FIX o GOTO) {bind=v, label= -$ l}
val cocase_ = (FIX o COCASE)
fun k_ tag fields = (FIX o K){tag = $ tag, fields=fields}
fun do_d_ t tag fields = (FIX o DO_D)(t, {tag = $ tag, fields=fields})
fun \: x ==> e = (FIX o LAMBDA o \)(+$ x, e)
fun ap_ f a = (FIX o AP)(f,a)
(* def mult(𝑙) ≔ case 𝑙 of { Nil β‡’ 1, Cons(π‘₯, π‘₯𝑠) β‡’ π‘₯ βˆ— mult(π‘₯𝑠) } *)
val example_1_1
= def_ "mult" ["l"] [] ::=
(case_
(var_ "l")
of_
[ -- "Nil" [] ==> (num_ 1)
, -- "Cons" ["x","xs"] ==> (op_ Op.*` (var_ "x")
(call_ "mult" [var_ "xs"] [])
)
]
)
(* def mult(𝑙) ≔ label 𝛼 { mult’(𝑙; 𝛼) }
def mult’(𝑙; 𝛼) ≔ case 𝑙 of { Nil β‡’ 1, Cons(π‘₯, π‘₯𝑠) β‡’ ifz(π‘₯, goto(0; 𝛼), π‘₯ βˆ— mult’(π‘₯𝑠; 𝛼)) }
*)
val example_1_2
= [ def_ "mult" ["l"] [] ::=
(label_ "a"
(call_ "mult'" [var_ "l"] ["a"])
)
, def_ "mult'" ["l"] ["a"] ::=
(case_
(var_ "l")
of_
[ -- "Nil" [] ==> (num_ 1)
, -- "Cons" ["x","xs"] ==> (ifz_ (var_ "x")
then_ (goto_ (num_ 0) "a")
else_ (op_ Op.*` (var_ "x")
(call_ "mult'" [var_ "xs"] ["a"])
)
)
]
)
]
(* def sum(π‘₯) ≔ case π‘₯ of {Nil β‡’ ⌜0⌝, Cons(𝑦, 𝑦𝑠) β‡’ 𝑦 + sum(𝑦𝑠)} *)
val example_2_4_0_1
= def_ "sum" ["x"] [] ::=
(case_
(var_ "x")
of_
[ -- "Nil" [] ==> (num_ 0)
, -- "Cons" ["y","ys"] ==> (op_ Op.+` (var_ "y")
(call_ "sum" [var_ "ys"] [])
)
]
)
(* def repeat(π‘₯) ≔ cocase {hd β‡’ π‘₯, tl β‡’ repeat(π‘₯)} *)
val example_2_4_0_2
= def_ "repeat" ["x"] [] ::=
(cocase_ [ -- "hd" [] ==> (var_ "x")
, -- "tl" [] ==> (call_ "repeat" [var_ "x"] [])
]
)
(* def swap(π‘₯) ≔ case π‘₯ of {Tup(𝑦, 𝑧) β‡’ Tup(𝑧, 𝑦)} *)
val example_2_4_1
= def_ "swap" ["x"] [] ::=
(case_
(var_ "x")
of_
[ -- "Tup" ["y","z"] ==> (k_ "Tup" [var_ "z", var_ "y"]) ]
)
(* def swap_lazy(π‘₯) ≔ cocase {fst β‡’ π‘₯ .snd, snd β‡’ π‘₯ .fst} *)
val example_2_4_2
= def_ "swap_lazy" ["x"] [] ::=
(cocase_ [ -- "fst" [] ==> (do_d_ (var_ "x") "snd" [])])
(* (πœ†π‘₯ .π‘₯ βˆ— π‘₯) ⌜2⌝ *)
val example_2_6
= ap_ (\: "x" ==> (op_ Op.*` (var_ "x") (var_ "x"))) (num_ 2)
val case_test
= (case_ (k_ "Pair" [num_ 1, num_ 2]) of_ [ -- "Pair" ["x", "y"] ==> (var_ "x") ])
end
val setting =
(* NONE *)
(SOME{limit=0,indent=1})
val print_def = print o Fun.pretty_print_def setting
(* val print_expr = print o (fn x => Fun.pretty_print setting x ^ "\n\n") *)
(* val _ = print_def example_1_1 *)
(* val _ = List.map print_def example_1_2 *)
(* val _ = print_def example_2_4_0_1 *)
(* val _ = print_def example_2_4_0_2 *)
(* val _ = print_def example_2_4_1 *)
(* val _ = print_def example_2_4_2 *)
(* val _ = print_expr example_2_6 *)
(* local open Fun
val apply = (fn FIX (AP (FIX (LAMBDA l), a)) => PartialEvalFun.p_eval_ap l a | _ => raise Empty)
val mul = (fn FIX (OP o_) => let val (l, r) = (case Op.destructor o_ of (_, (FIX (NUM l), FIX (NUM r))) => (l, r) | _ => raise Empty) in (FIX o NUM) (PartialEvalFun.p_eval_op o_ l r) end | _ => raise Empty )
in val _ = ( print_expr
o mul
o apply
) example_2_6
end *)
(* val _ = ( print_expr o PartialEvalFun.partial_eval_noInline_pass ) example_2_6 *)
(* val _ = (print
o (fn x => Core.pretty_print_proof setting x ^ "\n\n")
o PartialEvalCore.partial_eval_noInline_pass_proof
o Convert.translate
o (fn x => (print (Fun.pretty_print setting x ^ "\n\n"); x))) example_2_6 *)
(* val _ = print_def example_1_1 *)
val _ = ( List.map (print o (fn x => Core.pretty_print_def setting x ^ "\n")
o (fn Core.DEF {def, args, body} => Core.DEF {def=def, args=args, body= PartialEvalCore.partial_eval_noInline_pass body})
o Convert.definition_translation
)
example_1_2
)
(* val _ = (print
o (fn x => Core.pretty_print_proof setting x ^ "\n\n")
o PartialEvalCore.partial_eval_noInline_pass_proof
o Convert.translate
) case_test *)
end
val _ = print "\nDONE"
val _ = OS.Process.exit OS.Process.success
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment