Pattern matching for literals

src/ConETypeErase.ml

@@ -27,7 +27,7 @@ let rec tr_expr (e : S.expr) =
   match e with
   | EUnitPrf | EBoolPrf | EOptionPrf -> assert false
 
-  | ENum _ | ENum64 _ | EStr _ | EChr _ | EVar _ | EExtern _ ->
+  | ELit _ | EVar _ | EExtern _ ->
     let^ v = tr_expr_v e in
     T.EValue v
 
@@ -78,10 +78,8 @@ and tr_expr_v (e : S.expr) =
   match e with
   | EUnitPrf | EBoolPrf | EOptionPrf -> assert false
 
-  | ENum   n        -> return (T.VLit (LNum n))
-  | ENum64 n        -> return (T.VLit (LNum64 n))
-  | EStr   s        -> return (T.VLit (LStr s))
-  | EChr   c        -> return (T.VLit (LNum (Char.code c)))
+  | ELit   l        -> tr_expr_lit l
+
   | EVar   x        -> return (T.VVar x)
 
   | EExtern(name, _) -> return (T.VExtern name)
@@ -105,6 +103,14 @@ and tr_expr_vs es =
     let* vs = tr_expr_vs es in
     return (v :: vs)
 
+(** Translate a literal *)
+and tr_expr_lit (l : S.literal) =
+  match l with
+  | ENum   n      -> return (T.VLit (LNum n))
+  | ENum64 n      -> return (T.VLit (LNum64 n))
+  | EStr   s      -> return (T.VLit (LStr s))
+  | EChr   c      -> return (T.VLit (LNum (Char.code c)))
+
 (** Translate a recursive definition *)
 and tr_rec_def (rd : S.rec_def) =
   (rd.rd_var, tr_expr rd.rd_body)

src/DblParser/Attributes.ml

@@ -36,6 +36,7 @@ let rec make_vis_pattern (pt : Lang.Surface.pattern) =
   map_node begin function
   | PWildcard -> PWildcard
   | PId (_, ident) -> PId (true, ident)
+  | PLit l -> PLit l
   | PAnnot (pt, scheme) -> PAnnot (make_vis_pattern pt, scheme)
   | PCtor (pth, xs, ys) -> 
     PCtor 

src/DblParser/Desugar.ml

@@ -307,10 +307,10 @@ let rec tr_pattern (p : Raw.expr) =
   | EWildcard   -> make PWildcard
   | EUnit | ECtor _ | ESelect _ ->
     make (PCtor(tr_ctor_pattern p, [], []))
-  | ENum _      -> Error.fatal (Error.desugar_error p.pos)
-  | ENum64 _      -> Error.fatal (Error.desugar_error p.pos)
-  | EStr _      -> Error.fatal (Error.desugar_error p.pos)
-  | EChr _      -> Error.fatal (Error.desugar_error p.pos)
+  | ENum      n -> make (PLit (ENum n))
+  | ENum64    n -> make (PLit (ENum64 n))
+  | EStr      s -> make (PLit (EStr s))
+  | EChr      c -> make (PLit (EChr c))
   | EInterp _   -> Error.fatal (Error.desugar_error p.pos)
   | EParen    p -> make (tr_pattern p).data
   | EVar      x -> make (PId(false, IdVar x))
@@ -546,10 +546,10 @@ and tr_expr (e : Raw.expr) =
   | EParen e       -> make (tr_expr e).data
   | EUnit | EVar _ | EImplicit _ | ECtor _ | EMethod _ | EBOpID _ | EUOpID _ ->
     make (EPoly(tr_poly_expr e, []))
-  | ENum n -> make (ENum n)
-  | ENum64 n -> make (ENum64 n)
-  | EStr s -> make (EStr s)
-  | EChr c -> make (EChr c)
+  | ENum n -> make (ELit(ENum n))
+  | ENum64 n -> make (ELit(ENum64 n))
+  | EStr s -> make (ELit(EStr s))
+  | EChr c -> make (ELit(EChr c))
   | EInterp (s, xs) ->
     let tr_toString (expr : Raw.expr) (fmt : Raw.expr option) = 
       let mth = { pos = expr.pos; data = (Raw.EMethod (expr, "toString"))} in

src/DblParser/Import.ml

@@ -154,7 +154,7 @@ let define_module_path path =
   let open Lang.Surface in
   let make data = { pos = Position.nowhere; data } in
   make (DLetId(false, IdImplicit "~__modulePath__",
-    make (PE_Expr (make (EStr path)))))
+  make (PE_Expr (make (ELit(EStr path))))))
 
 let import_many imported imports =
   let mk_mod_def (n, imports, (d : File.def_list)) =

src/EffectInference/Expr.ml

@@ -313,21 +313,24 @@ and infer_type : type ed.
       T.Type.subst sub sch.sch_body,
       return_pure eff_req )
 
-  | ENum n ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_int) in
-    (T.ENum n, tp, return_pure eff_req)
-
-  | ENum64 n ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_int64) in
-    (T.ENum64 n, tp, return_pure eff_req)
-
-  | EStr s ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_string) in
-    (T.EStr s, tp, return_pure eff_req)
-
-  | EChr c ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_char) in
-    (T.EChr c, tp, return_pure eff_req)
+  | ELit l -> 
+    begin match l with
+    | ENum n ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_int) in
+      (T.ELit(ENum n), tp, return_pure eff_req)
+
+    | ENum64 n ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_int64) in
+      (T.ELit(ENum64 n), tp, return_pure eff_req)
+
+    | EStr s ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_string) in
+      (T.ELit(EStr s), tp, return_pure eff_req)
+
+    | EChr c ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_char) in
+      (T.ELit(EChr c), tp, return_pure eff_req)
+    end
 
   | EFn(x, sch, body, _) ->
     let sch = Type.tr_scheme_expr env sch in

src/EffectInference/ExprUtils.ml

@@ -144,8 +144,7 @@ let mk_rec_ctx ~evs ~cs ~targs ~named all_defs =
 
 let rec update_rec_body ~rec_ctx (e : T.expr) : T.expr =
   match e with
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ 
-  | EExtern _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EExtern _ ->
     e
 
   | EVar x ->

src/EffectInference/Pattern.ml

@@ -76,6 +76,7 @@ end
 type t =
   | PWildcard
   | PAs       of t * T.var
+  | PLit      of T.literal 
   | PCtor     of
       { name  : string;
         idx   : int;
@@ -105,7 +106,7 @@ let open_tvars env targs tvars =
 
 let rec check_type env (pat : S.pattern) tp =
   match pat.data with
-  | PWildcard | PAnnot _ | POr _ ->
+  | PWildcard | PLit _ | PAnnot _ | POr _ ->
     check_scheme env pat (T.Scheme.of_type tp)
 
   | PAs(pat, x) ->
@@ -186,6 +187,32 @@ and check_scheme env (pat : S.pattern) sch =
   match pat.data with
   | PWildcard -> (PWildcard, PEnv.empty)
 
+  | PLit l ->
+    let check_lit_scheme lit_tp =
+      begin match T.Scheme.to_type sch with
+      | Some tp ->
+          begin match T.Type.view tp, T.Type.view lit_tp with
+          | TVar x, TVar y -> assert (T.TVar.equal x y)
+          | _, _ -> assert false
+          end
+      | None -> assert false
+      end
+    in
+    begin match l with
+    | ENum n ->
+      check_lit_scheme (T.Type.t_var T.BuiltinType.tv_int);
+      (PLit (ENum n), PEnv.empty)
+    | ENum64 n ->
+      check_lit_scheme (T.Type.t_var T.BuiltinType.tv_int64);
+      (PLit (ENum64 n), PEnv.empty)
+    | EStr s ->
+      check_lit_scheme (T.Type.t_var T.BuiltinType.tv_string);
+      (PLit (EStr s), PEnv.empty)
+    | EChr c ->
+      check_lit_scheme (T.Type.t_var T.BuiltinType.tv_char);
+      (PLit (EChr c), PEnv.empty)
+    end
+
   | PAs(pat, x) ->
     let (pat, penv) = check_scheme env pat sch in
     (PAs(pat, x), PEnv.add_var penv x sch)

src/EffectInference/Pattern.mli

@@ -34,6 +34,7 @@ end
 type t =
   | PWildcard
   | PAs       of t * T.var
+  | PLit      of T.literal 
   | PCtor     of
       { name  : string;
         idx   : int;

src/EffectInference/PatternMatch.ml

@@ -98,7 +98,7 @@ let rec simplify_head x (cl : iclause) =
   | POr(pat1, pat2) :: pats ->
     simplify_head x { cl with c_patterns = pat1 :: pats } @
     simplify_head x { cl with c_patterns = pat2 :: pats }
-  | (PWildcard | PCtor _) :: _ -> [cl]
+  | (PWildcard | PLit _ | PCtor _) :: _ -> [cl]
 
 (** Normalize patterns at head position by simplifying as-patterns and
     expanding or-patterns in given clause list *)
@@ -119,6 +119,8 @@ let simplify_ctor idx (ctor : T.ctor_decl) tvs cl =
     let pats2 = List.map (fun _ -> Pattern.PWildcard) ctor.ctor_arg_schemes in
     Some { cl with c_patterns = pats1 @ pats2 @ pats }
 
+  | PLit _ :: _  -> assert false
+
   | PCtor pc :: pats when pc.idx = idx ->
     assert (List.length pc.tvars = List.length tvs);
     assert (List.length pc.named = List.length ctor.ctor_named);
@@ -146,6 +148,10 @@ type column_class =
   | CC_Wildcard
     (** All patterns wild-cards *)
 
+  | CC_Lit of T.literal list
+    (** There is a literal pattern in the column. It stores the list of all
+      literals. *)
+
   | CC_ADT of T.expr * T.ctor_decl list
     (** There is a constructor pattern in the column. It stores computationally
       irrelevant proof of the shape of the constructor and the list of all
@@ -160,6 +166,21 @@ let rec column_class (cls : iclause list) =
     begin match cl.c_patterns with
     | [] -> assert false
     | PWildcard :: _ -> column_class cls
+    | PLit lit :: _ -> 
+      let rec collect acc cls = 
+        match cls with
+        | [] -> acc
+        | cl :: cls ->
+          (match cl.c_patterns with
+          | [] -> assert false
+          | PWildcard :: _ -> collect acc cls
+          | PLit l :: _ ->
+              if List.exists (fun x -> x = l) acc
+              then collect acc cls
+              else collect (l :: acc) cls
+          | (PCtor _ | PAs (_, _) | POr(_, _)) :: _ -> assert false)
+      in
+      CC_Lit (collect [lit] cls)
     | PCtor cp :: _ -> CC_ADT(cp.proof, cp.ctors)
     | PAs _ :: _ | POr _ :: _ ->
       (* As-patterns and or-patterns should be already simplified *)
@@ -199,11 +220,85 @@ module Make(Ctx : MatchContext) = struct
       | CC_Wildcard ->
         tr_match (refocus ctx) xs (List.map drop_wildcard cls)
 
+      | CC_Lit(lits) ->
+        tr_match_lit ctx x xs cls lits
+
       | CC_ADT(proof, ctors) ->
         let match_cls = List.mapi (tr_match_clause ctx xs cls) ctors in
         T.EMatch(proof, T.EVar x, match_cls, Ctx.res_tp, Ctx.res_eff)
       end
 
+  and make_eq_type (lit: T.literal) = 
+    let tp_lit = 
+      match lit with 
+      | ENum n   -> T.Type.t_var T.BuiltinType.tv_int
+      | ENum64 n -> T.Type.t_var T.BuiltinType.tv_int64
+      | EStr s   -> T.Type.t_var T.BuiltinType.tv_string
+      | EChr c   -> T.Type.t_var T.BuiltinType.tv_char
+    in 
+    let tp_bool = T.Type.t_var T.BuiltinType.tv_bool in
+    let sch_lit = T.Scheme.of_type tp_lit in
+    let inner = T.Type.t_arrow sch_lit tp_bool T.Pure
+    in
+    T.Type.t_arrow sch_lit inner T.Pure 
+
+  and make_eq_expr (x : T.expr) (lit : T.literal) : T.expr =
+    let eq_tp = make_eq_type lit in
+    match lit with
+    | ENum n ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqInt", eq_tp), x), T.ELit(ENum n))
+    | ENum64 n ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqInt64", eq_tp), x), T.ELit(ENum64 n))
+    | EStr s ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqStr", eq_tp), x), T.ELit(EStr s))
+    | EChr c ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqInt", eq_tp), x), T.ELit(EChr c))
+
+  and make_eq_match x lit then_e else_e =
+    let cond = make_eq_expr(T.EVar x) lit in
+    let cl_true =
+      { T.cl_tvars = [];
+        T.cl_vars  = [];
+        T.cl_body  = then_e 
+      } in
+    let cl_false =
+      { T.cl_tvars = [];
+        T.cl_vars  = [];
+        T.cl_body  = else_e 
+      } in
+    T.EMatch(T.EBoolPrf, cond, [cl_false; cl_true], Ctx.res_tp, Ctx.res_eff)
+
+  (** Build a match clause for a literal *)
+  and tr_match_lit ctx x xs cls lits =
+    let is_default cl = 
+      match cl.c_patterns with
+      | (PWildcard | PAs _)  :: _ -> true
+      | _ -> false 
+    in
+    let drop cl =
+      match cl.c_patterns with
+      | _ :: pats -> { cl with c_patterns = pats }
+      | [] -> assert false
+    in
+    let default_cls = List.filter is_default cls in
+    let default_branch =
+      match default_cls with
+      | [] -> Error.fatal (Error.non_exhaustive_match ~pos:Ctx.pos ctx)
+      | _ -> tr_match (refocus ctx) xs (List.map drop default_cls)
+    in
+    List.fold_right (fun lit acc ->
+      let cls_lit =
+      List.filter (fun cl ->
+        match cl.c_patterns with
+        | PLit l :: _ -> (l = lit)
+        | PWildcard :: _ -> true
+        | _ -> false)
+      cls
+    in
+    let branch = tr_match (refocus ctx) xs (List.map drop cls_lit) in
+    make_eq_match x lit branch acc)
+    lits default_branch
+
   (** Build a match clause for a single constructor. *)
   and tr_match_clause ctx xs cls idx (ctor : T.ctor_decl) =
     let tvs =

src/Lang/ConE.mli

@@ -116,17 +116,8 @@ type data_def =
         (** Effect of the delimiter *)
     }
 
-(** Expressions *)
-type expr =
-  | EUnitPrf
-    (** ADT-shape proof for unit type *)
-
-  | EBoolPrf
-    (** ADT-shape proof for bool type *)
-
-  | EOptionPrf
-    (** ADT-shape proof for option type *)
-
+(** Literals *)
+and literal =
   | ENum of int
     (** Integer literal *)
 
@@ -139,6 +130,20 @@ type expr =
   | EChr of char
     (** Character literal *)
 
+(** Expressions *)
+type expr =
+  | EUnitPrf
+    (** ADT-shape proof for unit type *)
+
+  | EBoolPrf
+    (** ADT-shape proof for bool type *)
+
+  | EOptionPrf
+    (** ADT-shape proof for option type *)
+
+  | ELit of literal
+    (** Literal *)
+
   | EVar of var
     (** Variable *)