Add lab9

lab9/Program.fs

@@ -0,0 +1,365 @@
+(* syntax *)
+
+type ide = string
+
+type boolean =
+    | True
+    | False
+
+type exp =
+    | Eint of int
+    | Eplus of (exp * exp)
+    | Eminus of (exp * exp)
+    | Eide of ide
+    | Ebool of boolean
+    | Eeql of (exp * exp)
+    | Eleq of (exp * exp)
+    | Enot of exp
+    | Eand of (exp * exp)
+    | Eor of (exp * exp)
+    | Eifthenelse of (exp * exp * exp)
+
+type com =
+    | Cassign of ide * exp
+    | Cvar of ide * exp
+    | Cconst of ide * exp
+    | Cifthenelse of exp * pseq * pseq
+    | Cwhile of exp * pseq
+    | CDoNTimes of exp * pseq
+
+and pseq =
+    | Pseq of com * pseq
+    | Pend
+
+type prog = Prog of pseq * exp
+
+let rec exp_to_string (e: exp) =
+    match e with
+    | Eint i -> sprintf "%d" i
+    | Eplus (e1, e2) -> sprintf "(%s + %s)" (exp_to_string e1) (exp_to_string e2)
+    | Eminus (e1, e2) -> sprintf "(%s - %s)" (exp_to_string e1) (exp_to_string e2)
+    | Eide i -> i
+    | Ebool b ->
+        match b with
+        | True -> "true"
+        | False -> "false"
+    | Enot e -> sprintf "(not %s)" (exp_to_string e)
+    | Eand (e1, e2) -> sprintf "(%s and %s)" (exp_to_string e1) (exp_to_string e2)
+    | Eor (e1, e2) -> sprintf "(%s or %s)" (exp_to_string e1) (exp_to_string e2)
+    | Eeql (e1, e2) -> sprintf "(%s == %s)" (exp_to_string e1) (exp_to_string e2)
+    | Eleq (e1, e2) -> sprintf "(%s <= %s)" (exp_to_string e1) (exp_to_string e2)
+    | Eifthenelse (c, e1, e2) ->
+        sprintf "if %s then (%s) else (%s)" (exp_to_string c) (exp_to_string e1) (exp_to_string e2)
+
+let rec com_to_string (c: com) =
+    match c with
+    | Cassign (i, e) -> sprintf "%s := %s" i (exp_to_string e)
+    | Cvar (v, e) -> sprintf "var %s := %s" v (exp_to_string e)
+    | Cconst (v, e) -> sprintf "const %s = %s" v (exp_to_string e)
+    | Cifthenelse (cond, cthen, celse) ->
+        sprintf "if %s\nthen %s\nelse %s" (exp_to_string cond) (pseq_to_string cthen) (pseq_to_string celse)
+    | Cwhile (cond, body) -> sprintf "while %s\n%s" (exp_to_string cond) (pseq_to_string body)
+    | CDoNTimes (n, body) -> sprintf "do %s times:\n%s" (exp_to_string n) (pseq_to_string body)
+
+and pseq_to_string (s: pseq) =
+    match s with
+    | Pseq (c, Pend) -> sprintf "%s" (com_to_string c)
+    | Pseq (c, q) -> sprintf "%s;\n%s" (com_to_string c) (pseq_to_string q)
+    | Pend -> ""
+
+let prog_to_string (p: prog) =
+    match p with
+    | Prog (s, e) -> sprintf "%s;\nreturn %s" (pseq_to_string s) (exp_to_string e)
+
+(* error handling *)
+
+let unbound_identifier_error ide =
+    failwith (sprintf "unbound identifier %s" ide)
+
+let negative_natural_number_error () =
+    failwith "natural numbers must be positive or zero"
+
+let type_error () = failwith "type error"
+
+let memory_error () =
+    failwith "access to a location that is not available"
+
+let not_a_location_error i =
+    failwith (sprintf "not a location: %s" i)
+
+(* semantic domains *)
+
+type eval =
+    | Int of int
+    | Bool of bool
+
+type loc = int
+
+type mval = eval
+
+type store = int * (loc -> mval) (* il primo elemento della coppia è la minima locazione non definita *)
+
+let empty_store = (0, (fun l -> memory_error ()))
+
+let apply_store st l = (snd st) l
+
+let allocate: store -> loc * store =
+    fun st ->
+        let l = fst st in
+        let l1 = l + 1 in
+        let st1 = (l1, snd st) in
+        (l, st1)
+
+let update: store -> loc -> mval -> store =
+    fun st l mv ->
+        match st with
+        | (maxloc, fn) -> let fn1 l1 = if l = l1 then mv else fn l1 in (maxloc, fn1)
+
+type dval =
+    | E of eval
+    | L of loc
+
+type env = ide -> dval
+
+let empty_env = fun v -> unbound_identifier_error v
+
+let bind e v r = fun v1 -> if v1 = v then r else e v1
+
+let apply_env e v = e v
+
+let rec eval_to_string (e: eval) =
+    match e with
+    | Int i -> sprintf "%d" i
+    | Bool b -> if b then "true" else "false"
+
+(* denotational semantics *)
+
+let rec esem: exp -> env -> store -> eval =
+    fun e ev st ->
+        match e with
+        | Eint i ->
+            if i < 0 then
+                negative_natural_number_error ()
+            else
+                Int i
+        | Eplus (e1, e2) ->
+            (let s1 = esem e1 ev st in
+             let s2 = esem e2 ev st in
+
+             match (s1, s2) with
+             | (Int i1, Int i2) -> Int(i1 + i2)
+             | _ -> type_error ())
+        | Eminus (e1, e2) ->
+            let s1 = esem e1 ev st in
+            let s2 = esem e2 ev st in
+
+            (match (s1, s2) with
+             | (Int i1, Int i2) ->
+                 if i1 >= i2 then
+                     Int(i1 - i2)
+                 else
+                     negative_natural_number_error ()
+             | _ -> type_error ())
+        | Ebool b ->
+            (match b with
+             | True -> Bool true
+             | False -> Bool false)
+        | Eeql (e1, e2) ->
+            let s1 = esem e1 ev st in
+            let s2 = esem e2 ev st in
+
+            (match (s1, s2) with
+             | (Int i1, Int i2) ->
+                 if i1 = i2 then
+                     Bool true
+                 else
+                     Bool false
+             | _ -> type_error ())
+        | Eleq (e1, e2) ->
+            let s1 = esem e1 ev st in
+            let s2 = esem e2 ev st in
+
+            (match (s1, s2) with
+             | (Int i1, Int i2) ->
+                 if i1 <= i2 then
+                     Bool true
+                 else
+                     Bool false
+             | _ -> type_error ())
+        | Eand (e1, e2) ->
+            let s1 = esem e1 ev st in
+            let s2 = esem e2 ev st in
+
+            (match (s1, s2) with
+             | (Bool b1, Bool b2) -> Bool(b1 && b2)
+             | _ -> type_error ())
+        | Eor (e1, e2) ->
+            let s1 = esem e1 ev st in
+            let s2 = esem e2 ev st in
+
+            (match (s1, s2) with
+             | (Bool b1, Bool b2) -> Bool(b1 || b2)
+             | _ -> type_error ())
+        | Enot e ->
+            let s = esem e ev st in
+
+            (match s with
+             | Bool b -> Bool(not b)
+             | _ -> type_error ())
+        | Eifthenelse (c, e1, e2) ->
+            let sc = esem c ev st in
+
+            (match sc with
+             | Bool b -> esem (if b then e1 else e2) ev st
+             | _ -> type_error ())
+        | Eide i ->
+            let value = apply_env ev i
+
+            match value with
+            | L l -> apply_store st l
+            | E e -> e
+
+let rec csem: com -> env -> store -> (env * store) =
+    fun c ev st ->
+        match c with
+        | Cassign (i, e) ->
+            let s = esem e ev st
+
+            match apply_env ev i with
+            | L l -> let st1 = update st l s in (ev, st1)
+            | _ -> not_a_location_error i
+        | Cvar (i, e) ->
+            let s = esem e ev st in
+            let (newloc, st1) = allocate st in
+            let st2 = update st1 newloc s in
+            let ev1 = bind ev i (L newloc) in
+            (ev1, st2)
+        | Cconst (i, e) ->
+            let s = esem e ev st in
+            let ev1 = bind ev i (E s) in
+            (ev1, st)
+        | Cifthenelse (cond, cthen, celse) ->
+            let s = esem cond ev st in
+
+            match s with
+            | Bool b ->
+                if b then
+                    pssem cthen ev st // ERRORE: questo causa scoping dinamico, vale a dire, le variabili dichiarate nel ramo then possono essere viste dal seguito del programma
+                else
+                    pssem celse ev st
+            | _ -> type_error ()
+        | Cwhile (cond, body) ->
+            let s = esem cond ev st in
+
+            match st with
+            | (firstloc,stfn) ->
+
+              match s with
+              | Bool b ->
+                  if b then
+                      // ERRORE, non va restituito st1 ma st1 con "maxloc" (primo elemento della coppia) resettata
+                      (* let (ev1, st1) = pssem body ev st in
+                       * csem (Cwhile(cond, body)) ev st1  *)
+                      // Invece, resettiamo maxloc a quello vecchio per st1
+                      let (ev1, (firstloc',stfn')) = pssem body ev st in
+                      csem (Cwhile(cond, body)) ev (firstloc,stfn')
+                      (* NOTA CHE L'AMBIENTE VIENE BUTTATO VIA, LO STATO NO, PERCHE'? *)
+                  else
+                      (ev, st)
+              | _ -> type_error ()
+        | CDoNTimes (n,body) ->
+          let n = esem n ev st
+
+          match n with
+          | Int 0 -> (ev, st)
+          | Int m ->
+              let (ev1, st1) = pssem body ev st
+              csem (CDoNTimes(Eint(m-1),body)) ev st1
+          | _ -> type_error ()
+
+and pssem: pseq -> env -> store -> (env * store) =
+    fun s ev st ->
+        match s with
+        | Pend -> (ev, st)
+        | Pseq (c, q) ->
+            match csem c ev st with
+            | (ev1, st1) -> pssem q ev1 st1
+
+let rec psem: prog -> env -> store -> eval =
+    fun p ev st ->
+        match p with
+        | Prog (s, e) ->
+            let (ev1, st1) = pssem s ev st
+            esem e ev1 st1
+
+(* test *)
+
+let eval: prog -> unit =
+    fun p ->
+        printf "\n%s \n\n==> " (prog_to_string p)
+
+        try
+            printf "%s\n" (eval_to_string (psem p empty_env empty_store))
+        with
+        | Failure message -> printfn "error: %s\n" message
+
+let a () = failwith ""
+
+let l =
+    [ Prog(
+          Pseq(
+              Cvar("x", Eint 98),
+              (Pseq(
+                  Cvar("y", Eint 28),
+                  (Pseq(
+                      Cwhile(
+                          Enot(Eeql(Eide "x", Eide "y")),
+                          Pseq(
+                              Cifthenelse(
+                                  Eleq(Eide "x", Eide "y"),
+                                  Pseq(Cassign("y", Eminus(Eide "y", Eide "x")), Pend),
+                                  Pseq(Cassign("x", Eminus(Eide "x", Eide "y")), Pend)
+                              ),
+                              Pend
+                          )
+                      ),
+                      Pend
+                  ))
+              ))
+          ),
+          Eide "x"
+      ) ]
+
+let l2 =
+    [ Prog(
+          Pseq(
+              Cvar("x", Eint 1),
+              (Pseq(
+                  Cvar("y", Eint 0),
+                  Pseq(
+                    CDoNTimes(Eint(9),Pseq(Cassign("y", Eplus(Eide "y", Eide "x")),Pend)),
+                    Pend
+                  )
+              ))
+          ),
+          Eide "x"
+      ) ]
+
+let main = List.iter eval l
+let main2 = List.iter eval l2
+
+(*
+
+> dotnet run
+
+var x := 98;
+var y := 28;
+while (not (x == y))
+if (x <= y)
+then y := (y - x)
+else x := (x - y);
+return x
+
+==> 14
+
+*)