Remove unused kind_def (KD_) nodes from AST

8 files changed, 2 insertions, 203 deletions

diff --git a/src/ast.ml b/src/ast.ml
index f57c0488..ff3c998d 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -499,12 +499,6 @@ val_spec_aux =  (* Value type specification *)
 type
 'a kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
    KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
- | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
- | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
 
 type
 'a scattered_def_aux =  (* Function and type union definitions that can be spread across
diff --git a/src/initial_check.ml b/src/initial_check.ml
index bbc417d5..3e4cae51 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -690,16 +690,6 @@ let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def)
     let key = id_to_string id in
     let (kind,k) = to_ast_kind k_env kind in
     (match k.k with
-     | K_Typ | K_Lam _ ->
-       let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in
-       let kd_abrv = KD_aux(KD_abbrev(kind,id,to_ast_namescm name_scm_opt,typschm),(l,())) in
-       let typ = (match typschm with 
-           | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
-             begin match (typquant_to_quantkinds k_env tq) with
-               | [] -> {k = K_Typ}
-               | typs -> {k= K_Lam(typs,{k=K_Typ})}
-             end) in
-       kd_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
      | K_Nat ->
        let kd_nabrv = 
          (match typschm with
@@ -710,47 +700,7 @@ let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def)
              | _ -> typ_error l "Def with kind Nat cannot have universal quantification" None None None)) in
        kd_nabrv,(names,Envmap.insert k_env (key, k),def_ord)
      | _ -> assert false
-    )
-  | Parse_ast.KD_record(kind,id,name_scm_opt,typq,fields,_) -> 
-    let id = to_ast_id id in
-    let key = id_to_string id in
-    let (kind,k) = to_ast_kind k_env kind in
-    let typq,k_env,_ = to_ast_typquant k_env typq in
-    let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *)
-    let kd_rec = KD_aux(KD_record(kind,id,to_ast_namescm name_scm_opt,typq,fields,false),(l,())) in
-    let typ = (match (typquant_to_quantkinds k_env typq) with
-      | [ ] -> {k = K_Typ}
-      | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-    kd_rec, (names,Envmap.insert k_env (key,typ), def_ord)
-  | Parse_ast.KD_variant(kind,id,name_scm_opt,typq,arms,_) ->
-    let id = to_ast_id id in
-    let key = id_to_string id in
-    let kind,k = to_ast_kind k_env kind in
-    let typq,k_env,_ = to_ast_typquant k_env typq in
-    let arms = List.map (to_ast_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
-    let kd_var = KD_aux(KD_variant(kind,id,to_ast_namescm name_scm_opt,typq,arms,false),(l,())) in
-    let typ = (match (typquant_to_quantkinds k_env typq) with
-      | [ ] -> {k = K_Typ}
-      | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-    kd_var, (names,Envmap.insert k_env (key,typ), def_ord)
-  | Parse_ast.KD_enum(kind,id,name_scm_opt,enums,_) -> 
-    let id = to_ast_id id in
-    let key = id_to_string id in
-    let kind,k = to_ast_kind k_env kind in
-    let enums = List.map to_ast_id enums in
-    let keys = List.map id_to_string enums in
-    let kd_enum = KD_aux(KD_enum(kind,id,to_ast_namescm name_scm_opt,enums,false),(l,())) in (* Add check that all enums have unique names *)
-    let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
-    kd_enum, (names,k_env,def_ord)
-  | Parse_ast.KD_register(kind,id,t1,t2,ranges) -> 
-    let id = to_ast_id id in
-    let key = id_to_string id in
-    let kind,k = to_ast_kind k_env kind in
-    let n1 = to_ast_nexp k_env t1 in
-    let n2 = to_ast_nexp k_env t2 in
-    let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
-    KD_aux(KD_register(kind,id,n1,n2,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
-
+    ))
 
 let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
   Rec_aux((match r with
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 120a0db6..1776d510 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -431,11 +431,6 @@ val_spec_aux =  (* Value type specification *)
 type 
 kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
    KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
- | KD_record of kind * id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
- | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | KD_register of kind * id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
 
 type 
 dec_spec_aux =  (* Register declarations *)
diff --git a/src/parser.mly b/src/parser.mly
index 678a7cc9..8e7d81c6 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1276,30 +1276,7 @@ ktype_def:
     { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) $5 5 5)) }
   | Def kind tid Eq Num
     { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) (tlocl (ATyp_constant $5) 5 5) 5 5)) }
-  | Def kind tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,$4,$8,fst $10, snd $10)) }
-  | Def kind tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,$4,(mk_typqn ()), fst $9, snd $9)) }
-  | Def kind tid Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
-  | Def kind tid Eq Const Struct Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
-  | Def kind tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3,$4, $8, fst $10, snd $10)) }
-  | Def kind tid Eq Const Union typquant Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
-  | Def kind tid name_sect Eq Const Union Lcurly union_body Rcurly
-    { kdloc (KD_variant($2, $3,$4, mk_typqn (), fst $9, snd $9)) }
-  | Def kind tid Eq Const Union Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
-  | Def kind tid Eq Enumerate Lcurly enum_body Rcurly
-    { kdloc (KD_enum($2,$3, mk_namesectn (), $7,false)) }
-  | Def kind tid name_sect Eq Enumerate Lcurly enum_body Rcurly
-    { kdloc (KD_enum($2,$3,$4,$8,false)) }
-  | Def kind tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
-    { kdloc (KD_register($2,$3, $8, $10, $13)) }
-
-    
+
 def:
   | type_def
       { dloc (DEF_type($1)) }
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 8de81d4d..26249f75 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -565,35 +565,9 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
 let pp_lem_kindef ppf (KD_aux(kd,(l,annot))) =
   let print_kd ppf kd =
     match kd with
-    | KD_abbrev(kind,id,namescm,typschm) ->
-      fprintf ppf "@[<0>(KD_abbrev %a %a %a %a)@]"
-        pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
     | KD_nabbrev(kind,id,namescm,n) ->
       fprintf ppf "@[<0>(KD_nabbrev %a %a %a %a)@]"
         pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_nexp n
-    | KD_record(kind,id,nm,typq,fs,_) ->
-      let f_pp ppf (typ,id) =
-        fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
-      fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]"
-        kwd "KD_record" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
-    | KD_variant(kind,id,nm,typq,ar,_) ->
-      let a_pp ppf (Tu_aux(typ_u,l)) =
-        match typ_u with
-        | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
-                                pp_lem_typ typ pp_lem_id id pp_lem_l l
-        | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
-      in
-      fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]"
-        kwd "KD_variant" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
-    | KD_enum(kind,id,ns,enums,_) ->
-      let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
-      fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
-        kwd "KD_enum" pp_lem_kind kind pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
-    | KD_register(kind,id,n1,n2,rs) ->
-      let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
-      let pp_rids = (list_pp pp_rid pp_rid) in
-      fprintf ppf "@[<0>(%a %a %a %a %a [%a])@]"
-        kwd "KD_register" pp_lem_kind kind pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
   in
   fprintf ppf "@[<0>(KD_aux %a (%a, %a))@]" print_kd kd pp_lem_l l pp_annot annot
 
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 0b7ca48f..b1238f8a 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -598,55 +598,6 @@ let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with
                      doc_id_ocaml id;
                      equals;
                      doc_nexp nexp]
-  | KD_abbrev(_,id,nm,typschm) ->
-      doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm)
-  | KD_record(_,id,nm,typq,fs,_) ->
-      let f_pp (typ,id) = concat [doc_id_ocaml_type id; space; colon; doc_typ_ocaml typ; semi] in
-      let fs_doc = group (separate_map (break 1) f_pp fs) in
-      doc_op equals
-        (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc))
-  | KD_variant(_,id,nm,typq,ar,_) ->
-    let n = List.length ar in
-    let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in
-    doc_op equals
-      (concat [string "type"; space; doc_id_ocaml_type id;])
-      (if n > 246
-       then brackets (space ^^(doc_typquant_ocaml typq ar_doc))
-       else (doc_typquant_ocaml typq ar_doc))
-  | KD_enum(_,id,nm,enums,_) ->
-    let n = List.length enums in
-    let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor) enums) in
-    doc_op equals
-      (concat [string "type"; space; doc_id_ocaml_type id;])
-      (enums_doc)
-  | KD_register(_,id,n1,n2,rs) ->
-    let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in
-    let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
-    match n1,n2 with
-    | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
-      let dir = i1 < i2 in
-      let size = if dir then i2-i1 +1 else i1-i2 in
-      doc_op equals
-        ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val"))
-        (separate space [string "Vregister";
-                         (parens (separate comma_sp
-                                    [parens (separate space
-                                               [string "match init_val with";
-                                                pipe;
-                                                string "None";
-                                                arrow;
-                                                string "ref";
-                                                string "(Array.make";
-                                                doc_int size;
-                                                string "Vzero)";
-                                                pipe;
-                                                string "Some init_val";
-                                                arrow;
-                                                string "ref init_val";]);
-                                     doc_nexp n1;
-                                     string (if dir then "true" else "false");
-                                     string_lit (doc_id id);
-                                     brackets doc_rids]))])
 
 let doc_rec_ocaml (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> empty
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 546f229f..0f943efa 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -436,37 +436,8 @@ let doc_typdef (TD_aux(td,_)) = match td with
         ])
 
 let doc_kindef (KD_aux(kd,_)) = match kd with
-  | KD_abbrev(kind,id,nm,typschm) ->
-    doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_typscm typschm)
   | KD_nabbrev(kind,id,nm,n) ->
     doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_nexp n)
-  | KD_record(kind,id,nm,typq,fs,_) ->
-    let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in
-    let fs_doc = group (separate_map (break 1) f_pp fs) in
-    doc_op equals
-      (concat [string "def"; space;doc_kind kind; space; doc_id id; doc_namescm nm])
-      (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc))
-  | KD_variant(kind,id,nm,typq,ar,_) ->
-    let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in
-    doc_op equals
-      (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm])
-      (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc))
-  | KD_enum(kind,id,nm,enums,_) ->
-      let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in
-      doc_op equals
-        (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm])
-        (string "enumerate" ^^ space ^^ braces enums_doc)
-  | KD_register(kind,id,n1,n2,rs) ->
-      let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in
-      let doc_rids = group (separate_map (break 1) doc_rid rs) in
-      doc_op equals
-        (string "def" ^^ space ^^ doc_kind kind ^^ space ^^ doc_id id)
-        (separate space [
-          string "register bits";
-          brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2);
-          braces doc_rids;
-        ])
-
 
 let doc_rec (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> empty
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 3f3df45a..ddba4a6f 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -409,19 +409,6 @@ let typ_variants consider_var bound tunions =
 
 let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with
   | KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp
-  | KD_abbrev(_,id,_,typschm) ->
-    init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
-  | KD_record(_,id,_,typq,tids,_) ->
-    let binds = init_env (string_of_id id) in
-    let bounds = if consider_var then typq_bindings typq else mt in
-    binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
-  | KD_variant(_,id,_,typq,tunions,_) ->
-    let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
-    typ_variants consider_var bindings tunions
-  | KD_enum(_,id,_,ids,_) ->
-    Nameset.of_list (List.map string_of_id (id::ids)),mt
-  | KD_register(_,id,n1,n2,_) ->
-    init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2
 
 let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
   | TD_abbrev(id,_,typschm) -> init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)