src/Pure/envir.ML
author lcp
Tue, 18 Jan 1994 15:57:40 +0100
changeset 230 ec8a2b6aa8a7
parent 0 a5a9c433f639
child 247 bc10568855ee
permissions -rw-r--r--
Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	envir
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1988  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
(*Environments
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
  Should take account that typ is part of variable name,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
    otherwise two variables with same name and different types
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
    will cause errors!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
signature ENVIR = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  type 'a xolist
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  exception ENVIR of string * indexname;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  datatype env = Envir of {asol: term xolist,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
			   iTs: (indexname * typ) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
			   maxidx: int}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val alist_of : env -> (indexname * term) list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val alist_of_olist : 'a xolist -> (indexname * 'a) list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val empty : int->env
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val genvar  : string -> env * typ -> env * term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val genvars : string -> env * typ list -> env * term list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val lookup : env * indexname -> term option
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val norm_term : env -> term -> term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val null_olist : 'a xolist
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val olist_of_alist: (indexname * 'a) list -> 'a xolist
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val update : (indexname * term) * env -> env
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val vupdate : (indexname * term) * env -> env
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
functor EnvirFun () : ENVIR = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(*association lists with keys in ascending order, no repeated keys*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
datatype 'a xolist = Olist of (indexname * 'a) list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
exception ENVIR of string * indexname;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*look up key in ordered list*)  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
fun xsearch (Olist[], key) = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  | xsearch (Olist ((keyi,xi)::pairs), key) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
      if xless(keyi,key) then xsearch (Olist pairs, key)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
      else if key=keyi then Some xi  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
      else None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
(*insert pair in ordered list, reject if key already present*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun xinsert_new (newpr as (key, x), Olist al) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  let fun insert [] = [newpr]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
	| insert ((pair as (keyi,xi)) :: pairs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
	    if xless(keyi,key) then pair :: insert pairs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
	    else if key=keyi then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
		raise ENVIR("xinsert_new: already present",key)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
	    else newpr::pair::pairs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  in  Olist (insert al)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*insert pair in ordered list, overwrite if key already present*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
fun xinsert (newpr as (key, x), Olist al) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  let fun insert [] = [newpr]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
	| insert ((pair as (keyi,xi)) :: pairs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
	    if xless(keyi,key) then pair :: insert pairs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
	    else if key=keyi then newpr::pairs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
	    else newpr::pair::pairs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  in  Olist (insert al)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(*apply function to the contents part of each pair*)   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
fun xmap f (Olist pairs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  let fun xmp [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
	| xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  in Olist (xmp pairs)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(*allows redefinition of a key by "join"ing the contents parts*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
fun xmerge_olists join (Olist pairsa, Olist pairsb) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  let fun xmrg ([],pairsb) = pairsb
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
	| xmrg (pairsa,[]) = pairsa
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
	| xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
	    if xless(keya,keyb) then 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
		(keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
	    else if xless(keyb,keya) then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
		(keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
	    else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  in  Olist (xmrg (pairsa,pairsb))  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val null_olist = Olist[];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
fun alist_of_olist (Olist pairs) = pairs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
fun olist_of_alist pairs = foldr xinsert (pairs, Olist[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
(*updating can destroy environment in 2 ways!!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
   (1) variables out of range   (2) circular assignments
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
datatype env = Envir of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    {maxidx: int, 		(*maximum index of vars*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
     asol: term xolist,  	(*table of assignments to Vars*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
     iTs: (indexname*typ)list}	(*table of assignments to TVars*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
(*Generate a list of distinct variables.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  Increments index to make them distinct from ALL present variables. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
  let fun genvs (_, [] : typ list) : term list = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
        | genvs (n, T::Ts) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
            Var((name ^ radixstring(26,"a",n), maxidx+1), T) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
            :: genvs(n+1,Ts) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(*Generate a variable.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
fun genvar name (env,T) : env * term =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
  let val (env',[v]) = genvars name (env,[T])  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
  in  (env',v)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
fun update ((xname, t), Envir{maxidx, asol, iTs}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
  Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*The empty environment.  New variables will start with the given index.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
fun vupdate((a,t), env) = case t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
      Var(name',T) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
	if a=name' then env	(*cycle!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
	else if xless(a, name')  then  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
	   (case lookup(env,name') of  (*if already assigned, chase*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
		None => update((name', Var(a,T)), env)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
	      | Some u => vupdate((a,u), env))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
	else update((a,t), env)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
    | _ => update((a,t), env);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
(*Convert environment to alist*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
(*Beta normal form for terms (not eta normal form). 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
  Chases variables in env;  Does not exploit sharing of variable bindings
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  Does not check types, so could loop. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
local 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
      (*raised when norm has no effect on a term, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
        to encourage sharing instead of copying*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
  exception SAME;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
  fun norm_term1 (asol,t) : term =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
    let fun norm (Var (w,T)) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
	      (case xsearch(asol,w) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
		  Some u => normh u
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
		| None   => raise SAME)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
	  | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
	  | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
	  | norm (f $ t) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
	      ((case norm f of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
		 Abs(_,_,body) => normh(subst_bounds([t], body))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
	       | nf => nf $ normh t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
	      handle SAME => f $ norm t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
	  | norm _ =  raise SAME
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
	and normh t = (norm t) handle SAME => t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
    in normh t end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
  and norm_term2(asol,iTs,t) : term =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
    let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
	  | normT(TFree _) = raise SAME
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
	  | normT(TVar(v,_)) = (case assoc(iTs,v) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
		  Some(U) => normTh U
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
		| None => raise SAME)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
	and normTh T = ((normT T) handle SAME => T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
	and normTs([]) = raise SAME
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
	  | normTs(T::Ts) = ((normT T :: normTsh Ts)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
			     handle SAME => T :: normTs Ts)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
	and normTsh Ts = ((normTs Ts) handle SAME => Ts)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
	and norm(Const(a,T)) = Const(a, normT T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
	  | norm(Free(a,T)) = Free(a, normT T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
	  | norm(Var (w,T)) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
	      (case xsearch(asol,w) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
		  Some u => normh u
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
		| None   => Var(w,normT T))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
	  | norm(Abs(a,T,body)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
		(Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
	  | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
	  | norm(f $ t) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
	      ((case norm f of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
		 Abs(_,_,body) => normh(subst_bounds([t], body))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
	       | nf => nf $ normh t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
	      handle SAME => f $ norm t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
	  | norm _ =  raise SAME
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
	and normh t = (norm t) handle SAME => t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
    in normh t end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
(*curried version might be slower in recursive calls*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
fun norm_term (env as Envir{asol,iTs,...}) t : term =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
	if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207