Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Diff of /sml/branches/primop-branch-2/src/compiler/FLINT/kernel/lty.sml
ViewVC logotype

Diff of /sml/branches/primop-branch-2/src/compiler/FLINT/kernel/lty.sml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2020, Thu Aug 17 19:54:34 2006 UTC revision 2021, Thu Aug 17 20:36:49 2006 UTC
# Line 146  Line 146 
146                             * and SEQ[(PROJ(VOID, i))]. (ZHONG)                             * and SEQ[(PROJ(VOID, i))]. (ZHONG)
147                             *)                             *)
148    
 (* tycEnvElem: the tyc list is the set of arguments bound at an application,  
  * if the tycEnv element was the result of a lazy beta-reduction (SOME case),  
  * or NONE if the tycEnv element is the result of pushing a suspended subst  
  * through a lambda abstraction. The int is the original lambda depth of the  
  * arguments (SOME case) or of the lambda abstraction.  
  *)  
 type tycEnvElem = (tyc list option * int)  
   
149  (** definitions of lambda types *)  (** definitions of lambda types *)
150  datatype ltyI  datatype ltyI
151    = LT_TYC of tyc                              (* monomorphic type *)    = LT_TYC of tyc                              (* monomorphic type *)
# Line 477  Line 469 
469   *            UTILITY FUNCTIONS ON TYC ENVIRONMENT                         *   *            UTILITY FUNCTIONS ON TYC ENVIRONMENT                         *
470   ***************************************************************************)   ***************************************************************************)
471    
472  (* virtual tycEnv datatype  (* tycEnvs are represented by an encoding as tycs. The abstract representation
473   *   datatype tycEnv   * of tycEnvs would be given by:
474   *     = Empty   *
475   *     | B of tkind list * tyc list   *   datatype teBinder
476   *     | L of tkind list * int * tycEnv   *     = Beta of int * tyc list * tkind list
477     *     | Lamb of int * tkind list
478     *
479     *   type tycEnv = teBinder list
480     *
481     * Invariant: a tycEnv cannot terminate with a Lamb, i.e. the last binder
482     *   in a tycEnv must be a Beta. tycEnvs are created when a closure is created
483     *   when reducing a beta-redex (rule r1), and they are always initially of
484     *   of the form Beta(0,args,ks)::nil.
485   *)   *)
486    
487  (** utility functions for manipulating the tycEnv **)  datatype teBinder
488      = Beta of int * tyc list * tkind list
489  val emptyTycEnv : tycEnv = tc_injX(TC_SUM[])        (* Beta(j,args,ks):
490             created when reducing a beta redex (r1);
491  fun bindTycEnv (ks: tkind list, tycs : tyc list): tycEnv =           j: the embedding level of the original redex -- 0 if the redex was
492        tc_injX(TC_FN(ks,TC_SEQ tycs))              created by r1, or the nesting level of the new closure if by r12;
493             args: the tycs bound by the n-ary beta reduction, i.e. the arguments;
494  fun lamTycEnv (ks: tkind list, j: int, tenv: tycEnv) : tycEnv =           ks: the operator domain kinds *)
495        tc_injX(TC_PROJ(TC_FN(ks,tenv),j))    | Lamb of int * tkind list
496          (* Lamb(j,ks):
497             created when pushing a closure (Env) through a lambda (r10);
498             j: the nesting level of the closure just before r10 is applied,
499                i.e. the nesteing level of the abstraction relative to the
500                point where the closure was originally created;
501             ks: the kinds of the abstraction parameters *)
502    
503    val teEmpty : tycEnv = tc_injX(TC_SUM[])
504    
505    (** utility functions for manipulating tycEnvs and teBinders **)
506    
507    (* encoding teBinders as tycs:
508     * Beta(j,args,ks) <=> TC_FN(ks,TC_PROJ(TC_SEQ args, j))
509     * Lamb(j,ks) <=> TC_PROJ(TC_FN(ks,TC_SUM[]), j)
510     *)
511    fun teEncodeBinder (Beta(j,args,ks)) : tyc =
512          tc_injX(TC_FN(ks,tc_injX(TC_PROJ(tc_injX(TC_SEQ args), j))))
513      | teEncodeBinder (Lamb(j,ks)) =
514          tc_injX(TC_PROJ(tc_injX(TC_FN(ks,tc_injX(TC_SUM[])), j)))
515    
516    fun teDecodeBinder (tyc : tyc) : teBinder =
517        case tc_outX(tyc)
518         of TC_FN(ks,tyc') =>
519              (case tc_outX tyc'
520                 of TC_PROJ(tyc'',j) =>
521                      (case tc_outX tyc''
522                         of TC_SEQ(args) => Beta(j,args,ks)
523                          | bug "teDecodeBinder")
524                  | _ => bug "teDecodeBinder")
525          | TC_PROJ(tyc',j) =>
526              (case tc_outX tyc'
527                 of TC_FN(ks,_) => Lamb(j, ks)
528                  | _ => bug "teDecodeBinder")
529          | _ => bug "teDecodeBinder"
530    
531    fun teCons (b: teBinder, tenv: tycEnv) : tycEnv =
532        tc_injX(TC_PARROW(b,tenv))
533    
534    fun teDest (tenv: tycEnv) : (teBinder * tycEnv) option =
535        case tc_outX tenv
536         of TC_PARROW(b,tenv) => SOME(teDecodeBinder b, tenv)
537          | TC_SUM [] => NONE
538          | _ => bug "teDest"
539    
540  (* TycEnvUnbound -- raised when first element of a deBruijn index is  (* TeUnbound -- raised when first element of a deBruijn index is
541   * out of bounds *)   * out of bounds *)
542  exception UnboundTycEnv  exception TeUnbound
543    
544  datatype tycEnvElem  (* 1-based index lookup: assume i >= 1 *)
545    = B of tkind list * tyc list  fun teLookup(tenv : tycEnv, i: int) : teBinder option =
546    | L of tkind list * int        (case teDest tenv
547            of SOME(binder, tenv') =>
548  (* 1-based index lookup *)               if i > 1 then teLookup(tenv',i-1)
549  fun lookupTycEnv(tenv : tycEnv, i) : tycEnvElem =               else if i = 1 then SOME binder
     if i > 1 then  
       (case tc_outX tenv  
         of TC_PROJ(TC_FN(_,tenv),_) => lookupTycEnv(tenv,i-1)  (* L *)  
          | TC_SUM _ | TC_PROJ _ => raise UnboundTycEnv         (* Empty or B *)  
          | _ => bug "unexpected tycEnv in tycEnvLookup")  
     else if i = 1 then  
       (case tc_outX tenv  
         of TC_FN(ks,TC_SEQ(tycs)) => B(ks,tycs)   (* Bind *)  
          | TC_PROJ(TC_FN(ks,_,),j) => L(ks,j)     (* Lam *)  
          | TC_SUM _ => raise UnboundTycEnv        (* Empty *)  
          | _ => bug "unexpected tycEnv in tycEnvLookup")  
550      else bug "index 0 in tycEnvLookup"      else bug "index 0 in tycEnvLookup"
551             | NONE => NONE
 datatype tycEnvComp  
   = TEempty  
   | TEbind of tkind list * tyc list  
   | TElam of tkind list * int * tycEnv  
   
 fun splitTycEnv(tenv : tycEnv) : tycEnvComp =  
     (case tc_outX tenv  
       of TC_FN(ks,TC_SEQ(tycs)) => TEbind(ks,tycs)   (* B *)  
        | TC_PROJ(TC_FN(ks,tenv,),j) => TElam(ks,j,tenv)     (* L *)  
        | TC_SUM _ => TEempty)  
552    
553    
554  (***************************************************************************  (***************************************************************************
# Line 568  Line 590 
590      in Option.map h (tc_vs tyc)      in Option.map h (tc_vs tyc)
591      end      end
592    
593    
594  (** testing the "pointer" equality on normalized tkind, tyc, and lty *)  (** testing the "pointer" equality on normalized tkind, tyc, and lty *)
595  fun tk_eq (x: tkind, y) = (x = y)  fun tk_eq (x: tkind, y) = (x = y)
596  fun tc_eq (x: tyc, y) = (x = y)  fun tc_eq (x: tyc, y) = (x = y)
597  fun lt_eq (x: lty, y) = (x = y)  fun lt_eq (x: lty, y) = (x = y)
598    
599    
600  (** utility functions for updating tycs and ltys *)  (** utility functions for updating tycs and ltys *)
601  fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =  fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =
602        (tgt := (i, TC_IND (nt, old), AX_NO))        (tgt := (i, TC_IND (nt, old), AX_NO))
# Line 586  Line 610 
610        (tgt := (i, LT_IND (nt, old), x))        (tgt := (i, LT_IND (nt, old), x))
611    | lty_upd _ = bug "unexpected lty_upd on already normalized lty"    | lty_upd _ = bug "unexpected lty_upd on already normalized lty"
612    
613    
614  end (* structure Lty *)  end (* structure Lty *)

Legend:
Removed from v.2020  
changed lines
  Added in v.2021

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0