From 1bd4a3f1346d7a3fec0bd087aeba7a7539b402d6 Mon Sep 17 00:00:00 2001 From: lidiapodoluk Date: Wed, 20 May 2026 16:15:56 +0200 Subject: [PATCH 1/2] Added pattern matching for literals --- lib/Base/Types.fram | 2 +- src/ConETypeErase.ml | 10 ++- src/DblParser/Attributes.ml | 1 + src/DblParser/Desugar.ml | 8 +-- src/EffectInference/ExprUtils.ml | 2 +- src/EffectInference/Pattern.ml | 12 +++- src/EffectInference/Pattern.mli | 1 + src/EffectInference/PatternMatch.ml | 105 +++++++++++++++++++++++++++- src/Lang/ConE.mli | 13 +++- src/Lang/ConEPriv/SExprPrinter.ml | 18 +++-- src/Lang/ConEPriv/Syntax.ml | 6 ++ src/Lang/Surface.ml | 15 ++++ src/Lang/Unif.mli | 9 +++ src/Lang/UnifPriv/Ren.ml | 1 + src/Lang/UnifPriv/Syntax.ml | 7 ++ src/ToCore/Main.ml | 15 +++- src/TypeInference/Pattern.ml | 36 ++++++++-- src/TypeInference/RecDefs.ml | 5 +- test/ok/ok0154_literalMatch.fram | 37 ++++++++++ 19 files changed, 278 insertions(+), 25 deletions(-) create mode 100644 test/ok/ok0154_literalMatch.fram diff --git a/lib/Base/Types.fram b/lib/Base/Types.fram index cab416ea..8a5d136f 100644 --- a/lib/Base/Types.fram +++ b/lib/Base/Types.fram @@ -2,7 +2,7 @@ # See LICENSE for details. #} -pub data rec List A = [] | (::) of A, List A +pub data rec List A = [] | (::) of A, List A pub data Pair X Y = (,) of X, Y diff --git a/src/ConETypeErase.ml b/src/ConETypeErase.ml index b7903199..b9788e84 100644 --- a/src/ConETypeErase.ml +++ b/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 _ -> + | ENum _ | ENum64 _ | EStr _ | EChr _ | ELit _ | EVar _ | EExtern _ -> let^ v = tr_expr_v e in T.EValue v @@ -82,6 +82,7 @@ and tr_expr_v (e : S.expr) = | 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 +106,13 @@ 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) diff --git a/src/DblParser/Attributes.ml b/src/DblParser/Attributes.ml index a66fe241..f550ee7f 100644 --- a/src/DblParser/Attributes.ml +++ b/src/DblParser/Attributes.ml @@ -35,6 +35,7 @@ type attr_conf = { let rec make_vis_pattern (pt : Lang.Surface.pattern) = map_node begin function | PWildcard -> PWildcard + | PLit l -> PLit l | PId (_, ident) -> PId (true, ident) | PAnnot (pt, scheme) -> PAnnot (make_vis_pattern pt, scheme) | PCtor (pth, xs, ys) -> diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml index a3f987aa..9de60c5e 100644 --- a/src/DblParser/Desugar.ml +++ b/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)) diff --git a/src/EffectInference/ExprUtils.ml b/src/EffectInference/ExprUtils.ml index 8fe12cb7..35683ba4 100644 --- a/src/EffectInference/ExprUtils.ml +++ b/src/EffectInference/ExprUtils.ml @@ -145,7 +145,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 _ -> + | ELit _ | EExtern _ -> e | EVar x -> diff --git a/src/EffectInference/Pattern.ml b/src/EffectInference/Pattern.ml index 07784369..76af00f8 100644 --- a/src/EffectInference/Pattern.ml +++ b/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,7 +187,14 @@ and check_scheme env (pat : S.pattern) sch = match pat.data with | PWildcard -> (PWildcard, PEnv.empty) - | PAs(pat, x) -> + | PLit l -> + (match l with + | PNum n -> (PLit (ENum n), PEnv.empty) + | PNum64 n -> (PLit (ENum64 n), PEnv.empty) + | PStr s -> (PLit (EStr s), PEnv.empty) + | PChr c -> (PLit (EChr c), PEnv.empty)) + + | PAs(pat, x) -> let (pat, penv) = check_scheme env pat sch in (PAs(pat, x), PEnv.add_var penv x sch) diff --git a/src/EffectInference/Pattern.mli b/src/EffectInference/Pattern.mli index 5a9540e4..804c7951 100644 --- a/src/EffectInference/Pattern.mli +++ b/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; diff --git a/src/EffectInference/PatternMatch.ml b/src/EffectInference/PatternMatch.ml index 51e4692a..53487f04 100644 --- a/src/EffectInference/PatternMatch.ml +++ b/src/EffectInference/PatternMatch.ml @@ -88,7 +88,8 @@ let drop_wildcard (cl : iclause) = let rec simplify_head x (cl : iclause) = match cl.c_patterns with | [] -> assert false - | PAs(pat, y) :: pats -> + | (PWildcard | PLit _ | PCtor _) :: pats -> cl + | PAs(pat, y) :: pats -> let cl = { cl with c_patterns = pat :: pats; @@ -100,10 +101,16 @@ let rec simplify_head x (cl : iclause) = simplify_head x { cl with c_patterns = pat2 :: pats } | (PWildcard | PCtor _) :: _ -> [cl] +<<<<<<< HEAD (** Normalize patterns at head position by simplifying as-patterns and expanding or-patterns in given clause list *) let normalize_head_patterns x cls = List.concat_map (simplify_head x) cls +======= +(** Simplify as-patterns on the head position in given clause list *) +let rec simplify_as_patterns x (cls : iclause list) = + List.map (simplify_as_pattern x) cls +>>>>>>> c868a1f (Added pattern matching for literals) (* ========================================================================= *) @@ -119,6 +126,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 +155,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 +173,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 + | _ -> 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 *) @@ -179,6 +207,20 @@ module type MatchContext = sig val res_eff : T.ceffect end +let 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 + module Make(Ctx : MatchContext) = struct (** Main function of the translation. It solves a bit more general problem: it takes list of values [vs] and list of clauses [cls], where each of @@ -193,16 +235,77 @@ module Make(Ctx : MatchContext) = struct cl.c_used := true; make_body cl +<<<<<<< HEAD | x :: xs, cls -> let cls = normalize_head_patterns x cls in +======= + | x :: xs, cls -> + let cls = simplify_as_patterns x cls in +>>>>>>> c868a1f (Added pattern matching for literals) begin match column_class cls with | 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_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.ENum n) + | ENum64 n -> T.EApp(T.EApp(T.EExtern("dbl_eqInt64", eq_tp), x), T.ENum64 n) + | EStr s -> T.EApp(T.EApp(T.EExtern("dbl_eqStr", eq_tp), x), T.EStr s) + | EChr c -> T.EApp(T.EApp(T.EExtern("dbl_eqInt", eq_tp), x), T.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) = diff --git a/src/Lang/ConE.mli b/src/Lang/ConE.mli index ad561eb8..558f409c 100644 --- a/src/Lang/ConE.mli +++ b/src/Lang/ConE.mli @@ -1,4 +1,5 @@ (* This file is part of DBL, released under MIT license. + * See LICENSE for details. *) @@ -139,6 +140,9 @@ type expr = | EChr of char (** Character literal *) + | ELit of literal + (** Literal for pattern *) + | EVar of var (** Variable *) @@ -209,7 +213,7 @@ type expr = expression. *) (** Recursive definition *) -and rec_def = + and rec_def = { rd_var : var; (** Variable that stores recursive value. *) @@ -239,6 +243,13 @@ and match_clause = (** Body of the clause *) } +(** Literals for patterns *) +and literal = + | ENum of int + | ENum64 of int64 + | EStr of string + | EChr of char + (** Programs *) type program = expr diff --git a/src/Lang/ConEPriv/SExprPrinter.ml b/src/Lang/ConEPriv/SExprPrinter.ml index 43fd8254..17e8e4db 100644 --- a/src/Lang/ConEPriv/SExprPrinter.ml +++ b/src/Lang/ConEPriv/SExprPrinter.ml @@ -109,6 +109,7 @@ let rec tr_expr (e : expr) = | ENum64 n -> Sym (Int64.to_string n ^ "L") | EStr s -> Sym (Printf.sprintf "\"%s\"" (String.escaped s)) | EChr c -> Sym (Printf.sprintf "\'%s\'" (Char.escaped c)) + | ELit l -> tr_lit l | EVar x -> tr_var x | EFn _ -> List (Sym "fn" :: tr_fn e) | ETFun _ -> List (Sym "tfun" :: tr_tfun e) @@ -141,6 +142,13 @@ let rec tr_expr (e : expr) = | EReplExpr(e1, tp, e2) -> List [ Sym "repl-expr"; tr_expr e1; Sym ("{" ^ tp ^ "}"); tr_expr e2 ] +and tr_lit l = + match l with + | ENum n -> Sym (string_of_int n) + | ENum64 n -> Sym (Int64.to_string n ^ "L") + | EStr s -> Sym (Printf.sprintf "\"%s\"" (String.escaped s)) + | EChr c -> Sym (Printf.sprintf "\'%s\'" (Char.escaped c)) + and tr_fn e = match e with | EFn(x, sch, e) -> @@ -159,9 +167,9 @@ and tr_app e args = | ECApp e1 -> tr_app e1 (Sym "constr" :: args) | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | EVar _ | EFn _ | ETFun _ | ECAbs _ | ELet _ | ELetPure _ | ELetRec _ - | ERecCtx _ | EData _ | ECtor _ | EMatch _ | EShift _ | EReset _ | EExtern _ - | ERepl _ | EReplExpr _ -> + | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | ELet _ | ELetPure _ + | ELetRec _ | ERecCtx _ | EData _ | ECtor _ | EMatch _ | EShift _ | EReset _ + | EExtern _ | ERepl _ | EReplExpr _ -> List (tr_expr e :: args) and tr_defs e = @@ -183,8 +191,8 @@ and tr_defs e = ] :: tr_defs body | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | EVar _ | EFn _ | ETFun _ | ECAbs _ | EApp _ | ETApp _ | ECApp _ | ECtor _ - | EMatch _ | EShift _ | EExtern _ | ERepl _ | EReplExpr _ -> + | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | EApp _ | ETApp _ | ECApp _ + | ECtor _ | EMatch _ | EShift _ | EExtern _ | ERepl _ | EReplExpr _ -> [ tr_expr e ] and tr_rec_def rd = diff --git a/src/Lang/ConEPriv/Syntax.ml b/src/Lang/ConEPriv/Syntax.ml index 227de25b..cef20b35 100644 --- a/src/Lang/ConEPriv/Syntax.ml +++ b/src/Lang/ConEPriv/Syntax.ml @@ -31,6 +31,7 @@ type expr = | ENum64 of int64 | EStr of string | EChr of char + | ELit of literal | EVar of var | EFn of var * scheme * expr | ETFun of tvar * expr @@ -50,6 +51,11 @@ type expr = | EExtern of string * typ | ERepl of (unit -> expr) * typ * ceffect | EReplExpr of expr * string * expr +and literal = + | ENum of int + | ENum64 of int64 + | EStr of string + | EChr of char and rec_def = { rd_var : var; diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml index a6e38b97..591bd776 100644 --- a/src/Lang/Surface.ml +++ b/src/Lang/Surface.ml @@ -177,6 +177,8 @@ type pattern = pattern_data node and pattern_data = | PWildcard (** Wildcard pattern -- it matches everything *) + + | PLit of literal | PId of is_public * ident (** Pattern that binds an identifier *) @@ -186,6 +188,19 @@ and pattern_data = | PAnnot of pattern * scheme_expr (** Scheme annotation *) + +and literal = + | ENum of int + (** Integer literal *) + + | ENum64 of int64 + (** 64 bit integer literal *) + + | EStr of string + (** String literal *) + + | EChr of char + (** Char literal *) | POr of pattern * pattern (** Or-pattern: matches if either sub-pattern matches *) diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli index a4ce5d5b..b2547de3 100644 --- a/src/Lang/Unif.mli +++ b/src/Lang/Unif.mli @@ -286,6 +286,9 @@ and pattern_data = | PAs of pattern * var (** Pattern that binds a variable and continues with a subpattern *) + | PLit of literal + (** Literal pattern *) + | PCtor of string * int * proof_expr * tvar list * pattern list * pattern list (** ADT constructor pattern. It stores a name, constructor index, @@ -298,6 +301,12 @@ and pattern_data = | POr of pattern * pattern (** Or-pattern: matches if either sub-pattern matches *) +and literal = + | PNum of int + | PNum64 of int64 + | PStr of string + | PChr of char + (** Polymorphic expression *) type poly_expr = poly_expr_data node and poly_expr_data = diff --git a/src/Lang/UnifPriv/Ren.ml b/src/Lang/UnifPriv/Ren.ml index 2f43fa98..41d53be3 100644 --- a/src/Lang/UnifPriv/Ren.ml +++ b/src/Lang/UnifPriv/Ren.ml @@ -71,6 +71,7 @@ let rec rename_pattern ren (pat : pattern) = match pat.data with | PWildcard -> PWildcard | PAs(pat, x) -> PAs(rename_pattern ren pat, rename_var ren x) + | PLit(lit) -> PLit(lit) | PCtor(name, idx, prf, tvars, pats1, pats2) -> PCtor(name, idx, rename_proof_expr ren prf, List.map (rename_tvar ren) tvars, diff --git a/src/Lang/UnifPriv/Syntax.ml b/src/Lang/UnifPriv/Syntax.ml index b7bf4a27..7e543e9f 100644 --- a/src/Lang/UnifPriv/Syntax.ml +++ b/src/Lang/UnifPriv/Syntax.ml @@ -81,11 +81,18 @@ type pattern = pattern_data node and pattern_data = | PWildcard | PAs of pattern * var + | PLit of literal | PCtor of string * int * proof_expr * tvar list * pattern list * pattern list | PAnnot of pattern * scheme_expr | POr of pattern * pattern +and literal = + | PNum of int + | PNum64 of int64 + | PStr of string + | PChr of char + type poly_expr = poly_expr_data node and poly_expr_data = | EVar of var diff --git a/src/ToCore/Main.ml b/src/ToCore/Main.ml index eb5b56d2..dc75636b 100644 --- a/src/ToCore/Main.ml +++ b/src/ToCore/Main.ml @@ -15,7 +15,7 @@ let return x cont = cont x let rec tr_expr env (e : S.expr) = match e with | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | EVar _ | EExtern _ | ERepl _ | EReplExpr _ -> + | ELit _ | EVar _ | EExtern _ | ERepl _ | EReplExpr _ -> let^ v = tr_expr_v env e in T.EValue v @@ -91,7 +91,7 @@ and tr_let_expr ~pure x env (e : S.expr) cont = T.ELetPure(Relevant, x, tr_expr env e, cont ()) | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ -> + | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ -> T.ELetPure(Relevant, x, tr_expr env e, cont ()) | EApp _ | ETApp _ | ECApp _ | ELet _ | ELetPure _ | ELetRec _ | ERecCtx _ @@ -117,7 +117,7 @@ and tr_expr_as_var env e = and tr_expr_p env (e : S.expr) = match e with | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ -> + | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ -> return (tr_expr env e) | ETApp(e, tp) -> @@ -169,6 +169,7 @@ and tr_expr_v env (e : S.expr) = | 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_lit l | EVar x -> return (T.VVar x) | ELet(x, e1, e2) -> @@ -188,6 +189,14 @@ and tr_expr_v env (e : S.expr) = let* x = tr_expr_as_var env e in return (T.VVar x) +(** Translate a literal *) +and tr_lit l = + 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 list of expressions as list of values in expression building monad. *) and tr_expr_vs env es = diff --git a/src/TypeInference/Pattern.ml b/src/TypeInference/Pattern.ml index 94411b88..6f216968 100644 --- a/src/TypeInference/Pattern.ml +++ b/src/TypeInference/Pattern.ml @@ -178,7 +178,7 @@ let get_ctor_info ~pos env (cpath : S.ctor_name S.path) tp = (* ========================================================================= *) (** Translate a scheme expression into a target scheme, taking into account - the special treatment of optional parameter annotations. *) + the spe+cial treatment of optional parameter annotations. *) let tr_named_scheme_annot env (name : Name.t) sch_expr = let sch = T.SchemeExpr.to_scheme (Type.tr_scheme env sch_expr) in match name with @@ -193,6 +193,13 @@ let tr_named_scheme_annot env (name : Name.t) sch_expr = (* ========================================================================= *) +let literal_type (lit : S.literal) = + match lit with + | ENum _ -> T.Type.t_var T.BuiltinType.tv_int + | ENum64 _ -> T.Type.t_var T.BuiltinType.tv_int64 + | EStr _ -> T.Type.t_var T.BuiltinType.tv_string + | EChr _ -> T.Type.t_var T.BuiltinType.tv_char + let rec check_scheme env (pat : S.pattern) sch = let pos = pat.pos in let pp = Env.pp_tree env in @@ -201,11 +208,28 @@ let rec check_scheme env (pat : S.pattern) sch = | PWildcard -> (PartialEnv.empty, make T.PWildcard, T.Pure) - | PId(public, id) -> + | PLit l -> + let lit_tp = literal_type l in + begin match T.Scheme.to_type sch with + | None -> + Error.fatal (Error.non_polymorphic_pattern ~pos) + | Some tp -> + Error.check_unify_result ~pos + (Unification.subtype env lit_tp tp) + ~on_error:(Error.pattern_type_mismatch ~pp lit_tp tp); + end; + begin match l with + | ENum n -> (PartialEnv.empty, make (T.PLit (T.PNum n)), T.Pure) + | ENum64 n -> (PartialEnv.empty, make (T.PLit (T.PNum64 n)), T.Pure) + | EStr s -> (PartialEnv.empty, make (T.PLit (T.PStr s)), T.Pure) + | EChr c -> (PartialEnv.empty, make (T.PLit (T.PChr c)), T.Pure) + end + + | PId(public, id) -> let name = NameUtils.tr_ident ~pos ~pp id sch in let x = Var.fresh ~name:(Name.to_string name) () in let penv = PartialEnv.singleton_val ~public ~pos name x sch in - (penv, make (T.PAs(make T.PWildcard, x)), T.Pure) + (penv, make (T.PAs(make T.PWildcard, x)), T.Pure) | PCtor _ -> begin match T.Scheme.to_type sch with @@ -241,7 +265,7 @@ and check_type env (pat : S.pattern) tp = let pp = Env.pp_tree env in let make data = T.{ pos; pp; data } in match pat.data with - | PWildcard | PId _ | PAnnot _ | POr _ -> + | PWildcard | PLit _ | PId _ | PAnnot _ | POr _ -> let sch = T.Scheme.of_type tp in check_scheme env pat sch @@ -384,7 +408,11 @@ and check_named_pattern env np tvars named = let infer_scheme env (pat : S.pattern) = match pat.data with +<<<<<<< HEAD | PWildcard | PId _ | PCtor _ | POr _ -> +======= + | PWildcard | PLit _ | PId _ | PCtor _ -> +>>>>>>> c868a1f (Added pattern matching for literals) let tp = Env.fresh_uvar ~pos:pat.pos env T.Kind.k_type in let tp_expr = { T.pos = pat.pos; diff --git a/src/TypeInference/RecDefs.ml b/src/TypeInference/RecDefs.ml index 2e21e116..abb4c288 100644 --- a/src/TypeInference/RecDefs.ml +++ b/src/TypeInference/RecDefs.ml @@ -56,8 +56,9 @@ let rec prepare_rec_data env (def : S.def) = | PAnnot({ data = PId(public, id); _ }, sch) -> (env, make (D1_Label(x, public, id, Some(pat.pos, sch)))) - | PAnnot({ data = PWildcard | PCtor _ | PAnnot _ | POr _; _ }, _) - | PWildcard | PCtor _ | POr _ -> + | PAnnot({ data = PWildcard | PLit _ | PCtor _ | PAnnot _ | POr _; _ }, _) + + | PWildcard | PLit _ | PCtor _ | POr _ -> Error.fatal (Error.invalid_rec_def ~pos:def.pos) end diff --git a/test/ok/ok0154_literalMatch.fram b/test/ok/ok0154_literalMatch.fram new file mode 100644 index 00000000..e51b22cc --- /dev/null +++ b/test/ok/ok0154_literalMatch.fram @@ -0,0 +1,37 @@ +let f (x: Int) = + match x with + | 0 => 0 + | 1 => 1 + | 2 => 2 + | _ => 3 + end + +let fs (s: String) = + match s with + | "fram" => "fram" + | "compiler" => "not found :(" + | _ => "abcd" + end + +let fc (c: Char) = + match c with + | 'a' => 'a' + | 'b' => 'b' + | _ => 'c' + end + +data Pair X Y = (,) of X, Y + +let fp x y = + match (x,y) with + | (1,2) => 1 + | (_,_) => 0 + end + +let _ = f 3 +let _ = fs "abc" +let _ = fc 'x' +let _ = fp 1 2 + + + From 5d15f4a4ed6aa70b48b7547124404beeec3810c9 Mon Sep 17 00:00:00 2001 From: lidiapodoluk Date: Mon, 8 Jun 2026 12:26:22 +0200 Subject: [PATCH 2/2] added requested changes --- lib/Base/Types.fram | 2 +- src/ConETypeErase.ml | 8 ++--- src/DblParser/Desugar.ml | 8 ++--- src/DblParser/Import.ml | 2 +- src/EffectInference/Expr.ml | 33 +++++++++--------- src/EffectInference/ExprUtils.ml | 3 +- src/EffectInference/Pattern.ml | 34 +++++++++++++++---- src/EffectInference/PatternMatch.ml | 52 +++++++++++++++-------------- src/Lang/ConE.mli | 17 ++-------- src/Lang/ConEPriv/SExprPrinter.ml | 17 ++++------ src/Lang/ConEPriv/Syntax.ml | 4 --- src/Lang/Surface.ml | 40 +++++++++------------- src/Lang/Unif.mli | 27 +++++++++------ src/Lang/UnifPriv/Syntax.ml | 11 +++--- src/ToCore/Main.ml | 17 ++++------ src/TypeInference/Expr.ml | 48 +++++++++++++------------- src/TypeInference/ParamResolve.ml | 4 +-- src/TypeInference/Pattern.ml | 10 +++--- src/TypeInference/RecDefs.ml | 8 ++--- 19 files changed, 170 insertions(+), 175 deletions(-) diff --git a/lib/Base/Types.fram b/lib/Base/Types.fram index 8a5d136f..cab416ea 100644 --- a/lib/Base/Types.fram +++ b/lib/Base/Types.fram @@ -2,7 +2,7 @@ # See LICENSE for details. #} -pub data rec List A = [] | (::) of A, List A +pub data rec List A = [] | (::) of A, List A pub data Pair X Y = (,) of X, Y diff --git a/src/ConETypeErase.ml b/src/ConETypeErase.ml index b9788e84..1bf55196 100644 --- a/src/ConETypeErase.ml +++ b/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 _ | ELit _ | EVar _ | EExtern _ -> + | ELit _ | EVar _ | EExtern _ -> let^ v = tr_expr_v e in T.EValue v @@ -77,11 +77,6 @@ let rec tr_expr (e : S.expr) = 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) @@ -113,6 +108,7 @@ and tr_expr_lit (l : S.literal) = | 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) diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml index 9de60c5e..c007696d 100644 --- a/src/DblParser/Desugar.ml +++ b/src/DblParser/Desugar.ml @@ -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 diff --git a/src/DblParser/Import.ml b/src/DblParser/Import.ml index 3bfb3e6a..8764f87d 100644 --- a/src/DblParser/Import.ml +++ b/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)) = diff --git a/src/EffectInference/Expr.ml b/src/EffectInference/Expr.ml index c0caa55f..ccf9429e 100644 --- a/src/EffectInference/Expr.ml +++ b/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 diff --git a/src/EffectInference/ExprUtils.ml b/src/EffectInference/ExprUtils.ml index 35683ba4..281b6198 100644 --- a/src/EffectInference/ExprUtils.ml +++ b/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 _ - | ELit _ | EExtern _ -> + | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EExtern _ -> e | EVar x -> diff --git a/src/EffectInference/Pattern.ml b/src/EffectInference/Pattern.ml index 76af00f8..e5c9d926 100644 --- a/src/EffectInference/Pattern.ml +++ b/src/EffectInference/Pattern.ml @@ -187,12 +187,34 @@ and check_scheme env (pat : S.pattern) sch = match pat.data with | PWildcard -> (PWildcard, PEnv.empty) - | PLit l -> - (match l with - | PNum n -> (PLit (ENum n), PEnv.empty) - | PNum64 n -> (PLit (ENum64 n), PEnv.empty) - | PStr s -> (PLit (EStr s), PEnv.empty) - | PChr c -> (PLit (EChr c), 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 diff --git a/src/EffectInference/PatternMatch.ml b/src/EffectInference/PatternMatch.ml index 53487f04..6a0eed1f 100644 --- a/src/EffectInference/PatternMatch.ml +++ b/src/EffectInference/PatternMatch.ml @@ -101,16 +101,10 @@ let rec simplify_head x (cl : iclause) = simplify_head x { cl with c_patterns = pat2 :: pats } | (PWildcard | PCtor _) :: _ -> [cl] -<<<<<<< HEAD (** Normalize patterns at head position by simplifying as-patterns and expanding or-patterns in given clause list *) let normalize_head_patterns x cls = List.concat_map (simplify_head x) cls -======= -(** Simplify as-patterns on the head position in given clause list *) -let rec simplify_as_patterns x (cls : iclause list) = - List.map (simplify_as_pattern x) cls ->>>>>>> c868a1f (Added pattern matching for literals) (* ========================================================================= *) @@ -185,7 +179,7 @@ let rec column_class (cls : iclause list) = if List.exists (fun x -> x = l) acc then collect acc cls else collect (l :: acc) cls - | _ -> assert false) + | (PCtor _ | PAs (_, _)) :: _ -> assert false) in CC_Lit (collect [lit] cls) | PCtor cp :: _ -> CC_ADT(cp.proof, cp.ctors) @@ -207,20 +201,6 @@ module type MatchContext = sig val res_eff : T.ceffect end -let 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 - module Make(Ctx : MatchContext) = struct (** Main function of the translation. It solves a bit more general problem: it takes list of values [vs] and list of clauses [cls], where each of @@ -235,11 +215,15 @@ module Make(Ctx : MatchContext) = struct cl.c_used := true; make_body cl +<<<<<<< HEAD <<<<<<< HEAD | x :: xs, cls -> let cls = normalize_head_patterns x cls in ======= | x :: xs, cls -> +======= + | x :: xs, cls -> +>>>>>>> ae0f7b7 (added requested changes) let cls = simplify_as_patterns x cls in >>>>>>> c868a1f (Added pattern matching for literals) begin match column_class cls with @@ -254,13 +238,31 @@ module Make(Ctx : MatchContext) = struct 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.ENum n) - | ENum64 n -> T.EApp(T.EApp(T.EExtern("dbl_eqInt64", eq_tp), x), T.ENum64 n) - | EStr s -> T.EApp(T.EApp(T.EExtern("dbl_eqStr", eq_tp), x), T.EStr s) - | EChr c -> T.EApp(T.EApp(T.EExtern("dbl_eqInt", eq_tp), x), T.EChr c) + | 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 diff --git a/src/Lang/ConE.mli b/src/Lang/ConE.mli index 558f409c..756318c4 100644 --- a/src/Lang/ConE.mli +++ b/src/Lang/ConE.mli @@ -1,5 +1,4 @@ (* This file is part of DBL, released under MIT license. - * See LICENSE for details. *) @@ -128,20 +127,8 @@ type expr = | EOptionPrf (** ADT-shape proof for option type *) - | ENum of int - (** Integer literal *) - - | ENum64 of int64 - (** 64 bit integer literal *) - - | EStr of string - (** String literal *) - - | EChr of char - (** Character literal *) - | ELit of literal - (** Literal for pattern *) + (** Literal *) | EVar of var (** Variable *) @@ -213,7 +200,7 @@ type expr = expression. *) (** Recursive definition *) - and rec_def = +and rec_def = { rd_var : var; (** Variable that stores recursive value. *) diff --git a/src/Lang/ConEPriv/SExprPrinter.ml b/src/Lang/ConEPriv/SExprPrinter.ml index 17e8e4db..61fe3ec7 100644 --- a/src/Lang/ConEPriv/SExprPrinter.ml +++ b/src/Lang/ConEPriv/SExprPrinter.ml @@ -105,10 +105,6 @@ let rec tr_expr (e : expr) = | EUnitPrf -> Sym "unit-prf" | EBoolPrf -> Sym "bool-prf" | EOptionPrf -> Sym "option-prf" - | ENum n -> Sym (string_of_int n) - | ENum64 n -> Sym (Int64.to_string n ^ "L") - | EStr s -> Sym (Printf.sprintf "\"%s\"" (String.escaped s)) - | EChr c -> Sym (Printf.sprintf "\'%s\'" (Char.escaped c)) | ELit l -> tr_lit l | EVar x -> tr_var x | EFn _ -> List (Sym "fn" :: tr_fn e) @@ -166,10 +162,9 @@ and tr_app e args = | ETApp(e1, tp) -> tr_app e1 (List [ Sym "type"; tr_type tp ] :: args) | ECApp e1 -> tr_app e1 (Sym "constr" :: args) - | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | ELet _ | ELetPure _ - | ELetRec _ | ERecCtx _ | EData _ | ECtor _ | EMatch _ | EShift _ | EReset _ - | EExtern _ | ERepl _ | EReplExpr _ -> + | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _ + | ECAbs _ | ELet _ | ELetPure _ | ELetRec _ | ERecCtx _ | EData _ | ECtor _ + | EMatch _ | EShift _ | EReset _ | EExtern _ | ERepl _ | EReplExpr _ -> List (tr_expr e :: args) and tr_defs e = @@ -190,9 +185,9 @@ and tr_defs e = tr_var x; tr_expr ret ] :: tr_defs body - | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | EApp _ | ETApp _ | ECApp _ - | ECtor _ | EMatch _ | EShift _ | EExtern _ | ERepl _ | EReplExpr _ -> + | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _ + | ECAbs _ | EApp _ | ETApp _ | ECApp _ | ECtor _ | EMatch _ | EShift _ + | EExtern _ | ERepl _ | EReplExpr _ -> [ tr_expr e ] and tr_rec_def rd = diff --git a/src/Lang/ConEPriv/Syntax.ml b/src/Lang/ConEPriv/Syntax.ml index cef20b35..c6054ff1 100644 --- a/src/Lang/ConEPriv/Syntax.ml +++ b/src/Lang/ConEPriv/Syntax.ml @@ -27,10 +27,6 @@ type expr = | EUnitPrf | EBoolPrf | EOptionPrf - | ENum of int - | ENum64 of int64 - | EStr of string - | EChr of char | ELit of literal | EVar of var | EFn of var * scheme * expr diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml index 591bd776..2ba5882d 100644 --- a/src/Lang/Surface.ml +++ b/src/Lang/Surface.ml @@ -172,6 +172,20 @@ and ctor_decl_data = { cd_arg_schemes : scheme_expr list } +(** Literals *) +type literal = + | ENum of int + (** Integer literal *) + + | ENum64 of int64 + (** 64 bit integer literal *) + + | EStr of string + (** String literal *) + + | EChr of char + (** Char literal *) + (** Patterns *) type pattern = pattern_data node and pattern_data = @@ -188,19 +202,6 @@ and pattern_data = | PAnnot of pattern * scheme_expr (** Scheme annotation *) - -and literal = - | ENum of int - (** Integer literal *) - - | ENum64 of int64 - (** 64 bit integer literal *) - - | EStr of string - (** String literal *) - - | EChr of char - (** Char literal *) | POr of pattern * pattern (** Or-pattern: matches if either sub-pattern matches *) @@ -255,17 +256,8 @@ and expr_data = (** Unit expression. Used only as the expression after the last definition in a program. *) - | ENum of int - (** Integer literal *) - - | ENum64 of int64 - (** 64 bit integer literal *) - - | EStr of string - (** String literal *) - - | EChr of char - (** Char literal *) + | ELit of literal + (** Literal *) | EPoly of poly_expr_use * inst list (** Polymorphic expression with partial explicit instantiation, possibly diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli index b2547de3..a8556d7c 100644 --- a/src/Lang/Unif.mli +++ b/src/Lang/Unif.mli @@ -277,6 +277,20 @@ type proof_expr = (** Variable generated at the ADT definition, applied to the parameters of the ADT. *) +(* Literal *) +type literal = + | ENum of int + (** Integer literal *) + + | ENum64 of int64 + (** 64 bit integer literal *) + + | EStr of string + (** String literal *) + + | EChr of char + (** Character literal *) + (** Pattern *) type pattern = pattern_data node and pattern_data = @@ -344,17 +358,8 @@ and expr_data = | EInst of poly_expr * type_expr list * poly_fun list (** Instantiation of polymorphic expression *) - | ENum of int - (** Integer literal *) - - | ENum64 of int64 - (** 64 bit integer literal *) - - | EStr of string - (** String literal *) - - | EChr of char - (** Character literal *) + | ELit of literal + (* Literal *) | EFn of var * scheme_expr * expr * effct (** Effect-annotated lambda-abstraction. *) diff --git a/src/Lang/UnifPriv/Syntax.ml b/src/Lang/UnifPriv/Syntax.ml index 7e543e9f..0134b958 100644 --- a/src/Lang/UnifPriv/Syntax.ml +++ b/src/Lang/UnifPriv/Syntax.ml @@ -77,6 +77,12 @@ type proof_expr = | PE_Option of typ | PE_Var of var * typ list +type literal = + | ENum of int + | ENum64 of int64 + | EStr of string + | EChr of char + type pattern = pattern_data node and pattern_data = | PWildcard @@ -108,10 +114,7 @@ and poly_fun_data = and expr = expr_data node and expr_data = | EInst of poly_expr * type_expr list * poly_fun list - | ENum of int - | ENum64 of int64 - | EStr of string - | EChr of char + | ELit of literal | EFn of var * scheme_expr * expr * effct | EAppPoly of expr * poly_fun | EAppMono of expr * expr diff --git a/src/ToCore/Main.ml b/src/ToCore/Main.ml index dc75636b..3a7ed9ac 100644 --- a/src/ToCore/Main.ml +++ b/src/ToCore/Main.ml @@ -14,8 +14,8 @@ let return x cont = cont x (** Translate expression *) let rec tr_expr env (e : S.expr) = match e with - | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | ELit _ | EVar _ | EExtern _ | ERepl _ | EReplExpr _ -> + | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EExtern _ | ERepl _ + | EReplExpr _ -> let^ v = tr_expr_v env e in T.EValue v @@ -90,8 +90,8 @@ and tr_let_expr ~pure x env (e : S.expr) cont = | _ when pure -> T.ELetPure(Relevant, x, tr_expr env e, cont ()) - | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ -> + | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _ + | ECAbs _ | EExtern _ -> T.ELetPure(Relevant, x, tr_expr env e, cont ()) | EApp _ | ETApp _ | ECApp _ | ELet _ | ELetPure _ | ELetRec _ | ERecCtx _ @@ -116,8 +116,8 @@ and tr_expr_as_var env e = (** Translate an expression as pure expression *) and tr_expr_p env (e : S.expr) = match e with - | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ - | ELit _ | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ -> + | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _ + | ECAbs _ | EExtern _ -> return (tr_expr env e) | ETApp(e, tp) -> @@ -164,11 +164,6 @@ and tr_expr_v env (e : S.expr) = | EUnitPrf -> return v_unit_prf | EBoolPrf -> return v_bool_prf | EOptionPrf -> return v_option_prf - - | 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_lit l | EVar x -> return (T.VVar x) diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml index 243d1f89..8492655a 100644 --- a/src/TypeInference/Expr.ml +++ b/src/TypeInference/Expr.ml @@ -37,33 +37,33 @@ let infer_expr_type ~tcfix ?app_type env (e : S.expr) = er_constr = [] } - | ENum n -> - { er_expr = make (T.ENum n); - er_type = Infered (T.Type.t_var T.BuiltinType.tv_int); - er_effect = Pure; - er_constr = [] - } - - | ENum64 n -> - { er_expr = make (T.ENum64 n); - er_type = Infered (T.Type.t_var T.BuiltinType.tv_int64); - er_effect = Pure; - er_constr = [] - } - - | EStr s -> - { er_expr = make (T.EStr s); - er_type = Infered (T.Type.t_var T.BuiltinType.tv_string); - er_effect = Pure; - er_constr = [] - } - - | EChr c -> - { er_expr = make (T.EChr c); + | ELit l -> + begin match l with + | ENum n -> + { er_expr = make (T.ELit(ENum n)); + er_type = Infered (T.Type.t_var T.BuiltinType.tv_int); + er_effect = Pure; + er_constr = [] + } + | ENum64 n -> + { er_expr = make (T.ELit(ENum64 n)); + er_type = Infered (T.Type.t_var T.BuiltinType.tv_int64); + er_effect = Pure; + er_constr = [] + } + | EStr s -> + { er_expr = make (T.ELit(EStr s)); + er_type = Infered (T.Type.t_var T.BuiltinType.tv_string); + er_effect = Pure; + er_constr = [] + } + | EChr c -> + { er_expr = make (T.ELit(EChr c)); er_type = Infered (T.Type.t_var T.BuiltinType.tv_char); er_effect = Pure; er_constr = [] } + end | EPoly(e, inst) -> let (p_ctx, e, sch) = PolyExpr.infer_use_scheme ~tcfix ?app_type env e in @@ -316,7 +316,7 @@ let check_expr_type ~tcfix env (e : S.expr) tp = let pp = Env.pp_tree env in let make data = T.{ pos; pp; data } in match e.data with - | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | EPoly _ | EApp _ + | EUnit | ELit _ | EPoly _ | EApp _ | EAnnot _ | EAnnotEff _ | EAnnotTotal _ -> check_expr_type_default ~tcfix env e tp diff --git a/src/TypeInference/ParamResolve.ml b/src/TypeInference/ParamResolve.ml index e7618a9f..fe4150b8 100644 --- a/src/TypeInference/ParamResolve.ml +++ b/src/TypeInference/ParamResolve.ml @@ -244,9 +244,9 @@ and resolve_implicit ~resolve_env rctx iname sch = (* Special implicits *) let (param_expr, param_tvar) = match iname with | "~__line__" -> - (make (T.ENum pos.pos_start_line), T.BuiltinType.tv_int) + (make (T.ELit(ENum pos.pos_start_line)), T.BuiltinType.tv_int) | "~__file__" -> - (make (T.EStr pos.pos_fname), T.BuiltinType.tv_string) + (make (T.ELit(EStr pos.pos_fname)), T.BuiltinType.tv_string) | _ -> Error.fatal (Error.cannot_resolve_implicit ~pos iname) in (* Check types *) let param_sch = T.Scheme.of_type (T.Type.t_var param_tvar) in diff --git a/src/TypeInference/Pattern.ml b/src/TypeInference/Pattern.ml index 6f216968..1dc7139d 100644 --- a/src/TypeInference/Pattern.ml +++ b/src/TypeInference/Pattern.ml @@ -178,7 +178,7 @@ let get_ctor_info ~pos env (cpath : S.ctor_name S.path) tp = (* ========================================================================= *) (** Translate a scheme expression into a target scheme, taking into account - the spe+cial treatment of optional parameter annotations. *) + the special treatment of optional parameter annotations. *) let tr_named_scheme_annot env (name : Name.t) sch_expr = let sch = T.SchemeExpr.to_scheme (Type.tr_scheme env sch_expr) in match name with @@ -219,10 +219,10 @@ let rec check_scheme env (pat : S.pattern) sch = ~on_error:(Error.pattern_type_mismatch ~pp lit_tp tp); end; begin match l with - | ENum n -> (PartialEnv.empty, make (T.PLit (T.PNum n)), T.Pure) - | ENum64 n -> (PartialEnv.empty, make (T.PLit (T.PNum64 n)), T.Pure) - | EStr s -> (PartialEnv.empty, make (T.PLit (T.PStr s)), T.Pure) - | EChr c -> (PartialEnv.empty, make (T.PLit (T.PChr c)), T.Pure) + | ENum n -> (PartialEnv.empty, make (T.PLit(T.ENum n)), T.Pure) + | ENum64 n -> (PartialEnv.empty, make (T.PLit(T.ENum64 n)), T.Pure) + | EStr s -> (PartialEnv.empty, make (T.PLit(T.EStr s)), T.Pure) + | EChr c -> (PartialEnv.empty, make (T.PLit(T.EChr c)), T.Pure) end | PId(public, id) -> diff --git a/src/TypeInference/RecDefs.ml b/src/TypeInference/RecDefs.ml index abb4c288..a6fefd7a 100644 --- a/src/TypeInference/RecDefs.ml +++ b/src/TypeInference/RecDefs.ml @@ -57,7 +57,7 @@ let rec prepare_rec_data env (def : S.def) = (env, make (D1_Label(x, public, id, Some(pat.pos, sch)))) | PAnnot({ data = PWildcard | PLit _ | PCtor _ | PAnnot _ | POr _; _ }, _) - + | PWildcard | PLit _ | PCtor _ | POr _ -> Error.fatal (Error.invalid_rec_def ~pos:def.pos) end @@ -305,8 +305,8 @@ let rec guess_rec_fun_type env (e : S.expr) tp = rfb_body_tp = tp }, T.Impure - | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | EPoly _ | EApp _ | EDefs _ - | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ | EExtern _ | ERepl _ -> + | EUnit | ELit _ | EPoly _ | EApp _ | EDefs _ | EMatch _ | EHandler _ + | EHandlerFn _ | EEffect _ | EExtern _ | ERepl _ -> let pp = Env.pp_tree env in { rfb_type = { T.pos = pos; T.pp = pp; T.data = T.TE_Type tp }; rfb_args = []; @@ -545,7 +545,7 @@ let update_rec_body ~pos fds (body : T.poly_fun) = let make data = { body with data = data } in match e.data with - | ENum _ | ENum64 _ | EStr _ | EChr _ | EExtern _ -> e + | ELit _ | EExtern _ -> e | EFn(x, sch, body, Impure) -> make (T.EFn(x, sch, make (T.ERecCtx body), Impure))