(* Lingay implementations of various theoretically important operations *)
(* needed e.g. for full abstraction/definability results.               *)
(* The existence of such well-typed programs (with certain behaviours)  *)
(* serves as a stringent test of the design of the language.            *)


(* John Longley, started 28 April 2008 *)


(* Some dummy type definitions *)

type RW         = {rw : int->int} ;
type RW'        = {rw : int->int , rw': int->int}  ;
type obj        = {m  : int->int} ;
type obj'       = {m  : int->int , m' : int->int} ;
type tausuper   = RW  -> obj ;
type tausuper'  = RW' -> obj ;
type tauself    = RW' -> obj' ;

type selfstate  = [selfstate  : int-oint] ;    (* can be linear *)
type superstate = [superstate : int-oint] ;
type selfarg    = [selfarg    : int-oint] ;
type superarg   = [superarg   : int-oint] ;

(* Some useful coercions: *)

val forgetNewMethods =
    fn self : tauself => fn RW':RW' => 
	split self RW' as {m=m} +> newMethods
        in {m=m}
        end ;

val coerceApply =
    fn supermethods : !(tausuper -o tausuper) =>
      (* note bang now needed here *)
      fn super' : tausuper' =>
        fn RW':RW' => 
	    split RW' as {rw=rw, rw'=rw'} +> dummy in
                supermethods (fn RW:RW => super' {rw=RW.rw, rw'=rw'}) 
                             {rw=rw}
            (* could be done polymorphically in rw' if we had *)
            (* reusable row variables *)
            end ;


(* Concrete implementation of the "extend" operation. *)
(* New version using refined treatment of fields,     *)
(* with no reliance on row polymorphism.              *)
(* Note that several -o's have become ->'s.           *)

type StuffType = {
     fst : { methods     : tausuper -> tausuper ,
             constructor : superarg -> superstate } ,
     snd : tausuper' -> tauself -> tauself ,
     thd : selfarg -> { superarg : superarg ,
                        extender : superstate -o selfstate }
     } ;	

val extendOp =
   fn stuff : StuffType =>
     split stuff as 
        { fst=superclass, snd=methodimpl, thd=constrimpl } +> d1
     in split superclass as 
           { methods=supermethods, constructor = superconstr } +> d2
        in { methods = fn this : tauself => 
	                 methodimpl  
	                 (coerceApply supermethods (forgetNewMethods this))
                         this ,
             constructor = fn selfarg : selfarg =>
                         split (constrimpl selfarg)
                         as {superarg=superarg, extender=extender} +> d3
                         in extender $ (superconstr superarg)
                         end }
        end
     end ;

(* This typechecks correctly with the intended type:             *)
(*     extendOp : (StuffType -o                                  *)
(*                {methods: (tauself -> tauself),                *)
(*                  constructor: (selfarg -> selfstate)})        *) 
(*                (none)                                         *)
(* Lovely! *)


(* Some retractions etc. associated with the universal type "forest". *)

type univ = { m : ! (int -o int) } ; 
(* Maybe dispense with labelled record. !(int -o int) is fine.   *)

(* Isomorphism between univ and forest *)

val univToForest = 
    rec u2f : univ-oforest => 
        oncefn u : univ => fold forest 
            (oncefn n:int =>
                {label = u.m n , rest = u2f $ u}) ;

(* val univToForest : ({m: (int -> int)} -o forest) (none)       *)

(* Typechecker/definition bug:                                   *)
(* Definition of groundlessness wrong for int, bool, forest.     *)
(* In implementation, also wrong for -o types.                   *)

(* The other direction: partially typechecked                    *)
(* (Linear classes not supported by implementation yet)          *)
(* In any case, needs reworking if linear classes have to have ground type
   constructor arguments. *)


(*
val seq = fn x:{} => fn y:int => y ;

type forestRW = {read : {}-o{f:forest}, write : {f:forest}-o{}} ;

val forestToUnivClass = 
    linear extend (linear triv) with
       oncefn super : {} => 
       oncefn self  : {m : !(forestRW -o int -o int)} =>
           {m = prom (oncefn rw : forestRW =>
                split rw as {read=read, write=write} +> d in
                      oncefn n: int =>
                         split (unfold forest ((read $ {}).f) $ n) as
                            {label = p, rest = f} +> d
                         in seq (write $ {f=f}) p
                         end
                end)} ,
       oncefn f : forest => {superarg = {} , 
                             extender = oncefn x : {} => {f=f}}
    end ;

val forestToUniv = prom (linear constr forestToUnivClass) ; 

*)

(* Dummy for now *)
val forestToUniv = rec f2u : forest -> univ => f2u ;


(* The retraction "univ * univ <| univ" is now easy. *)

(* Dummy implementations of some coding functions.   *)
(* Typechecker bug: Special constants like _intSuc don't work.   *)

type tagInt = {t : bool, i : int} ;
val tag = rec f : tagInt -> int => f ;
val detag = rec f : int -> tagInt => f ;

val embedUnivPair = 
    oncefn upair : {fst:univ, snd:univ} =>
        split upair as {fst=fst, snd=snd} +> d in
            {m = fn n:int => 
	        split detag n as {t=t,i=i} +> d' in
                    if t then fst.m i else snd.m i
                end} 
            :: univ
        end ;

val projectUnivPair =
    oncefn u : univ =>
        { fst = {m = fn n:int => u.m (tag {t=true, i=n})} :: univ ,
          snd = {m = fn n:int => u.m (tag {t=false,i=n})} :: univ } ;
(* Typechecker bug: Fails if order of record components t,i is reversed. *)


(* The retraction forest -o forest <| forest *)

type tree = {label:int, rest:forest} ;
type branching = int -o tree ;

val FF = fn b : branching => fold forest b ;
val UF = fn f : forest => unfold forest f ;


(* We use the following slightly simplified version of catchcont: *)

val dummyTest = rec test : !(int -o tree) => test ;

val pseudopromote = rec PP : (int -o tree) -> !(int -o tree) => PP ;
(* To be implemented by means of a linear class *)

type OnceCatchcontType =
    [ result : {value  : int , 
                more   : (int -o tree) -o forest} ,
      query  : {arg    : int ,
                resume : tree -o {l:int, r:forest}} ] ;
(* Typechecker bug: *)
(* Lingering l,r in Catchcont type should be value,residue *)

(* Perhaps [ ... ] should be saved for lists: *)
(* use [| ... |] for labelled sums?           *)

val oncecatchcont =
    fn body : (int -o tree) -o {value:int, residue:forest} =>
        case catchcont x : !(int -o tree) => body $ (der x) of
            % result r =>
                 split r as {value=v, more=M} +> d in
                    % result 
                       {value = v, 
                        more = oncefn x : int -o tree => 
                                 M $ (pseudopromote x)}
                    :: OnceCatchcontType
                 end
          | % query q =>
                 split q as {arg=a, resume=R} +> d in
                    % query
                       {arg = a,
                        resume = oncefn t:tree => R $ t $ dummyTest}
                    :: OnceCatchcontType
                 end
        end ;

(* It's a runtime fact about oncecatchcont that dummyTest and the dummy *)
(* parts of pseudopromote are never invoked *)

(* Question re grammar: should juxtaposition bind more tightly than $ ? *)
(* N.B. brackets in the phrase "M $ (pseudopromote x)" above *)


(* Now the abstraction operation.                                   *)
(* Some painful syntax is needed to simulate mutual recursion.      *)

val diverge = rec f:{}->int => f ;

val tagL = fn i:int => tag {t=true, i=i} ;
val tagR = fn i:int => tag {t=false,i=i} ;
val detagL = 
    fn j:int => 
	split detag j as {t=t,i=i} +> d in
            if t then i else diverge{}
        end ;
val detagR = 
    fn j:int => 
	split detag j as {t=t,i=i} +> d in
            if t then diverge{} else i
        end ;

type abstrBodyType = {
    fst : (branching -o forest) -> forest ,
    snd : (branching -o tree) -> tree
    } ;

val abstract (* : (forest -o forest) -o forest *) =
    split 
       rec abstr : abstrBodyType =>
          split abstr as {fst=abstr', snd=abstr''} +> d in  
	    { fst = fn P : branching -o forest =>
	            FF (oncefn h:int => 
		       abstr'' (oncefn g : branching => 
	                           (UF (P$g)) $ (detagR h))) ,
	      snd = oncefn R : branching -o tree =>
		    case 
                         oncecatchcont (oncefn x : int -o tree => 
			    split R $ x as {label=l, rest=r} +> d in
                               {value=l, residue=r} 
                            end)
		    of
		         % result r => 
                            split r as {value=v, more=M} +> d in 
                                {label = tagR v , 
                                 rest = abstr' M} 
                            end
		       | % query q => 
                            split q as {arg=a, resume=R} +> d in 
				{label = tagL a ,
				 rest = FF (oncefn h:int =>  
					    abstr'' (oncefn b:branching =>
                                                split R $ {label= detagL h,
                                                           rest = (FF b)}
                                                as {l=l, r=r} +> d
                                                in {label=l, rest=r}
                                                end))}
	                    end 
		    end }
	  end
    as {fst=abstr', snd=abstr''} +> rest
    in
       oncefn f : forest -o forest =>
	  abstr' (oncefn b : branching => f $ (FF b))
    end ;

(* Hurrah!! This now typechecks...                        *) 
(* val abstract : ((forest -o forest) -o forest) (none)   *)

(* Application operation to be added (easy). *)


(* The retraction !forest <| forest *)

(* A simple "counter" class *)

type intRW = {read : {}->{i:int}**'@r, write : {i:int}**'@r->{}} ;
type CounterType = {next : {}->int} ;
val seq = fn x:{} => fn y:int => y ;
val suc = fn x:int => x ;   (* want _intSuc here *)

val CounterImpl = extend triv with
    oncefn super : intRW -> {} =>
    oncefn self  : intRW -> CounterType =>
    fn rw : intRW =>
        split rw as {read=read, write=write} +> d in
        {next = fn u:{} => 
                let val w:{} = write (read{} +> {i=suc(read{}.i)})
                in read{}.i end}
                (* Not the natural way to write it (three reads!).  *)
                (* Want a more generous "let rule" for writesafety. *)
                (* Perhaps just desugar lets as split expressions?  *)
        end ,
    oncefn u:{} => {superarg={}, extender = oncefn v:{} => {i=0}}
end ;

(* The following need some arithmetic *)
val indexTag = fn i:int => fn j:int => i ;
val indexOf = fn i:int => i ;
val mainOf  = fn i:int => i ;
val stripIndex = fn i:int => fn j:int => i ;  


type univ' = ! (int -o int) ; 

val makeBangedForest =
    fn U:univ' =>
       let val count:CounterType = constr CounterImpl $ {} in
       let val component : int->forest =
           rec component : int->forest =>
               fn i:int => fold forest
                   (oncefn m:int =>
                       let val c:int = count.next{} in
                           {label = stripIndex (U (indexTag m i)) c ,
                            rest = component c}
                       end) 
       in prom (FF (oncefn m:int => (UF (component 0) $ m))) 
               (* thunking needed to make a promotable value *)
       end end ;

val bangProject = fn f:forest =>
    makeBangedForest (forestToUniv f . m) ;


(* Embedding !forest in forest, using catchcopy. *)

(* Is catchcopy equivalent to general promotion? *)

val force = fn e : {} -> {value:int, residue:forest} =>
    (* representative of a general type with ground and groundless parts *)
    case catchcopy test:int->{} => 
            split e{} as {value=n, residue=f} +> d in
                 {value = test n, residue = f}
            end
    of %query q =>
            split q as {arg=n, resume=R} +> d in
                {value = n,
                 residue = prom (fold forest (oncefn m:int =>
                     UF (der R $ {} $ (rec test:int->{} => test).r) $ m))}
            end
     | %result r => {value=0, residue=rec ff:!forest => ff}  (* not used *)
    end ;
(* N.B. The evaluation of e{} only happens once; the result is memoized. *)
(* The thunked application of der R may happen multiple times, but this  *)
(* doesn't do any "real work".                                           *)

type ValueType = [value:int, arg:int] ;
val Rvalue = fn v:int => %value v :: ValueType ;
val Qarg   = fn a:int => %arg a   :: ValueType ;

type ResidueType = [more: (int->tree) -o forest, 
                    resume: tree -o (int->tree) -o {l:int, r:forest}] ;
val Rmore = 
    fn M:(int->tree)-o forest => 
        %more M :: ResidueType ;
val Qresume = 
    fn R:tree-o(int->tree)-o {l:int, r:forest} => 
	%resume R :: ResidueType ;

type VR  = {value:ValueType, residue:ResidueType} ;
type VR' = {value:ValueType, residue:!ResidueType} ;

val force1 = rec f:({}->VR)->VR' => f ;
(* can be defined analogously to force above *)

val catchcopyImpl =
    fn body : (int->tree) -> {value:int, residue:forest} =>
            force1 (fn t:{} =>
                case catchcont test : int->tree => body test of
                    % result r =>
                        split r as {value=v, more=M} +> d in
                            {value = Rvalue v, residue = Rmore M}
                        end
                  | % query q =>
                        split q as {arg=a, resume=R} +> d in
                            {value = Qarg a, residue = Qresume R}
                        end
                end) ;
    (* Boring repackaging omitted *)

(* Hmmm, can we get from !(A+B) to !A+!B ? Yes. *)

(* So indeed, catchcopy is equivalent to force, which is itself *)
(* tantamount to allowing promotion of non-values.              *)
(* (Of these, force might make the best language primitive.)    *)


(*
(* Old: *)

val infiltrate = 
    rec infiltrate : !forest -> TestType -> !forest =>
        fn f : !forest => fn test : TestType =>
            prom (FF (oncefn m:int =>
                let val node : !tree = prom (UF (der f) $ m) in
                let val n : int = (der node).label in
                let val f' : !forest = 
                    prom (fold forest (oncefn m:int => 
	                UF((der node).rest) $ m)) in
                let val t : {} = test n in
                    {label = n, rest = infiltrate f' test}
                end end end end)) ;

(* The value restriction on promotions was proving painful here. *)
*)

val copyApply = 
    fn f:!forest => fn m:int => 
       force (fn u:{} => 
           split (UF (der f) $ m) as {label=n, rest=f'} +> d
           in {value=n, residue=f'}
           end) ;

(* Now just a bit of functional programming to finish things off: *)

val intSuc  = fn i:int => i ;
val intLess = fn i:int => fn j:int => true ;

val extract = rec extract : (int->!forest)->int->forest =>
    fn subforests : int->!forest => fn nextIndex : int =>
        fold forest (oncefn m:int =>
	    if intLess (indexOf m) nextIndex then
               split copyApply (subforests (indexOf m)) (mainOf m) 
                   as {value=n, residue=G} +> d
               in {label = indexTag n nextIndex,
                   rest  = extract
                             (fn i:int => if i=nextIndex then G 
                                          else subforests i)
                             (intSuc nextIndex)}
               end
            else {label=0, rest = der (subforests 0)}) ;
(* Suspected typechecker bug: Doesn't allow rest = rec f:forest=>f. 
   Seems to treat f as a *free* variable: being non-reusable, 
   blocks promotion. *)

val bangEmbed = fn F:!forest => extract (fn i:int => F) 1 ;


(* Now, think about the semantics of "local state snapback". 
   It seems fairly clear that catchcont's resume operations should
   restore local state, and that this makes the retractions for
   -o and ! work well together.

   What's more confusing is the treatment of local state in
   the *implicit* backtracking performed by "thread".
   The idea of "saving some context" whenever we do a "write"
   seems a bit bizarre, and a bit worrying.
*)


(* Extracting the approximation operator from a class implementation. *)
(* Some dummy types, and others derived from them. *)

(* First an "old" version, for method implementation types with RW operations
   "on the outside": *)

(* Type machinery for a sample classimpl type *)

type unit      = {} ;
type arbitrary = int -o int ;
type reusable  = int -> int ;

type arg      = [arg    : arbitrary] ;
type return   = [return : arbitrary] ;
type obj      = {m : ! (arg -o return)} ;
type state    = {field  : reusable} ;     (* must be reusable *)
type conarg   = [conarg : arbitrary] ;
type c_impl   = classimpl state,obj,conarg end ;

(* Type machinery for "approx" extraction *)

type obj'     = {m : arg -> return,
                 m': arg -> return} ;

type basicRW  = {read   : unit->reusable,
                 write  : reusable->unit} ;
type stateRW  = {fieldRW: basicRW} ;
type state'   = {field  : reusable , rwStore : stateRW} ;
type RW_RW    = {read   : unit->stateRW,
                 write  : stateRW->unit} ;
type state'RW = {fieldRW : basicRW , rwStoreRW : RW_RW} ;

type tau_c     = stateRW -> obj ;  (* reusable *)
type tau_super = state'RW -> obj ;
type tau_c'    = state'RW -> obj' ;

type conarg'  = stateRW ;
type c'_impl  = classimpl state',obj',conarg' end ;

(* Type machinery for "init" extraction *)

type obj''    = {m : arg -> return,
                 get_field : unit -> reusable} ;
type tau_c''  = stateRW -> obj'' ;
type c''_impl = classimpl state,obj'',conarg end ;

(* Now the extraction code itself *)

type c_rep    = {approx : tau_c -> tau_c, 
                 init   : conarg -> state} ;   

val dummyConarg = prom (%conarg (oncefn x:int=>x)) ;

val implToRep =
    fn c : c_impl => {
        approx = fn selfimpl : tau_c =>
                   (* must somehow coerce this to be argsafe *)
           let val c' : c'_impl = 
               extend c with
                   (* method impl *)
                   fn super : tau_super => 
                   fn self  : tau_c' =>
                   fn state'rw : state'RW => 
                       let val var_rw:stateRW = state'rw.rwStoreRW.read {}
	               in {m = (selfimpl {fieldRW=state'rw.fieldRW}).m , 
                           m' = (super {fieldRW = var_rw.fieldRW,
                                        rwStoreRW = state'rw.rwStoreRW})
                       (* we should be allowed (state'rw +> var_rw) here *)
                                .m}
                       end ,
                   (* constructor impl *)
                   fn var_rw:conarg' => 
                        {superarg = der dummyConarg,
                             (* Intriguingly, initialization of       *)
                             (* superclass fields is irrelevant here! *)
                         extender = oncefn s:state =>
                                    {field=s.field, rwStore=var_rw}}
               end
           in 
               fn var_rw:stateRW =>
                   let val testObj:obj' = constr c' $ var_rw 
                   in {m = testObj.m'}
                   end
           end ,
        init = let val c'' : c''_impl =
                   extend c with
                       (* method impl *)
                       fn super : tau_c => fn self : tau_c'' =>
                       fn state_rw:stateRW =>
                           {m = (super state_rw).m ,
                            get_field = state_rw.fieldRW.read} ,
                       (* constructor impl *)
                       fn a:conarg => 
			    {superarg = a, extender = oncefn s:state=>s}
                   end
               in 
                   fn a:conarg => (constr c'' $ a).get_field {}
               end 
        } ;

(* 
Simplified version for typechecking in current implementation:

val implToRep =
    fn c : c_impl => {
        approx = fn selfimpl : tau_c =>
                    (* must somehow coerce this to be argsafe *)
           let val c' : c'_impl = rec c':c'_impl => c'
           in 
               fn var_rw:stateRW =>
                   let val testObj:obj' = constr c' $ var_rw 
                   in {m = testObj.m'}
                   end
           end ,
        init = let val c'' : c''_impl = rec c'':c''_impl => c''
               in 
                   fn a:conarg => (constr c'' $ a).get_field {}
               end 
        } ;

Method and constructor impls also typechecked separately.
*)

(* Should also add the other half "repToImpl" *)
(* (easier in the absence of polymorphism!)   *)


(* Second version, for revised definition of $\tau \natural \sigma$.
   Read/write operations supplied once per method invocation, rather than
   once per object instantiation. *)

(* Type machinery for a sample classimpl type: as above *)

(* Type machinery for "approx" extraction *)

type basicRW  = {read   : unit->reusable,
                 write  : reusable->unit} ;
type stateRW  = {fieldRW: basicRW} ;
type argRW = {arg:arg, rw:stateRW} ;

type obj'   = {m : ! (arg -o return) ,
               m': ! (argRW -o return)} ;

type tau_c  = {m : ! (stateRW -o arg -o return)} ;
type tau_c' = {m : ! (stateRW -o arg -o return),
               m': ! (stateRW -o arg -o return)} ;

type c'_impl = classimpl state,obj',conarg ;  (* replace conarg by unit? *)

(* Type machinery for "init" extraction: as above *)

type obj''    = {m : arg -> return,
                 get_field : unit -> reusable} ;
type tau_c''  = stateRW -> obj'' ;
type c''_impl = classimpl state,obj'',conarg end ;

(* Now the extraction code itself *)

type c_rep    = {approx : tau_c -> tau_c, 
                 init   : conarg -> state} ;   

val dummyConarg = prom (%conarg (oncefn x:int=>x)) ;

val implToRep =
    fn c : c_impl => {
        approx = fn selfimpl : tau_c =>  
           let val c' : c'_impl = 
               extend c with
                   (* method impl *)
                   fn super : tau_c => fn self : tau_c' =>
                      {m = selfimpl.m , 
                           (* argsafe coercion to be added *)
                       m'= prom (oncefn dummy_rw:stateRW => 
                                 oncefn {arg=x, rw=var_rw} :argRW =>
                                    super.m var_rw $ x)} ,
                   (* constructor impl *)
                   fn k:conarg =>
                      {superarg = k,   (* possibly irrelevant! *)
                       extender = oncefn s:state => s}
               end
               val testObj : obj' = constr c' $ dummyConarg
                   (* Problem: what if this diverges? *)
           in
               {m = prom (oncefn rw:stateRW => oncefn x:arg =>
                          testObj.m' {arg=x, rw=rw})}
           end ,
        init = let val c'' : c''_impl =
                   extend c with
                       (* method impl *)
                       fn super : tau_c => fn self : tau_c'' =>
                          {m = super.m ,
                           get_field = prom (oncefn rw:state_RW =>
                                             oncefn u:unit =>
                                             rw.fieldRW.read u)} ,
                       (* constructor impl *)
                       fn k:conarg => 
			   {superarg = k, extender = oncefn s:state=>s}
                    end
               in 
                   fn k:conarg => (constr c'' $ k).get_field {}
               end 
        } ;


(* The other way - easier *)

val repToImpl = fn R : c_rep =>
    extend triv with
       (* methods *)
       fn super : {} => fn self : tau_c => 
	   R.approx self  (* argsafe coercion to be added *) ,
       (* constructor *)
       fn k:conarg =>
           {superarg = {}, extender => 
            oncefn u:{} => R.init k}
    end ;


(* Now, just for a laugh, let's try to simplify 
        repToImpl (implToRep c)
   (ignoring argsafety issues).

let val c'' : c''_impl =
    extend c with
       (* method impl *)
       fn super : tau_c => fn self : tau_c'' =>
          {m = super.m ,
           get_field = prom (oncefn rw:state_RW =>
                             oncefn u:unit =>
                             rw.fieldRW.read u)} ,
       (* constructor impl *)
       fn k:conarg =>
          {superarg = k, extender = oncefn s:state=>s}
in
        extend triv with
           (* methods *)
           fn super : {} => fn self : tau_c => 
           let val c' : c'_impl = 
               extend c with
                   (* method impl *)
                   fn super : tau_c => fn self' : tau_c' =>
                      {m = self.m ,
                       m'= prom (oncefn dummy_rw:stateRW => 
                                 oncefn {arg=x, rw=var_rw} :argRW =>
                                    super.m var_rw $ x)} ,
                   (* constructor impl *)
                   fn k:conarg =>
                      {superarg = k,   (* possibly irrelevant! *)
                       extender = oncefn s:state => s}
               end
               val testObj : obj' = constr c' $ dummyConarg
           in
               {m = prom (oncefn rw:stateRW => oncefn x:arg =>
                          testObj.m' {arg=x, rw=rw})}
           end ,

           (* constructor *)
           fn k:conarg =>
               {superarg = {}, extender => 
                oncefn u:{} => (constr c'' k).get_field {}}
        end 
end ;


All looks very plausible ;>)
*)


(* The argsafe retraction, of type tau_c -> tau_c. *)
(* Strictly a syntactic context rather than a self-contained function *)

(* We give the necessary type declarations again for convenience *)

type unit      = {} ;
type arbitrary = int -o int ;
type reusable  = int -> int ;
type ground    = int ;

type state    = reusable ;  (* may assume groundless *)
type arg      = [arg    : arbitrary] ;
type return   = [return : ground] ;     (* for first attempt *)
type obj      = {m : ! (arg -o return)} ;

type basicRW  = {read   : unit->state,
                 write  : state->unit} ;
type stateRW  = {fieldRW: basicRW} ;
type tau_c    = {m : ! (stateRW -o arg -o return)} ;

type univ = !(int -o int) ;   (* omit {m:...} *)

type forestRep = {label:int, rest:forest} ;
val diverge = rec f:unit->forestRep => f ;

type implMove  = [| returnMove:int, argMove:int, readRequest:int, 
                    readResultMove:int, writeRequest:int |] ;


(* context makeArgsafe [impl : tau_c] = *)

    let val implScript = implToUniv impl
        (* An "imperative" script for the banged value "impl" 
           is created here where it is globally accessible. *)
    in  {m = prom (oncefn state_rw : stateRW =>
                   oncefn x : arg =>   (* the critical UNSAFE variable *)
             split state_rw.fieldRW as {read=read, write=write} in
                (* Body of this split now has to be WRITESAFE *)

             let val argScript = argToUniv x in
                (* Any state created by argToUniv should live onboard *)

             let val scriptPortion = rec scriptPortion : localAdmin->forest =>
                (* Extracts portion of implScript for value passed to "write" *)
                (* Crucially, no dependence here on argScript or x. *)
                fn la:localAdmin =>
                   fold forest (fn m =>
                      let val n' = implScript (encodeWriteMove la m) in
                         case decodeWriteMove la m n' of
                            %proper n => 
	                       {label=n, rest=scriptPortion (updateLA la m n)}
                          | %other {} => diverge {}
                               (* non-argsafe behaviour is expunged here *)
                         end
                      end)         
             in

             let val playScripts = rec playScripts : admin->int->retAdmin =>
                (* plays impl against arg, as far as next "return" move *)
                fn admin:admin => fn om:int =>

                case decodeImplMove (implScript om) of
                (* we'll omit some niceties concerning lifting moves etc. *)

                   %returnMove m => {return=m, admin=admin}

                 | %argMove m => playScripts admin (codeArgMove (argScript m))

                 | %readRequest i => 
                      let val newReadScript = bangStateToForest (force read)
                       (* the additional bang here allows us later to backtrack 
                          to any residue of any read result *)
                      in playScripts (addReadScript newReadScript i admin)
                                     (readAck i admin)
                      end

                 | %readResultMove m =>
                      split playReadResult m admin as
                         (* this has to select the appropriate bangState forest,
                            and then play the appropriate move against it *)
                         {move=m', admin=admin'}
                      in playScripts admin' (codeReadMove m')
                      end

                 | %writeRequest i => 
                      let val u = write (forestToState(scriptPortion(initLA i)))
                      in playScripts admin (*unchanged?*) (writeAck i admin)
                      end
                end
             in    

             let val returnScript = rec returnScript : admin->forest =>
                fn admin:admin =>
                fold forest (fn m:int => 
                   split playScripts admin (codeReturnMove m)
                   as {return=m', admin=admin'}
                   in {label=m', rest=returnScript admin'}
                   end
             in 
                univToReturn (returnScript trivAdmin) 
                (* Again, state created by univToReturn should live onboard *)
             end end end end end)}
    end ;

(* Requires the following programs, for which
   (dummy?) implementations should be supplied: 

(* Mappings to/from universal type: will depend on types involved *)
   implToUniv        : tau_c -> univ
   argToUniv         : arg -> univ
   bangStateToForest : !state -> forest
   forestToState     : forest -> state
   forestToReturn    : forest -> return

(* Coding/decoding for implScript moves *)
   decodeImplMove    : int -> implMove
   codeReturnMove    : int -> int
   codeArgMove       : int -> int
   codeReadMove      : int -> int

(* Bookkeeping for playScripts *)
   type admin = ?
   type retAdmin  = {return:int, admin:admin} ;
   trivAdmin
   addReadScript     : univ -> int -> admin -> admin
   readAck           : int -> admin -> int
   writeAck          : int -> admin -> int
   playReadResult    : int -> admin -> {move:int, admin:admin}

(* Bookkeeping for scriptPortion *)
   type localAdmin = ? 
   initLA            : int -> localAdmin
   encodeWriteMove   : localAdmin -> int -> int
   decodeWriteMove   : localAdmin -> int -> int -> [| proper:int, other:unit |]
   updateLA          : localAdmin -> int -> int -> localAdmin
*)


(* Now a similar bunch of stuff for linear classes *)

(* Type machinery for a sample linear classimpl type *)

type unit      = {} ;
type arbitrary = int -o int ;
type ground    = [ground : int] ;

type arg       = [arg    : ground] ;
type return    = [return : arbitrary] ;
type obj       = {m : ! (arg -o return)} ;
type state     = {field  : arbitrary} ;
type conarg    = [conarg : arbitrary] ;
type lin_c_impl  = linear classimpl state,obj,conarg end ;

(* Extraction stuff *)

type argstate    = {value:arg, state:state} ;
type returnstate = {value:return, state:state} ;
type unitstate   = {value:unit, state:state} ;
type statestate  = {value:state, state:state} ;
type lin_tau_c   = {m : ! (argstate -o returnstate)}
type obj'        = {m : ! (arg -o return),
                    m': ! (arg -o return),
                    read: !(unit -o state)} ;
type lin_c'_impl = linear classimpl state,obj',state end ;
type lin_tau_c'  = {m : ! (argstate -o returnstate),
                    m': ! (argstate -o returnstate),
                    read : ! (unitstate -o statestate)} ;

type obj''       = {m : ! (arg -o return), 
                    read : ! (unit -o state)} ;
type lin_c''_impl = linear classimpl state,obj'',conarg end ;
type lin_tau_c''  = {m : ! (argstate -o returnstate),
                     read : ! (unitstate -o statestate)} ;

type lin_c_rep   = {approx : lin_tau_c -> lin_tau_c,
                    init   : conarg -> state} ;

(* The easy direction first - almost identical to nonlinear case *)

val linRepToImpl = fn R : lin_c_rep =>
    extend linear triv with
       fn super : {} => fn self : lin_tau_c =>
           R.approx self  (* coercion to be added here *) ,
       fn k:conarg => {superarg = {}, extender => oncefn u:{} => R.init k}
    end ;

(* The extraction thing *)

val linImplToRep =
    fn c : lin_c_impl => {
       approx = fn selfimpl : lin_tau_c =>
          let val c' : c'_impl = 
             extend c with 
                (* method impl *)
                fn super : lin_tau_c => fn self : lin_tau_c' =>
                   {m = selfimpl.m ,  (* coercion to be added *)
                    m'= super.m ,     (* should eta-expand?   *)
                    read = fn {value=u:unit, state=s:state} =>
                              {value=s, state=dummyState} (* linear in s *)
                   } ,
                (* constructor impl *)
                fn s:state =>
                   {superarg = dummyConarg,  (* again, divergence issue! *)
                    extender = oncefn s':state => s}
             end
          in
             {m = fn {value=a:arg, state=s:state} =>
                  let val obj = new c' s in
                     {value = obj.m'(a), state=obj.read{}}
                  end}
             (* Or create a single test object with read/write methods *)
          end ,
       init = let val c'' : c''_impl = 
                 extend c with
                    fn super : lin_tau_c => fn self : lin_tau_c'' =>
                      {m = super.m,    (* eta-expand? *)
                       read = fn {value=u:unit, state=s:state} =>
                                 {value=s, state=dummyState} (* linear *)
                      } ,
                    fn k:conarg => {superarg = k, 
                                    extender = oncefn s:state=>s}
                 end
              in 
                 fn k:conarg => (new c'' k).read {}
              end
       } ;


(* Finally, the appropriate "metasafe retraction" for linear classes. 
   Ensures self/super methods are called serially. 
   Remarkably analogous to makeArgsafe above, although types are
   completely different. *)

type implMove = [| returnMove:int, stateMove:int,
                   selfCall:int, selfResultMove:int |] ;

(* context makeMetasafeLin [approx : lin_tau_c -> lin_tau_c] = *)

   let val implScript = implToUniv impl
   in  fn self : lin_tau_c =>
       {m = fn {value=x:arg, state=s:state} => 

            let val stateScript = stateToUniv (compPart state) in

            let val scriptPortion = rec scriptPortion:localAdmin->forest =>
                (* extracts portion of implScript for pair passed to self *)
                fn la:localAdmin =>
                   fold forest (fn m =>
                      let val n' = implScript (encodeSelfArgMove la m) in
                          case decodeSelfArgMove la m n' of
                             %selfArgMove n => 
                                {label=n, rest=scriptPortion (updateLA la m n)}
                           | %stateMove n => ...stateScript...  
                             (* bit of play needed - add stuff here *)
                             (* suggests how to extend makeArgsafe? *)
                           | %other {} => diverge {}
                             (* nested calls to self are expunged here *)
                      end)
            in

            let val playToRet = rec playToRet : admin->int->retAdmin =>
                (* plays impl against state, as far as return point *)
                fn admin:admin => fn om:int =>

                case decodeImplMove (implScript om) of
                (* again, omit lifting niceties *)

                   %returnMove m => {return=m, admin=admin}

                 | %stateMove m => playToRet admin (codeStateMove (stateScript m))

                 | %selfCall i => 
                       let val newSelfResult =
                          bangRetStateToForest (force (fn u:unit =>
                             self.m (forestToArgState (scriptPortion (initLA i)))))
                             (* need to legitimate this call to "self"! *)
                       in playToRet (addSelfResult newSelfResult i admin)
                                    (selfAck newSelfResult i admin)
                       end  
                       (* ground parts of arg/ret need more attention *)

                 | %selfResultMove m => 
                       split playSelfResult m admin as
                          {move=m', admin=admin'}
                       in playToRet admin' (codeSelfResultMove m')

                end
            in
            let val {return=r0, admin=admin0} = 
		playToRet trivAdmin (codeGroundInfo x s)
               (* dependence on "self" is finished by this point *)
            in
            let val playAfterRet = rec playAfterRet : admin->int->retAdmin =>
                (* plays as far as next return point *)
                fn admin:admin => fn om:int =>
                case decodeImplMove (implScript om) of
                   %returnMove m => {return=m, admin=admin}
                 | %stateMove m => playToRet admin (codeStateMove (stateScript m))
                 | %selfResultMove m => 
                       split playSelfResult m admin as
                          {move=m', admin=admin'}
                       in playToRet admin' (codeSelfResultMove m')
                 | %selfCall i => playAfterRet admin om (* diverge *)
                       (* delayed calls to self are expunged here *)
                end
            in
            let val returnScript = rec returnScript : admin->forest =>
                fn admin:admin =>
                fold forest (fn m:int => 
                   split playAfterRet admin (codeReturnMove m)
                   as {return=m', admin=admin'}
                   in {label=m', rest=returnScript admin'}
                   end
            in
               combineReturn r0 (univToReturn (returnScript admin0))
            end end end end end end}
   end ;


(* Requires the following programs:

   compPart

   implToUniv
   stateToUniv
   bangRetStateToForest
   forestToArgState

   decodeImplMove  : int -> implMove
   codeStateMove
   codeSelfResultMove
   codeReturnMove
   codeGroundInfo

   type admin = ?
   type retAdmin = {return:int, admin:admin} ;
   trivAdmin
   addSelfResult
   selfAck
   playSelfResult

   type localAdmin = ?
   initLA
   encodeSelfArgMove
   decodeSelfArgMove
   updateLA   
*)