further progress

7 files changed, 140 insertions, 8 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 69fe63cb..d571c916 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -448,12 +448,15 @@ and map_mpexp_annot_aux f = function
   | MPat_pat mpat -> MPat_pat (map_mpat_annot f mpat)
   | MPat_when (mpat, guard) -> MPat_when (map_mpat_annot f mpat, map_exp_annot f guard)
 
+and map_mapcl_annot f (MCL_aux (MCL_mapcl (mpexp1, mpexp2), annot)) =
+  MCL_aux (MCL_mapcl (map_mpexp_annot f mpexp1, map_mpexp_annot f mpexp2), f annot)
+
 and map_mpat_annot f (MP_aux (mpat, annot)) = MP_aux (map_mpat_annot_aux f mpat, f annot)
 and map_mpat_annot_aux f = function
   | MP_lit lit -> MP_lit lit
   | MP_id id -> MP_id id
   | MP_app (id, mpats) -> MP_app (id, List.map (map_mpat_annot f) mpats)
-  | MP_record (fmpats, b) -> MP_record (List.map (map_fpat_annot f) fmpats, b)
+  | MP_record (fmpats, b) -> MP_record (List.map (map_mfpat_annot f) fmpats, b)
   | MP_tup mpats -> MP_tup (List.map (map_mpat_annot f) mpats)
   | MP_list mpats -> MP_list (List.map (map_mpat_annot f) mpats)
   | MP_vector_concat mpats -> MP_vector_concat (List.map (map_mpat_annot f) mpats)
@@ -462,6 +465,7 @@ and map_mpat_annot_aux f = function
   | MP_string_append (mpat1, mpat2) -> MP_string_append (map_mpat_annot f mpat1, map_mpat_annot f mpat2)
 
 and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot)
+and map_mfpat_annot f (MFP_aux (MFP_mpat (id, mpat), annot)) = MFP_aux (MFP_mpat (id, map_mpat_annot f mpat), f annot)
 and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
 and map_letbind_annot_aux f = function
   | LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp)
@@ -784,6 +788,9 @@ let rec pat_ids (P_aux (pat_aux, _)) =
      IdSet.union (pat_ids pat1) (pat_ids pat2)
   | P_record (fpats, _) ->
      List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty
+  | P_string_append (pat1, pat2) ->
+     IdSet.union (pat_ids pat1) (pat_ids pat2)
+
 and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat
 
 let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) =
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 7ac5058f..6fb1c576 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -177,7 +177,9 @@ val map_pexp_annot : ('a annot -> 'b annot) -> 'a pexp -> 'b pexp
 val map_lexp_annot : ('a annot -> 'b annot) -> 'a lexp -> 'b lexp
 val map_letbind_annot : ('a annot -> 'b annot) -> 'a letbind -> 'b letbind
 val map_mpat_annot : ('a annot -> 'b annot) -> 'a mpat -> 'b mpat
+val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat
 val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp
+val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl
 
 (* Extract locations from identifiers *)
 val id_loc : id -> Parse_ast.l
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 793d6657..b766daa1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -771,11 +771,11 @@ let rec to_ast_mpat k_env def_ord (Parse_ast.MP_aux(mpat,l)) =
       if mpats = []
       then MP_id (to_ast_id id)
       else MP_app(to_ast_id id, List.map (to_ast_mpat k_env def_ord) mpats)
-    | Parse_ast.MP_record(fpats,_) ->
+    | Parse_ast.MP_record(mfpats,_) ->
       MP_record(List.map
-                 (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) ->
-              FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,())))
-                 fpats, false)
+                 (fun (Parse_ast.MFP_aux(Parse_ast.MFP_mpat(id,mfp),l)) ->
+              MFP_aux(MFP_mpat(to_ast_id id, to_ast_mpat k_env def_ord mfp),(l,())))
+                 mfpats, false)
     | Parse_ast.MP_vector(mpats) -> MP_vector(List.map (to_ast_mpat k_env def_ord) mpats)
     | Parse_ast.MP_vector_concat(mpats) -> MP_vector_concat(List.map (to_ast_mpat k_env def_ord) mpats)
     | Parse_ast.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat k_env def_ord) mpats)
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index d845265f..3969663a 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -424,7 +424,7 @@ type mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only
  | MP_lit of lit
  | MP_id of id
  | MP_app of id * ( mpat) list
- | MP_record of ( fpat) list * bool
+ | MP_record of ( mfpat) list * bool
  | MP_vector of ( mpat) list
  | MP_vector_concat of ( mpat) list
  | MP_tup of ( mpat) list
@@ -435,6 +435,12 @@ type mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only
 and mpat =
  | MP_aux of ( mpat_aux) * l
 
+and mfpat_aux =  (* Mapping field pattern, why does this have to exist *)
+ | MFP_mpat of id * mpat
+
+and mfpat =
+ | MFP_aux of mfpat_aux * l
+
 type mpexp_aux =
  | MPat_pat of ( mpat)
  | MPat_when of ( mpat) * ( exp)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8a222431..c1d5f1cb 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3386,9 +3386,112 @@ let merge_funcls (Defs defs) =
     | d -> d
   in Defs (List.map merge_in_def defs)
 
+
+let rec exp_of_mpat (MP_aux (mpat, annot)) =
+  let empty_vec = E_aux (E_vector [], annot) in
+  let concat_vectors annot vec1 vec2 = (* TODO FIXME, this should be OK for typing but doesn't attach location information properly *)
+    E_aux (E_vector_append (vec1, vec2), annot)
+  in
+  match mpat with
+  | MP_lit lit                      -> E_aux (E_lit lit, annot)
+  | MP_id id                        -> E_aux (E_id id, annot)
+  | MP_app (id, args)               -> E_aux (E_app (id, (List.map exp_of_mpat args)), annot)
+  | MP_record (mfpats, flag)        -> E_aux (E_record (fexps_of_mfpats mfpats flag annot), annot)
+  | MP_vector mpats                 -> E_aux (E_vector (List.map exp_of_mpat mpats), annot)
+  | MP_vector_concat mpats          -> List.fold_right (concat_vectors annot) (List.map exp_of_mpat mpats) empty_vec
+  | MP_tup mpats                    -> E_aux (E_tuple (List.map exp_of_mpat mpats), annot)
+  | MP_list mpats                   -> E_aux (E_list (List.map exp_of_mpat mpats), annot)
+  | MP_cons (mpat1, mpat2)          -> E_aux (E_cons (exp_of_mpat mpat1, exp_of_mpat mpat2), annot)
+  | MP_string_append (mpat1, mpat2) -> E_aux (E_app (mk_id "string_append", [exp_of_mpat mpat1; exp_of_mpat mpat2]), annot)
+
+and fexps_of_mfpats mfpats flag annot =
+  let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
+    FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot)
+  in
+  FES_aux (FES_Fexps (List.map fexp_of_mfpat mfpats, flag), annot)
+
+let rec pat_of_mpat (MP_aux (mpat, annot)) =
+  match mpat with
+  | MP_lit lit                      -> P_aux (P_lit lit, annot)
+  | MP_id id                        -> P_aux (P_id id, annot)
+  | MP_app (id, args)               -> P_aux (P_app (id, (List.map pat_of_mpat args)), annot)
+  | MP_record (mfpats, flag)        -> P_aux (P_record ((fpats_of_mfpats mfpats), flag), annot)
+  | MP_vector mpats                 -> P_aux (P_vector (List.map pat_of_mpat mpats), annot)
+  | MP_vector_concat mpats          -> P_aux (P_vector_concat (List.map pat_of_mpat mpats), annot)
+  | MP_tup mpats                    -> P_aux (P_tup (List.map pat_of_mpat mpats), annot)
+  | MP_list mpats                   -> P_aux (P_list (List.map pat_of_mpat mpats), annot)
+  | MP_cons (mpat1, mpat2)          -> P_aux ((P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2), annot))
+  | MP_string_append (mpat1, mpat2) -> P_aux ((P_string_append (pat_of_mpat mpat1, pat_of_mpat mpat2), annot))
+
+and fpats_of_mfpats mfpats =
+  let fpat_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
+    FP_aux (FP_Fpat (id, pat_of_mpat mpat), annot)
+  in
+  List.map fpat_of_mfpat mfpats
+
+let rewrite_defs_realise_mappings (Defs defs) =
+  let realise_mpexps forwards mpexp1 mpexp2 =
+    let mpexp_pat, mpexp_exp =
+      if forwards then mpexp1, mpexp2
+      else mpexp2, mpexp1
+    in
+    let exp =
+      match mpexp_exp with
+      | MPat_aux ((MPat_pat mpat), _) -> exp_of_mpat mpat
+      | MPat_aux ((MPat_when (mpat, _), _)) -> exp_of_mpat mpat
+    in
+    match mpexp_pat with
+    | MPat_aux (MPat_pat mpat, annot) -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
+    | MPat_aux (MPat_when (mpat, guard), annot) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)
+  in
+  let realise_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
+    let pexp = realise_mpexps forwards mpexp1 mpexp2 in
+    FCL_aux (FCL_Funcl (id, pexp), (l, ()))
+  in
+  let realise_mapdef (MD_aux (MD_mapping (id, mapcls), ((l, (tannot:tannot)) as annot))) =
+    let forwards_id = mk_id (string_of_id id ^ "_forwards#") in
+    let backwards_id = mk_id (string_of_id id ^ "_backwards#") in
+    let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
+    let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+    let env = match mapcls with
+      | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot
+      | _ -> Type_check.typ_error l "mapping with no clauses?"
+    in
+    let (typq, bidir_typ) = Env.get_val_spec id env in
+    let forwards_typ = match bidir_typ with
+      | Typ_aux (Typ_bidir (typ1, typ2), l) -> Typ_aux (Typ_fn (typ1, typ2, no_effect), l)
+      | _ -> Type_check.typ_error l "non-bidir type of mapping?"
+    in
+    let backwards_typ = match bidir_typ with
+      | Typ_aux (Typ_bidir (typ1, typ2), l) -> Typ_aux (Typ_fn (typ2, typ1, no_effect), l)
+      | _ -> Type_check.typ_error l "non-bidir type of mapping?"
+    in
+    (* let env = Env.update_val_spec forwards_id (typq, forwards_typ) env in
+     * let env = Env.update_val_spec backwards_id (typq, backwards_typ) env in *)
+    let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let forwards_spec, env = Type_check.check_val_spec env forwards_spec in
+    let backwards_spec, env = Type_check.check_val_spec env backwards_spec in
+    let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
+    let forwards_fun : unit fundef = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl true forwards_id) mapcls)), (l, ()))) in
+    let backwards_fun : unit fundef = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl false backwards_id) mapcls)), (l, ()))) in
+    Printf.printf "%s\n%!" (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string);
+    Printf.printf "%s\n%!" (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string);
+    let forwards_fun, _ = Type_check.check_fundef env forwards_fun in
+    let backwards_fun, _ = Type_check.check_fundef env backwards_fun in
+    forwards_spec @ forwards_fun @ backwards_spec @ backwards_fun
+  in
+  let rewrite_def def =
+    match def with
+    | DEF_mapdef mdef -> realise_mapdef mdef
+    | d -> [d]
+  in
+  Defs (List.map rewrite_def defs |> List.flatten)
+
 let recheck_defs defs = fst (check initial_env defs)
 
 let rewrite_defs_lem = [
+  ("realise_mappings", rewrite_defs_realise_mappings);
   ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
@@ -3424,6 +3527,7 @@ let rewrite_defs_lem = [
 let rewrite_defs_ocaml = [
     (* ("undefined", rewrite_undefined); *)
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("realise_mappings", rewrite_defs_realise_mappings);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("pat_lits", rewrite_defs_pat_lits);
   ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
@@ -3444,6 +3548,7 @@ let rewrite_defs_ocaml = [
 
 let rewrite_defs_c = [
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("realise_mappings", rewrite_defs_realise_mappings);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("pat_lits", rewrite_defs_pat_lits);
   ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
@@ -3462,6 +3567,7 @@ let rewrite_defs_c = [
 
 let rewrite_defs_interpreter = [
     ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+    ("realise_mappings", rewrite_defs_realise_mappings);
     ("pat_string_append", rewrite_defs_pat_string_append);
     ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
     ("tuple_assignments", rewrite_tuple_assignments);
diff --git a/src/type_check.ml b/src/type_check.ml
index f7668f21..0eaec4f8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2156,6 +2156,7 @@ let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l,
 
 let strip_mpat : 'a mpat -> unit mpat = function mpat -> map_mpat_annot (fun (l, _) -> (l, ())) mpat
 let strip_mpexp : 'a mpexp -> unit mpexp = function mpexp -> map_mpexp_annot (fun (l, _) -> (l, ())) mpexp
+let strip_mapcl : 'a mapcl -> unit mapcl = function mapcl -> map_mapcl_annot (fun (l, _) -> (l, ())) mapcl
 
 let fresh_var =
   let counter = ref 0 in
@@ -2610,8 +2611,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           end
        | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f)
      end
-  | P_app (f, _) when not (Env.is_union_constructor f env) ->
-     typ_error l (string_of_id f ^ " is not a union constructor in pattern " ^ string_of_pat pat)
+  | P_app (f, _) when (not (Env.is_union_constructor f env) && not (Env.is_mapping f env)) ->
+     typ_error l (string_of_id f ^ " is not a union constructor or mapping in pattern " ^ string_of_pat pat)
   | P_as (pat, id) ->
      let (typed_pat, env, guards) = bind_pat env pat typ in
      annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env, guards
diff --git a/src/type_check.mli b/src/type_check.mli
index 9507302d..d74e9562 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -209,6 +209,9 @@ val strip_pexp : 'a pexp -> unit pexp
 (** Strip the type annotations from an l-expression *)
 val strip_lexp : 'a lexp -> unit lexp
 
+val strip_mpexp : 'a mpexp -> unit mpexp
+val strip_mapcl : 'a mapcl -> unit mapcl
+
 (** {2 Checking expressions and patterns} *)
 
 (** Check an expression has some type. Returns a fully annotated
@@ -223,6 +226,10 @@ val infer_exp : Env.t -> unit exp -> tannot exp
 
 val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp
 
+val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t
+
+val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t  
+
 val prove : Env.t -> n_constraint -> bool
 
 val solve : Env.t -> nexp -> Big_int.num option
@@ -236,6 +243,8 @@ val bind_pat : Env.t -> unit pat -> typ -> tannot pat * Env.t * unit Ast.exp lis
    on patterns that have previously been type checked. *)
 val bind_pat_no_guard : Env.t -> unit pat -> typ -> tannot pat * Env.t
 
+val typ_error : Ast.l -> string -> 'a
+
 (** {2 Destructuring type annotations} Partial functions: The
    expressions and patterns passed to these functions must be
    guaranteed to have tannots of the form Some (env, typ) for these to
@@ -247,6 +256,7 @@ val env_of_annot : Ast.l * tannot -> Env.t
 val typ_of : tannot exp -> typ
 val typ_of_annot : Ast.l * tannot -> typ
 
+
 val pat_typ_of : tannot pat -> typ
 val pat_env_of : tannot pat -> Env.t