scattered mappings

4 files changed, 39 insertions, 2 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 6f131e63..51820b29 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -894,6 +894,27 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
           | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,unit,effects_opt,[]),(l,())))),false) in
                     (No_def,envs),((id,(partial_def,k_local))::partial_defs)
           | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
+      | Parse_ast.SD_scattered_mapping id ->
+         let id = to_ast_id id in
+         let _,_,k_local = to_ast_tannot_opt k_env def_ord (Parse_ast.Typ_annot_opt_aux (Parse_ast.Typ_annot_opt_none, Parse_ast.Unknown)) in
+         (match (def_in_progress id partial_defs) with
+          | None -> let partial_def = ref ((DEF_mapdef(MD_aux(MD_mapping(id, []), (l, ())))), false) in
+                    (No_def,envs),((id,(partial_def,k_local))::partial_defs)
+          | Some(d,k) -> typ_error l "Scattered mapping definition header name already in use by scattered definition" (Some id) None None)
+
+      | Parse_ast.SD_scattered_mapcl (id, mapcl) ->
+         let id = to_ast_id id in
+         (match (def_in_progress id partial_defs) with
+          | None -> typ_error l "Scattered mapping definition clause does not match any existing mapping definition headers" (Some id) None None
+          | Some (d, k) ->
+             (match !d with
+              | DEF_mapdef(MD_aux(MD_mapping(_,mcls),ml)),false ->
+                 let (MCL_aux (mapcl_aux, _)) = to_ast_mapcl (names,k_env,def_ord) mapcl in
+                 d := DEF_mapdef(MD_aux(MD_mapping(id, mcls @ [MCL_aux (mapcl_aux, (l, ()))]), ml)), false;
+                 (No_def,envs),partial_defs
+              | _, true -> typ_error l "Scattered mapping definition clause extends ended definition" (Some id) None None
+              | _ -> typ_error l "Scattered mapping definition doesn't match existing definition header" (Some id) None None))
+
       | Parse_ast.SD_scattered_funcl(funcl) ->
          (match funcl with
           | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_),_) ->
@@ -945,6 +966,9 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
               | (DEF_fundef(_) as def),false ->
                  d:= (def,true);
                  ((Finished def), envs),partial_defs
+              | (DEF_mapdef(_) as def),false ->
+                 d := (def,true);
+                 ((Finished def), envs),partial_defs
               | _, true ->
                  typ_error l "Scattered definition ended multiple times" (Some id) None None
               | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b34ba1d2..a6b519e5 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -498,6 +498,8 @@ scattered_def_aux =  (* Function and type union definitions that can be spread a
  | SD_scattered_funcl of funcl (* scattered function definition clause *)
  | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
  | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_mapping of id
+ | SD_scattered_mapcl of id * mapcl
  | SD_scattered_end of id (* scattered definition end *)
 
 
diff --git a/src/parser.mly b/src/parser.mly
index e1c6bd12..23516068 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1327,6 +1327,8 @@ scattered_def:
     { mk_sd (SD_scattered_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos }
   | Function_ id
     { mk_sd (SD_scattered_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
+  | Mapping id
+    { mk_sd (SD_scattered_mapping $2) $startpos $endpos }  
 
 scattered_clause:
   | Doc Function_ Clause funcl
@@ -1334,6 +1336,7 @@ scattered_clause:
   | Function_ Clause funcl
     { mk_sd (SD_scattered_funcl $3) $startpos $endpos }
 
+
 def:
   | fun_def
     { DEF_fundef $1 }
@@ -1359,6 +1362,8 @@ def:
     { DEF_scattered $1 }
   | Union Clause id Eq type_union
     { DEF_scattered (mk_sd (SD_scattered_unioncl ($3, $5)) $startpos $endpos) }
+  | Mapping Clause id Eq mapcl
+    { DEF_scattered (mk_sd (SD_scattered_mapcl ($3, $5)) $startpos $endpos) }
   | End id
     { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) }
   | default_def
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e9afd415..69d35da6 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2851,7 +2851,10 @@ let rec rewrite_defs_pat_string_append =
                                         pat2 => expr
                                       }
      *)
-    | P_aux (P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _) :: pats), psa_annot) ->
+    | P_aux (P_string_append (
+                 P_aux (P_lit (L_aux (L_string s, _) as lit), _)
+                 :: pats
+               ), psa_annot) ->
 
        let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in
        stringappend_counter := !stringappend_counter + 1;
@@ -2891,7 +2894,10 @@ let rec rewrite_defs_pat_string_append =
                                               pat2 => expr
                                             }
      *)
-    | P_aux (P_string_append (P_aux (P_app (Id_aux (Id builtin_id, _), [P_aux (P_id (Id_aux (Id var_id, _)), _)] ) , _) :: pats), psa_annot)
+    | P_aux (P_string_append (
+                 P_aux (P_app (Id_aux (Id builtin_id, _), [P_aux (P_id (Id_aux (Id var_id, _)), _)] ) , _)
+                 :: pats
+               ), psa_annot)
          when List.mem_assoc builtin_id builtins ->
 
        (* common things *)