Adding Support for User Defined Datatypes and Logical Functions

Gillian-C/lib/gilgen.ml

@@ -1061,6 +1061,8 @@ let trans_program
         imports = [];
         lemmas = Hashtbl.create 1;
         preds = Hashtbl.create 1;
+        funcs = Hashtbl.create 1;
+        datatypes = Hashtbl.create 1;
         only_specs = Hashtbl.create 1;
         macros = Hashtbl.create 1;
         bi_specs = make_hashtbl (fun p -> p.BiSpec.bispec_name) bi_specs;

Gillian-JS/lib/Compiler/JSIL2GIL.ml

@@ -502,6 +502,9 @@ let jsil2core_prog (prog : EProg.t) : ('a, string) GProg.t =
       ~procs:new_procs
       ~macros:(translate_tbl prog.macros jsil2gil_macro)
       ~bi_specs:(translate_tbl prog.bi_specs jsil2gil_bispec)
-      ~proc_names:prog.proc_names ~predecessors:(Hashtbl.create 1) ()
+      ~proc_names:prog.proc_names ~predecessors:(Hashtbl.create 1)
+      ~datatypes:(Hashtbl.create 1)
+      ~funcs:(Hashtbl.create 1) (* TODO *)
+      ()
   in
   result

GillianCore/GIL_Syntax/Constructor.ml

@@ -0,0 +1,9 @@
+type t = TypeDef__.constructor = {
+  constructor_name : string;
+  constructor_source_path : string option;
+  constructor_loc : Location.t option;
+  constructor_num_fields : int;
+  constructor_fields : Type.t option list;
+  constructor_datatype : string;
+}
+[@@deriving yojson]

GillianCore/GIL_Syntax/Datatype.ml

@@ -0,0 +1,7 @@
+type t = TypeDef__.datatype = {
+  datatype_name : string;
+  datatype_source_path : string option;
+  datatype_loc : Location.t option;
+  datatype_constructors : Constructor.t list;
+}
+[@@deriving yojson]

GillianCore/GIL_Syntax/Expr.ml

@@ -16,6 +16,9 @@ type t = TypeDef__.expr =
       (** Existential quantification. *)
   | ForAll of (string * Type.t option) list * t
       (** Universal quantification. *)
+  | ConstructorApp of string * t list  (** Datatype constructor *)
+  | FuncApp of string * t list  (** Function application *)
+  | Cases of t * (string * string list * t) list
 [@@deriving eq, ord]
 
 let to_yojson = TypeDef__.expr_to_yojson
@@ -377,6 +380,18 @@ let rec map_opt
             match map_e e with
             | Some e' -> Some (ForAll (bt, e'))
             | _ -> None)
+        | ConstructorApp (n, les) ->
+            aux les (fun les -> ConstructorApp (n, les))
+        | FuncApp (n, les) -> aux les (fun les -> FuncApp (n, les))
+        | Cases (e, cs) ->
+            let cs =
+              List_utils.flaky_map
+                (fun (c, bs, e) ->
+                  let e = map_e e in
+                  Option.map (fun e -> (c, bs, e)) e)
+                cs
+            in
+            Option.map (fun cs -> Cases (e, cs)) cs
       in
       Option.map f_after mapped_expr
 
@@ -414,6 +429,25 @@ let rec pp fmt e =
       Fmt.pf fmt "(forall %a . %a)"
         (Fmt.list ~sep:Fmt.comma pp_var_with_type)
         bt pp e
+  | ConstructorApp (n, ll) ->
+      Fmt.pf fmt "'%s(%a)" n (Fmt.list ~sep:Fmt.comma pp) ll
+  | FuncApp (n, ll) -> Fmt.pf fmt "%s(%a)" n (Fmt.list ~sep:Fmt.comma pp) ll
+  | Cases (scrutinee, branches) ->
+      Fmt.pf fmt "@[<v 2>case %a {@," pp scrutinee;
+      List.iteri
+        (fun i (constructor, binders, expr) ->
+          Fmt.pf fmt "  %s" constructor;
+          (match binders with
+          | [] -> ()
+          | _ ->
+              Fmt.pf fmt "(";
+              Fmt.pf fmt "%a" (Fmt.list ~sep:(Fmt.any ", ") Fmt.string) binders;
+              Fmt.pf fmt ")");
+          Fmt.pf fmt " -> %a" pp expr;
+          if i < List.length branches - 1 then Fmt.pf fmt ";@,"
+          else Fmt.pf fmt "@,")
+        branches;
+      Fmt.pf fmt "}@]"
 
 let rec full_pp fmt e =
   match e with
@@ -476,6 +510,7 @@ let rec is_concrete (le : t) : bool =
   | BinOp (e1, _, e2) -> loop [ e1; e2 ]
   | LstSub (e1, e2, e3) -> loop [ e1; e2; e3 ]
   | NOp (_, les) | EList les | ESet les -> loop les
+  | ConstructorApp (_, _) | FuncApp _ | Cases _ -> false
 
 let is_concrete_zero_i : t -> bool = function
   | Lit (Int z) -> Z.equal Z.zero z

GillianCore/GIL_Syntax/Func.ml

@@ -0,0 +1,8 @@
+type t = TypeDef__.func = {
+  func_name : string;
+  func_source_path : string option;
+  func_loc : Location.t option;
+  func_num_params : int;
+  func_params : (string * Type.t option) list;
+  func_definition : Expr.t;
+}

GillianCore/GIL_Syntax/Gil_syntax.ml

@@ -6,7 +6,10 @@ module BiSpec = BiSpec
 module Branch_case = Branch_case
 module Cmd = Cmd
 module Constant = Constant
+module Constructor = Constructor
+module Datatype = Datatype
 module Expr = Expr
+module Func = Func
 module Flag = Flag
 module LCmd = LCmd
 module Lemma = Lemma