Décembre 2020 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer] Deleted branch heap
by Simon Génier 22 Déc '20

22 Déc '20

Simon Génier deleted branch heap at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch warning-40-be-gone
by Simon Génier 22 Déc '20

22 Déc '20

Simon Génier deleted branch warning-40-be-gone at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 4 commits: Add primitives for separate allocation and initialization.
by Simon Génier 22 Déc '20

22 Déc '20

Simon Génier pushed to branch master at Stefan / Typer Commits: ffb8bf48 by Simon Génier at 2020-12-06T21:28:13-05:00 Add primitives for separate allocation and initialization. - - - - - 955c3940 by Simon Génier at 2020-12-12T06:59:37-05:00 Fix a couple of warning 40. - - - - - 085f3f58 by Simon Génier at 2020-12-22T12:40:18-05:00 Merge branch 'warning-40-be-gone' - - - - - 5335bac8 by Simon Génier at 2020-12-22T12:40:34-05:00 Merge branch 'heap' - - - - - 10 changed files: - btl/builtins.typer - + samples/heap.typer - src/REPL.ml - src/builtin.ml - src/eval.ml - src/heap.ml - src/lexp.ml - src/opslexp.ml - src/option.ml - src/pexp.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -476,4 +476,22 @@ Test_neq = Built-in "Test.neq"; datacons-label<-string : String -> ##DataconsLabel; datacons-label<-string = Built-in "datacons-label<-string"; +Heap_unsafe-alloc : Int -> ##Heap Int; +Heap_unsafe-alloc = Built-in "Heap.alloc"; + +Heap_unsafe-free : Int -> ##Heap Unit; +Heap_unsafe-free = Built-in "Heap.free"; + +Heap_unsafe-export : Int -> ##Heap ?t; +Heap_unsafe-export = Built-in "Heap.export"; + +Heap_unsafe_store_header : Int -> ##DataconsLabel -> ##Heap Unit; +Heap_unsafe_store_header = Built-in "Heap.store-header"; + +Heap_unsafe-store-cell : Int -> Int -> ?t -> ##Heap Unit; +Heap_unsafe-store-cell = Built-in "Heap.store-cell"; + +Heap_unsafe-load-cell : Int -> Int -> ##Heap ?t; +Heap_unsafe-load-cell = Built-in "Heap.load-cell"; + %%% builtins.typer ends here. ===================================== samples/heap.typer ===================================== ===================================== src/REPL.ml ===================================== @@ -66,7 +66,7 @@ let print_input_line i = let ieval_error = Log.log_error ~section:"IEVAL" let print_and_clear_log () = - if (not Log.typer_log_config.print_at_log) then + if (not Log.typer_log_config.Log.print_at_log) then Log.print_and_clear_log () let handle_stopped_compilation msg = ===================================== src/builtin.ml ===================================== @@ -152,17 +152,14 @@ let register_builtin_csts () = add_builtin_cst "Eq" DB.type_eq; add_builtin_cst "Eq.refl" DB.eq_refl +let type_arrow_0 = + mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in - let _ = new_builtin_type - "IO" (mkArrow (Anormal, (dloc, None), - DB.type0, dloc, DB.type0)) in - let _ = new_builtin_type - "Ref" (mkArrow (Anormal, (dloc, None), - DB.type0, dloc, DB.type0)) in - let _ = new_builtin_type - "Array" (mkArrow (Anormal, (dloc, None), - DB.type0, dloc, DB.type0)) in + let _ = new_builtin_type "IO" type_arrow_0 in + let _ = new_builtin_type "Ref" type_arrow_0 in + let _ = new_builtin_type "Array" type_arrow_0 in let _ = new_builtin_type "FileHandle" DB.type0 in () ===================================== src/eval.ml ===================================== @@ -56,13 +56,18 @@ let global_eval_trace = ref ([], []) let global_eval_ctx = ref make_runtime_ctx (* let eval_max_recursion_depth = ref 23000 *) -let builtin_functions - = ref (SMap.empty : ((location -> eval_debug_info - -> value_type list -> value_type) - (* The primitive's arity. *) - * int) SMap.t) +(* eval error are always fatal *) +let error loc ?print_action msg = + Log.log_error ~section:"EVAL" ~loc:loc ?print_action msg; + Log.internal_error msg + +type builtin_function = + location -> eval_debug_info -> value_type list -> value_type + +(** A map of the function name to its implementation and arity. *) +let builtin_functions : (builtin_function * int) SMap.t ref = ref SMap.empty -let add_builtin_function name f arity = +let add_builtin_function name (f : builtin_function) arity = builtin_functions := SMap.add name (f, arity) (!builtin_functions) let append_eval_trace trace (expr : elexp) = @@ -81,11 +86,6 @@ let rec_depth trace = let (a, b) = trace in List.length b -(* eval error are always fatal *) -let error loc ?print_action msg = - Log.log_error ~section:"EVAL" ~loc ?print_action msg; - Log.internal_error msg - let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg ===================================== src/heap.ml ===================================== @@ -18,11 +18,21 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see <http://www.gnu.org/licenses/>. *) +(** A heap of Typer objects that can be partially initialized. *) + +open Builtin open Env +open Eval open Lexp -open Pexp + +module IMap = Util.IMap type location = Util.location +type symbol = Sexp.symbol +type value = Env.value_type + +type size = int +type addr = int let error ~(location : location) (message : string) : 'a = Log.log_fatal ~section:"HEAP" ~loc:location message @@ -30,11 +40,113 @@ let error ~(location : location) (message : string) : 'a = let dloc = Util.dummy_location let type0 = Debruijn.type0 let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) +let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) + +let next_free_address : addr ref = ref 1 + +type t = (symbol option ref * value option array) IMap.t ref + +let heap : t = ref IMap.empty + +let alloc (cells_count : size) : addr = + let address = !next_free_address in + next_free_address := address + 1; + heap := IMap.add address (ref None, Array.make cells_count None) !heap; + address + +let free (address : addr) : unit = + heap := IMap.remove address !heap + +(** If address points to a fully initialized object, returns it. *) +let export (address : addr) : value = + let rec export_cells cells n acc = + if n == 0 + then acc + else + let n = n - 1 in + export_cells cells n (Option.get cells.(n) :: acc) + in + let constructor, cells = IMap.find address !heap in + Env.Vcons (Option.get !constructor, export_cells cells (Array.length cells) []) + +(** Initializes the header of the object so it is valid for the given data + constructor. *) +let store_header + (location : location) + (address : addr) + (datacons : value) + : unit = -let datacons_label_of_string location depth = function + match datacons with + | Env.Vcons (symbol, []) + -> let constructor, _ = IMap.find address !heap in + constructor := Some symbol + | _ -> error ~location ("not a data constructor: " ^ Env.value_string datacons) + +(** If [address] points to an object of at least [cell_index + 1] cells, mutates + the value at that index. *) +let store_cell (address : addr) (cell_index : int) (value : value) : unit = + let _, cells = IMap.find address !heap in + cells.(cell_index) <- Some value + +(** If [address] points to an object of at least [cell_index + 1] cells and the + cell at [cell_index] is initialized, returns the value at that index. *) +let load_cell (address : addr) (cell_index : int) : value = + let _, cells = IMap.find address !heap in + Option.get cells.(cell_index) + +let datacons_label_of_string : builtin_function = + fun location _ + -> function | [Vstring _ as label] -> label - | _ -> error ~location "`##datacons-label<-string` expects 1 string argument" + | _ -> error ~location "`datacons-label<-string` expects [##DataconsLabel]." + +let heap_alloc : builtin_function = + fun location _ + -> function + | [Vint size] -> Vcommand (fun () -> Vint (alloc size)) + | _ -> error ~location "`Heap.alloc` expects [Int]." + +let heap_free : builtin_function = + fun location _ + -> function + | [Vint address] -> Vcommand (fun () -> free address; Vint 0) + | _ -> error ~location "`Heap.free` expects [Int]." + +let heap_export : builtin_function = + fun location _ + -> function + | [Vint address] -> Vcommand (fun () -> export address) + | _ -> error ~location "`Heap.export` expects [Int]." + +let heap_store_header : builtin_function = + fun location _ + -> function + | [Vint address; datacons] + -> Vcommand (fun () -> store_header location address datacons; Vint 0) + | _ -> error ~location "`Heap.store-header` expects [Int; 'a]" + +let heap_store_cell : builtin_function = + fun location _ + -> function + | [Vint address; Vint cell_index; value] + -> Vcommand (fun () -> store_cell address cell_index value; Vint 0) + | _ -> error ~location "`Heap.store-header` expects [Int; Int; 'a]" + +let heap_load_cell : builtin_function = + fun location _ + -> function + | [Vint address; Vint cell_index; value] + -> Vcommand (fun () -> load_cell address cell_index) + | _ -> error ~location "`Heap.store-cell` expects [Int; Int]" let register_builtins () = - Builtin.add_builtin_cst "DataconsLabel" type_datacons_label; - Eval.add_builtin_function "datacons-label<-string" datacons_label_of_string 1 + add_builtin_cst "DataconsLabel" type_datacons_label; + add_builtin_cst "Heap" type_heap; + add_builtin_function "datacons-label<-string" datacons_label_of_string 1; + add_builtin_function "Heap.alloc" heap_alloc 1; + add_builtin_function "Heap.free" heap_alloc 1; + add_builtin_function "Heap.export" heap_alloc 1; + add_builtin_function "Heap.store-header" heap_store_header 2; + add_builtin_function "Heap.store-cell" heap_store_cell 3; + add_builtin_function "Heap.load-cell" heap_load_cell 2; ===================================== src/lexp.ml ===================================== @@ -40,6 +40,8 @@ type meta_id = int (* Identifier of a meta variable. *) type label = symbol +include Pexp.ArgKind + (*************** Elaboration to Lexp *********************) (* The scoping of `Let` is tricky: ===================================== src/opslexp.ml ===================================== @@ -194,7 +194,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + mkCall (DB.eq_refl, + [L.Aerasable, elevel; + L.Aerasable, etype; + L.Aerasable, e]) in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -423,10 +426,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(L.Aerasable, tlvl); (* Typelevel *) + (L.Aerasable, tltp); (* Inductive type *) + (L.Anormal, hlxp); (* Lexp of the branch head *) + (L.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -773,12 +776,12 @@ and check'' erased ctx e = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(L.Aerasable, tlvl); (* Typelevel *) + (L.Aerasable, tltp); (* Inductive type *) + (L.Anormal, hlxp); (* Lexp of the branch head *) + (L.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push Aerasable nerased in + let nerased = dbset_push L.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter ===================================== src/option.ml ===================================== @@ -25,3 +25,8 @@ let equal (inner_equal : 'a -> 'a -> bool) (l : 'a t) (r : 'a t) : bool = | Some l, Some r -> inner_equal l r | None, None -> true | _ -> false + +let get (o : 'a option) : 'a = + match o with + | Some v -> v + | None -> invalid_arg "expected Some" ===================================== src/pexp.ml ===================================== @@ -29,7 +29,10 @@ let pexp_error loc = Log.log_error ~section:"PEXP" ~loc (*************** The Pexp Parser *********************) -type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +module ArgKind = struct + type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +end +include ArgKind (* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5a31e9929baf768c824a9ddc3421007a… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5a31e9929baf768c824a9ddc3421007a… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][ja/various_fixes] 5 commits: Qualify the constructors to fix warning 40.
by Jean-Alexandre Barszcz 15 Déc '20

15 Déc '20

Jean-Alexandre Barszcz pushed to branch ja/various_fixes at Stefan / Typer Commits: c3a0c909 by Simon Génier at 2020-12-15T13:40:02-05:00 Qualify the constructors to fix warning 40. - - - - - 88ed302a by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars. - - - - - bca144df by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump. - - - - - 2e6e34d2 by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional. - - - - - 4d942a98 by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/opslexp.ml (fv): Check that the memoized value is still ok. - - - - - 5 changed files: - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/opslexp.ml - tests/unify_test.ml Changes: ===================================== src/REPL.ml ===================================== @@ -66,7 +66,7 @@ let print_input_line i = let ieval_error = Log.log_error ~section:"IEVAL" let print_and_clear_log () = - if (not Log.typer_log_config.print_at_log) then + if (not Log.typer_log_config.Log.print_at_log) then Log.print_and_clear_log () let handle_stopped_compilation msg = ===================================== src/debruijn.ml ===================================== @@ -43,6 +43,7 @@ module M = Myers open Fmt module S = Subst +module P = Pexp let fatal = Log.log_fatal ~section:"DEBRUIJN" @@ -99,13 +100,13 @@ let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, + mkArrow (P.Aerasable, lv, type_level, dloc, - mkArrow (Aerasable, tv, + mkArrow (P.Aerasable, tv, mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), + mkArrow (P.Anormal, (dloc, None), mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), + mkArrow (P.Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) @@ -114,17 +115,17 @@ let eq_refl = let tv = (dloc, Some "t") in let xv = (dloc, Some "x") in mkBuiltin ((dloc, "Eq.refl"), - mkArrow (Aerasable, lv, + mkArrow (P.Aerasable, lv, type_level, dloc, - mkArrow (Aerasable, tv, + mkArrow (P.Aerasable, tv, mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, + mkArrow (P.Aerasable, xv, mkVar (tv, 0), dloc, mkCall (type_eq, - [Aerasable, mkVar (lv, 2); - Aerasable, mkVar (tv, 1); - Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)]))))) + [P.Aerasable, mkVar (lv, 2); + P.Aerasable, mkVar (tv, 1); + P.Anormal, mkVar (xv, 0); + P.Anormal, mkVar (xv, 0)]))))) (* easier to debug with type annotations *) ===================================== src/elab.ml ===================================== @@ -1690,11 +1690,16 @@ let rec sform_case ctx loc sargs ot = match sargs with let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in - (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer sbody (ectx_new_scope nctx) in - let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx, - Inferred (mkSusp ltp s)) + let s, off = + List.fold_left (fun (s, off) decls -> + (OL.lexp_defs_subst loc s decls, off + List.length decls)) + (S.identity, 0) declss in + let ot = U.option_map (fun t -> mkSusp t (S.shift off)) ot in + let bdy, ot = elaborate nctx sbody ot in + let ot = match ot with + | Inferred t -> Inferred (mkSusp t s) + | _ -> ot in + (lexp_let_decls declss bdy nctx, ot) | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc ===================================== src/opslexp.ml ===================================== @@ -194,7 +194,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + mkCall (DB.eq_refl, + [P.Aerasable, elevel; + P.Aerasable, etype; + P.Aerasable, e]) in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -423,10 +426,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(P.Aerasable, tlvl); (* Typelevel *) + (P.Aerasable, tltp); (* Inductive type *) + (P.Anormal, hlxp); (* Lexp of the branch head *) + (P.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -773,12 +776,12 @@ and check'' erased ctx e = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(P.Aerasable, tlvl); (* Typelevel *) + (P.Aerasable, tltp); (* Inductive type *) + (P.Anormal, hlxp); (* Lexp of the branch head *) + (P.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push Aerasable nerased in + let nerased = dbset_push P.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter @@ -972,11 +975,22 @@ and fv (e : lexp) : (DB.set * mv_set) = -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in - (* FIXME: Flush the memoization table whenever the metavar table - * is modified, since that can affect the output of `fv`. *) - try LMap.find fv_memo e - with Not_found - -> let r = fv' e in + let ofvs = LMap.find_opt fv_memo e in + (* The memoized value depends on the metavariable table. When it + changes, we have to recompute the free variables. Instead of + flushing the table after every instantiation, we check that no + free metavars are actually instantiated. For this to work, we + assume that the table changes monotonously: metavariables can be + instantiated, but the instantiations cannot be undone. *) + match ofvs with + | Some ((_, (mvfs, _)) as fvs) + when IMap.for_all + (fun mv _ -> match metavar_lookup mv with + | MVar _ -> true + | MVal _ -> false) + mvfs + -> fvs + | _ -> let r = fv' e in LMap.add fv_memo e r; r @@ -1170,6 +1184,9 @@ and clean_map cases = (l, args, erase_type (L.push_susp expr subst)) in SMap.map clean_branch cases +(* The following entry points to erasure, `erase_type` and + `clean_decls`, check that no metavariables are left before + performing the erasure itself. *) let erase_type lxp = let _, (mvs, _) = fv lxp in if not (IMap.is_empty mvs) then @@ -1183,6 +1200,11 @@ let erase_type lxp = ("Metavariables in erase_type :"); erase_type lxp +(* Textually identical to the previous definition of `clean_decls`, + but calls the new `erase_type`, which checks for metavars. *) +let clean_decls decls = + List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls + (** Turning a set of declarations into an object. **) ===================================== tests/unify_test.ml ===================================== @@ -29,6 +29,7 @@ open Fmt open Utest_lib module U = Util +module P = Pexp (* default environment *) let ectx = Elab.default_ectx @@ -98,10 +99,10 @@ let _ = (fun (ectx, i) (name, lexp) -> Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, + [("f", (mkArrow (P.Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("g", (mkArrow (P.Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("h", (mkArrow (P.Anormal, (dloc, Some "x"), nat, dloc, + mkArrow (P.Anormal, (dloc, Some "y"), shift nat 1, dloc, shift nat 2)))); ("a", nat); ("b", nat)] in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/98273563cc1b270e59974d242b47e485… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/98273563cc1b270e59974d242b47e485… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][sexp-case] 4 commits: Add a sexp-case macro.
by Simon Génier 12 Déc '20

12 Déc '20

Simon Génier pushed to branch sexp-case at Stefan / Typer Commits: aadf51c9 by Simon Génier at 2020-12-12T05:50:08-05:00 Add a sexp-case macro. This macro lets you write case-like expressions for Sexp, which I hope are neater than Sexp_dispatch. The code is quite tedious because it is written to be loaded quite early, before some key macros like the enhanced case and lambda. This is because sexp-case is meant to help macro authorship, including these quite complicated macros! It was also necessary to shuffle a few definitions in pervasive.typer to allow us to write it as early as possible. Was it a waste of time to write this macro when Sexp_wrapper exists? Probably. I was not aware of the existence of Sexp_wrapper until I was almost done with sexp-case_. - - - - - 36bdbe04 by Simon Génier at 2020-12-12T05:50:30-05:00 Use sexp-case in a few places. - - - - - 272c2a39 by Simon Génier at 2020-12-12T06:53:24-05:00 Better error messages when => is missing in sexp-case. - - - - - 7060dab9 by Simon Génier at 2020-12-12T07:21:13-05:00 Use sexp-case in case.typer. - - - - - 3 changed files: - btl/case.typer - btl/pervasive.typer - + btl/sexp-case.typer Changes: ===================================== btl/case.typer ===================================== @@ -70,30 +70,24 @@ in Sexp_node (Sexp_symbol "##datacons") %% `cons expr1 expr2 ... ` %% expand-tuple-ctor : Sexp -> Sexp; -expand-tuple-ctor sexp = let - - err = (lambda _ -> Sexp_error); - -in Sexp_dispatch sexp - (lambda s ss -> +expand-tuple-ctor sexp = + sexp-case sexp + | node s ss => if (Sexp_eq s (Sexp_symbol "_\,_")) then (Sexp_node tuple-ctor ss) else - (Sexp_node s ss)) - (lambda _ -> sexp) - err err err err; + (Sexp_node s ss) + | symbol _ => sexp + | _ => Sexp_error; %% %% Is tuple %% tuple? : Sexp -> Bool; -tuple? sexp = let - - sfalse = (lambda _ -> false); - -in Sexp_dispatch sexp - (lambda s _ -> Sexp_eq s tuple-ctor) - sfalse sfalse sfalse sfalse sfalse; +tuple? sexp = + sexp-case sexp + | node s _ => Sexp_eq s tuple-ctor + | _ => false; %% %% Get matched expression (e.g. case (var1,var2,...) | ...) @@ -108,20 +102,15 @@ in Sexp_dispatch sexp %% It used to be more useful.) %% get-tup-exprs : Sexp -> List Sexp; -get-tup-exprs sexp = let - - err = (lambda _ -> cons Sexp_error nil); - - get-tup-exprs-helper : Sexp -> List Sexp -> List Sexp; - get-tup-exprs-helper s ss = case (Sexp_eq (Sexp_symbol "_\,_") s) - | true => cons (Sexp_node s ss) nil % tuple - %% constructor or function called (only 1 pattern) - | false => cons (Sexp_node s ss) nil; - -in Sexp_dispatch sexp - get-tup-exprs-helper - (lambda s -> cons (Sexp_symbol s) nil) - err err err err; +get-tup-exprs sexp = + sexp-case sexp + | node s ss => + (case (Sexp_eq (Sexp_symbol "_\,_") s) + | true => cons (Sexp_node s ss) nil % tuple + %% constructor or function called (only 1 pattern) + | false => cons (Sexp_node s ss) nil) + | symbol s => cons (Sexp_symbol s) nil + | _ => cons Sexp_error nil; %% %% Some alias to clarify type of functions @@ -148,9 +137,6 @@ dflt? v = Sexp_eq dflt-var v; %% get-branches : List Sexp -> List Sexp -> List (Pair Pats Code); get-branches vars sexps = let - - perr = (lambda _ -> pair (cons Pat_error nil) Code_error); - %% here, sexp is a node of patterns (the lhs of a "_=>_"-node) to-case : Sexp -> Pair Pats Code; to-case sexp = let @@ -161,14 +147,14 @@ get-branches vars sexps = let else (List_map expand-tuple-ctor (get-tup-exprs sexp)); - in Sexp_dispatch sexp - - (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) - %% expecting a Sexp_node as second argument to _=>_ - | true => pair (tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) - | false => pair (cons Pat_error nil) Code_error) - - perr perr perr perr perr; + in + sexp-case sexp + | node s ss => + (case (Sexp_eq (Sexp_symbol "_=>_") s) + %% expecting a Sexp_node as second argument to _=>_ + | true => pair (tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) + | false => pair (cons Pat_error nil) Code_error) + | _ => pair (cons Pat_error nil) Code_error; %% map all "_=>_"-node to (patterns, body) pair helper : List Sexp -> List (Pair Pats Code); @@ -184,40 +170,38 @@ in helper sexps; %% kinds : Sexp -> IO (List Bool); kinds pat = let - - %% - %% errors used in Sexp_dispatch - %% - serr = lambda _ -> Sexp_error; - strerr = K "< error >"; - xserr = lambda _ -> (nil : List Sexp); - %% %% Get constructor of `pat` %% ctor : String; ctor = let ctor-name : Sexp -> String; - ctor-name pat = Sexp_dispatch pat - (lambda s ss -> ctor-name s) - I strerr strerr strerr strerr; + ctor-name pat = + sexp-case pat + | node s _ => ctor-name s + | symbol s => s + | _ => "< error >"; in ctor-name pat; %% %% Get args from the `pat` node %% args : List Sexp; - args = Sexp_dispatch pat - (lambda s ss -> ss) - (lambda _ -> (nil : List Sexp)) % FIXME: Redundant type annotation. - xserr xserr xserr xserr; + args = + sexp-case pat + | node _ ss => ss + | _ => + % FIXME: Redundant type annotation. + (nil : List Sexp); %% %% Just get a String from a symbol %% str_of_sym : Sexp -> String; - str_of_sym arg = Sexp_dispatch arg - (lambda _ _ -> "< error >") I strerr strerr strerr strerr; + str_of_sym arg = + sexp-case arg + | symbol s => s + | _ => "< error >"; %% %% map function for all pattern's variables @@ -230,20 +214,17 @@ kinds pat = let %% arguments with name, other without name and all this in a random order %% mf : Elab_Context -> Sexp -> Int -> Bool; - mf env arg i = Sexp_dispatch arg - (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:=_")) then - ( if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then - (Elab_is-nth-erasable ctor i env) - else - (Elab_is-arg-erasable ctor (str_of_sym (List_nth 0 ss Sexp_error)) env) ) - else - (false)) - (lambda _ -> false) - (lambda _ -> false) - (lambda _ -> false) - (lambda _ -> false) - (lambda _ -> false); - + mf env arg i = + sexp-case arg + | node s ss => + if (Sexp_eq s (Sexp_symbol "_:=_")) then + (if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then + (Elab_is-nth-erasable ctor i env) + else + (Elab_is-arg-erasable ctor (str_of_sym (List_nth 0 ss Sexp_error)) env) ) + else + (false) + | _ => false; %% %% What to do if argument are named (`(arg-name := x)`)? @@ -265,14 +246,6 @@ in ks; %% renamed-pat : Sexp -> List Sexp -> IO Sexp; renamed-pat pat names = let - - %% - %% errors used in Sexp_dispatch - %% - serr = lambda _ -> Sexp_error; - strerr = lambda _ -> "< error >"; - xserr = lambda _ -> (nil : List Sexp); - %% %% true if `pat` is a tuple, false if it is a %% single expression @@ -290,10 +263,11 @@ renamed-pat pat names = let %% Get the constructor of the pattern as argument %% ctor : Sexp -> String; - ctor pat = Sexp_dispatch pat - (lambda s _ -> ctor s) - (lambda s -> s) - strerr strerr strerr strerr; + ctor pat = + sexp-case pat + | node s _ => ctor s + | symbol s => s + | _ => "< error >"; %% %% Map function to rename `pat` with symbol in `names` @@ -305,8 +279,9 @@ renamed-pat pat names = let %% and if it already use explicit field or not %% mf : List Bool -> Sexp -> Int -> Sexp; - mf kinds v i = Sexp_dispatch v - (lambda sym ss -> + mf kinds v i = + sexp-case v + | node sym ss => if (Sexp_eq sym (Sexp_symbol "_:=_")) then if (List_nth i kinds false) then %% if client use multiple name for the same erasable args, @@ -319,21 +294,22 @@ renamed-pat pat names = let (Sexp_node (Sexp_symbol "_:=_") (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else - (List_nth i names Sexp_error)) - (lambda _ -> if tup then + (List_nth i names Sexp_error) + | symbol _ => if tup then (Sexp_node (Sexp_symbol "_:=_") (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else - (List_nth i names Sexp_error)) - serr serr serr serr; + (List_nth i names Sexp_error) + | _ => Sexp_error; in do { pat <- IO_return pat; kinds <- kinds pat; - IO_return (Sexp_dispatch pat - (lambda s ss -> Sexp_node s (List_mapi (mf kinds) ss)) - (lambda s -> Sexp_symbol s) - serr serr serr serr); + IO_return + (sexp-case pat + | node s ss => Sexp_node s (List_mapi (mf kinds) ss) + | symbol s => Sexp_symbol s + | _ => Sexp_error); }; %% @@ -342,34 +318,28 @@ in do { %% is-pat : Pat -> IO Bool; is-pat pat = let - - %% - %% errors used in Sexp_dispatch - %% - err = lambda _ -> IO_return false; - serr = lambda _ -> "< error >"; - %% %% Get a String from a Sexp_symbol %% sym-str : Sexp -> String; - sym-str sexp = Sexp_dispatch sexp - (lambda _ _ -> serr ()) - (lambda str -> str) - serr serr serr serr; - -in Sexp_dispatch pat - (lambda sym _ -> do { + sym-str sexp = + sexp-case sexp + | symbol str => str + | _ => "< error >"; + +in + sexp-case pat + | node sym _ => do { env <- Elab_getenv (); ctor <- IO_return (Elab_isconstructor (sym-str sym) env); tupl <- IO_return (Sexp_eq sym (Sexp_symbol "_\,_")); IO_return (or ctor tupl); - }) - (lambda sym -> do { + } + | symbol sym => do { env <- Elab_getenv (); IO_return (Elab_isconstructor sym env); - }) - err err err err; + } + | _ => IO_return false; %% %% Takes two pattern and return true if the two pattern @@ -377,20 +347,15 @@ in Sexp_dispatch pat %% same-ctor? : Pat -> Pat -> Bool; same-ctor? p0 p1 = let - - %% - %% error used in Sexp_dispatch - %% - err = lambda _ -> Pat_error; - %% %% Get the constructor of a pattern %% ctor-of : Pat -> Sexp; - ctor-of p = Sexp_dispatch p - (lambda s _ -> s) - (lambda s -> Sexp_symbol s) - err err err err; + ctor-of pat = + sexp-case pat + | node s _ => s + | symbol _ => pat + | _ => Pat_error; %% Compare head of node of both pattern in Sexp_eq (ctor-of p0) (ctor-of p1); @@ -403,12 +368,6 @@ in Sexp_eq (ctor-of p0) (ctor-of p1); %% introduced-vars : Pat -> IO (List Var); introduced-vars pat = let - - %% - %% error used in Sexp_dispatch - %% - serr = lambda _ -> IO_return (pair 0 nil); - %% %% List of kind of pattern argument %% @@ -433,8 +392,9 @@ introduced-vars pat = let IO_return (case p | pair x _ => x); }; - in Sexp_dispatch v - (lambda s ss -> do { + in + sexp-case v + | node s ss => do { o <- o; % bind i <- i; ks <- ks; @@ -445,8 +405,8 @@ introduced-vars pat = let (IO_return (pair (i + 1) (List_concat o (cons (List_nth 1 ss Var_error) nil)))) else (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))); - }) - (lambda s -> do { + } + | symbol s => do { o <- o; % bind i <- i; sym <- IO_return (Sexp_symbol s); @@ -455,18 +415,16 @@ introduced-vars pat = let (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))) else (IO_return (pair (i + 1) (List_concat o (cons sym nil)))); - }) - serr serr serr serr; + } + | _ => IO_return (pair 0 nil); -in Sexp_dispatch pat - (lambda _ ss -> do { +in + sexp-case pat + | node _ ss => do { p <- (List_foldl ff (IO_return (pair 0 nil)) ss); - IO_return (case p - | pair _ xs => xs); - }) - (lambda _ -> IO_return nil) % constructor as a unique symbol (`true`, etc) - (lambda _ -> IO_return nil) (lambda _ -> IO_return nil) % error - (lambda _ -> IO_return nil) (lambda _ -> IO_return nil); % error + IO_return (case p | pair _ xs => xs); + } + | _ => IO_return nil; %% %% Wrap the third argument (`fun`) with a `let` definition for each variables @@ -503,9 +461,6 @@ in List_map mf ps; %% pattern-sub-pats : Pat -> IO (List Pat); pattern-sub-pats pat = let - - err = lambda _ -> IO_return nil; - %% %% dflt-var mean there's no sub pattern %% @@ -522,17 +477,18 @@ pattern-sub-pats pat = let (IO_return dflt-var); }; -in Sexp_dispatch pat - (lambda ctor args -> do { +in + sexp-case pat + | node ctor args => do { r <- io-list (List_map map-arg args); IO_return r; - }) - (lambda sym -> do { + } + | symbol sym => do { %% constructor has no argument %% so there can't be any sub pattern IO_return nil; - }) - err err err err; + } + | _ => IO_return nil; %% %% Takes a List of similar pattern (i.e. patterns with same constructor) @@ -1025,7 +981,9 @@ case-impl args = let %% Expecting only one Sexp_node containing a case with arguments -in (Sexp_dispatch (List_nth 0 args Sexp_error) - case1 err err err err err); +in + sexp-case List_nth 0 args Sexp_error + | node s ss => case1 s ss + | _ => IO_return Sexp_error; case-macro = macro case-impl; ===================================== btl/pervasive.typer ===================================== @@ -36,6 +36,18 @@ Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); some = datacons Option some; none = datacons Option none; +%%%% `Result` type + +Result : Type -> Type -> Type; +Result = lambda α -> lambda β -> typecons Result (ok α) (err β); + +ok : (α : Type) ≡> (β : Type) ≡> α -> Result α β; +ok = lambda α ≡> lambda β ≡> datacons (Result α β) ok; + +err : (α : Type) ≡> (β : Type) ≡> β -> Result α β; +err = lambda α ≡> lambda β ≡> datacons (Result α β) err; + + %%%% List functions List_length : List ?a -> Int; % Recursive defs aren't generalized :-( @@ -84,25 +96,99 @@ List_nth = lambda n -> lambda xs -> lambda d -> case xs | true => x | false => List_nth (n - 1) xs d; -%%%% A more flexible `lambda` +%%%% Quasi-Quote macro + +%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) +%% +%% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) +%% +%% => x %% An `Sexp` which we use to represents an *error*. Sexp_error = Sexp_symbol "<error>"; +%% Takes an Sexp `x` as argument and return an Sexp which represents code +%% which will construct an Sexp equivalent to `x` at run-time. +%% This is basically *cross stage persistence* for Sexp. +quote1 : Sexp -> Sexp; +quote1 x = let + qlist : List Sexp -> Sexp; + qlist xs = case xs + | nil => Sexp_symbol "nil" + | cons x xs => Sexp_node (Sexp_symbol "cons") + (cons (quote1 x) + (cons (qlist xs) nil)); + make_app = lambda str -> lambda sexp -> + Sexp_node (Sexp_symbol str) (cons sexp nil); + + node = lambda op -> lambda y -> + case (Sexp_eq op (Sexp_symbol "uquote")) + | true => List_head Sexp_error y + | false => Sexp_node (Sexp_symbol "##Sexp.node") + (cons (quote1 op) + (cons (qlist y) nil)); + symbol s = make_app "##Sexp.symbol" (Sexp_string s); + string s = make_app "##Sexp.string" (Sexp_string s); + integer i = make_app "##Sexp.integer" + (make_app "##Int->Integer" (Sexp_integer i)); + float f = make_app "##Sexp.float" (Sexp_float f); + block sxp = + %% FIXME ##Sexp.block takes a string (and prelexes + %% it) but we have a sexp, what should we do? + Sexp_symbol "<error FIXME block quoting>"; + in Sexp_dispatch x node symbol string integer float block; + +%% quote definition +quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); + +%%%% "Module" access + +__\.__ = + let mksel = lambda o -> lambda f -> + let constructor = Sexp_node (Sexp_symbol "##datacons") + (cons (Sexp_symbol "?") + (cons (Sexp_symbol "cons") + nil)); + pattern = Sexp_node constructor + (cons (Sexp_node (Sexp_symbol "_:=_") + (cons f (cons (Sexp_symbol "v") + nil))) + nil); + branch = Sexp_node (Sexp_symbol "_=>_") + (cons pattern (cons (Sexp_symbol "v") nil)); + in Sexp_node (Sexp_symbol "case_") + (cons (Sexp_node (Sexp_symbol "_|_") + (cons o (cons branch nil))) + nil) + in macro (lambda args + -> IO_return + case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error); + +%%%% Sexp-Case macro + +define-operator "sexp-case" () 43; +sexp-case-lib = load "btl/sexp-case.typer"; +sexp-case_ = macro (lambda (sexps : List Sexp) -> IO_return (sexp-case-lib.sexp-case-impl sexps)); + +%%%% A more flexible `lambda` + %% Sexp_to_list : Sexp -> List Sexp -> List Sexp; Sexp_to_list s = lambda exceptions -> - let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! - Sexp_dispatch - s - (node := lambda head -> lambda tail - -> case List_find (Sexp_eq head) exceptions - | some _ => singleton () + sexp-case s + | node head tail + => (case List_find (Sexp_eq head) exceptions + | some _ => cons s nil | none => cons head tail) - (symbol := lambda s - -> case String_eq "" s + | symbol name + => (case String_eq "" name | true => nil - | false => singleton ()) - singleton singleton singleton singleton; + | false => cons s nil) + | _ => cons s nil; multiarg_lambda = %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. @@ -191,47 +277,6 @@ I x = x; K : ?a -> (b : Type) ≡> b -> ?a; K x y = x; -%%%% Quasi-Quote macro - -%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) -%% -%% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) -%% -%% => x - -%% Takes an Sexp `x` as argument and return an Sexp which represents code -%% which will construct an Sexp equivalent to `x` at run-time. -%% This is basically *cross stage persistence* for Sexp. -quote1 : Sexp -> Sexp; -quote1 x = let - qlist : List Sexp -> Sexp; - qlist xs = case xs - | nil => Sexp_symbol "nil" - | cons x xs => Sexp_node (Sexp_symbol "cons") - (cons (quote1 x) - (cons (qlist xs) nil)); - make_app str sexp = - Sexp_node (Sexp_symbol str) (cons sexp nil); - - node op y = case (Sexp_eq op (Sexp_symbol "uquote")) - | true => List_head Sexp_error y - | false => Sexp_node (Sexp_symbol "##Sexp.node") - (cons (quote1 op) - (cons (qlist y) nil)); - symbol s = make_app "##Sexp.symbol" (Sexp_string s); - string s = make_app "##Sexp.string" (Sexp_string s); - integer i = make_app "##Sexp.integer" - (make_app "##Int->Integer" (Sexp_integer i)); - float f = make_app "##Sexp.float" (Sexp_float f); - block sxp = - %% FIXME ##Sexp.block takes a string (and prelexes - %% it) but we have a sexp, what should we do? - Sexp_symbol "<error FIXME block quoting>"; - in Sexp_dispatch x node symbol string integer float block; - -%% quote definition -quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); - %%%% The `type` declaration macro %% Build a declaration: @@ -273,52 +318,37 @@ type-impl = lambda (x : List Sexp) -> %% Type name --^ ^------^ constructors %% Return a list contained inside a node sexp. - let knil = K nil; - kerr = K Sexp_error; - - get-list : Sexp -> List Sexp; - get-list node = Sexp_dispatch node - (lambda op lst -> lst) % Nodes - knil % Symbol - knil % String - knil % Integer - knil % Float - knil; % List of Sexp + let get-list : Sexp -> List Sexp; + get-list node = + sexp-case node + | node _ lst => lst + | _ => (nil : List Sexp); %% Get a name (symbol) from a sexp %% - (name t) -> name %% - name -> name get-name : Sexp -> Sexp; get-name sxp = - Sexp_dispatch sxp - (lambda op _ -> get-name op) % Nodes - (lambda _ -> sxp) % Symbol - kerr % String - kerr % Integer - kerr % Float - kerr; % List of Sexp + sexp-case sxp + | node op _ => get-name op + | symbol _ => sxp + | _ => Sexp_error; get-args : Sexp -> List Sexp; get-args sxp = - Sexp_dispatch sxp - (lambda _ args -> args) % Nodes - (lambda _ -> (nil : List Sexp)) % Symbol - (lambda _ -> (nil : List Sexp)) % String - (lambda _ -> (nil : List Sexp)) % Integer - (lambda _ -> (nil : List Sexp)) % Float - (lambda _ -> (nil : List Sexp)); % List of Sexp + sexp-case sxp + | node _ args => args + | _ => (nil : List Sexp); get-type : Sexp -> Sexp; get-type sxp = - Sexp_dispatch sxp - (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error - | false => sxp) - (lambda _ -> sxp) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error); + sexp-case sxp + | node s ss + => (case Sexp_eq s (Sexp_symbol "_:_") + | true => List_nth 1 ss Sexp_error + | false => sxp) + | symbol _ => sxp + | _ => Sexp_error; get-head = List_head Sexp_error; @@ -404,32 +434,6 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair; -__\.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); - %% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) | triplet (x : a) (y : b) (z : c); @@ -677,14 +681,9 @@ Test_file = macro (lambda args -> let (cons (Sexp_symbol "unit") nil); %% Expecting a String and nothing else -in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) - (lambda _ _ -> ret) - (lambda _ -> ret) - %% `load` is a special form and takes a Sexp rather than a real `String` - (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) - (lambda _ -> ret) - (lambda _ -> ret) - (lambda _ -> ret)) +in IO_return (sexp-case List_nth 0 args Sexp_error + | string s => quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test) + | _ => ret) ); %%% pervasive.typer ends here. ===================================== btl/sexp-case.typer ===================================== @@ -0,0 +1,426 @@ +%%% sexp-case.typer --- Case-like syntactic sugar for Sexp_dispatch. +%%% +%%% Language: builtins, quote, and uquote. + +NodeAcc : Type; +NodeAcc = + typecons + NodeAcc + (node-acc (head-var : Sexp) (tail-var : Sexp) (expr : Sexp)) +; + +node-acc : Sexp -> Sexp -> Sexp -> NodeAcc; +node-acc = datacons NodeAcc node-acc; + +AtomAcc : Type; +AtomAcc = typecons AtomAcc (atom-acc (var : Sexp) (expr : Sexp)); + +atom-acc : Sexp -> Sexp -> AtomAcc; +atom-acc = datacons AtomAcc atom-acc; + +SexpCaseAcc : Type; +SexpCaseAcc = + typecons + SexpCaseAcc + (sexp-case-acc + (node-acc : Option NodeAcc) + (symbol-acc : Option AtomAcc) + (string-acc : Option AtomAcc) + (int-acc : Option AtomAcc) + (float-acc : Option AtomAcc) + (block-acc : Option AtomAcc) + (otherwise-expr : Sexp)) +; + +sexp-case-acc : + Option NodeAcc -> + Option AtomAcc -> + Option AtomAcc -> + Option AtomAcc -> + Option AtomAcc -> + Option AtomAcc -> + Sexp -> + SexpCaseAcc +; +sexp-case-acc = datacons SexpCaseAcc sexp-case-acc; + +sexp<-sexp-case-acc : Sexp -> SexpCaseAcc -> Sexp; +sexp<-sexp-case-acc = lambda target -> lambda acc -> + let + otherwise-expr = + case acc + | sexp-case-acc _ _ _ _ _ _ otherwise-expr => otherwise-expr + ; + + node-λ = + case acc + | sexp-case-acc node-acc' _ _ _ _ _ _ => + case node-acc' + | none => quote (lambda _ -> lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | node-acc head-var tail-var expr => + quote + (lambda (uquote head-var) -> + lambda (uquote tail-var) -> + (uquote expr)) + ; + + symbol-λ = + case acc + | sexp-case-acc _ symbol-acc _ _ _ _ _ => + case symbol-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + string-λ = + case acc + | sexp-case-acc _ _ string-acc _ _ _ _ => + case string-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + int-λ = + case acc + | sexp-case-acc _ _ _ int-acc _ _ _ => + case int-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + float-λ = + case acc + | sexp-case-acc _ _ _ _ float-acc _ _ => + case float-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + block-λ = + case acc + | sexp-case-acc _ _ _ _ _ block-acc _ => + case block-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + in + quote + (Sexp_dispatch + (uquote target) + (uquote node-λ) + (uquote symbol-λ) + (uquote string-λ) + (uquote int-λ) + (uquote float-λ) + (uquote block-λ)) +; + +%% +%% Case-like syntax for sexps that expands to a call to Sexp_dispatch. +%% +%% For example, +%% +%% sexp-case ?e +%% | node h t => ?e-node +%% | symbol n => ?e-symbol +%% | _ => ?e-else +%% +%% is turned into +%% +%% Sexp_dispatch +%% ?e +%% (lambda h t -> ?e-node) +%% (lambda n -> ?e-symbol) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% +%% TODO: allow subpatterns? +%% +%% sexp-case ?e +%% | node (symbol "_=>_") (cons pattern (cons expr nil)) => ?e-double-arrow +%% | _ => ?e-else +%% +sexp-case-impl : List Sexp -> Sexp; +sexp-case-impl = lambda args -> + let + not-bottom : Sexp; + not-bottom = Sexp_symbol "_|_"; + + sexp-symbol-name : Sexp -> Option String; + sexp-symbol-name = lambda perhaps-a-symbol -> + let none-string = none (a := String) + in + Sexp_dispatch + perhaps-a-symbol + (lambda _ -> lambda _ -> none-string) + (lambda name -> some name) + (lambda _ -> none-string) + (lambda _ -> none-string) + (lambda _ -> none-string) + (lambda _ -> none-string) + ; + + parse-node-pattern : + SexpCaseAcc -> + Sexp -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-node-pattern = lambda acc -> lambda expr -> lambda pargs -> + case pargs + | nil => err "todo 1" + | cons head-var pargs' => + case pargs' + | nil => err "todo 2" + | cons tail-var pargs'' => + case pargs'' + | cons _ _ => err "todo 3" + | nil => + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case na + | some _ => err "todo 4" + | none => + let na' = some (node-acc head-var tail-var expr) + in ok (sexp-case-acc na' sym-a str-a ia fa ba oe) + ; + + parse-atom-pattern : + String -> + (Sexp -> Result SexpCaseAcc String) -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-atom-pattern = + lambda pattern-name -> lambda update-acc -> lambda pargs -> + case pargs + | nil => + err (String_concat "missing binding for pattern " pattern-name) + | cons var pargs' => + case pargs' + | cons _ _ => + err (String_concat "too many bindings for pattern " pattern-name) + | nil => + update-acc var + ; + + update-symbol-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-symbol-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case sym-a + | some _ => err "multiple symbol patterns" + | none => + let sym-a' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a' str-a ia fa ba oe) + ; + + update-string-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-string-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case str-a + | some _ => err "multiple string patterns" + | none => + let str-a' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a' ia fa ba oe) + ; + + update-int-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-int-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case ia + | some _ => err "multiple int patterns" + | none => + let ia' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a ia' fa ba oe) + ; + + update-float-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-float-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case fa + | some _ => err "multiple float patterns" + | none => + let fa' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a ia fa' ba oe) + ; + + update-block-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-block-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case ba + | some _ => err "multiple block patterns" + | none => + let ba' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a ia fa ba' oe) + ; + + parse-otherwise-pattern : + SexpCaseAcc -> + Sexp -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-otherwise-pattern = lambda acc -> lambda expr -> lambda pargs -> + case pargs + | cons _ _ => err "stray syntax after _" + | nil => + case acc + | sexp-case-acc na sym-a str-a ia fa ba _ => + ok (sexp-case-acc na sym-a str-a ia fa ba expr) + ; + + parse-pattern : + SexpCaseAcc -> + Sexp -> + Sexp -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-pattern = lambda acc -> lambda expr -> lambda head -> lambda tail -> + case sexp-symbol-name head + | none => err "not a symbol" + | some name => + case String_eq name "node" + | true => + parse-node-pattern acc expr tail + | false => + case String_eq name "symbol" + | true => + parse-atom-pattern "symbol" (update-symbol-acc acc expr) tail + | false => + case String_eq name "string" + | true => + parse-atom-pattern "string" (update-string-acc acc expr) tail + | false => + case String_eq name "int" + | true => + parse-atom-pattern "int" (update-int-acc acc expr) tail + | false => + case String_eq name "float" + | true => + parse-atom-pattern "float" (update-float-acc acc expr) tail + | false => + case String_eq name "block" + | true => + parse-atom-pattern "block" (update-block-acc acc expr) tail + | false => + case String_eq name "_" + | true => + parse-otherwise-pattern acc expr tail + | false => err "_" + ; + + parse-arm : SexpCaseAcc -> Sexp -> List Sexp -> Result SexpCaseAcc String; + parse-arm = lambda acc -> lambda head -> lambda tail -> + case sexp-symbol-name head + | none => err "expected patterns and expressions to be delineated by `=>`" + | some head-name => + case String_eq head-name "_=>_" + | false => + err + (String_concat + "expected patterns and expressions to be delineated by `=>`, but I see `" + (String_concat head-name "`")) + | true => + case tail + | nil => err "todo 13" + | cons pattern tail' => + case tail' + | nil => err "todo 14" + | cons expr tail'' => + case tail'' + | cons _ _ => err "todo 15" + | nil => + Sexp_dispatch + pattern + (parse-pattern acc expr) + (lambda _ -> parse-pattern acc expr pattern nil) + (lambda _ -> err "invalid pattern: string") + (lambda _ -> err "invalid pattern: int") + (lambda _ -> err "invalid pattern: float") + (lambda _ -> err "invalid pattern: block") + ; + + parse-arms : List Sexp -> Result SexpCaseAcc String; + parse-arms = lambda arms -> + let + loop : List Sexp -> SexpCaseAcc -> Result SexpCaseAcc String; + loop = lambda arms -> lambda acc -> + case arms + | nil => ok acc + | cons arm arms => + let + result : Result SexpCaseAcc String; + result = + Sexp_dispatch + arm + (parse-arm acc) + (lambda _ -> err "invalid arm: symbol") + (lambda _ -> err "invalid arm: string") + (lambda _ -> err "invalid arm: int") + (lambda _ -> err "invalid arm: float") + (lambda _ -> err "invalid arm: block") + ; + in + case result + | (err (α := SexpCaseAcc) (β := String)) _ => result + | (ok (α := SexpCaseAcc) (β := String)) acc => loop arms acc + ; + + missing-wildcard : Sexp; + missing-wildcard = Sexp_symbol "missing wildcard pattern"; + in + loop arms (sexp-case-acc none none none none none none missing-wildcard) + ; + + expand-sexp-case : Sexp -> List Sexp -> Sexp; + expand-sexp-case = lambda head -> lambda tail -> + case Sexp_eq head not-bottom + | false => Sexp_symbol "expected arms delineated by `|`" + | true => + case tail + | nil => Sexp_symbol "expected at least one arm" + | cons target arms => + case parse-arms arms + | (err (α := SexpCaseAcc) (β := String)) message => + let message = String_concat "<error: " (String_concat message ">") + in Sexp_symbol message + | (ok (α := SexpCaseAcc) (β := String)) acc => + sexp<-sexp-case-acc target acc + ; + in + case args + | nil => Sexp_symbol "todo" + | cons head tail => + case tail + | nil => + Sexp_dispatch + head + expand-sexp-case + (lambda _ -> Sexp_symbol "invalid case expression: symbol") + (lambda _ -> Sexp_symbol "invalid case expression: string") + (lambda _ -> Sexp_symbol "invalid case expression: int") + (lambda _ -> Sexp_symbol "invalid case expression: float") + (lambda _ -> Sexp_symbol "invalid case expression: block") + | cons _ _ => Sexp_symbol "todo" +; View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ab7984ee22961868b0346b69c1c34e07… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ab7984ee22961868b0346b69c1c34e07… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][warning-40-be-gone] Fix a couple of warning 40.
by Simon Génier 12 Déc '20

12 Déc '20

Simon Génier pushed to branch warning-40-be-gone at Stefan / Typer Commits: 955c3940 by Simon Génier at 2020-12-12T06:59:37-05:00 Fix a couple of warning 40. - - - - - 4 changed files: - src/REPL.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml Changes: ===================================== src/REPL.ml ===================================== @@ -66,7 +66,7 @@ let print_input_line i = let ieval_error = Log.log_error ~section:"IEVAL" let print_and_clear_log () = - if (not Log.typer_log_config.print_at_log) then + if (not Log.typer_log_config.Log.print_at_log) then Log.print_and_clear_log () let handle_stopped_compilation msg = ===================================== src/lexp.ml ===================================== @@ -40,6 +40,8 @@ type meta_id = int (* Identifier of a meta variable. *) type label = symbol +include Pexp.ArgKind + (*************** Elaboration to Lexp *********************) (* The scoping of `Let` is tricky: ===================================== src/opslexp.ml ===================================== @@ -194,7 +194,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + mkCall (DB.eq_refl, + [L.Aerasable, elevel; + L.Aerasable, etype; + L.Aerasable, e]) in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -423,10 +426,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(L.Aerasable, tlvl); (* Typelevel *) + (L.Aerasable, tltp); (* Inductive type *) + (L.Anormal, hlxp); (* Lexp of the branch head *) + (L.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -773,12 +776,12 @@ and check'' erased ctx e = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(L.Aerasable, tlvl); (* Typelevel *) + (L.Aerasable, tltp); (* Inductive type *) + (L.Anormal, hlxp); (* Lexp of the branch head *) + (L.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push Aerasable nerased in + let nerased = dbset_push L.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter ===================================== src/pexp.ml ===================================== @@ -29,7 +29,10 @@ let pexp_error loc = Log.log_error ~section:"PEXP" ~loc (*************** The Pexp Parser *********************) -type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +module ArgKind = struct + type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +end +include ArgKind (* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol View it on GitLab: https://gitlab.com/monnier/typer/-/commit/955c39406a9397a0b11922deedcfe4dac… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/955c39406a9397a0b11922deedcfe4dac… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][ocaml-toplevel] Create a toplevel with Typer's modules
by Jean-Alexandre Barszcz 12 Déc '20

12 Déc '20

Jean-Alexandre Barszcz pushed to branch ocaml-toplevel at Stefan / Typer Commits: f6c2ab2f by Jean-Alexandre Barszcz at 2020-12-12T02:18:53-05:00 Create a toplevel with Typer's modules - - - - - 1 changed file: - GNUmakefile Changes: ===================================== GNUmakefile ===================================== @@ -113,6 +113,22 @@ run/typer-file: run/test-file: @./$(BUILDDIR)/test +# Typer modules in an ocaml toplevel +## Creates the packed module `Typer` to avoid module name clashes +## with ocaml's compiler-libs (`Lexer`, `Env`, etc.) +toplevel: typer + # ============================ + # Build toplevel + # ============================ + @find $(BUILDDIR)/src -name *.ml -not -name REPL.ml -not -name debug.ml\ + | xargs basename -a -s .ml > typer.mlpack + @echo "typer" > typer.mltop + $(OCAMLBUILD) -I src $(OBFLAGS) typer.top + @$(RM) typer.mltop typer.mlpack + +run/toplevel: toplevel + rlwrap $(BUILDDIR)/typer.top -I $(BUILDDIR) + # Compile into bytecode using ocamlc in profiling mode. # Generate a ocamlprof.dump file. profiling-cp: View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f6c2ab2f2f0407ae69ab00f76312bf068… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f6c2ab2f2f0407ae69ab00f76312bf068… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch ocaml-toplevel
by Jean-Alexandre Barszcz 12 Déc '20

12 Déc '20

Jean-Alexandre Barszcz pushed new branch ocaml-toplevel at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/ocaml-toplevel You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][sexp-case] Use sexp-case in a few places.
by Simon Génier 11 Déc '20

11 Déc '20

Simon Génier pushed to branch sexp-case at Stefan / Typer Commits: ab7984ee by Simon Génier at 2020-12-11T22:31:44-05:00 Use sexp-case in a few places. - - - - - 2 changed files: - btl/pervasive.typer - btl/sexp-case.typer Changes: ===================================== btl/pervasive.typer ===================================== @@ -172,26 +172,23 @@ __\.__ = %%%% Sexp-Case macro define-operator "sexp-case" () 43; -sexp-case_ = - let lib = load "btl/sexp-case.typer" - in macro lib.sexp-case-impl; +sexp-case-lib = load "btl/sexp-case.typer"; +sexp-case_ = macro (lambda (sexps : List Sexp) -> IO_return (sexp-case-lib.sexp-case-impl sexps)); %%%% A more flexible `lambda` %% Sexp_to_list : Sexp -> List Sexp -> List Sexp; Sexp_to_list s = lambda exceptions -> - let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! - Sexp_dispatch - s - (node := lambda head -> lambda tail - -> case List_find (Sexp_eq head) exceptions - | some _ => singleton () + sexp-case s + | node head tail + => (case List_find (Sexp_eq head) exceptions + | some _ => cons s nil | none => cons head tail) - (symbol := lambda s - -> case String_eq "" s + | symbol name + => (case String_eq "" name | true => nil - | false => singleton ()) - singleton singleton singleton singleton; + | false => cons s nil) + | _ => cons s nil; multiarg_lambda = %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. @@ -321,52 +318,37 @@ type-impl = lambda (x : List Sexp) -> %% Type name --^ ^------^ constructors %% Return a list contained inside a node sexp. - let knil = K nil; - kerr = K Sexp_error; - - get-list : Sexp -> List Sexp; - get-list node = Sexp_dispatch node - (lambda op lst -> lst) % Nodes - knil % Symbol - knil % String - knil % Integer - knil % Float - knil; % List of Sexp + let get-list : Sexp -> List Sexp; + get-list node = + sexp-case node + | node _ lst => lst + | _ => (nil : List Sexp); %% Get a name (symbol) from a sexp %% - (name t) -> name %% - name -> name get-name : Sexp -> Sexp; get-name sxp = - Sexp_dispatch sxp - (lambda op _ -> get-name op) % Nodes - (lambda _ -> sxp) % Symbol - kerr % String - kerr % Integer - kerr % Float - kerr; % List of Sexp + sexp-case sxp + | node op _ => get-name op + | symbol _ => sxp + | _ => Sexp_error; get-args : Sexp -> List Sexp; get-args sxp = - Sexp_dispatch sxp - (lambda _ args -> args) % Nodes - (lambda _ -> (nil : List Sexp)) % Symbol - (lambda _ -> (nil : List Sexp)) % String - (lambda _ -> (nil : List Sexp)) % Integer - (lambda _ -> (nil : List Sexp)) % Float - (lambda _ -> (nil : List Sexp)); % List of Sexp + sexp-case sxp + | node _ args => args + | _ => (nil : List Sexp); get-type : Sexp -> Sexp; get-type sxp = - Sexp_dispatch sxp - (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error - | false => sxp) - (lambda _ -> sxp) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error); + sexp-case sxp + | node s ss + => (case Sexp_eq s (Sexp_symbol "_:_") + | true => List_nth 1 ss Sexp_error + | false => sxp) + | symbol _ => sxp + | _ => Sexp_error; get-head = List_head Sexp_error; @@ -699,14 +681,9 @@ Test_file = macro (lambda args -> let (cons (Sexp_symbol "unit") nil); %% Expecting a String and nothing else -in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) - (lambda _ _ -> ret) - (lambda _ -> ret) - %% `load` is a special form and takes a Sexp rather than a real `String` - (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) - (lambda _ -> ret) - (lambda _ -> ret) - (lambda _ -> ret)) +in IO_return (sexp-case List_nth 0 args Sexp_error + | string s => quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test) + | _ => ret) ); %%% pervasive.typer ends here. ===================================== btl/sexp-case.typer ===================================== @@ -155,7 +155,7 @@ sexp<-sexp-case-acc = lambda target -> lambda acc -> %% | node (symbol "_=>_") (cons pattern (cons expr nil)) => ?e-double-arrow %% | _ => ?e-else %% -sexp-case-impl : List Sexp -> IO Sexp; +sexp-case-impl : List Sexp -> Sexp; sexp-case-impl = lambda args -> let not-bottom : Sexp; @@ -389,10 +389,10 @@ sexp-case-impl = lambda args -> expand-sexp-case : Sexp -> List Sexp -> Sexp; expand-sexp-case = lambda head -> lambda tail -> case Sexp_eq head not-bottom - | false => Sexp_error + | false => Sexp_symbol "todo" | true => case tail - | nil => Sexp_error + | nil => Sexp_symbol "todo" | cons target arms => case parse-arms arms | (err (α := SexpCaseAcc) (β := String)) message => @@ -402,19 +402,18 @@ sexp-case-impl = lambda args -> sexp<-sexp-case-acc target acc ; in - IO_return - case args - | nil => Sexp_error - | cons head tail => - case tail - | nil => - Sexp_dispatch - head - expand-sexp-case - (lambda _ -> Sexp_symbol "invalid case expression: symbol") - (lambda _ -> Sexp_symbol "invalid case expression: string") - (lambda _ -> Sexp_symbol "invalid case expression: int") - (lambda _ -> Sexp_symbol "invalid case expression: float") - (lambda _ -> Sexp_symbol "invalid case expression: block") - | cons _ _ => Sexp_error + case args + | nil => Sexp_symbol "todo" + | cons head tail => + case tail + | nil => + Sexp_dispatch + head + expand-sexp-case + (lambda _ -> Sexp_symbol "invalid case expression: symbol") + (lambda _ -> Sexp_symbol "invalid case expression: string") + (lambda _ -> Sexp_symbol "invalid case expression: int") + (lambda _ -> Sexp_symbol "invalid case expression: float") + (lambda _ -> Sexp_symbol "invalid case expression: block") + | cons _ _ => Sexp_symbol "todo" ; View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ab7984ee22961868b0346b69c1c34e070… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ab7984ee22961868b0346b69c1c34e070… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch sexp-case
by Simon Génier 11 Déc '20

11 Déc '20

Simon Génier pushed new branch sexp-case at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/sexp-case You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Décembre 2020