Stefan pushed to branch graveline at Stefan / Typer

Commits: 33a23595 by Stefan Monnier at 2018-07-21T21:29:49Z Make isconstructor pure and boolean; and ignore names in lctx

* btl/builtins.typer (Elab_isbound, Elab_isconstructor): Make pure and Bool. * samples/case.typer (is_ctor): Adjust accordingly.

* src/debruijn.ml (lctx_olookup, lctx_olookup_type) (lctx_olookup_value): Delete.

* src/elab.ml (elab_p_id): Not recursive. (check_case): Use Eval.constructor_p.

* src/eval.ml (sexp_dispatch): Remove dead code. (is_bound): Use senv_lookup. (constructor_p): New function, extracted from Elab.check_case. (is_constructor): Use it.

* tests/elabctx_test.ml (v2o_bool): New function. ("Elab_isbound", "Elab_isconstructor"): Adjust to new types of isbound and isconstructor. Add test case for alias to a constructor.

- - - - -

6 changed files:

- btl/builtins.typer - samples/case.typer - src/debruijn.ml - src/elab.ml - src/eval.ml - tests/elabctx_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -257,9 +257,9 @@ gensym = Built-in "gensym" : Unit -> IO Sexp;

Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context;

-Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> IO Int; +Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool;

-Elab_isconstructor = Built-in "Elab.isconstructor" - : String -> Elab_Context -> IO Int; +Elab_isconstructor = Built-in "Elab.isconstructor" + : String -> Elab_Context -> Bool;

%%% builtins.typer ends here.

===================================== samples/case.typer ===================================== @@ -51,7 +51,7 @@ get_exprs : Sexp -> List Sexp; get_exprs sexp = let

err = (lambda _ -> cons Sexp_error nil); - + get_exprs_helper : Sexp -> List Sexp -> List Sexp; get_exprs_helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s) | true => (ss) % tuple @@ -100,10 +100,10 @@ get_cases sexps = let

to_case : Sexp -> Pattern; to_case sexp = Sexp_dispatch sexp - + (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) % expecting a Sexp_node as second argument to _=>_ - | true => (branch + | true => (branch (List_map (lambda ctor -> var_test ctor) (get_exprs (List_nth 0 ss Sexp_error))) (List_nth 1 ss Sexp_error)) | false => (dflt_branch (Sexp_node s ss))) @@ -112,7 +112,7 @@ get_cases sexps = let (lambda s -> dflt_branch (Sexp_string s)) (lambda i -> dflt_branch (Sexp_integer i)) (lambda f -> dflt_branch (Sexp_float f)) - + (lambda ss -> dflt_branch ss);

helper : List Sexp -> List Pattern; @@ -122,15 +122,14 @@ in helper sexps;

%% %% return true if v is a ctor -%% +%% is_ctor : Sexp -> IO Bool; is_ctor v = Sexp_dispatch v - (lambda _ _ -> IO_return true) + (lambda _ _ -> IO_return true) (lambda s -> do { env <- Elab_getenv (); - b <- Elab_isconstructor s env; - IO_return (Int_eq b 1); + IO_return (Elab_isconstructor s env); }) (lambda _ -> IO_return false) (lambda _ -> IO_return false) (lambda _ -> IO_return false) (lambda _ -> IO_return false); @@ -140,18 +139,18 @@ is_ctor v = Sexp_dispatch v %%

rename_nth : Int -> Sexp -> Sexp -> IO Sexp; -rename_nth n ctor sym = let +rename_nth n ctor sym = let

mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int -> IO (List Sexp) -> IO (List Sexp); mapiif f b i xs = let - + helper : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int -> List Sexp -> IO (List Sexp); helper f b i xs = case xs | nil => IO_return nil | cons x xs => (let - + apply : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int -> List Sexp -> IO (List Sexp); apply f b i xs = do @@ -159,7 +158,7 @@ rename_nth n ctor sym = let xs <- (helper f b (i + 1) xs); IO_return (cons (f x i) xs); }; - + continue : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int -> List Sexp -> IO (List Sexp); continue f b i xs = do @@ -167,27 +166,27 @@ rename_nth n ctor sym = let xs <- (helper f b i xs); IO_return (cons x xs); }; - + in do { bv <- b x; (if_then_else_ bv (apply f b i xs) (continue f b i xs)); }); - + in do { xs <- xs; helper f b i xs; }; - + err = (lambda _ -> Sexp_symbol "<not a ctor (0)>"); - + %% %% Check for ctor within englobing ctor and rename variable %% - + sub_ctor : Sexp -> Int -> Sexp; - sub_ctor ctor i = Sexp_dispatch ctor + sub_ctor ctor i = Sexp_dispatch ctor (lambda s ss -> if_then_else_ (Int_eq i n) (sym) (Sexp_symbol "_")) @@ -195,7 +194,7 @@ rename_nth n ctor sym = let (sym) (Sexp_symbol "_")) err err err err ; - + io_err = (lambda _ -> IO_return (Sexp_symbol "<not a ctor (1)>"));

in (Sexp_dispatch ctor @@ -209,12 +208,12 @@ in (Sexp_dispatch ctor

%% %% Expand sub pattern into sub_test -%% and optionaly push_var when there's +%% and optionaly push_var when there's %%

expand_cases : List Pattern -> IO (List Pattern); expand_cases pats = let - + foldi : (Sexp -> Int -> ?a -> ?a) -> Int -> ?a -> List Sexp -> ?a; foldi f i o xs = case xs @@ -225,15 +224,15 @@ expand_cases pats = let get_sub_pattern ctor = let

err = (lambda _ -> Sexp_error); - + no_pattern : List Sexp -> ? -> IO (List Sexp); no_pattern pats = (lambda _ -> IO_return pats); - + helper : List Sexp -> IO (List Sexp); helper vars = List_foldl (lambda pats var -> do { pats <- pats; - Sexp_dispatch var + Sexp_dispatch var (lambda s ss -> IO_return (cons (Sexp_node s ss) pats)) (lambda s -> do { @@ -244,7 +243,7 @@ expand_cases pats = let }) (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) }) (IO_return nil) vars; - + in Sexp_dispatch ctor (lambda s ss -> helper ss) (no_pattern nil) (no_pattern nil) @@ -255,30 +254,30 @@ expand_cases pats = let | push_var n => IO_bind all (lambda all -> IO_return (List_concat all (cons (push_var n) nil))) | _ => (let - + expand : VarTest -> IO (List VarTest); expand test = let - + %% I don't expect to use multiple not_unique_sym at the same time %% so the name may be reused - + not_unique_sym : Sexp; not_unique_sym = Sexp_symbol " %not gensym% "; - + t : Sexp; t = case test | (var_test t) => t | (sub_test _ t) => t | _ => Sexp_error; - + renamed : Int -> IO VarTest; renamed i = case test - | (var_test t) => IO_bind (rename_nth i t not_unique_sym) + | (var_test t) => IO_bind (rename_nth i t not_unique_sym) (lambda t -> IO_return (var_test t)) | (sub_test v t) => IO_bind (rename_nth i t not_unique_sym) (lambda t -> IO_return (sub_test v t)) | _ => IO_return (var_test Sexp_error); - + sub_pattern : IO (List Sexp); sub_pattern = do { @@ -288,11 +287,11 @@ expand_cases pats = let

sub_case : IO (List VarTest); sub_case = let - + helper : Sexp -> VarTest -> List VarTest -> IO (List VarTest); - helper c r o = IO_return (List_concat o + helper c r o = IO_return (List_concat o (cons r (cons (sub_test not_unique_sym c) nil))); - + l : IO (List VarTest); l = do { @@ -305,14 +304,14 @@ expand_cases pats = let helper c r o; }) 0 (IO_return nil) sub_pattern) }; - + in do { l <- l; sub_pattern <- sub_pattern; IO_return (cons (push_var (List_length sub_pattern)) l); }; - + in do { sub_pattern <- sub_pattern; @@ -329,23 +328,23 @@ expand_cases pats = let IO_return (List_concat all sub_case); }) }; - + in expand test);

expand_all : Pattern -> IO Pattern; expand_all p = case p | (dflt_branch _) => IO_return p | (branch cs f) => (let - + ctors : IO (List VarTest); ctors = (List_foldl expand_one (IO_return nil) cs); - + stop_on_id : List VarTest -> IO Pattern; - stop_on_id ctors = if_then_else_ + stop_on_id ctors = if_then_else_ (Int_eq (List_length cs) (List_length ctors)) (IO_return (branch ctors f)) (expand_all (branch ctors f)); - + in do { ctors <- ctors; @@ -369,7 +368,7 @@ pattern_to_sexp vars pats = let (_=>_ _ (uquote fail))))) | none => (quote (##case_ (_|_ (uquote var) (_=>_ (uquote ctor) (uquote succ))))); - + push : Int -> List Sexp -> List Sexp; push n vars = if_then_else_ (Int_<= n 1) (vars) @@ -381,7 +380,7 @@ pattern_to_sexp vars pats = let chain_ctors vars tests succ fail = case vars | (cons v vv) => (case tests | (cons t tt) => (case t - | (var_test t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) + | (var_test t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) (to_case v t (chain_ctors vv tt succ fail) none) (to_case v t (chain_ctors vv tt succ fail) (some fail)) | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) @@ -392,7 +391,7 @@ pattern_to_sexp vars pats = let | nil => (case tests | (cons t tt) => (case t | (var_test _) => Sexp_error - | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) + | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) (to_case v t (chain_ctors vars tt succ fail) none) (to_case v t (chain_ctors vars tt succ fail) (some fail)) | (push_var n) => (chain_ctors (push n vars) tt succ fail)) @@ -402,9 +401,9 @@ pattern_to_sexp vars pats = let chain_ctors_nofail vars tests succ = case vars | (cons v vv) => (case tests | (cons t tt) => (case t - | (var_test t) => + | (var_test t) => (to_case v t (chain_ctors_nofail vv tt succ) none) - | (sub_test v t) => + | (sub_test v t) => (to_case v t (chain_ctors_nofail vars tt succ) none) | (push_var n) => (chain_ctors_nofail (push n vars) tt succ)) | nil => Sexp_error) @@ -425,27 +424,27 @@ pattern_to_sexp vars pats = let last_to_sexp vars pat = case pat | (dflt_branch f) => f | (branch tests f) => (chain_ctors_nofail vars tests f); - + test_fun : List Sexp -> Pattern -> Sexp -> Sexp; test_fun vars pat fail = (quote (lambda (_ : Unit) -> (uquote (one_to_sexp vars pat (quote ((uquote fail) ())))))); - + last_test_fun : List Sexp -> Pattern -> Sexp; last_test_fun vars pat = (quote (lambda (_ : Unit) -> (uquote (last_to_sexp vars pat)))); - + %% Same thing as not_unique_sym, I can reuse the name because %% only the last defined is important - + fail_sym : Sexp; fail_sym = Sexp_symbol " %fail sym% "; - + helper : List Sexp -> List Pattern -> Sexp; helper vars pats = case pats | (cons p pats) => (case pats | (cons _ _) => Sexp_node (Sexp_symbol "let_in_") - (cons (Sexp_node (Sexp_symbol "_;_") - (cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym + (cons (Sexp_node (Sexp_symbol "_;_") + (cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym (cons (helper vars pats) nil))) nil)) (cons (test_fun vars p fail_sym) nil)) | nil => (last_test_fun vars p)) @@ -466,37 +465,37 @@ case_ = macro (lambda args -> let

case0 : List Sexp -> IO Sexp; case0 args = let - + vars : List Sexp; vars = case args | (cons s ss) => get_exprs s | nil => nil; - + pats : List Pattern; pats = case args | (cons s ss) => get_cases ss | nil => nil; - + num_vars : IO (List Sexp); num_vars = get_num_vars vars; - + free_vars : IO (List Sexp); free_vars = get_num_vars vars; - + vars_wrap : List Sexp -> List Sexp -> Sexp -> IO Sexp; vars_wrap fvars nvars fun = let - + rvars : List Sexp; rvars = List_reverse vars nil; - + nfun : Sexp; nfun = fun; - + in IO_return ( (foldi (lambda v i fun -> (quote ( let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun)))) 0 nfun vars)); - + in do { pats <- expand_cases pats;

===================================== src/debruijn.ml ===================================== @@ -342,31 +342,11 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!")

-let lctx_olookup (ctx : lexp_context) (var : string) : (int * env_elem) option = - let rec _lctx_olookup ctx var idx = - try (let elem = M.car ctx in match elem with - | ((_,Some name),_,_) as elem -> (if (name = var) - then (Some (idx,elem)) - else _lctx_olookup (M.cdr ctx) var (idx + 1)) - | _ -> error dloc ("error in lctx_olookup")) - with Not_found -> None - in (_lctx_olookup ctx var 0) - let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in let (_, _, t) = lctx_lookup ctx vref in mkSusp t (S.shift (i + 1))

-let lctx_olookup_type (ctx : lexp_context) (var : string) : lexp option = - let oelem = lctx_olookup ctx var in match oelem with - | Some (i,(_, _, t)) -> Some (mkSusp t (S.shift (i + 1))) - | None -> None - -let lctx_olookup_value (ctx : lexp_context) (var : string) : lexp option = - let oelem = lctx_olookup ctx var in match oelem with - | Some (i,(_, LetDef (o, v), _)) -> Some (push_susp v (S.shift (i + 1))) - | None -> None - let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let (_, i) = vref in match lctx_lookup ctx vref with

===================================== src/elab.ml ===================================== @@ -392,7 +392,7 @@ let generalize (nctx : elab_context) e = wrap (IMap.mem id nes) vname mt'' l e' in loop (IMap.empty) len mfvs

-and elab_p_id ((l,name) : symbol) : vname = +let elab_p_id ((l,name) : symbol) : vname = (l, match name with "_" -> None | _ -> Some name)

(* Infer or check, as the case may be. *) @@ -724,13 +724,9 @@ and check_case rtype (loc, target, ppatterns) ctx = match pat with | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) - -> (try let idx = senv_lookup name ctx in - match OL.lexp_whnf (mkVar (var, idx)) - (ectx_to_lctx ctx) with - | Cons _ (* It's indeed a constructor! *) - -> add_branch (Symbol (l, name)) [] - | _ -> add_default var (* A named default branch. *) - with e -> add_default var) + -> if Eval.constructor_p name ctx then + add_branch (Symbol (l, name)) [] + else add_default var (* A named default branch. *)

| Ppatcons (pctor, pargs) -> add_branch pctor pargs in

===================================== src/eval.ml ===================================== @@ -586,9 +586,6 @@ and sexp_dispatch loc depth args = let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) let rctx = ctx_blk in eval blk (add_rte_variable vdummy (Vsexp b) rctx) - | _ -> - print_string "match error\n"; flush stdout; - error loc "sexp_dispatch error"

(* -------------------------------------------------------------------------- *) and print_eval_result i lxp = @@ -737,17 +734,24 @@ let getenv loc depth args_val = match args_val with let set_getenv (ectx : elab_context) = _last_elab_context := ectx

let is_bound loc depth args_val = match args_val with - | [Vstring name; Velabctx ectx] -> Vcommand (fun () -> - let t = lctx_olookup (ectx_to_lctx ectx) name in match t with - | Some _ -> (Vint 1) - | _ -> (Vint 0) ) + | [Vstring name; Velabctx ectx] + -> o2v_bool (try (ignore (senv_lookup name ectx); true) + with Senv_Lookup_Fail _ -> false) | _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments"

+let constructor_p name ectx = + try let idx = senv_lookup name ectx in + (* Use `lexp_whnf` so that `name` can be indirectly + * defined as a constructor + * (e.g. as in `let foo = cons in case foo x xs | ...` *) + match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with + | Cons _ -> true (* It's indeed a constructor! *) + | _ -> false + with Senv_Lookup_Fail _ -> false + let is_constructor loc depth args_val = match args_val with - | [Vstring name; Velabctx ectx] -> Vcommand (fun () -> - let t = lctx_olookup_value (ectx_to_lctx ectx) name in match t with - | Some (Cons _) -> (Vint 1) - | _ -> (Vint 0) ) + | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) | _ -> error loc "Elab.isconstructor takes an Elab_Context and a String as arguments"

let array_append loc depth args_val = match args_val with

===================================== tests/elabctx_test.ml ===================================== @@ -41,6 +41,11 @@ let _ = (add_test "ELABCTX" "Elab_getenv" (fun () -> | _ -> failure ()) )

+let v2o_bool v = match v with + | Vcons ((_, "false"), []) -> false + | Vcons ((_, "true"), []) -> true + | _ -> raise Not_found + let _ = (add_test "ELABCTX" "Elab_isbound" (fun () -> let dcode = " return = IO_return; @@ -51,45 +56,35 @@ let _ = (add_test "ELABCTX" "Elab_isbound" (fun () -> { env <- (Elab_getenv ());

- b <- (Elab_isbound "Int" env); - - return b; + return (Elab_isbound "Int" env); };

b = do { env <- (Elab_getenv ());

- b <- (Elab_isbound "List" env); - - return b; + return (Elab_isbound "List" env); };

c = do { env <- (Elab_getenv ());

- b <- (Elab_isbound "Elab_isbound" env); - - return b; + return (Elab_isbound "Elab_isbound" env); };

d = do { env <- (Elab_getenv ());

- b <- (Elab_isbound "do" env); - - return b; + return (Elab_isbound "do" env); };

e = do { env <- (Elab_getenv ());

- b <- (Elab_isbound "randomunusednameabc123" env); - - return b; + return (Elab_isbound "randomunusednameabc123" env); };" in

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in @@ -98,13 +93,11 @@ let _ = (add_test "ELABCTX" "Elab_isbound" (fun () ->

let ret = Elab.eval_expr_str ecode ectx rctx in

- match ret with - | [Vcommand a; Vcommand b; Vcommand c; - Vcommand d; Vcommand e] -> - ( match (a (), b (), c (), d (), e ()) with - | (Vint 1, Vint 1, Vint 1, Vint 1, Vint 0) -> success () - | _ -> failure () ) - | _ -> failure ()) + try match List.map (function (Vcommand cmd) -> v2o_bool (cmd ()) + | _ -> raise Not_found) ret with + | [true; true; true; true; false] -> success () + | _ -> failure () + with _ -> failure ()) )

let _ = (add_test "ELABCTX" "Elab_isconstructor" (fun () -> @@ -112,103 +105,90 @@ let _ = (add_test "ELABCTX" "Elab_isconstructor" (fun () -> return = IO_return;

nop = (lambda _ -> return ()); + othercons = cons;

af = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "Int" env); - - return b; + return (Elab_isconstructor "Int" env); };

bf = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "List" env); - - return b; + return (Elab_isconstructor "List" env); };

cf = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "Elab_isbound" env); - - return b; + return (Elab_isconstructor "Elab_isbound" env); };

df = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "do" env); - - return b; + return (Elab_isconstructor "do" env); };

ef = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "randomunusednameabc123" env); - - return b; + return (Elab_isconstructor "randomunusednameabc123" env); };

at = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "cons" env); - - return b; + return (Elab_isconstructor "cons" env); };

bt = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "nil" env); - - return b; + return (Elab_isconstructor "nil" env); };

ct = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "true" env); - - return b; + return (Elab_isconstructor "true" env); };

dt = do { env <- (Elab_getenv ());

- b <- (Elab_isconstructor "false" env); + return (Elab_isconstructor "false" env); + }; + + et = do + { + env <- (Elab_getenv ());

- return b; + return (Elab_isconstructor "othercons" env); };" in

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in

- let ecode = "af; bf; cf; df; ef; at; bt; ct; dt;" in + let ecode = "af; bf; cf; df; ef; at; bt; ct; dt; et;" in

let ret = Elab.eval_expr_str ecode ectx rctx in

- match ret with - | [Vcommand af; Vcommand bf; Vcommand cf; Vcommand df; Vcommand ef; - Vcommand at; Vcommand bt; Vcommand ct; Vcommand dt] -> - ( match (af (), bf (), cf (), df (), ef (), - at (), bt (), ct (), dt ()) with - | (Vint 0, Vint 0, Vint 0, Vint 0, Vint 0, - Vint 1, Vint 1, Vint 1, Vint 1) -> success () - | _ -> failure () ) - | _ -> failure ()) + try match List.map (function (Vcommand cmd) -> v2o_bool (cmd ()) + | _ -> raise Not_found) ret with + | [false; false; false; false; false; + true; true; true; true; true] -> success () + | _ -> failure () + with _ -> failure ()) )

View it on GitLab: https://gitlab.com/monnier/typer/commit/33a235957c9c9a3f09bd54598f54a001d0b9...