allowed TiML typechecker to mention types defined in pre-determined m…

…odules; changing strings from primitive type to user-defined type using array
wangpengmit · Apr 10, 2018 · cd3fd9b · cd3fd9b
1 parent f3162ef
commit cd3fd9b
Show file tree

Hide file tree

Showing 28 changed files with 153 additions and 151 deletions.
diff --git a/base-types.sml b/base-types.sml
@@ -1,16 +1,18 @@
 structure BaseTypes = struct
 datatype base_type =
          Int
-         | String
          | Bool
+         | Byte
+         (* | String *)
 
 fun eq_base_type (t : base_type, t') = t = t'
 
 fun str_bt bt =
   case bt of
       Int => "int"
-    | String => "string"
     | Bool => "bool"
+    | Byte => "byte"
+    (* | String => "string" *)
 
 end
 
diff --git a/elaborate.sml b/elaborate.sml
@@ -165,10 +165,12 @@ local
                   Unit r
                 else if x = "int" then
                   BaseType (Int, r)
-                else if x = "string" then
-                  BaseType (String, r)
                 else if x = "bool" then
                   BaseType (Bool, r)
+                else if x = "byte" then
+                  BaseType (Byte, r)
+                (* else if x = "string" then *)
+                (*   BaseType (String, r) *)
                 else if x = "_" then
                   UVar ((), r)
                 else
@@ -293,7 +295,7 @@ local
                 (* else if x = "never" andalso eia = false then *)
                 (*   ENever (elab_mt (S.VarT (NONE, ("_", r))), r) *)
                 else if x = "__&empty_array" andalso eia = false then
-                  ET (ETEmptyArray, elab_mt (S.VarT (NONE, ("_", r))), r)
+                  EEmptyArray (elab_mt (S.VarT (NONE, ("_", r))), r)
                 else if x = "__&builtin" then raise Error (r, "should be '__&builtin \"name\"'")
                 else
                   def ()
@@ -330,24 +332,26 @@ local
 	| S.Let (return, decs, e, r) =>
           ELet (elab_return return, Unbound.Bind (Teles $ map elab_decl decs, elab e), r)
 	| S.Const (c, r) =>
-          let
-            fun unescape s =
-              let
-                val ls = String.explode s
-                fun loop (ls, acc) =
-                  case ls of
-                      #"\\" :: #"n" :: ls => loop (ls, #"\n" :: acc)
-                    | c :: ls => loop (ls, c :: acc)
-                    | [] => acc
-              in
-                String.implode $ rev $ loop (ls, [])
-              end
-          in
-            case c of
+            (case c of
                 S.ECInt n => EConstInt (n, r)
 	      | S.ECNat n => EConstNat (n, r)
-	      | S.ECString s => EConstString (unescape s, r)
-          end
+	      | S.ECString s =>
+                let
+                  fun unescape s =
+                    let
+                      val ls = String.explode s
+                      fun loop (ls, acc) =
+                        case ls of
+                            #"\\" :: #"n" :: ls => loop (ls, #"\n" :: acc)
+                          | c :: ls => loop (ls, c :: acc)
+                          | [] => acc
+                    in
+                      String.implode $ rev $ loop (ls, [])
+                    end
+                  val s = unescape s
+                in
+                  ENewArrayValues (BaseType (Byte, r), map (fn c => EByte (c, r)) $ String.explode s, r)
+                end)
 	| S.BinOp (EBApp, e1, e2, r) =>
 	  let 
 	    fun default () = EApp (elab e1, elab e2)
@@ -359,10 +363,11 @@ local
 		     if x = "__&fst" then EFst (elab e2, r)
 		     else if x = "__&snd" then ESnd (elab e2, r)
 		     else if x = "__&not" then EUnOp (EUPrim EUPBoolNeg, elab e2, r)
-		     else if x = "__&int2str" then EUnOp (EUInt2Str, elab e2, r)
+		     (* else if x = "__&int2str" then EUnOp (EUInt2Str, elab e2, r) *)
 		     else if x = "__&nat2int" then EUnOp (EUNat2Int, elab e2, r)
 		     else if x = "__&array_length" then EUnOp (EUArrayLen, elab e2, r)
-		     else if x = "__&print" then EUnOp (EUPrint, elab e2, r)
+		     (* else if x = "__&print" then EUnOp (EUPrint, elab e2, r) *)
+		     else if x = "__&printc" then EUnOp (EUPrintc, elab e2, r)
                      else if x = "__&builtin" then
                        (case e2 of
                             S.Const (S.ECString s, _) =>

diff --git a/examples/pervasive.timl b/examples/pervasive.timl
@@ -0,0 +1,5 @@
+structure Pervasive = struct
+
+datatype some_nat = SomeNat {n : Nat} of nat {n}
+
+end
diff --git a/examples/stdlib.pkg b/examples/stdlib.pkg
@@ -1,4 +1,5 @@
 (* standard library *)
+pervasive.timl
 basic.timl
 nat.timl
 list.timl

diff --git a/examples/string.timl b/examples/string.timl
@@ -5,7 +5,7 @@ structure String = struct
 
 open Array
 
-datatype string = String {len : Nat} of array char {len}
+datatype string = String {len : Nat} of array byte {len}
 
 new_string "abc" == String (new_array {'a', 'b', 'c'})
 
@@ -45,15 +45,15 @@ fun print s =
     ()
 end
 
-fun nat2chars {d : Nat} {i : Nat | 10 ** d <= i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list char {d+1} using d =
-  ifdec i #< #10 then [nat2char i]
-  else int2char (nat2int i mod 10) :: @nat2chars {d-1} {_} (i #/ 10)
+fun nat2bytes {d : Nat} {i : Nat | 10 ** d <= i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list byte {d+1} using d =
+  ifdec i #< #10 then [nat2byte i]
+  else int2byte (nat2int i mod 10) :: @nat2bytes {d-1} {_} (i #/ 10)
 
 fun int2str i return using 20 =
   let
     val Nat n = int2nat i
   in
-    String (fromList $ rev $ list2ilist chars)
+    String (fromList $ rev $ nat2bytes n)
   end
 
 end
diff --git a/expr-fn.sml b/expr-fn.sml
@@ -39,6 +39,7 @@ datatype expr =
          | EEI of expr_EI * expr * idx
          | EET of expr_ET * expr * mtype
          | ET of expr_T * mtype * region
+         | ENewArrayValues of mtype * expr list * region
 	 | EAbs of (ptrn, expr) bind
 	 | EAbsI of (sort, expr) ibind_anno * region
 	 | EAppConstr of (cvar * bool) * mtype list * idx list * expr * (int * mtype) option

diff --git a/expr-util.sml b/expr-util.sml
@@ -10,14 +10,15 @@ infixr 0 $
 
 val EUFst = EUProj ProjFst
 val EUSnd = EUProj ProjSnd
-val EUInt2Str = EUPrim EUPInt2Str
+(* val EUInt2Str = EUPrim EUPInt2Str *)
 val EBAdd = EBPrim EBPIntAdd
 val EBNatAdd = EBNat EBNAdd
 
 fun ETT r = EConst (ECTT, r)
 fun EConstInt (n, r) = EConst (ECInt n, r)
 fun EConstNat (n, r) = EConst (ECNat n, r)
-fun EConstString (n, r) = EConst (ECString n, r)
+(* fun EConstString (n, r) = EConst (ECString n, r) *)
+fun EByte (c, r) = EConst (ECByte c, r)
 fun EFst (e, r) = EUnOp (EUFst, e, r)
 fun ESnd (e, r) = EUnOp (EUSnd, e, r)
 fun EApp (e1, e2) = EBinOp (EBApp, e1, e2)
@@ -33,6 +34,7 @@ fun EBuiltin (name, t, r) = ET (ETBuiltin name, t, r)
 fun ENew (e1, e2) = EBinOp (EBNew, e1, e2)
 fun ERead (e1, e2) = EBinOp (EBRead, e1, e2)
 fun EWrite (e1, e2, e3) = ETriOp (ETWrite, e1, e2, e3)
+fun EEmptyArray (t, r) = ENewArrayValues (t, [], r)
 
 fun collect_Pair e =
   case e of

diff --git a/expr.sig b/expr.sig
@@ -30,6 +30,7 @@ signature EXPR = sig
            | EEI of Operators.expr_EI * expr * idx
            | EET of Operators.expr_ET * expr * mtype
            | ET of Operators.expr_T * mtype * Region.region
+           | ENewArrayValues of mtype * expr list * Region.region
 	   | EAbs of (ptrn, expr) Unbound.bind
 	   | EAbsI of (sort, expr) Binders.ibind_anno * Region.region
 	   | EAppConstr of (cvar * bool) * mtype list * idx list * expr * (int * mtype) option

diff --git a/get-region.sml b/get-region.sml
@@ -132,6 +132,7 @@ fun get_region_e e =
     | EEI (_, e, i) => combine_region (get_region_e e) (get_region_i i)
     | EET (_, e, t) => combine_region (get_region_e e) (get_region_mt t)
     | ET (_, _, r) => r
+    | ENewArrayValues (_, _, r) => r
     | EAbs bind => get_region_bind get_region_pn get_region_e bind
     | EAbsI (_, r) => r
     | EAppConstr ((x, _), _, _, e, _) => combine_region (get_region_cvar x) (get_region_e e)

diff --git a/micro-timl/cc.sml b/micro-timl/cc.sml
@@ -569,7 +569,6 @@ fun cc e =
       | EAscTime (e, i) => EAscTime (cc e, i)
       | ENever t => ENever (cc_t t)
       | EBuiltin (name, t) => EBuiltin (name, cc_t t)
-      | EEmptyArray t => EEmptyArray (cc_t t)
       | ETriOp (ETWrite, e1, e2, e3) => EWrite (cc e1, cc e2, cc e3)
       | EHalt e => EHalt (cc e)
       | _ => raise Unimpl $ "cc(): " ^ (ExportPP.pp_e_to_string (NONE, NONE) $ ExportPP.export (NONE, NONE) ([], [], [], []) e)

diff --git a/micro-timl/code-gen.sml b/micro-timl/code-gen.sml
@@ -86,7 +86,7 @@ fun cg_c c =
     | ECNat n => WCNat n
     | ECInt n => WCInt n
     | ECBool n => WCBool n
-    | ECString s => raise Impossible $ "cg_c() on ECString"
+    (* | ECString s => raise Impossible $ "cg_c() on ECString" *)
 
 fun cg_v ectx v =
   case v of
@@ -198,16 +198,14 @@ fun cg_e reg_counter (params as (ectx, itctx, rctx)) e =
                 end
               | EUnOp (EUInj (inj, t), v) =>
                 [IInj' (r, inj, cg_v ectx v, cg_t t)]
-              | EConst (ECString s) =>
-                [IString (r, s)]
+              (* | EConst (ECString s) => *)
+              (*   [IString (r, s)] *)
               | EUnOp (EUUnfold, v) =>
                 [IUnfold' (r, cg_v ectx v)]
               | EUnOp (EUTiML opr, v) =>
                 [IUnOp' (cg_expr_un_op opr, r, cg_v ectx v)]
               | EMallocPair (v1, v2) =>
                 [IMallocPair' (r, (cg_v ectx v1, cg_v ectx v2))]
-              | EEmptyArray t =>
-                [IEmptyArray (r, Inner $ cg_t t)]
               | EPairAssign (v1, proj, v2) =>
                 let
                   val r' = fresh_reg ()

diff --git a/micro-timl/cps.sml b/micro-timl/cps.sml
@@ -310,9 +310,6 @@ fun cps (e, t_e) (k, j_k) =
     | S.EBuiltin (name, t) =>
       (* [[ builtin ]](k) = k(builtin) *)
       (k $$ EBuiltin (name, cps_t t), j_k %+ T_1)
-    | S.EEmptyArray t =>
-      (* [[ empty_array ]](k) = let x = empty_array in k(x) *)
-      (k $$ EEmptyArray (cps_t t), j_k %+ T_1)
     | S.ERec bind =>
       (* [[ fix x.e ]](k) = k (fix x. [[e]](id)) *)
       let
@@ -564,8 +561,10 @@ fun cps (e, t_e) (k, j_k) =
                 in
                   (t_e, opr)
                 end
-              | EUTiML EUPrint =>
-                (TString, opr)
+              | EUTiML EUPrintc =>
+                (TByte, opr)
+              (* | EUTiML EUPrint => *)
+              (*   (TString, opr) *)
               | EUTiML EUInt2Str =>
                 (TInt, opr)
       in
@@ -846,7 +845,6 @@ and check_decl e =
          check_value e2;
          check_value e3)
       | EMallocPair _ => ()
-      | EEmptyArray _ => ()
       | EPairAssign (e1, _, e2) =>
         (check_value e1;
          check_value e2)

diff --git a/micro-timl/micro-timl-ex-pp.sml b/micro-timl/micro-timl-ex-pp.sml
@@ -636,16 +636,6 @@ fun pp_e (params as (str_var, str_i, str_s, str_k, pp_t)) s (depth_t, depth) e =
           str ")";
           close_box ()
         )
-      | EEmptyArray t =>
-        (
-          open_hbox ();
-          str "EEmptyArray";
-          space ();
-          str "(";
-          pp_t t;
-          str ")";
-          close_box ()
-        )
       | ENewArrayValues (t, es) =>
         (
           open_vbox ();

diff --git a/micro-timl/micro-timl-ex-util.sml b/micro-timl/micro-timl-ex-util.sml
@@ -22,14 +22,16 @@ fun MakeTUni (name, k, t) = TUni $ TBindAnno ((name, k), t)
 fun TUniKind (name, t) = MakeTUni (name, KType, t)
 fun TUniKind_Many (names, t) = foldr TUniKind t names
 
-val TCString = TCTiML BaseTypes.String
+(* val TCString = TCTiML BaseTypes.String *)
 val TCInt = TCTiML BaseTypes.Int
 val TCBool = TCTiML BaseTypes.Bool
+val TCByte = TCTiML BaseTypes.Byte
 val TUnit = TConst TCUnit
 val TEmpty = TConst TCEmpty
-val TString = TConst TCString
+(* val TString = TConst TCString *)
 val TInt = TConst TCInt
 val TBool = TConst TCBool
+val TByte = TConst TCByte
 fun TSum (t1, t2) = TBinOp (TBSum, t1, t2)
 fun TProd (t1, t2) = TBinOp (TBProd, t1, t2)
 fun TAppIs (t, is) = foldl (swap TAppI) t is

diff --git a/micro-timl/micro-timl-ex.sml b/micro-timl/micro-timl-ex.sml
@@ -31,7 +31,6 @@ datatype ('var, 'idx, 'sort, 'kind, 'ty) expr =
          | ENever of 'ty
          | EBuiltin of string * 'ty
          | ELet of ('var, 'idx, 'sort, 'kind, 'ty) expr * ('var, 'idx, 'sort, 'kind, 'ty) expr ebind
-         | EEmptyArray of 'ty
          | ENewArrayValues of 'ty * ('var, 'idx, 'sort, 'kind, 'ty) expr list
          (* extensions from MicroTiML *)
          | ELetIdx of 'idx * ('var, 'idx, 'sort, 'kind, 'ty) expr ibind
@@ -1132,7 +1131,6 @@ fun default_expr_visitor_vtable
           | EPairAssign data => #visit_EPairAssign vtable this env data
           | EProjProtected data => #visit_EProjProtected vtable this env data
           | EHalt data => #visit_EHalt vtable this env data
-          | EEmptyArray t => EEmptyArray $ #visit_ty vtable this env t
           | ENewArrayValues (t, es) => ENewArrayValues (#visit_ty vtable this env t, visit_list (#visit_expr vtable this) env es)
       end
     fun visit_EVar this env data =
@@ -1932,7 +1930,6 @@ fun is_value e =
     | EVar _ => true (* variables denote values *)
     | ENever _ => true
     | EBuiltin _ => true
-    | EEmptyArray _ => false
     | _ => false
     (* | _ => *)
     (*   case fst $ collect_EAscTypeTime $ fst $ collect_EAppIT e of *)