source: src/joint/Joint_paolo.ma @ 2155

Last change on this file since 2155 was 2155, checked in by tranquil, 8 years ago

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File size: 19.7 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "common/Graphs.ma".
6include "utilities/lists.ma".
7include "common/LabelledObjects.ma".
8include "ASM/Util.ma".
9include "common/StructuredTraces.ma".
10
11(* Here is the structure of parameter records (downward edges are coercions,
12   the ↓ edges are the only explicitly defined coercions). lin_params and
13   graph_params are simple wrappers of unserialized_params, and the coercions
14   from them to params instantiate the missing bits with values for linarized
15   programs and graph programs respectively.
16
17        lin_params      graph_params
18              |   \_____ /____   |
19              |         /     \  |
20              |        /      ↓  ↓
21              |       |      params
22              |       |        |
23              |       |   stmt_params
24              |       |    /   
25          unserialized_params             
26            |            \       
27            |             \     
28            |         local_params
29            |              |   
30    step_params       funct_params
31
32step_params : types needed to define steps (stmts with a default fallthrough)
33stmt_params : adds successor type needed to define statements
34funct_params : types of result register and parameters of function
35local_params : adds types of local registers
36params : adds type of code and related properties *)
37
38inductive possible_flows : Type[0] ≝
39| Labels : list label → possible_flows
40| Call : possible_flows.
41
42record step_params : Type[1] ≝
43 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
44 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
45 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
46 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
47 ; dpl_reg: Type[0]   (* low address registers *)
48 ; dph_reg: Type[0]   (* high address registers *)
49 ; dpl_arg: Type[0]   (* low address registers *)
50 ; dph_arg: Type[0]   (* high address registers *)
51 ; snd_arg : Type[0]  (* second argument of binary op *)
52 ; pair_move: Type[0] (* argument of move instructions *)
53 ; call_args: Type[0] (* arguments of function calls *)
54 ; call_dest: Type[0] (* possible destination of function computation *)
55 (* other instructions not fitting in the general framework *)
56 ; ext_seq : Type[0]
57(* ; ext_branch : Type[0]
58 ; ext_branch_labels : ext_branch → list label*)
59 ; ext_call : Type[0]
60 ; ext_tailcall : Type[0]
61 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
62 }.
63
64inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
65  | COMMENT: String → joint_seq p globals
66  | COST_LABEL: costlabel → joint_seq p globals
67  | MOVE: pair_move p → joint_seq p globals
68  | POP: acc_a_reg p → joint_seq p globals
69  | PUSH: acc_a_arg p → joint_seq p globals
70  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
71  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
72  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
73  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
74  (* int done with generic move *)
75(*| INT: generic_reg p → Byte → joint_seq p globals *)
76  | CLEAR_CARRY: joint_seq p globals
77  | SET_CARRY: joint_seq p globals
78  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
79  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
80  | extension_seq : ext_seq p → joint_seq p globals.
81
82axiom EmptyString : String.
83definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
84
85notation "r ← a1 .op. a2" with precedence 60 for
86  @{'op2 $op $r $a1 $a2}.
87notation "r ← . op . a" with precedence 60 for
88  @{'op1 $op $r $a}.
89notation "r ← a" with precedence 60 for
90  @{'mov $r $a}. (* to be set in individual languages *)
91notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
92  @{'opaccs $op $r $s $a1 $a2}.
93
94interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
95interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
96interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
97
98coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
99  extension_seq on _s : ext_seq ? to joint_seq ??.
100
101inductive joint_call (p : step_params) : Type[0] ≝
102  | CALL_ID: ident → call_args p → call_dest p → joint_call p
103  | extension_call : ext_call p → joint_call p.
104
105coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
106  extension_call on _s : ext_call ? to joint_call ?.
107 
108inductive joint_branch (p : step_params) : Type[0] ≝
109  | COND: acc_a_reg p → label → joint_branch p
110  (*| extension_branch : ext_branch p → joint_branch p*).
111
112(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
113  extension_branch on _s : ext_branch ? to joint_branch ?.*)
114
115inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
116  | step_seq : joint_seq p globals → joint_step p globals
117  | step_call : joint_call p → joint_step p globals
118  | step_branch : joint_branch p → joint_step p globals.
119
120coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
121  step_seq on _s : joint_seq ?? to joint_step ??.
122coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
123  step_call on _s : joint_call ? to joint_step ??.
124coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
125  step_branch on _s : joint_branch ? to joint_step ??.
126
127definition step_flows ≝ λp,globals.λs : joint_step p globals.
128  match s with
129  [ step_seq _ ⇒ Labels … [ ]
130  | step_call _ ⇒ Call
131  | step_branch s ⇒
132    match s with
133    [ COND _ l ⇒ Labels … [l]
134    (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
135    ]
136  ].
137
138definition step_labels ≝
139  λp, globals.λs : joint_step p globals.
140    match step_flows … s with
141    [ Labels lbls ⇒ lbls
142    | Call ⇒ [ ]
143    ].
144
145definition step_forall_labels : ∀p : step_params.∀globals.
146    (label → Prop) → joint_step p globals → Prop ≝
147λp,g,P,inst. All … P (step_labels … inst).
148
149definition step_classifier :
150  ∀p : step_params.∀globals.
151    joint_step p globals → status_class ≝ λp,g,s.
152  match s with
153  [ step_seq _ ⇒ cl_other
154  | step_call _ ⇒ cl_call
155  | step_branch _ ⇒ cl_jump
156  ].
157
158record funct_params : Type[1] ≝
159  { resultT : Type[0]
160  ; paramsT : Type[0]
161  }.
162 
163record local_params : Type[1] ≝
164 { funct_pars :> funct_params
165 ; localsT: Type[0]
166 }.
167
168record unserialized_params : Type[1] ≝
169 { u_inst_pars :> step_params
170 ; u_local_pars :> local_params
171 }.
172
173record stmt_params : Type[1] ≝
174  { uns_pars :> unserialized_params
175  ; succ : Type[0]
176  ; succ_label : succ → option label
177  }.
178
179inductive joint_fin_step (p: step_params): Type[0] ≝
180  | GOTO: label → joint_fin_step p
181  | RETURN: joint_fin_step p
182  | tailcall : ext_tailcall p → joint_fin_step p.
183
184definition fin_step_flows ≝ λp.λs : joint_fin_step p.
185  match s with
186  [ GOTO l ⇒ Labels … [l]
187  | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *)
188  ].
189
190definition fin_step_labels ≝
191  λp.λs : joint_fin_step p.
192    match fin_step_flows … s with
193    [ Labels lbls ⇒ lbls
194    | Call ⇒ [ ]
195    ].
196
197definition fin_step_classifier :
198  ∀p : stmt_params.
199    joint_fin_step p → status_class
200  ≝ λp,s.
201  match s with
202  [ GOTO _ ⇒ cl_other
203  | _ ⇒ cl_return
204  ].
205
206inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
207  | sequential: joint_step p globals → succ p → joint_statement p globals
208  | final: joint_fin_step p → joint_statement p globals.
209
210definition stmt_classifier :
211  ∀p : stmt_params.∀globals.
212    joint_statement p globals → status_class
213  ≝ λp,g,s.
214  match s with
215  [ sequential stp _ ⇒ step_classifier p g stp
216  | final stp ⇒ fin_step_classifier p stp
217  ].
218
219coercion extension_fin_to_fin_step : ∀p : stmt_params.
220  ∀s : ext_tailcall p.joint_fin_step p ≝
221  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
222
223coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
224  ∀s : joint_fin_step p.joint_statement p globals ≝
225  final on _s : joint_fin_step ? to joint_statement ??.
226
227record params : Type[1] ≝
228 { stmt_pars :> stmt_params
229 ; codeT: list ident → Type[0]
230 ; code_point : Type[0]
231 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
232 ; point_of_label : ∀globals.codeT globals → label → option code_point
233 ; point_of_succ : code_point → succ stmt_pars → code_point
234 }.
235
236definition code_has_point ≝
237  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
238
239interpretation "code membership" 'mem p c = (code_has_point ?? c p).
240
241definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
242unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
243
244definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
245  match pt with
246  [ mk_Sig pt' pt_prf ⇒
247    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
248    [ Some x ⇒ λ_.x
249    | None ⇒ λabs.⊥
250    ] (refl …)
251  ]. normalize in pt_prf;
252    >abs in pt_prf; // qed.
253
254definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
255  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
256
257definition forall_statements_i :
258  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
259    codeT p globals → Prop  ≝
260  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
261
262lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
263#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
264
265lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
266  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
267#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
268
269definition code_has_label ≝ λp,globals,c,l.
270  match point_of_label p globals c l with
271  [ Some pt ⇒ code_has_point … c pt
272  | None ⇒ false
273  ].
274
275definition stmt_explicit_labels :
276  ∀p,globals.
277  joint_statement p globals → list label ≝
278  λp,globals,stmt. match stmt with
279  [ sequential c _ ⇒ step_labels … c
280  | final c ⇒ fin_step_labels … c
281  ].
282
283definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
284  option label ≝
285 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
286 
287definition stmt_labels : ∀p : stmt_params.∀globals.
288    joint_statement p globals → list label ≝
289  λp,g,stmt.
290  (match stmt_implicit_label … stmt with
291     [ Some l ⇒ [l]
292     | None ⇒ [ ]
293     ]) @ stmt_explicit_labels … stmt.
294
295definition stmt_forall_labels ≝
296  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
297  All … P (stmt_labels … s).
298
299lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
300  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
301#p#globals#P #s
302whd in ⊢ (% → ?);
303whd in ⊢ (???% → ?);
304elim (stmt_implicit_label ???) [2: #next * #_] //
305qed.
306
307lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
308  stmt_forall_labels … P s →
309    opt_All … P (stmt_implicit_label … s).
310#p#globals#P#s
311whd in ⊢ (% → ?);
312whd in ⊢ (???% → ?);
313elim (stmt_implicit_label ???)
314[ //
315| #next * #Pnext #_ @Pnext
316]
317qed.
318
319definition code_forall_labels ≝
320  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
321
322lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
323  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
324  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
325
326record lin_params : Type[1] ≝
327  { l_u_pars : unserialized_params }.
328 
329lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
330#tag #A #lbl #l elim l [*]
331** [2: #id] #a #tl #IH
332[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
333  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
334  @eq_identifier_elim #Heq normalize nodelta
335  [ #_ normalize / by /]
336| whd in ⊢ (?%→?%?);
337]
338#H >(index_of_label_from_internal … H)
339@le_S_S @(IH H)
340qed.
341
342(* mv *)
343lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
344#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
345#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
346qed.
347
348lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
349#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
350#n' #H @le_S_S @(IH … H)
351qed.
352
353lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
354#A #l elim l
355[ #n #ABS @⊥ /2 by absurd/
356| #hd #tl #IH * normalize //
357]
358qed.
359
360definition lin_params_to_params ≝
361  λlp : lin_params.
362     mk_params
363      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
364    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
365    (* code_point ≝ *)ℕ
366    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
367    (* point_of_label ≝ *)(λglobals,c,lbl.
368      If occurs_exactly_once ?? lbl c then with prf do
369        return index_of_label ?? lbl c
370      else
371        None ?)
372    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
373
374coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
375  on _lp : lin_params to params.
376 
377lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
378  ∀pt.pt ∈ code = leb (S pt) (|code|).
379#lp #globals #code elim code
380[ #pt %
381| #hd #tl #IH * [%]
382  #n @IH
383]qed.
384
385lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
386  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
387#lp #globals #code #lbl
388whd in match (code_has_label ????);
389whd in match (point_of_label ????);
390elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
391#Heq >Heq normalize nodelta
392[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
393  #ABS elim(absurd ?? ABS) -ABS
394  @index_of_label_length assumption ]] %
395qed.
396
397record graph_params : Type[1] ≝
398  { g_u_pars : unserialized_params }.
399
400(* One common instantiation of params via Graphs of joint_statements
401   (all languages but LIN) *)
402definition graph_params_to_params ≝
403  λgp : graph_params.
404     mk_params
405      (mk_stmt_params (g_u_pars gp) label (Some ?))
406    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
407    (* code_point ≝ *)label
408    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
409    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
410    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
411
412coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
413on _gp : graph_params to params.
414
415lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
416  ∀pt.code_has_point … code pt = mem_set … code pt.
417#gp#globals*#m*#i % qed.
418
419lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
420  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
421#gp #globals * #m * #i % qed.
422
423definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
424  λs : joint_statement p globals.
425  match s with
426  [ sequential _ n ⇒ P n
427  | _ ⇒ True
428  ].
429
430definition statement_closed : ∀globals.∀p : params.
431  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
432λglobals,p,code,pt,s.
433  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
434  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
435
436definition code_closed : ∀p : params.∀globals.
437  codeT p globals → Prop ≝ λp,globals,code.
438    forall_statements_i … (statement_closed … code) code.
439
440(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
441definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
442  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
443
444record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
445{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
446  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
447  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
448     following, right? *)
449(*  joint_if_sig: signature;  -- dropped in front end *)
450  joint_if_result   : resultT p;
451  joint_if_params   : paramsT p;
452  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
453(*CSC: XXXXX stacksize unused for LTL-...*)
454  joint_if_stacksize: nat;
455  joint_if_code     : codeT p globals ;
456  joint_if_entry : point_in_code … joint_if_code ;
457  joint_if_exit : point_in_code … joint_if_code
458}.
459
460definition joint_closed_internal_function ≝
461  λglobals,p.
462    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
463
464definition set_joint_code ≝
465  λglobals: list ident.
466  λpars: params.
467  λint_fun: joint_internal_function globals pars.
468  λgraph: codeT pars globals.
469  λentry.
470  λexit.
471    mk_joint_internal_function globals pars
472      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
473      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
474      graph entry exit.
475
476definition set_joint_if_graph ≝
477  λglobals.λpars : graph_params.
478  λgraph.
479  λp:joint_internal_function globals pars.
480  λentry_prf.
481  λexit_prf.
482    set_joint_code globals pars p
483      graph
484      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
485      (mk_Sig … (joint_if_exit ?? p) exit_prf).
486
487definition set_luniverse ≝
488  λglobals,pars.
489  λp : joint_internal_function globals pars.
490  λluniverse: universe LabelTag.
491   mk_joint_internal_function globals pars
492    luniverse (joint_if_runiverse … p) (joint_if_result … p)
493    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
494    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
495
496definition set_runiverse ≝
497  λglobals,pars.
498  λp : joint_internal_function globals pars.
499  λruniverse: universe RegisterTag.
500   mk_joint_internal_function globals pars
501    (joint_if_luniverse … p) runiverse (joint_if_result … p)
502    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
503    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
504   
505(* Specialized for graph_params *)
506definition add_graph ≝
507  λg_pars : graph_params.λglobals.λl:label.λstmt.
508    λp:joint_internal_function globals g_pars.
509   let code ≝ add … (joint_if_code … p) l stmt in
510    mk_joint_internal_function ? g_pars
511     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
512     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
513     code
514     (pi1 … (joint_if_entry … p))
515     (pi1 … (joint_if_exit … p)).
516>graph_code_has_point whd in match code; >mem_set_add
517@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
518#x #H <graph_code_has_point @H
519qed.
520
521definition set_locals ≝
522  λglobals,pars.
523  λp : joint_internal_function globals pars.
524  λlocals.
525   mk_joint_internal_function globals pars
526    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
527    (joint_if_params … p) locals (joint_if_stacksize … p)
528    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
529
530definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
531
532definition joint_program ≝
533 λp:params. program (λglobals. joint_function globals p) nat.
Note: See TracBrowser for help on using the repository browser.