(*  Title:      Jinja/J/Examples.thy

    Author:     Christoph Petzinger
    Copyright   2004 Technische Universitaet Muenchen
*)

section ‹Example Expressions›

theory Examples imports Expr begin

definition classObject::"J_mb cdecl"
where
  "classObject == (''Object'','''',[],[])"


definition classI :: "J_mb cdecl"
where
  "classI ==
  (''I'', Object,
  [],
  [(''mult'',[Integer,Integer],Integer,[''i'',''j''],
   if (Var ''i'' «Eq¬ Val(Intg 0)) (Val(Intg 0))
   else Var ''j'' «Add¬
       Var this ∙ ''mult''([Var ''i'' «Add¬ Val(Intg (- 1)),Var ''j'']))
  ])"


definition classL :: "J_mb cdecl"
where
  "classL ==
  (''L'', Object,
  [(''F'',Integer), (''N'',Class ''L'')],
  [(''app'',[Class ''L''],Void,[''l''],
   if (Var this ∙ ''N''{''L''} «Eq¬ null)
      (Var this ∙ ''N''{''L''} := Var ''l'')
   else (Var this ∙ ''N''{''L''}) ∙ ''app''([Var ''l'']))
  ])"


definition testExpr_BuildList :: "expr"
where
  "testExpr_BuildList ==
  {''l1'':Class ''L'' := new ''L'';
   Var ''l1''∙''F''{''L''} := Val(Intg 1);;
  {''l2'':Class ''L'' := new ''L'';
   Var ''l2''∙ ''F''{''L''} := Val(Intg 2);;
  {''l3'':Class ''L'' := new ''L'';
   Var ''l3''∙ ''F''{''L''} := Val(Intg 3);;
  {''l4'':Class ''L'' := new ''L'';
   Var ''l4''∙ ''F''{''L''} := Val(Intg 4);;
   Var ''l1''∙''app''([Var ''l2'']);;
   Var ''l1''∙''app''([Var ''l3'']);;
   Var ''l1''∙''app''([Var ''l4''])}}}}"

definition testExpr1 ::"expr"
where
  "testExpr1 == Val(Intg 5)"
definition testExpr2 ::"expr"
where
  "testExpr2 == BinOp (Val(Intg 5)) Add (Val(Intg 6))"
definition testExpr3 ::"expr"
where
  "testExpr3 == BinOp (Var ''V'') Add (Val(Intg 6))"
definition testExpr4 ::"expr"
where
  "testExpr4 == ''V'' := Val(Intg 6)"
definition testExpr5 ::"expr"
where
  "testExpr5 == new ''Object'';; {''V'':(Class ''C'') := new ''C''; Var ''V''∙''F''{''C''} := Val(Intg 42)}"
definition testExpr6 ::"expr"
where
  "testExpr6 == {''V'':(Class ''I'') := new ''I''; Var ''V''∙''mult''([Val(Intg 40),Val(Intg 4)])}"

definition mb_isNull:: "expr"
where
  "mb_isNull == Var this ∙ ''test''{''A''} «Eq¬ null "

definition mb_add:: "expr"
where
  "mb_add == (Var this ∙ ''int''{''A''} :=( Var this ∙ ''int''{''A''} «Add¬ Var ''i''));; (Var this ∙ ''int''{''A''})"

definition mb_mult_cond:: "expr"  
where
  "mb_mult_cond == (Var ''j'' «Eq¬ Val (Intg 0)) «Eq¬ Val (Bool False)"

definition mb_mult_block:: "expr"
where
  "mb_mult_block == ''temp'':=(Var ''temp'' «Add¬ Var ''i'');;''j'':=(Var ''j'' «Add¬ Val (Intg (- 1)))"

definition mb_mult:: "expr"
where
  "mb_mult == {''temp'':Integer:=Val (Intg 0); While (mb_mult_cond) mb_mult_block;; ( Var this ∙ ''int''{''A''} := Var ''temp'';; Var ''temp'' )}"

definition classA:: "J_mb cdecl"
where
  "classA ==
  (''A'', Object,
  [(''int'',Integer),
   (''test'',Class ''A'') ],
  [(''isNull'',[],Boolean,[], mb_isNull),
   (''add'',[Integer],Integer,[''i''], mb_add),
   (''mult'',[Integer,Integer],Integer,[''i'',''j''], mb_mult) ])"
  

definition testExpr_ClassA:: "expr"
where
  "testExpr_ClassA ==
  {''A1'':Class ''A'':= new ''A'';
  {''A2'':Class ''A'':= new ''A'';
  {''testint'':Integer:= Val (Intg 5);
   (Var ''A2''∙ ''int''{''A''} := (Var ''A1''∙ ''add''([Var ''testint''])));;
   (Var ''A2''∙ ''int''{''A''} := (Var ''A1''∙ ''add''([Var ''testint''])));;
   Var ''A2''∙ ''mult''([Var ''A2''∙ ''int''{''A''}, Var ''testint'']) }}}"

end