Adding explicit order to for loops

5 files changed, 49 insertions, 32 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 29bedd12..e7b92019 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -350,7 +350,8 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_app_infix(left,op,right) -> E_app_infix(to_ast_exp k_env left, to_ast_id op, to_ast_exp k_env right)
     | Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env) exps)
     | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3)
-    | Parse_ast.E_for(id,e1,e2,e3,e4) -> E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3, to_ast_exp k_env e4)
+    | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> 
+      E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3,to_ast_order k_env atyp, to_ast_exp k_env e4)
     | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env) exps)
     | Parse_ast.E_vector_indexed(iexps) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps)
     | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env vexp, to_ast_exp k_env exp)
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index f498295c..122fd928 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -590,7 +590,7 @@ and interp_main t_level l_env l_mem exp =
                         | V_lit(L_false) -> interp_main t_level l_env lm els
                         | _ -> (Error "Type error, not provided boolean for if",lm,l_env) end)
                       (fun a -> update_stack a (add_to_top_frame (fun c -> (E_if c thn els))))
-    | E_for id from to_ by exp ->
+    | E_for id from to_ by order exp ->
       resolve_outcome (interp_main t_level l_env l_mem from)
                       (fun from_val lm le ->
                         match from_val with
@@ -608,13 +608,13 @@ and interp_main t_level l_env l_mem exp =
                                                     then (Value(V_lit L_unit),lm,le)
                                                     else interp_main t_level le lm 
                                                       (E_block [(E_let (LB_val_implicit (P_id id) (E_lit (L_num from_num))) exp);
-                                                                (E_for id (E_lit (L_num (from_num + by_num))) (E_lit (L_num to_num)) (E_lit (L_num by_num)) exp)])
+                                                                (E_for id (E_lit (L_num (from_num + by_num))) (E_lit (L_num to_num)) (E_lit (L_num by_num)) order exp)])
                                                   | _ -> (Error "by must be a number",lm,le) end)
-                                                (fun a -> update_stack a (add_to_top_frame (fun b -> (E_for id (E_lit (L_num from_num)) (E_lit (L_num to_num)) b exp))))
+                                                (fun a -> update_stack a (add_to_top_frame (fun b -> (E_for id (E_lit (L_num from_num)) (E_lit (L_num to_num)) b order exp))))
                                             | _ -> (Error "to must be a number",lm,le) end)
-                                           (fun a -> update_stack a (add_to_top_frame (fun t -> (E_for id (E_lit (L_num from_num)) t by exp))))
+                                           (fun a -> update_stack a (add_to_top_frame (fun t -> (E_for id (E_lit (L_num from_num)) t by order exp))))
                         | _ -> (Error "from must be a number",lm,le) end)
-                       (fun a -> update_stack a (add_to_top_frame (fun f -> (E_for id f to_ by exp))))
+                       (fun a -> update_stack a (add_to_top_frame (fun f -> (E_for id f to_ by order exp))))
     | E_case exp pats ->
       resolve_outcome (interp_main t_level l_env l_mem exp)
                       (fun v lm le ->
diff --git a/src/parser.mly b/src/parser.mly
index 7b415ea0..856d3266 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -536,26 +536,33 @@ right_atomic_exp:
     { eloc (E_if($2,$4,$6)) }
   | If_ exp Then exp
     { eloc (E_if($2,$4, eloc (E_lit(lloc L_unit)))) }
-  | Foreach id Id atomic_exp Id atomic_exp By atomic_exp exp
-    { if $3 <> "from" then
+  | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp In typ Rparen exp
+    { if $4 <> "from" then
        raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $5 <> "to" && $5 <> "downto" then
+      if $6 <> "to" then
+       raise (Parse_error_locn ((loc ()),"Missing \"to\" in foreach loop"));
+      eloc (E_for($3,$5,$7,$9,$11,$13)) }
+  | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp
+    { if $4 <> "from" then
+       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
+      if $6 <> "to" && $6 <> "downto" then
        raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
-      let step =
-        if $5 = "to"
-        then $8
-        else eloc (E_app_infix(eloc (E_lit(lloc (L_num 0))), idl (Id "-"), $8)) in
-      eloc (E_for($2,$4,$6,step,$9)) }
-  | Foreach id Id atomic_exp Id atomic_exp exp
-    { if $3 <> "from" then
+      let order =
+        if $6 = "to"
+        then ATyp_aux(ATyp_inc,(locn 6 6))
+        else ATyp_aux(ATyp_dec,(locn 6 6)) in
+      eloc (E_for($3,$5,$7,$9,order,$11)) }
+  | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp
+    { if $4 <> "from" then
        raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $5 <> "to" && $5 <> "downto" then
+      if $6 <> "to" && $6 <> "downto" then
        raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
-      let step =
-        if $5 = "to"
-        then eloc (E_lit(lloc (L_num 1)))
-        else eloc (E_lit(lloc (L_num (-1)))) in
-      eloc (E_for($2,$4,$6,step,$7)) }
+      let step = eloc (E_lit(lloc (L_num 1))) in
+      let ord = 
+        if $6 = "to"
+        then ATyp_aux(ATyp_inc,(locn 6 6))
+        else ATyp_aux(ATyp_dec,(locn 6 6)) in
+      eloc (E_for($3,$5,$7,step,ord,$9)) }
   | letbind In exp
     { eloc (E_let($1,$3)) }
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 285dc56c..236bfc91 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -221,9 +221,9 @@ and pp_exp ppf (E_aux(e,_)) =
   | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
   | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
   | E_if(c,t,e) -> fprintf ppf "@[<0>%a %a @[<1>%a %a@] @[<1>%a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
-  | E_for(id,exp1,exp2,exp3,exp4) ->
-    fprintf ppf "@[<0> %a %a %a %a %a %a %a %a@ @[<1>%a@]@]" 
-      kwd "foreach " pp_id id kwd " from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 pp_exp exp4
+  | E_for(id,exp1,exp2,exp3,order,exp4) ->
+    fprintf ppf "@[<0> %a %a (%a %a %a %a %a %a %a %a)@ @[<1>%a@]@]" 
+      kwd "foreach " pp_id id kwd "from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 kwd "in" pp_ord order pp_exp exp4
   | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]"
   | E_vector_indexed(iexps) -> 
     let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in
@@ -523,9 +523,9 @@ and pp_lem_exp ppf (E_aux(e,_)) =
   | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
   | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
   | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
-  | E_for(id,exp1,exp2,exp3,exp4) ->
-    fprintf ppf "@[<0>(%a %a %a %a %a@ @[<1> %a @])@]" 
-      kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_exp exp4
+  | E_for(id,exp1,exp2,exp3,order,exp4) ->
+    fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" 
+      kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
   | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
   | E_vector_indexed(iexps) -> 
     let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
diff --git a/src/type_check.ml b/src/type_check.ml
index c6a0d406..a75c690f 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -511,7 +511,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp,[],pure_e))),
        expect_t,Envmap.intersect then_env else_env,then_c@else_c@c1,
        union_effects ef1 (union_effects then_ef else_ef))
-    | E_for(id,from,to_,step,block) -> 
+    | E_for(id,from,to_,step,order,block) -> 
       (* TODO::: This presently assumes increasing; this should be checked if that's the assumption we want *)
       let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in
       let ft,tt,st = {t=Tapp("enum",[TA_nexp fb;TA_nexp fr])},
@@ -519,10 +519,19 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let from',from_t,_,from_c,from_ef = check_exp envs ft from in
       let to_',to_t,_,to_c,to_ef = check_exp envs tt to_ in
       let step',step_t,_,step_c,step_ef = check_exp envs st step in
-      let new_annot = Some(([],{t=Tapp("enum",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp,[],pure_e) in
+      let new_annot,local_cs = 
+	match (aorder_to_ord order).order with
+	  | Oinc ->
+	    (Some(([],{t=Tapp("enum",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp,[],pure_e),
+	     [LtEq(l,{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});LtEq(l,fb,tb)])
+	  | Odec ->
+	    (Some(([],{t=Tapp("enum",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp,[],pure_e),
+	     [GtEq(l,{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});GtEq(l,fb,tb)])
+	  | _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic")
+      in
       let (block',b_t,_,b_c,b_ef) = check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot))) expect_t block in
-      (E_aux(E_for(id,from',to_',step',block'),(l,Some(([],b_t),Emp,[],pure_e))),expect_t,Envmap.empty,
-       b_c@from_c@to_c@step_c,(union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef))))
+      (E_aux(E_for(id,from',to_',step',order,block'),(l,Some(([],b_t),Emp,local_cs,pure_e))),expect_t,Envmap.empty,
+       b_c@from_c@to_c@step_c@local_cs,(union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef))))
     | E_vector(es) ->
       let item_t = match expect_t.t with
         | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t