logical-foundations/imp1.ml
2020-06-03 21:46:06 -05:00

211 lines
4.5 KiB
OCaml

type bool =
| True
| False
(** val negb : bool -> bool **)
let negb = function
| True -> False
| False -> True
type nat =
| O
| S of nat
type 'a option =
| Some of 'a
| None
type sumbool =
| Left
| Right
(** val add : nat -> nat -> nat **)
let rec add n m =
match n with
| O -> m
| S p -> S (add p m)
(** val mul : nat -> nat -> nat **)
let rec mul n m =
match n with
| O -> O
| S p -> add m (mul p m)
(** val sub : nat -> nat -> nat **)
let rec sub n m =
match n with
| O -> n
| S k -> (match m with
| O -> n
| S l -> sub k l)
(** val eqb : nat -> nat -> bool **)
let rec eqb n m =
match n with
| O -> (match m with
| O -> True
| S _ -> False)
| S n' -> (match m with
| O -> False
| S m' -> eqb n' m')
(** val leb : nat -> nat -> bool **)
let rec leb n m =
match n with
| O -> True
| S n' -> (match m with
| O -> False
| S m' -> leb n' m')
(** val bool_dec : bool -> bool -> sumbool **)
let bool_dec b1 b2 =
match b1 with
| True -> (match b2 with
| True -> Left
| False -> Right)
| False -> (match b2 with
| True -> Right
| False -> Left)
type ascii =
| Ascii of bool * bool * bool * bool * bool * bool * bool * bool
(** val ascii_dec : ascii -> ascii -> sumbool **)
let ascii_dec a b =
let Ascii (x, x0, x1, x2, x3, x4, x5, x6) = a in
let Ascii (b8, b9, b10, b11, b12, b13, b14, b15) = b in
(match bool_dec x b8 with
| Left ->
(match bool_dec x0 b9 with
| Left ->
(match bool_dec x1 b10 with
| Left ->
(match bool_dec x2 b11 with
| Left ->
(match bool_dec x3 b12 with
| Left ->
(match bool_dec x4 b13 with
| Left ->
(match bool_dec x5 b14 with
| Left -> bool_dec x6 b15
| Right -> Right)
| Right -> Right)
| Right -> Right)
| Right -> Right)
| Right -> Right)
| Right -> Right)
| Right -> Right)
type string =
| EmptyString
| String of ascii * string
(** val string_dec : string -> string -> sumbool **)
let rec string_dec s x =
match s with
| EmptyString -> (match x with
| EmptyString -> Left
| String (_, _) -> Right)
| String (a, s0) ->
(match x with
| EmptyString -> Right
| String (a0, s1) ->
(match ascii_dec a a0 with
| Left -> string_dec s0 s1
| Right -> Right))
(** val eqb_string : string -> string -> bool **)
let eqb_string x y =
match string_dec x y with
| Left -> True
| Right -> False
type 'a total_map = string -> 'a
(** val t_update : 'a1 total_map -> string -> 'a1 -> string -> 'a1 **)
let t_update m x v x' =
match eqb_string x x' with
| True -> v
| False -> m x'
type state = nat total_map
type aexp =
| ANum of nat
| AId of string
| APlus of aexp * aexp
| AMinus of aexp * aexp
| AMult of aexp * aexp
type bexp =
| BTrue
| BFalse
| BEq of aexp * aexp
| BLe of aexp * aexp
| BNot of bexp
| BAnd of bexp * bexp
(** val aeval : state -> aexp -> nat **)
let rec aeval st = function
| ANum n -> n
| AId x -> st x
| APlus (a1, a2) -> add (aeval st a1) (aeval st a2)
| AMinus (a1, a2) -> sub (aeval st a1) (aeval st a2)
| AMult (a1, a2) -> mul (aeval st a1) (aeval st a2)
(** val beval : state -> bexp -> bool **)
let rec beval st = function
| BTrue -> True
| BFalse -> False
| BEq (a1, a2) -> eqb (aeval st a1) (aeval st a2)
| BLe (a1, a2) -> leb (aeval st a1) (aeval st a2)
| BNot b1 -> negb (beval st b1)
| BAnd (b1, b2) ->
(match beval st b1 with
| True -> beval st b2
| False -> False)
type com =
| CSkip
| CAss of string * aexp
| CSeq of com * com
| CIf of bexp * com * com
| CWhile of bexp * com
(** val ceval_step : state -> com -> nat -> state option **)
let rec ceval_step st c = function
| O -> None
| S i' ->
(match c with
| CSkip -> Some st
| CAss (l, a1) -> Some (t_update st l (aeval st a1))
| CSeq (c1, c2) ->
(match ceval_step st c1 i' with
| Some st' -> ceval_step st' c2 i'
| None -> None)
| CIf (b, c1, c2) ->
(match beval st b with
| True -> ceval_step st c1 i'
| False -> ceval_step st c2 i')
| CWhile (b1, c1) ->
(match beval st b1 with
| True ->
(match ceval_step st c1 i' with
| Some st' -> ceval_step st' c i'
| None -> None)
| False -> Some st))