Août 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] * btl/types.typer (sexp_dispatch_): Generalize type
by Stefan 28 Aoû '16

28 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: 89b8df07 by Stefan Monnier at 2016-08-28T22:58:52-04:00 * btl/types.typer (sexp_dispatch_): Generalize type - - - - - 2 changed files: - btl/types.typer - samples/quote.typer Changes: ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -96,25 +96,28 @@ tail = lambda a ≡> % Macro % ----------------------------------------------------- -block_ = Built-in "block_" ((List Sexp) -> Sexp); -symbol_ = Built-in "symbol_" (String -> Sexp); -string_ = Built-in "string_" (String -> Sexp); -node_ = Built-in "node_" (Sexp -> (List Sexp) -> Sexp); -integer_ = Built-in "integer_" (Int -> Sexp); -float_ = Built-in "float_" (Float -> Sexp); +block_ = Built-in "block_" (List Sexp -> Sexp); +symbol_ = Built-in "symbol_" (String -> Sexp); +string_ = Built-in "string_" (String -> Sexp); +node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); +integer_ = Built-in "integer_" (Int -> Sexp); +float_ = Built-in "float_" (Float -> Sexp); % Macro : Type; -Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); +Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp)); Macro_ = inductive-cons Macro Macro_ ; -sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp - -> (Sexp -> List Sexp -> Sexp) - -> (String -> Sexp) - -> (String -> Sexp) - -> (Int -> Sexp) - -> (Float -> Sexp) - -> (List Sexp -> Sexp) - -> Sexp); +sexp_dispatch_ = Built-in "sexp_dispatch_" ( + (a : Type) ≡> + Sexp + -> (Sexp -> List Sexp -> a) + -> (String -> a) + -> (String -> a) + -> (Int -> a) + -> (Float -> a) + -> (List Sexp -> a) + -> a + ); % ----------------------------------------------------- % Monads ===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -44,7 +44,7 @@ quote' = lambda (x : List Sexp) -> let target = head Sexp x; tl = tail Sexp x; - rhd = sexp_dispatch_ target + rhd = sexp_dispatch_ (a := Sexp) target node symbol string integer float block; rtl = case tl View it on GitLab: https://gitlab.com/monnier/typer/commit/89b8df076d92eadb9ccf9244db65a3b8ada…

1 0

[Git][monnier/typer][master] * btl/types.typer (length, head, tail): Make type erasable
by Stefan 28 Aoû '16

28 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: f33ba8a5 by Stefan Monnier at 2016-08-28T22:27:46-04:00 * btl/types.typer (length, head, tail): Make type erasable * src/opslexp.ml (erase_type): Adjust indices after removing an erasable formal argument. - - - - - 2 changed files: - btl/types.typer - src/opslexp.ml Changes: ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -71,22 +71,22 @@ List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); nil = inductive-cons List nil; cons = inductive-cons List cons; -length : (a : Type) => List a -> Int; -length = lambda a => +length : (a : Type) ≡> List a -> Int; +length = lambda a ≡> lambda xs -> case xs | nil => 0 | cons hd tl => (1 + (length(a := a) tl)); -head : (a : Type) => List a -> a; -head = lambda a => +head : (a : Type) ≡> List a -> a; +head = lambda a ≡> lambda xs -> case xs | nil => nil | cons hd tl => hd; -tail : (a : Type) => List a -> List a; -tail = lambda a => +tail : (a : Type) ≡> List a -> List a; +tail = lambda a ≡> lambda xs -> case xs | nil => nil ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -327,11 +327,12 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Var(v) -> E.Var(v) | L.Cons(_, s) -> E.Cons(s) - | L.Lambda(kind, vdef, _, body) -> - if kind != P.Aerasable then - E.Lambda(vdef, erase_type body) - else - erase_type body + | L.Lambda (P.Aerasable, _, _, body) -> + (* The var shouldn't appear in body, basically, but we need + * to adjust the debruijn indices of other vars, hence the subst. *) + erase_type (L.push_susp body (S.substitute Builtin.type0)) + | L.Lambda (_, vdef, _, body) -> + E.Lambda (vdef, erase_type body) | L.Let(l, decls, body) -> E.Let(l, (clean_decls decls), (erase_type body)) @@ -349,7 +350,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Arrow _ -> E.Type | L.SortLevel _ -> E.Type | L.Sort _ -> E.Type - (* Still useful to some extend *) + (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Inductive(l, label) and filter_arg_list lst = View it on GitLab: https://gitlab.com/monnier/typer/commit/f33ba8a5bf9221188f9d82534981088be75…

1 0

[Git][monnier/typer][master] * src/lparse.ml (get_int): Remove
by Stefan 28 Aoû '16

28 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: 277049a0 by Stefan Monnier at 2016-08-28T01:06:43-04:00 * src/lparse.ml (get_int): Remove (_lexp_p_infer): Use type_int instead. - - - - - 1 changed file: - src/lparse.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -124,9 +124,6 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx) -(* build type0 from ctx *) -let get_int ctx = build_var "Int" ctx - (* shift all variables by an offset *) let senv_lookup name ctx = senv_lookup name ctx + !_shift_glob @@ -146,7 +143,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* Block/String/Integer/Float *) | Pimm value -> (Imm(value), match value with - | Integer _ -> get_int ctx + | Integer _ -> type_int | Float _ -> type_float | String _ -> type_string; | _ -> lexp_error tloc "Could not find type"; View it on GitLab: https://gitlab.com/monnier/typer/commit/277049a0fad4331ae4b0ca8c16a4d63f447…

1 0

[Git][monnier/typer][master] Try and break some dependencies. Remove unnecessary "Type" builtin
by Stefan 28 Aoû '16

28 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: 4647f3a4 by Stefan Monnier at 2016-08-28T01:04:54-04:00 Try and break some dependencies. Remove unnecessary "Type" builtin * src/opslexp.ml: Rename from typecheck.ml. Add erasure code. * src/lparse.ml (get_type0): Remove. (empty_lctx): Remove. (default_lctx, default_rctx): Merge. Add "Type" and "Type1". * src/lexp.ml (vdef, vref): Move to util.ml. * src/util.ml (vdef, vref): Move from lexp.ml. * src/env.ml: Don't open Myers. Remove false dependency on Debruijn. * src/elexp.ml: Don't depend on Lexp. Move erasure code to opslexp.ml. * src/debruijn.ml (env_extend): Inline the functions it uses. (senv_add_var, env_add_var_info): Remove. * src/builtin.ml (type2): New var. (sexp_eq): Use sexp_equal. * btl/types.typer (Type): Remove. - - - - - 12 changed files: - btl/types.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml → src/opslexp.ml - src/util.ml Changes: ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -35,7 +35,6 @@ % Base Types % ----------------------------------------------------- -Type = Built-in "Type"; Int = Built-in "Int"; Float = Built-in "Float"; String = Built-in "String"; ===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -54,7 +54,7 @@ open Builtin open Env open Debruijn -module TC = Typecheck +module OL = Opslexp module EL = Elexp (* how to handle arrow keys ? *) @@ -124,7 +124,8 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = let ierase_type (lexps: (ldecl list list * lexpr list)) = let (ldecls, lexprs) = lexps in - (EL.clean_toplevel ldecls), (List.map EL.erase_type lexprs) + (List.map OL.clean_decls ldecls), + (List.map OL.erase_type lexprs) let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * lexp_context) = let pdecls, pexprs = pexps in @@ -158,7 +159,7 @@ let _raw_eval f str lctx rctx = let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in let lxps, lctx = lexp_p_decls pxps lctx in - let elxps = EL.clean_toplevel lxps in + let elxps = List.map OL.clean_decls lxps in let rctx = eval_decls_toplevel elxps rctx in (* This is for consistency with ieval *) [], lctx, rctx ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -81,13 +81,11 @@ let set_predef name lexp = (* Builtin types *) let dloc = dummy_location -let slevel0 = SortLevel (SLn 0) -let slevel1 = SortLevel (SLn 1) -let type0 = Sort (dloc, Stype slevel0) -let type1 = Sort (dloc, Stype slevel1) +let type0 = Sort (dloc, Stype (SortLevel (SLn 0))) +let type1 = Sort (dloc, Stype (SortLevel (SLn 1))) +let type2 = Sort (dloc, Stype (SortLevel (SLn 2))) let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel) -let type_level = Builtin ((dloc, "TypeLevel"), type_level) let op_binary t = Arrow (Aexplicit, None, t, dloc, Arrow (Aexplicit, None, t, dloc, t)) @@ -236,15 +234,8 @@ let int_eq loc depth args_val ctx = let sexp_eq loc depth args_val ctx = match args_val with - | [Vsexp(s1); Vsexp(s2)] -> ( - match s1, s2 with - | Symbol(_, s1), Symbol(_, s2) -> btyper (s1 = s2) - | String(_, s1), String(_, s2) -> btyper (s1 = s2) - | Integer(_, s1), Integer(_, s2) -> btyper (s1 = s2) - | Float(_, s1), Float(_, s2) -> btyper (s1 = s2) - | _ -> tfalse) - | _ -> builtin_error loc "int_eq expects 2 sexp" - + | [Vsexp (s1); Vsexp (s2)] -> btyper (sexp_equal s1 s2) + | _ -> builtin_error loc "sexp_eq expects 2 sexp" let open_impl loc depth args_val ctx = ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -100,23 +100,15 @@ let rec senv_lookup (name: string) (ctx: lexp_context): int = else *) raw_idx -(* We first add variable into our map. Later on, we will add them into - * the environment. The reason for this is that the type info is - * known after lexp parsing which need the index fist *) -let senv_add_var (loc, name) ctx = - let ((n, map), e, f) = ctx in - (try let _ = senv_lookup name ctx in - debruijn_warning loc ("Variable Shadowing " ^ name); - with Not_found -> ()); - let nmap = StringMap.add name n map in - ((n + 1, nmap), e, f) - -let env_add_var_info var (ctx: lexp_context) = - let (a, env, f) = ctx in - (a, cons (var) env, f) - let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = - env_add_var_info (1, Some def, v, t) (senv_add_var def ctx) + let (loc, name) = def in + let ((n, map), env, f) = ctx in + (try let _ = senv_lookup name ctx in + debruijn_warning loc ("Variable Shadowing " ^ name); + with Not_found -> ()); + let nmap = StringMap.add name n map in + (* FIXME: Why a db_offset of 1? *) + ((n + 1, nmap), cons (1, Some def, v, t) env, f) let _name_error loc estr str = ===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -46,7 +46,7 @@ open Lexer open Lparse open Eval module EL = Elexp -module TC = Typecheck +module OL = Opslexp (* definitions *) open Grammar @@ -335,7 +335,7 @@ let main () = let cctx = lctx_to_cctx ctx in (* run type check *) List.iter (fun (_, lxp, _) -> - let _ = TC.check cctx lxp in ()) flexps; + let _ = OL.check cctx lxp in ()) flexps; print_string (" " ^ (make_line '-' 76)); print_string "\n";)); @@ -347,7 +347,7 @@ let main () = (if (get_p_option "lctx") then( print_lexp_ctx nctx; print_string "\n")); - let clean_lxp = EL.clean_toplevel lexps in + let clean_lxp = List.map OL.clean_decls lexps in (* Eval declaration *) let rctx = default_rctx in ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -34,11 +34,10 @@ open Sexp (* Sexp type *) open Pexp (* Aexplicit *) -module L = Lexp module U = Util -type vdef = L.vdef -type vref = L.vref +type vdef = U.vdef +type vref = U.vref type label = symbol module SMap = U.SMap @@ -62,75 +61,6 @@ type elexp = (* Inductive takes a slot in the env that is why it need to be here *) | Inductive of U.location * label -let rec erase_type (lxp: L.lexp): elexp = - - match lxp with - | L.Imm(s) -> Imm(s) - | L.Builtin(v, _) -> Builtin(v) - | L.Var(v) -> Var(v) - | L.Cons(_, s) -> Cons(s) - - | L.Lambda(kind, vdef, _, body) -> - if kind != Aerasable then - Lambda(vdef, erase_type body) - else - erase_type body - - | L.Let(l, decls, body) -> - Let(l, (clean_decls decls), (erase_type body)) - - | L.Call(fct, args) -> - Call((erase_type fct), (filter_arg_list args)) - - | L.Case(l, target, _, _, cases, default) -> - Case(l, (erase_type target), (clean_map cases), - (clean_maybe default)) - - | L.Susp(l, s) -> erase_type (L.push_susp l s) - - (* To be thrown out *) - | L.Arrow _ -> Type - | L.SortLevel _ -> Type - | L.Sort _ -> Type - (* Still useful to some extend *) - | L.Inductive(l, label, _, _) -> Inductive(l, label) - -and filter_arg_list lst = - let rec filter_arg_list lst acc = - match lst with - | (kind, lxp)::tl -> - let acc = if kind != Aerasable then - (erase_type lxp)::acc else acc in - filter_arg_list tl acc - | [] -> List.rev acc in - filter_arg_list lst [] - -and clean_decls decls = - List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls - -(* toplevel is a list of value *) -and clean_toplevel decls = - List.map (fun v -> clean_decls v) decls - -and clean_maybe lxp = - match lxp with - | Some lxp -> Some (erase_type lxp) - | None -> None - -and clean_map cases = - let clean_arg_list lst = - let rec clean_arg_list lst acc = - match lst with - | (kind, var)::tl -> - let acc = if kind != Aerasable then - var::acc else acc in - clean_arg_list tl acc - | [] -> List.rev acc in - clean_arg_list lst [] in - - SMap.mapi (fun key (l, args, expr) -> - (l, (clean_arg_list args), (erase_type expr))) cases - let rec elexp_location e = match e with | Imm s -> sexp_location s ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -34,12 +34,9 @@ open Util (* msg_error *) open Fmt (* make_title, table util *) open Sexp -(* open Lexp ( * lexp_print *) open Elexp -open Myers -open Debruijn - +module M = Myers let dloc = dummy_location @@ -56,7 +53,7 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of string * elexp * (((string option * value_type) ref myers) * (int * int)) + | Closure of string * elexp * (((string option * value_type) ref M.myers) * (int * int)) | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy @@ -110,11 +107,11 @@ let value_name v = (* Runtime Environ *) type env_cell = (string option * value_type) ref -type runtime_env = (env_cell myers) * (int * int) +type runtime_env = (env_cell M.myers) * (int * int) -let make_runtime_ctx = (nil, (0, 0)) +let make_runtime_ctx = (M.nil, (0, 0)) -let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in length l +let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in M.length l let is_free_var idx ctx = let (l, (osize, _)) = ctx in @@ -125,7 +122,7 @@ let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): value_type = let (l, _) = ctx in try ( - let ref_cell = (nth idx l) in + let ref_cell = (M.nth idx l) in let (tn, x) = !ref_cell in match (tn, name) with | (Some n1, Some n2) -> ( @@ -154,12 +151,12 @@ let rte_shift vref ctx = let add_rte_variable name (x: value_type) (ctx: runtime_env): runtime_env = let (l, b) = ctx in - let lst = (cons (ref (name, x)) l) in + let lst = (M.cons (ref (name, x)) l) in (lst, b) let set_rte_variable idx name (lxp: value_type) ctx = let (l, _) = ctx in - let ref_cell = (nth idx l) in + let ref_cell = (M.nth idx l) in let (n, _) = !ref_cell in match (n, name) with @@ -177,16 +174,16 @@ let set_rte_variable idx name (lxp: value_type) ctx = (* it allow us to remove temporary variables when we enter a new scope * ) let local_ctx ctx = let (l, (_, _)) = ctx in - let osize = length l in + let osize = M.length l in (l, (osize, 0)) let select_n (ctx: runtime_env) n: runtime_env = let (l, a) = ctx in let r = ref nil in - let s = (length l) - 1 in + let s = (M.length l) - 1 in for i = 0 to n - 1 do - r := (cons (nth (s - i) l) (!r)); + r := (M.cons (M.nth (s - i) l) (!r)); done; ((!r), a) @@ -195,7 +192,7 @@ let select_n (ctx: runtime_env) n: runtime_env = (* and create a clean context free of function arguments *) let temp_ctx (ctx: runtime_env): runtime_env = let (l, (osize, _)) = ctx in - let tsize = length l in + let tsize = M.length l in (* Check if temporary variables are present *) if tsize != osize then( (* remove them @@ -214,7 +211,7 @@ let nfirst_rte_var n ctx = loop 0 [] let print_myers_list l print_fun = - let n = (length l) - 1 in + let n = (M.length l) - 1 in print_string (make_title " ENVIRONMENT "); make_rheader [(None, "INDEX"); @@ -225,7 +222,7 @@ let print_myers_list l print_fun = print_string " | "; ralign_print_int (n - i) 5; print_string " | "; - print_fun (nth (n - i) l); + print_fun (M.nth (n - i) l); done; print_string (make_sep '=') ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -40,9 +40,9 @@ open Lexp (* Varbind *) open Elexp open Builtin open Grammar - open Debruijn open Env +module OL = Opslexp (* eval error are always fatal *) @@ -107,7 +107,7 @@ let rec _eval lxp ctx i: (value_type) = and get_predef_eval name ctx = let r = (get_rte_size ctx) - !builtin_size in let v = mkSusp (get_predef_raw name) (S.shift r) in - _eval (erase_type v) ctx 0 + _eval (OL.erase_type v) ctx 0 and eval_var ctx lxp v = let ((loc, name), idx) = v in @@ -388,7 +388,7 @@ let from_lctx (ctx: lexp_context) rm: runtime_env = let vxp = match exp with | Some lxp -> let octx = add_rte_variable name Vdummy (!rctx) in - let lxp = (erase_type lxp) in + let lxp = (OL.erase_type lxp) in (try (eval lxp octx) with e -> elexp_print lxp; print_string "\n"; raise e) ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -34,17 +34,8 @@ open Grammar (* open Unify *) module S = Subst -(*************** DeBruijn indices for variables *********************) - -(* Occurrence of a variable's symbol: we use DeBruijn index, and for - * debugging purposes, we remember the name that was used in the source - * code. *) -type vdef = U.location * string -type db_index = int (* DeBruijn index. *) -type db_offset = int (* DeBruijn index offset. *) -type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vdef * db_index - +type vdef = U.vdef +type vref = U.vref type label = symbol ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,7 +48,7 @@ open Eval open Grammar open Builtin -module TC = Typecheck +module OL = Opslexp module EL = Elexp module SU = Subst @@ -125,7 +125,6 @@ let build_var name ctx = Var((dloc, name), type0_idx) (* build type0 from ctx *) -let get_type0 ctx = build_var "Type" ctx let get_int ctx = build_var "Int" ctx (* shift all variables by an offset *) @@ -184,11 +183,10 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let lxp = _type_shift lxp sh in let v = Arrow(kind, ovar, ltp, tloc, lxp) in - v, (get_type0 ctx) + v, type0 (* Pinductive *) | Pinductive (label, formal_args, ctors) -> - let type0 = get_type0 ctx in let nctx = ref ctx in (* (arg_kind * pvar * pexp option) list *) let formal = List.map (fun (kind, var, opxp) -> @@ -318,7 +316,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = * Built-in *) | Builtin _ -> e | _ -> - (if TC.conv_p inferred_t t then () else debug_msg ( + (if OL.conv_p inferred_t t then () else debug_msg ( print_string "1 exp "; lexp_print e; print_string "\n"; print_string "2 inf "; lexp_print inferred_t; print_string "\n"; print_string "3 Ann "; lexp_print t; print_string "\n"; @@ -413,7 +411,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs (* Explicit-implicit argument. *) - -> (match TC.lexp_whnf ltp ctx with + -> (match OL.lexp_whnf ltp ctx with | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) when aname = aname' -> let parg = pexp_parse sarg in @@ -424,7 +422,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Explicit arg to non-function") | sarg :: sargs (* Process Argument *) - -> (match TC.lexp_whnf ltp ctx with + -> (match OL.lexp_whnf ltp ctx with | Arrow (Aexplicit, _, arg_type, _, ret_type) -> let parg = pexp_parse sarg in let larg = _lexp_p_check parg arg_type ctx i in @@ -439,7 +437,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let handle_funcall () = - match TC.lexp_whnf body ctx with + match OL.lexp_whnf body ctx with | Builtin((_, "Built-in"), _) -> ( (* ------ SPECIAL ------ *) @@ -476,7 +474,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* user defined macro *) | false ->( (* Get the macro *) - let lxp = match TC.lexp_whnf body ctx with + let lxp = match OL.lexp_whnf body ctx with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | lxp -> print_string "\n"; @@ -488,7 +486,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let arg = olist2tlist_lexp sargs ctx in let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = EL.erase_type lxp in + let elexp = OL.erase_type lxp in let rctx = (from_lctx ctx 0) in _global_eval_trace := []; @@ -644,7 +642,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* build new function *) let arg = olist2tlist_lexp sargs ctx in let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = EL.erase_type lxp in + let elexp = OL.erase_type lxp in let rctx = (from_lctx ctx 0) in (* get a list of declaration *) @@ -931,15 +929,13 @@ let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 * --------------------------------------------------------- *) (* Make lxp context with built-in types *) -let empty_lctx = - let lctx = make_lexp_context in - let lxp = Builtin((dloc, "Built-in"), type0) in - env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 - -let default_lctx = +let default_lctx, default_rctx = (* Empty context *) let lctx = make_lexp_context in + let lctx = env_extend lctx (dloc, "Type1") (LetDef type1) type2 in + let lctx = env_extend lctx (dloc, "Type") (LetDef type0) type1 in + (* FIXME: Add builtins directly here. *) let lxp = Builtin((dloc, "Built-in"), type0) in let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in @@ -962,7 +958,7 @@ let default_lctx = builtin_size := get_size lctx; (* Once default builtin are set we can populate the predef table *) - try + let lctx = try List.iter (fun name -> let idx = senv_lookup name lctx in let v = Var((dloc, name), idx) in @@ -970,30 +966,11 @@ let default_lctx = (* -- DONE -- *) lctx with e -> - lctx - - -(* Make runtime context with built-in types *) -let default_rctx = - (* Empty context *) - let lctx = make_lexp_context in - let lxp = Builtin((dloc, "Built-in"), type0) in - let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in - - (* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "types.typer") in - let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - - _parsing_internals := true; - let d, lctx = lexp_p_decls pxps lctx in - _parsing_internals := false; - + lctx in let rctx = make_runtime_ctx in - let rctx = eval_decls_toplevel (EL.clean_toplevel d) rctx in - _global_eval_trace := []; - rctx + let rctx = eval_decls_toplevel (List.map OL.clean_decls d) rctx in + _global_eval_trace := []; + lctx, rctx (* String Parsing * --------------------------------------------------------- *) @@ -1023,13 +1000,13 @@ let lexp_decl_str str lctx = let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in - let elxps = List.map EL.erase_type lxps in + let elxps = List.map OL.erase_type lxps in (eval_all elxps rctx silent) let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in - let elxps = (EL.clean_toplevel lxps) in + let elxps = (List.map OL.clean_decls lxps) in (eval_decls_toplevel elxps rctx), lctx ===================================== src/typecheck.ml → src/opslexp.ml ===================================== --- a/src/typecheck.ml +++ b/src/opslexp.ml @@ -1,4 +1,4 @@ -(* typecheck.ml --- Check a Lexp expression's type +(* opslexp.ml --- Operations on Lexps Copyright (C) 2011-2016 Free Software Foundation, Inc. @@ -28,10 +28,12 @@ module P = Pexp (* open Myers *) (* open Grammar *) open Lexp +module E = Elexp +module L = Lexp (* open Unify *) module S = Subst -module L = List +(* module L = List *) module B = Builtin module DB = Debruijn @@ -177,7 +179,7 @@ let rec check ctx e = | Susp (e, s) -> check ctx (push_susp e s) | Let (_, defs, e) -> let tmp_ctx = - L.fold_left (fun ctx (v, e, t) + List.fold_left (fun ctx (v, e, t) -> (match check ctx t with | Sort (_, Stype _) -> () | _ -> (U.msg_error "TC" (lexp_location t) @@ -185,12 +187,12 @@ let rec check ctx e = Myers.cons (0, Some v, ForwardRef, t) ctx) ctx defs in let (new_ctx, _) = - L.fold_left (fun (ctx,recursion_offset) (v, e, t) + List.fold_left (fun (ctx,recursion_offset) (v, e, t) -> let t' = check tmp_ctx e in assert_type e t t'; (Myers.cons (recursion_offset, Some v, LetDef e, t) ctx, recursion_offset - 1)) - (ctx, L.length defs) + (ctx, List.length defs) defs in check new_ctx e | Arrow (ak, v, t1, l, t2) @@ -216,7 +218,7 @@ let rec check ctx e = check (Myers.cons (0, Some v, Variable, t) ctx) e)) | Call (f, args) -> let ft = check ctx f in - L.fold_left (fun ft (ak,arg) + List.fold_left (fun ft (ak,arg) -> let at = check ctx arg in match ft with | Arrow (ak', v, t1, l, t2) @@ -299,8 +301,8 @@ let rec check ctx e = :: indtype fargs (start_index - 1) in let rec fieldargs fieldtypes = match fieldtypes with - | [] -> Call (it, indtype fargs (L.length fieldtypes - + L.length fargs - 1)) + | [] -> Call (it, indtype fargs (List.length fieldtypes + + List.length fargs - 1)) | (ak, vd, ftype) :: fieldtypes -> Arrow (ak, vd, ftype, lexp_location ftype, fieldargs fieldtypes) in @@ -315,3 +317,71 @@ let rec check ctx e = "Cons of a non-inductive type!"; B.type_int)) +(*********** Type erasure, before evaluation. *****************) + +let rec erase_type (lxp: L.lexp): E.elexp = + + match lxp with + | L.Imm(s) -> E.Imm(s) + | L.Builtin(v, _) -> E.Builtin(v) + | L.Var(v) -> E.Var(v) + | L.Cons(_, s) -> E.Cons(s) + + | L.Lambda(kind, vdef, _, body) -> + if kind != P.Aerasable then + E.Lambda(vdef, erase_type body) + else + erase_type body + + | L.Let(l, decls, body) -> + E.Let(l, (clean_decls decls), (erase_type body)) + + | L.Call(fct, args) -> + E.Call((erase_type fct), (filter_arg_list args)) + + | L.Case(l, target, _, _, cases, default) -> + E.Case(l, (erase_type target), (clean_map cases), + (clean_maybe default)) + + | L.Susp(l, s) -> erase_type (L.push_susp l s) + + (* To be thrown out *) + | L.Arrow _ -> E.Type + | L.SortLevel _ -> E.Type + | L.Sort _ -> E.Type + (* Still useful to some extend *) + | L.Inductive(l, label, _, _) -> E.Inductive(l, label) + +and filter_arg_list lst = + let rec filter_arg_list lst acc = + match lst with + | (kind, lxp)::tl -> + let acc = if kind != P.Aerasable then + (erase_type lxp)::acc else acc in + filter_arg_list tl acc + | [] -> List.rev acc in + filter_arg_list lst [] + +and clean_decls decls = + List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls + +and clean_maybe lxp = + match lxp with + | Some lxp -> Some (erase_type lxp) + | None -> None + +and clean_map cases = + let clean_arg_list lst = + let rec clean_arg_list lst acc = + match lst with + | (kind, var)::tl -> + let acc = if kind != P.Aerasable then + var::acc else acc in + clean_arg_list tl acc + | [] -> List.rev acc in + clean_arg_list lst [] in + + SMap.mapi (fun key (l, args, expr) -> + (l, (clean_arg_list args), (erase_type expr))) cases + + ===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -23,12 +23,22 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module SMap = Map.Make (struct type t = string let compare = String.compare end) - type charpos = int type bytepos = int type location = { file : string; line : int; column : charpos } let dummy_location = {file=""; line=0; column=0} +(*************** DeBruijn indices for variables *********************) + +(* Occurrence of a variable's symbol: we use DeBruijn index, and for + * debugging purposes, we remember the name that was used in the source + * code. *) +type vdef = location * string +type db_index = int (* DeBruijn index. *) +type db_offset = int (* DeBruijn index offset. *) +type db_revindex = int (* DeBruijn index counting from the root. *) +type vref = vdef * db_index + type bottom = | B_o_t_t_o_m_ of bottom (* print debug info *) View it on GitLab: https://gitlab.com/monnier/typer/commit/4647f3a454f9f422364a308b21f9df9d92e…

1 0

[Git][monnier/typer][master] * src/lparse.ml (lexp_call): Rewrite to work one-arg at a time
by Stefan 27 Aoû '16

27 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: d05adcab by Stefan Monnier at 2016-08-27T10:50:37-04:00 * src/lparse.ml (lexp_call): Rewrite to work one-arg at a time Add basic support for explicit-implicit args. Use lexp_whnf. (lexp_call.get_return_type): Remove. (_lexp_p_infer, lexp_read_pattern, lexp_decls_macro): Adjust to new env_lookup_expr. (_lexp_parse_all.loop): Don't use List.hd when not needed. * src/typecheck.ml (lexp_whnf): New function. * src/debruijn.ml (env_lookup_expr): Return an option. * src/builtin.ml (get_attribute_impl, declexpr_impl): Adjust accordingly. * btl/types.typer (length): One more explicit-implicit arg. - - - - - 7 changed files: - DESIGN - btl/types.typer - src/builtin.ml - src/debruijn.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1655,6 +1655,60 @@ Look ma! No axioms! Or almost: with these classical definitions we cannot prove the classical axiom of choice as a theorem, so if you need it, you have to add it as an axiom. +* Co-induction + +Coinductive data is basically defined by observation, so what is often +written as something like + + codata Stream α + | Nil + | Cons α (Stream α) + +really means something like: + + type StreamAccessor + | Car | Cdr + Stream α = + (a : StreamAccessor) + -> case a + | Car => Maybe α + | Cdr => Maybe (Stream α) + +And with length, that could turn into: + + type StreamAccessor n + | Empty? | Car (n > 0) | Cdr (n > 0) + Stream α n = + (a : StreamAccessor n) + -> case a + | Empty? => Maybe (n > 0) + | Car _ => α + | Cdr _ => Stream α (n - 1) + +In either case, the definition of `Stream` is recursive and doesn't follow +the supported forms of recursion in CIC (i.e. inductive types and inductive +functions) so it requires ad-hoc support. + +It would help to have something akin to the "impredicative encoding" of +inductive types to get an intuitive idea of what should be safe and what +might be dangerous. + +Let's try for `Stream α`: + + Stream α = + (β : Type) -> (a : StreamAccessor) + -> (case a + | Car => Maybe α -> β + | Cdr => Maybe β -> β) + -> β + +So we'd define + + numbers' n β a = case a + | Car => λ f -> f (just n) + | Cdr => λ f -> f (just ¿?¿) %% (numbers' (n + 1)) + numbers = numbers' 0 + * Papers ** BigBang: Designing a statically typed scripting language ** Dependently typed Racket ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -77,7 +77,7 @@ length = lambda a => lambda xs -> case xs | nil => 0 - | cons hd tl => (1 + (length a tl)); + | cons hd tl => (1 + (length(a := a) tl)); head : (a : Type) => List a -> a; head = lambda a => ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -303,7 +303,7 @@ let get_attribute_impl loc largs ctx ftype = | _ -> builtin_error loc "get-attribute expects two arguments" in let lxp = get_property ctx (vi, vn) (ai, an) in - let ltype = env_lookup_expr ctx ((loc, an), ai) in + let Some ltype = env_lookup_expr ctx ((loc, an), ai) in lxp, ltype let new_attribute_impl loc largs ctx ftype = @@ -331,7 +331,7 @@ let declexpr_impl loc largs ctx ftype = | [Var((_, vn), vi)] -> (vi, vn) | _ -> builtin_error loc "declexpr expects one argument" in - let lxp = env_lookup_expr ctx ((loc, vn), vi) in + let Some lxp = env_lookup_expr ctx ((loc, vn), vi) in let ltp = env_lookup_type ctx ((loc, vn), vi) in lxp, ftype ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -34,6 +34,7 @@ open Util open Lexp +module L = Lexp open Myers open Fmt (*open Typecheck env_elem and env_type *) @@ -146,15 +147,13 @@ let env_lookup_type ctx (v : vref): lexp = let (_, _, _, ltp) = _env_lookup ctx v in mkSusp ltp (S.shift (idx + 0)) -let env_lookup_expr ctx (v : vref): lexp = +let env_lookup_expr ctx (v : vref): lexp option = let (_, idx) = v in let (r, _, lxp, _) = _env_lookup ctx v in - - let lxp = match lxp with - | LetDef lxp -> lxp - | _ -> Sort (dummy_location, Stype (SortLevel (SLn 0))) in - - mkSusp lxp (S.shift (idx + 1 - r)) + match lxp with + | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) + (* FIXME: why Sort here? *) + | _ -> None let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx)) ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -351,105 +351,6 @@ let lexp_to_string e = | Builtin _ -> "Builtin" | _ -> "lexp_to_string: not implemented" - - -(* Apply substitution `s' and then reduce to weak head normal form. - * WHNF implies: - * - Not a Let. - * - Not a let-bound variable. - * - Not a Susp. - * - Not an instantiated Metavar. - * - Not a Call (Lambda _). - * - Not a Call (Call _). - * - Not a Call (_, []). - * - Not a Case (Cons _). - * - Not a Call (MetaSet, ..). - *) -(* let rec lexp_whnf (s : lexp VMap.t) e = - * match e with - * | (Imm _ | Builtin _) -> e - * | Sort (_, (StypeLevel | StypeOmega | Stype (SortLevel (SLn _)))) -> e - * | Sort (l, Stype e) -> Sort (l, Stype (mk_susp s e)) - * | SortLevel (SLn _) -> e - * | SortLevel (SLsucc e) -> - * (match lexp_whnf s e with - * | SortLevel (SLn n) -> SortLevel (SLn (n + 1)) - * | e' -> SortLevel (SLsucc e')) - * | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, mk_susp s t1, l, mk_susp s t2) - * | Lambda (ak, v, t, e) -> Lambda (ak, v, mk_susp s t, mk_susp s e) - * | Call (f, args) -> - * List.fold_left (fun e (ak,arg) -> - * match e with - * | Builtin (b,_,_) -> - * (match builtin_reduce b [] arg with - * | Some e -> e - * | _ -> Call (e, [(ak, mk_susp s arg)])) - * | Call (Builtin (b,_,_), args) -> - * (match builtin_reduce b args arg with - * | Some e -> e - * | _ -> Call (e, [(ak, mk_susp s arg)])) - * | Lambda (_, (_,v), _, body) - * -> lexp_whnf (VMap.add v (mk_susp s arg) VMap.empty) body - * | Call (f, args) -> Call (f, (ak, mk_susp s arg) :: args) - * | _ -> Call (e, [(ak, mk_susp s arg)])) - * (lexp_whnf s f) args - * | Inductive (id, t, branches) - * -> Inductive (id, mk_susp s t, SMap.map (mk_susp s) branches) - * | Cons (t, tag) -> Cons (mk_susp s t, tag) - * | Case (l, e, t, branches, default) - * -> let select name actuals - * = try let (l,formals,body) = SMap.find name branches in - * lexp_whnf (List.fold_left2 (fun s (_,a) (_,(_,f)) -> - * VMap.add f a s) - * s actuals formals) - * body - * with Not_found -> - * match default with - * | None -> msg_error l "Unmatched constructor"; - * mk_meta_dummy VMap.empty l - * | Some body -> lexp_whnf s body - * in - * (match lexp_whnf s e with - * | Cons (_, (_,name)) -> select name [] - * | Call (Cons (_, (_, name)), actuals) -> select name actuals - * | e -> Case (l, e, t, - * SMap.map (fun (l,args,body) - * -> (l, args, mk_susp s body)) - * branches, - * match default with Some e -> Some (mk_susp s e) - * | None -> None)) - * | Susp (s', e) -> lexp_whnf (lexp_subst_subst s s') e - * | Metavar (_,MetaFoF,r) -> - * (match !r with | MetaSet e -> lexp_whnf s e | _ -> e) - * | Metavar (l, MetaGraft s', r) -> - * let s' = (lexp_subst_subst s s') in - * (match !r with MetaSet e -> lexp_whnf s' e - * (\* FIXME: filter s' w.r.t `venv'. *\) - * | MetaUnset (venv,_,_) -> Metavar (l, MetaGraft s', r)) - * (\* BEWARE: we need a recursive environment, which is kinda painful - * * to create (tho we could use ref'cells), so we use a hack instead. *\) - * | Let (l,decls,body) - * -> let decls' = List.map (fun (v, e, t) -> (v, mk_susp s e, mk_susp s t)) - * decls in - * let s' = List.fold_left (fun s ((l',v),e,t) -> - * VMap.add v (Let (l, decls', Var (l', v))) s) - * s decls - * in lexp_whnf s' body - * | Var (l,v) - * -> (try match VMap.find v s with - * (\* Hack attack! A recursive binding, let's unroll it here. *\) - * | Let (_,decls,Var (_, v')) when v = v' - * -> let e = List.fold_left (fun e ((_,v'), e', _) -> - * if v = v' then e' else e) - * (\* This metavar is just a placeholder - * * which should be dropped. *\) - * (mk_meta_dummy VMap.empty l) decls - * (\* Here we stay in `s' to keep the recursive bindings. *\) - * in lexp_whnf s (lexp_copy e) - * | e -> lexp_whnf VMap.empty (lexp_copy e) - * with Not_found -> e) *) - - (* (* In non-recursion calls, `s' is always empty. *) let lexp_conv_p env = lexp_conv_p env VMap.empty ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -235,7 +235,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) - let idt = env_lookup_expr ctx (vr, idx) in + let Some idt = env_lookup_expr ctx (vr, idx) in (* make Base type *) let inductive_type = Var((loc, type_name), idx) in @@ -391,8 +391,8 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = Case (loc, tlxp, tltp, return_type, lpattern, dflt), return_type (* Identify Call Type and return processed call *) -and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = - let loc = pexp_location fun_name in +and lexp_call (func: pexp) (sargs: sexp list) ctx i = + let loc = pexp_location func in let from_lctx ctx = try (from_lctx ctx) with e ->( @@ -400,60 +400,70 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = print_eval_trace (); raise e) in - (* consume Arrows and args together *) - let rec get_return_type name i ltp args = - match (nosusp ltp), args with - | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) - | _, _ -> lexp_warning loc - (name ^ " was provided with too many args. Expected: " ^ - (string_of_int i)); ltp in - (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned * Constructor : a constructor is returned * Anonymous : lambda *) (* retrieve function's body *) - let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in + let body, ltp = _lexp_p_infer func ctx (i + 1) in let ltp = nosusp ltp in - let handle_named_call (loc, name) = + let rec handle_fun_args largs sargs ltp = match sargs with + | [] -> largs, ltp + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs + (* Explicit-implicit argument. *) + -> (match TC.lexp_whnf ltp ctx with + | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) + when aname = aname' + -> let parg = pexp_parse sarg in + let larg = _lexp_p_check parg arg_type ctx i in + handle_fun_args ((ak, larg) :: largs) sargs + (L.mkSusp ret_type (S.substitute larg)) + | _ -> lexp_fatal (sexp_location sarg) + "Explicit arg to non-function") + | sarg :: sargs + (* Process Argument *) + -> (match TC.lexp_whnf ltp ctx with + | Arrow (Aexplicit, _, arg_type, _, ret_type) + -> let parg = pexp_parse sarg in + let larg = _lexp_p_check parg arg_type ctx i in + handle_fun_args ((Aexplicit, larg) :: largs) sargs + (L.mkSusp ret_type (S.substitute larg)) + | Arrow _ as t -> lexp_print t; print_string "\n"; + sexp_print sarg; print_string "\n"; + lexp_fatal (sexp_location sarg) + "Expected non-explicit arg" + | _ -> lexp_fatal (sexp_location sarg) + "Explicit arg to non-function") in + + let handle_funcall () = + + match TC.lexp_whnf body ctx with + | Builtin((_, "Built-in"), _) + -> ( + (* ------ SPECIAL ------ *) + match !_parsing_internals, sargs with + | true, [String (_, str)] -> + Builtin((loc, str), ltp), ltp + + | true, [String (_, str); stp] -> + let ptp = pexp_parse stp in + let ltp, _ = _lexp_p_infer ptp ctx (i + 1) in + Builtin((loc, str), ltp), ltp + + | true, _ -> + lexp_error loc "Wrong Usage of \"Built-in\""; + dlxp, dltype + + | false, _ -> + lexp_error loc "Use of \"Built-in\" in user code"; + dlxp, dltype) + + | e -> (* Process Arguments *) - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - - try (* Check if the function was defined *) - let idx = senv_lookup name ctx in - let vf = (make_var name idx loc) in - - match nosusp (env_lookup_expr ctx ((loc, name), idx)) with - | Builtin((_, "Built-in"), _) ->( - (* ------ SPECIAL ------ *) - match !_parsing_internals, largs with - | true, [Imm(String (_, str))] -> - Builtin((loc, str), ltp), ltp - - | true, [Imm(String (_, str)); ltp] -> - Builtin((loc, str), ltp), ltp - - | true, _ -> - lexp_error loc "Wrong Usage of \"Built-in\""; - dlxp, dltype - - | false, _ -> - lexp_error loc "Use of \"Built-in\" in user code"; - dlxp, dltype) - - | e -> - let ret_type = get_return_type name 0 ltp new_args in - Call(vf, new_args), ret_type - - with Not_found -> - lexp_error loc ("The function \"" ^ name ^ "\" was not defined"); - let vf = (make_var name (-1) loc) in - Call(vf, new_args), ltp in + let largs, ret_type = handle_fun_args [] sargs ltp in + Call (body, List.rev largs), ret_type in let handle_macro_call (loc, name) = (* check for builtin *) @@ -465,20 +475,10 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* user defined macro *) | false ->( - (* look up for definition *) - let idx = try senv_lookup name ctx - with Not_found -> - lexp_fatal loc ("Could not find Variable: " ^ name) in - (* Get the macro *) - let lxp = try env_lookup_expr ctx ((loc, name), idx) - with Not_found -> - lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ - " is not a correct index.") in - - let lxp = match nosusp lxp with + let lxp = match TC.lexp_whnf body ctx with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | _ -> + | lxp -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; lexp_print lxp; print_string "\n"; @@ -512,36 +512,12 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = _lexp_p_infer pxp ctx (i + 1)) in (* determine function type *) - match fun_name, ltp with - (* Anonymous *) - | ((Plambda _), _) -> - (* Process Arguments *) - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - Call(body, new_args), ltp - - | (Pvar (l, n), Var((_, "Macro"), _)) -> - (* FIXME: check db_idx points to a Macro type *) - handle_macro_call (l, n) - - (* Call to Vanilla or constructor *) - | (Pvar v, _) -> handle_named_call v - - (* Constructor. This case is rarely used *) - | (Pcons(_, v), _) -> handle_named_call v - - | Pcall(fct, sargs2), ltp -> - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - let body, ltp = lexp_call fct sargs2 ctx (i + 1) in - Call(body, new_args), ltp - - | e, _ -> - pexp_print e; print_string "\n"; - print_string ((pexp_to_string e) ^ "\n"); - lexp_fatal (pexp_location e) "This expression cannot be called" + match func, ltp with + (* FIXME: Rather than check a var name, define a builtin for it. *) + (* FIXME: Don't force func to be a Pvar. *) + | (Pvar (l, n), Var((_, "Macro"), _)) -> handle_macro_call (l, n) + (* FIXME: Handle special-forms here as well! *) + | _ -> handle_funcall () (* Read a pattern and create the equivalent representation *) @@ -555,15 +531,15 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match nosusp (env_lookup_expr ctx ((loc, name), idx)) with - (* We are matching a constructor *) - | Cons _ -> (name, loc, []), ctx + match env_lookup_expr ctx ((loc, name), idx) with + (* We are matching a constructor *) + | Some (Cons _) -> (name, loc, []), ctx - (* name is defined but is not a constructor *) - (* it technically could be ... (expr option) *) - (* What about Var -> Cons ? *) - | _ -> let nctx = env_extend ctx var (LetDef target) dltype in - (name, loc, []), nctx) + (* name is defined but is not a constructor *) + (* it technically could be ... (expr option) *) + (* What about Var -> Cons ? *) + | _ -> let nctx = env_extend ctx var (LetDef target) dltype in + (name, loc, []), nctx) (* would it not make a default match too? *) with Not_found -> @@ -641,9 +617,9 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = " is not a correct index.") in (* get stored function *) - let lxp = match nosusp lxp with - | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | _ -> print_string "\n"; + let lxp = match lxp with + | Some (Call(Var((_, "Macro_"), _), [(_, fct)])) -> fct + | Some lxp -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; lexp_print lxp; print_string "\n"; lexp_fatal loc "Macro is ill formed" in @@ -846,8 +822,8 @@ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> (List.rev acc) - | _ -> let lxp, _ = _lexp_p_infer (List.hd plst) ctx (i + 1) in - (loop (List.tl plst) ctx (lxp::acc)) in + | pe :: plst -> let lxp, _ = _lexp_p_infer pe ctx (i + 1) in + (loop plst ctx (lxp::acc)) in (loop p ctx []) ===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -33,6 +33,7 @@ open Lexp module S = Subst module L = List module B = Builtin +module DB = Debruijn let conv_erase = true (* If true, conv ignores erased terms. *) @@ -99,6 +100,28 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 +(* Reduce to weak head normal form. + * WHNF implies: + * - Not a Let. + * - Not a let-bound variable. + * - Not a Susp. + * - Not an instantiated Metavar. + * - Not a Call (Lambda _). + * - Not a Call (Call _). + * - Not a Call (_, []). + * - Not a Case (Cons _). + * - Not a Call (MetaSet, ..). + *) +let rec lexp_whnf e ctx = match e with + | Var v -> (match DB.env_lookup_expr ctx v with + | None -> e + (* FIXME: We shouldn't do this blindly for recursive definitions! *) + | Some e' -> lexp_whnf e' ctx) + | Susp (e, s) -> lexp_whnf (push_susp e s) ctx + (* FIXME: Obviously incomplete! *) + | e -> e + + (********* Testing if a lexp is properly typed *********) View it on GitLab: https://gitlab.com/monnier/typer/commit/d05adcab62ee2637006f96556c49ce30c94…

1 0

[Git][monnier/typer][master] Fix syntax of explicit-implicit args
by Stefan 27 Aoû '16

27 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: e5fa8b6d by Stefan Monnier at 2016-08-27T10:35:44-04:00 Fix syntax of explicit-implicit args * typer-mode.el (typer-smie-grammar): Fix grammar for `:=`. Add if/then/else to the grammar. Remove `:-` and `:≡`. * tests/sexp_test.ml: Add test for `:=` and if/then/else. * tests/eval_test.ml, tests/macro_test.ml: Use explicit implicit args. * src/grammar.ml (default_grammar): Update from type-mode.el. * doc/manual.texi (Core Syntax): Only keep `:=` for explicit args. * src/builtin.ml (get_attribute_impl, declexpr_impl) (is_builtin_macro): Silence compiler-warning. * btl/types.typer (length): Pass explicitly implicit parameter. - - - - - 9 changed files: - DESIGN - btl/types.typer - doc/manual.texi - src/builtin.ml - src/grammar.ml - tests/eval_test.ml - tests/macro_test.ml - tests/sexp_test.ml - typer-mode.el Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -99,7 +99,6 @@ or "implicit". This has 2 downsides: * Syntax arw ::= '≡>' | '=>' | '->' -assign::= ':≡' | ':=' | ':-' colon ::= ':::' | '::' | ':' exp ::= '(' id ':' exp ')' arw exp | exp arw exp #Function Types | 'let' decls 'in' exp @@ -115,8 +114,8 @@ decl ::= id ':' exp simple_arg ::= id | '('id ':' exp')' formal_arg ::= id | '(' id colon exp ')' ind_arg ::= exp | '(' id colon exp ')' -pat_arg ::= id | '(' id assign pattern ')' -actual_arg ::= exp | '(' id assign exp ')' +pat_arg ::= id | '(' id ':=' pattern ')' +actual_arg ::= exp | '(' id ':=' exp ')' An identifier which starts with a question mark is one meant to be generalized as an implicit/erasable argument. E.g. @@ -1434,7 +1433,13 @@ need to do anyway. Does it come with a cost? That depends on the universe-level of the equality type. -*** E.g. if (=) is in Type 0: +We can encode equality in CoC: + + eq x y = ∀f. f x -> f y + eq_refl : ∀x. eq x x + eq_refl x f P = P + +*** E.g. if (x = y) is in Type 0: type (=) (t:Type l) (a:t) : t -> Type 0 refl: a = a @@ -1461,7 +1466,7 @@ this should not affect typing very much since so the level of T is not affected. -*** E.g. if (=) is in Type l: +*** E.g. if (x = y) is in Type l: type (=) (t:Type l) (a:t) : t -> Type l refl: a = a @@ -1506,6 +1511,21 @@ make sense for "erasable" terms. Also, by marking "large" elements of inductive definitions as erasable, we'd get something similar to preventing strong elimination for them. +E.g. in cast-ultimate.v I had to use axioms like + + EQ_ex : Exists K1 TF1 = Exists K2 TF2 -> (∀F. F K1 TF1 = F K2 TF2) + +whose soundness is actually not known. +With impredicative erasable args we do not need an axiom de define: + + EQ_ex : Exists(K:≡K1) TF1 = Exists(K:≡K2) TF2 + -> (∀F. F(K:≡K1) TF1 = F(K:≡K2) TF2) + +Notice how F only takes an erasable version of K1 and K2, thus +imposing a constraint on the axiom which might indeed be sufficient to make +it sound. Hopefully it's also still sufficient for the cast-ultimate.v proof +to go through! + ** Universe level of equality In current Coq, homogenous equality is: @@ -1553,6 +1573,31 @@ Which I guess is comparable to: type (~=) (t1:Type l) (a1:t1) (t2:Type l) (Q:t1 = t2) : t2 -> Type l refl: a1 ~= (coerce Q a1) +*** "Natural" level via encoding + +Let's check the "natural" level of the "eq" encoding: + + eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) -> + (l':Level) ≡> (T':Type l') ≡> (f:T -> T') -> f x -> f y + eq x y : Typeω + +Ouch! But if we consider that the level of inductive definitions is +normally unaffected by the level at which they're eliminated (contrary to +what happens for the kind of impredicative encoding used here) we could +treat it more like + + eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) -> + (T':Type 0) ≡> (f:T -> T') -> f x -> f y + eq x y : Type l + +Which gives us the dreaded "Type (l+1)" if T is "Type l". +But if x and y are types, we should be able to cut the middle man: + + eq' = λ(l : Level) ≡> λ(x : Type l) (y : Type l) -> + (T':Type 0) ≡> (f : Type l -> T') -> f x -> f y + eq' x y : Type l + +but that doesn't seem to help. ** Inference @@ -1698,23 +1743,11 @@ sacrificing normalization. ** http://albatross-lang.sourceforge.net ** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf ** Read +*** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03] *** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf *** A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi, Andrew Gacek and Gopalan Nadathur *** How OCaml type checker works, http://okmij.org/ftp/ML/generalization.html -* Skip lists - -SkipList a - | Empty - | Cons (val : a) (next : SkipList a) (skip : Nat) (dest : SkipList a) - -At position 2^n, we want skip=2^(n-1) -At position 2^n+2^(n-1) we want two contradictory things: -- skip=2^(n-1) to get to the pivotal 2^n (for when we start before - 2^n+2^(n-1) and need to go past 2^n). -- skip=2^(n-2) to do the binary search between 2^n+2^(n-1) and 2^n (for when - we don't want to go past 2^n, e.g. because we started from before - 2^(n+1)). * Related languages ** Idris ** F-star (https://www.fstar-lang.org) ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -138,6 +138,12 @@ FileHandle = Built-in "FileHandle"; % define operation on file handle run-io = Built-in "run-io" ( + %% FIXME: runIO should have type IO Unit -> b -> b + %% or IO a -> b -> b, which means "run the IO, throw away the result, + %% and then return the second argument unchanged". The "dummy" b argument + %% is actually crucial to make sure the result of runIO is used, otherwise + %% the whole call would look like a dead function call and could be + %% optimized away! (a : Type) ≡> (b : Type) ≡> IO a -> (a -> IO b) -> (IO b) -> Unit); @@ -163,6 +169,7 @@ has-attribute = Built-in "has-attribute" (Macro); % Context Accessors % ----------------------------------------------------- +%% FIXME: These should be functions! decltype = Built-in "decltype" Macro; declexpr = Built-in "declexpr" Macro; ===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -119,7 +119,6 @@ The core syntax of the language is as follows: @example arw ::= '≡>' | '=>' | '->' -assign::= ':≡' | ':=' | ':-' colon ::= ':::' | '::' | ':' exp ::= id | '(' id ':' exp ')' arw exp @@ -137,12 +136,12 @@ decl ::= id ':' exp simple_arg ::= id | '(' id ':' exp ')' formal_arg ::= id | '(' id colon exp ')' ind_arg ::= exp | '(' id colon exp ')' -pat_arg ::= id | '(' id assign id ' )' -actual_arg ::= exp | '(' id assign exp ')' +pat_arg ::= id | '(' id ':=' id ' )' +actual_arg ::= exp | '(' id ':=' exp ')' label ::= id @end example -The three different kinds of arrows, assign symbols and colons are +The three different kinds of arrows and colons are used respectively for @emph{erasable} arguments, @emph{implicit} arguments, and @emph{explicit} arguments. @emph{explicit} arguments are the normal kind of arguments we're all familiar with. ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -347,8 +347,11 @@ let decltype_impl loc largs ctx ftype = ltype, type0 let builtin_macro = [ + (* FIXME: These should be functions! *) ("decltype", decltype_impl); ("declexpr", declexpr_impl); + (* FIXME: These are not macros but `special-forms`. + * We should add here `let_in_`, `case_`, etc... *) ("get-attribute", get_attribute_impl); ("new-attribute", new_attribute_impl); ("has-attribute", has_attribute_impl); @@ -366,7 +369,7 @@ let get_macro_impl loc name = with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found") let is_builtin_macro name = - try SMap.find name macro_impl_map; true + try let _ = SMap.find name macro_impl_map in true with Not_found -> false ===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml @@ -66,37 +66,38 @@ let default_stt : token_env = let default_grammar : grammar = List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) SMap.empty - [("^", Some 165, Some 152); - ("/", Some 140, Some 153); - ("*", Some 141, Some 154); - ("-", Some 109, Some 128); - ("+", Some 110, Some 129); - ("!=", Some 111, Some 89); - (">=", Some 112, Some 90); - ("<=", Some 113, Some 91); - (">", Some 114, Some 92); - ("<", Some 115, Some 93); - ("==", Some 116, Some 94); - ("&&", Some 77, Some 95); + [("^", Some 166, Some 153); + ("/", Some 141, Some 154); + ("*", Some 142, Some 155); + ("-", Some 110, Some 129); + ("+", Some 111, Some 130); + ("!=", Some 112, Some 90); + (">=", Some 113, Some 91); + ("<=", Some 114, Some 92); + (">", Some 115, Some 93); + ("<", Some 116, Some 94); + ("==", Some 117, Some 95); + ("&&", Some 78, Some 96); ("||", Some 53, Some 65); (",", Some 41, Some 41); - (":≡", Some 166, Some 0); - (":-", Some 167, Some 1); - (":=", Some 168, Some 2); - ("::", Some 169, Some 17); - (":::", Some 170, Some 16); - (";", Some 15, Some 15); + ("::", Some 167, Some 17); + (":::", Some 168, Some 16); + ("then", Some 2, Some 1); + (";", Some 14, Some 14); ("type", None, Some 30); ("=", Some 28, Some 29); - ("in", Some 4, Some 66); + (":=", Some 170, Some 15); + ("in", Some 3, Some 67); + ("else", Some 1, Some 66); ("|", Some 54, Some 54); - (")", Some 3, None); - ("->", Some 117, Some 98); - ("=>", Some 117, Some 97); - ("≡>", Some 117, Some 96); - ("let", None, Some 4); - (":", Some 78, Some 78); - ("lambda", None, Some 117); + (")", Some 0, None); + ("->", Some 118, Some 99); + ("=>", Some 118, Some 98); + ("≡>", Some 118, Some 97); + ("let", None, Some 3); + (":", Some 79, Some 79); + ("lambda", None, Some 118); ("case", None, Some 42); - ("(", None, Some 3) + ("if", None, Some 2); + ("(", None, Some 0) ] ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -350,14 +350,14 @@ let _ = (add_test "EVAL" "List" (fun () -> reset_eval_trace (); let dcode = " - my_list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + my_list = (cons(a := Int) 1 (cons(a := Int) 2 (cons(a := Int) 3 (cons(a := Int) 4 (nil(a := Int)))))); " in let rctx, lctx = eval_decl_str dcode lctx rctx in - let rcode = "(length Int my_list); - (head Int my_list); - (head Int (tail Int my_list));" in + let rcode = "(length(a := Int) my_list); + (head(a := Int) my_list); + (head(a := Int) (tail(a := Int) my_list));" in (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -48,8 +48,8 @@ let _ = (add_test "MACROS" "macros base" (fun () -> (* define 'lambda x -> x * x' using macros *) let dcode = " my_fun = lambda (x : List Sexp) -> - let hd = head Sexp x in - (node_ (symbol_ \"_*_\") (cons hd (cons hd nil))); + let hd = head(a := Sexp) x in + (node_ (symbol_ \"_*_\") (cons(a := Sexp) hd (cons(a := Sexp) hd (nil(a := Sexp))))); sqr = Macro_ my_fun; " in @@ -71,10 +71,10 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " decls-impl = lambda (x : List Sexp) -> - cons (node_ (symbol_ \"_=_\") - (cons (symbol_ \"a\") (cons (integer_ 1) nil))) - (cons (node_ (symbol_ \"_=_\") - (cons (symbol_ \"b\") (cons (integer_ 2) nil))) nil); + cons(a := Sexp) (node_ (symbol_ \"_=_\") + (cons(a := Sexp) (symbol_ \"a\") (cons(a := Sexp) (integer_ 1) (nil(a := Sexp))))) + (cons(a := Sexp) (node_ (symbol_ \"_=_\") + (cons(a := Sexp) (symbol_ \"b\") (cons(a := Sexp) (integer_ 2) (nil(a := Sexp))))) (nil(a := Sexp))); my-decls = Macro_ decls-impl; ===================================== tests/sexp_test.ml ===================================== --- a/tests/sexp_test.ml +++ b/tests/sexp_test.ml @@ -36,6 +36,9 @@ let test_sexp_eqv dcode1 dcode2 = let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y" +let _ = test_sexp_eqv "(x := y)" "_:=_ x y" +let _ = test_sexp_eqv "if A then B else C -> D" "if A then B else (C -> D)" +let _ = test_sexp_eqv "A : B -> C" "A : (B -> C)" let _ = test_sexp_eqv "f __; y" "(f ( __; ) y)" let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2" "case_ ( _|_ e ( _=>_ p1 e1) ( _=>_ p2 e2))" ===================================== typer-mode.el ===================================== --- a/typer-mode.el +++ b/typer-mode.el @@ -86,7 +86,7 @@ (smie-merge-prec2s (smie-bnf->prec2 '((id) - (exp ("(" exp ")") + (exp ("(" exp ")") ("(" explicit-arg ")") (exp "->" exp) (exp "=>" exp) (exp "≡>" exp) ("let" decls "in" exp) (exp ":" exp) @@ -96,7 +96,7 @@ ("lambda" simple_arg "≡>" exp) ("case" exp-branches) ;; ("letrec" decl "in" exp) - ;; ("if" exp "then" exp "else" exp) + ("if" exp "then" exp "else" exp) ) (simple_arg (id) ("(" typed_arg ")")) (typed_arg (id ":" exp)) @@ -106,7 +106,8 @@ (decls (decls ";" decls) (decl)) (decl (id ":" exp) (exp "=" exp) ("type" inductive_branches)) (inductive_branches (exp) (inductive_branches "|" inductive_branches)) - (explicit-arg (id ":=" exp) (id ":-" exp) (id ":≡" exp)) + (explicit-arg (id ":=" exp) ;; (id ":-" exp) (id ":≡" exp) + ) (exp-branches (exp "|" branches)) (branches (branches "|" branches) (pattern "=>" exp))) '((assoc ";") @@ -127,6 +128,11 @@ (assoc ":") ;Should this be left or right? (right "->" "=>" "≡>") ) + ;; There's also ambiguity with "else": should "...A else B => C" + ;; mean "(...A else B) => C" or "...A else (B => C)". + ;; I think it should be "...A else (B => C)". + '((nonassoc "else") + (nonassoc ":" "=>" "->" "≡>")) ) ;; Precedence of "=" is tricky as well. Cases to consider: ;; - "x : e1 = e2" View it on GitLab: https://gitlab.com/monnier/typer/commit/e5fa8b6d9a995df0ea54f8df84c71e2f034…

1 0

[Git][monnier/typer][unification] 3 commits: Tweak use of substitutions and unsusp
by Stefan 26 Aoû '16

26 Aoû '16

Stefan pushed to branch unification at Stefan / Typer Commits: c17b5a1f by Stefan Monnier at 2016-08-26T23:47:10-04:00 Tweak use of substitutions and unsusp * src/lexp.ml (subst): Newtype. (mkSusp): Also apply eagerly to Metavar. (push_susp): Rename from unsusp. (nosusp): Rename from ususp_all. (_lexp_to_str): Use push_susp. - - - - - 536bba67 by Stefan Monnier at 2016-08-26T23:51:29-04:00 * src/lexp.ml (push_susp): Don't be so picky. - - - - - a964be1b by Stefan Monnier at 2016-08-26T23:54:31-04:00 Merge branch 'trunk' into unification - - - - - 0 changed files: Changes: View it on GitLab: https://gitlab.com/monnier/typer/compare/85c06461b075f72f81da8013daa30d0fb2…

1 0

[Git][monnier/typer][master] 2 commits: Tweak use of substitutions and unsusp
by Stefan 26 Aoû '16

26 Aoû '16

Stefan pushed to branch master at Stefan / Typer Commits: c17b5a1f by Stefan Monnier at 2016-08-26T23:47:10-04:00 Tweak use of substitutions and unsusp * src/lexp.ml (subst): Newtype. (mkSusp): Also apply eagerly to Metavar. (push_susp): Rename from unsusp. (nosusp): Rename from ususp_all. (_lexp_to_str): Use push_susp. - - - - - 536bba67 by Stefan Monnier at 2016-08-26T23:51:29-04:00 * src/lexp.ml (push_susp): Don't be so picky. - - - - - 5 changed files: - src/elexp.ml - src/lexp.ml - src/lparse.ml - src/subst.ml - src/typecheck.ml Changes: ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -86,7 +86,7 @@ let rec erase_type (lxp: L.lexp): elexp = Case(l, (erase_type target), (clean_map cases), (clean_maybe default)) - | L.Susp(l, s) -> erase_type (L.unsusp l s) + | L.Susp(l, s) -> erase_type (L.push_susp l s) (* To be thrown out *) | L.Arrow _ -> Type ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -53,13 +53,14 @@ type label = symbol (* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) type ltype = lexp + and subst = lexp S.subst and lexp = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort | Builtin of vdef * ltype | Var of vref - | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *) + | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vdef * lexp * ltype) list * lexp | Arrow of arg_kind * vdef option * ltype * U.location * lexp @@ -109,9 +110,12 @@ type varbind = let rec mkSusp e s = if S.identity_p s then e else + (* We apply the substitution eagerly to some terms. + * There's no deep technical rason for that: + * it just seemed like a good idea to do it eagerly when it's easy. *) match e with | Susp (e, s') -> mkSusp e (scompose s' s) - | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) + | Var (l,v) -> slookup s l v | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> Var (l, i)) @@ -271,16 +275,13 @@ let rec lexp_location e = let vdummy = (U.dummy_location, "dummy") let maybev mv = match mv with None -> vdummy | Some v -> v -let rec unsusp e s = (* Push a suspension one level down. *) +let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel _ -> e | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e - | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; - mkSusp e (scompose s' s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) @@ -321,10 +322,19 @@ let rec unsusp e s = (* Push a suspension one level down. *) match default with | None -> default | Some e -> Some (mkSusp e s)) - -let unsusp_all e = + (* Susp should never appear around Var/Susp/Metavar because mkSusp + * pushes the subst into them eagerly. IOW if there's a Susp(Var..) + * or Susp(Metavar..) it's because some chunk of code should use mkSusp + * rather than Susp. *) + | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *) + push_susp e (scompose s' s) + | (Var _) + -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) + push_susp (mkSusp e s) S.identity + +let nosusp e = (* Return `e` without `Susp`. *) match e with - | Susp(e, s) -> unsusp e s + | Susp(e, s) -> push_susp e s | _ -> e let lexp_to_string e = @@ -668,7 +678,7 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_to_str e) - | Susp _ -> _lexp_to_str ctx (unsusp_all exp) + | Susp (e, s) -> _lexp_to_str ctx (push_susp e s) | Var ((loc, name), idx) -> name ^ (index idx) ; ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -241,7 +241,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let inductive_type = Var((loc, type_name), idx) in (* Get constructor args *) - let formal, args = match unsusp_all idt with + let formal, args = match nosusp idt with | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> @@ -297,7 +297,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) - let ltp, lbtp = match unsusp_all t with + let ltp, lbtp = match nosusp t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in @@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* consume Arrows and args together *) let rec get_return_type name i ltp args = - match (unsusp_all ltp), args with + match (nosusp ltp), args with | _, [] -> ltp | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc @@ -416,7 +416,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - let ltp = unsusp_all ltp in + let ltp = nosusp ltp in let handle_named_call (loc, name) = (* Process Arguments *) @@ -428,7 +428,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in - match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with | Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with @@ -476,7 +476,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in - let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; @@ -555,7 +555,7 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) | Cons _ -> (name, loc, []), ctx @@ -641,7 +641,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = " is not a correct index.") in (* get stored function *) - let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -21,6 +21,28 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module U = Util +(* Implementation of the subsitution calculus. + * + * As a general rule, try not to use the constructors of the `subst' + * datatype, but use the following entry points instead. + * Constructor functions: + * - S.identity + * - S.cons + * - S.mkShift + * - S.shift + * - S.compose + * - S.substitute + * - S.sink + * Destructor functions: + * - S.identity_p + * - S.lookup + * + * This implementation is generic (i.e. can be with various datatypes + * implementing the associated lambda-calculus), which is the reason for + * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`. + * So in general, you'll want to use Lexp.scompose and Lexp.slookup + * for those functions. + *) (* Suspensions definitions. * @@ -236,6 +258,7 @@ let shift (m:db_offset) = mkShift Identity m (* The trivial substitution which doesn't do anything. *) let identity = Identity +(* Test if a substitution is trivial. The "_p" stands for "predicate". *) let identity_p s = match s with | Identity -> true | _ -> false (* Compose two substitutions. This implements the merging rules. ===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -110,7 +110,7 @@ let lookup_type ctx vref = let lookup_value ctx vref = let (_, i) = vref in match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o))) + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> None let assert_type e t t' = @@ -151,7 +151,7 @@ let rec check ctx e = | Builtin (_, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v - | Susp (e, s) -> check ctx (unsusp e s) + | Susp (e, s) -> check ctx (push_susp e s) | Let (_, defs, e) -> let tmp_ctx = L.fold_left (fun ctx (v, e, t) View it on GitLab: https://gitlab.com/monnier/typer/compare/e54bbd6d3f50ce539b9669e07cec546057…

1 0

[Git][monnier/typer][unification] 8 commits: fix throw exception for partial application
by BONNEVALLE Vincent 26 Aoû '16

26 Aoû '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 4ef9006d by n3f4s at 2016-08-22T17:07:33+02:00 fix throw exception for partial application - - - - - d00bf033 by n3f4s at 2016-08-22T20:17:04+02:00 remove useless printing - - - - - da4bebac by n3f4s at 2016-08-23T23:15:52+02:00 remove debug printing - - - - - 343fb9c2 by Stefan Monnier at 2016-08-23T20:26:42-04:00 * tests/sexp_test.ml (test_sexp_add): New function. Use it. - - - - - 2331f785 by Stefan Monnier at 2016-08-23T20:28:44-04:00 * tests/sexp_test.ml (test_sexp_eqv): New fun. Add some tests * src/sexp.ml (sexp_equal, sexp_eq_list): New funcs. * src/prelexer.ml (pretokens_equal, pretokens_eq_list): New funs. - - - - - c9bd8ae0 by Stefan Monnier at 2016-08-23T20:30:22-04:00 * src/lexer.ml (nexttoken.lexsym): Fix __<something> handling - - - - - e54bbd6d by Stefan Monnier at 2016-08-23T20:34:24-04:00 * src/grammar.ml (char_kind): New type (token_env): Move here; use it. (default_stt): Adjust accordingly. Add entry for '.' tho not currently obeyed. * src/lexer.ml (token_env): Move to util.ml. (nexttoken, nexttoken.lexsym): Adjust to new token_env type. * src/lparse.ml (_lexp_expr_str): * src/pexp.ml (_pexp_expr_str): Use `token_type'. * src/debruijn.ml (has_property): Remove unused var. - - - - - 85c06461 by n3f4s at 2016-08-25T17:30:34+02:00 Merge branch 'master' into unification - - - - - 9 changed files: - DESIGN - src/debruijn.ml - src/grammar.ml - src/lexer.ml - src/lparse.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - tests/sexp_test.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1,5 +1,12 @@ -*- outline -*- +New: +- extend the stt table to give precedence for "inner op chars" to use within + identifiers (i.e. the "." for module naming). +- "Confusion is power: blurring the line between Bool and Type". + Maybe have "if" use a "Decidable" type class, or maybe automatically + turn "e : t : Bool" into "e : t = true : Type"? + * Categories of arguments We want different categories of arguments. I'm thinking here of the following categories, which are not necessarily mutually-exclusive: @@ -841,16 +848,6 @@ univalence n = ua ¹ n , ua n , ua- n , ua- n , ua- n -* Modules and macros -If we want to be able to call a macro from another module (via -"Module.macro <args>"), then we have to allow macro calls to have a "name" -that's not just a symbol but a module-ref (i.e. a potentially complex -expression), so it's not obvious how to distinguish macro calls from -function calls, short of normalizing Pcall's function argument. - -Solution: macros have a different type, so if M.x has type "macro", we know -we should normalize it to get the actual macro. - * Modules Modules should be able to hold definitions which are universe-polymorphic, @@ -1003,32 +1000,10 @@ Tokens will be made of any sequence of letters other than blanks/comments. special tokens: a(b are 3 tokens if ( is special, but a_(_b is a single (magic) token. -** To affect lexing and parsing, declarations have to take effect before the - whole file is parsed. At first we could say that parsing stops (to allow - evaluation) at every top-level semi-colon, or after every top-level - closer. But what about - - module Toto = { - define _::_ a b = ... - define foo = 1 :: 2 - } - - This seems very reasonable, but requires evaluation in the middle of the - parse of a top-level construct. So we have to handle some top-level - elements (like "module = ...") specially. - - E.g.: - - make it imperative: "module toto;" is a self-contained top-level - expression which affects the interpretation of subsequent expressions - to be considered as within `toto'. - - if we disallow declarations of new special tokens within such a module, - then we could re-parse the remaining expressions after finding the - definition for _::_. - - make it possible for the evaluation of expressions to read the rest - of the input (and hence lex&parse it any way it wants). - - define special "reader macros", so "module". - - define {...} as special so it gets read and passed to `module' - without parsing. +** Structured identifiers +We want to support identifiers with inner structure, such as "foo.bar.baz". + +This could be lexed into a Node identical to that of ( __.__ foo bar baz) ** Provide syntax for backquote&unquote Since "," is to be used as separator, maybe (,e) and (`e) could be used? @@ -1379,6 +1354,7 @@ when they're only used in irrelevant args might relieve the tension. ** Papers *** occurrence checks: [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011] *** pruning: [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA 2011] +*** http://www.cs.cmu.edu/~fp/papers/jicslp96.pdf * Universes ** Universe polymorphism ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -233,8 +233,8 @@ let has_property ctx (var_i, var_n) (att_i, att_n): bool = try let pmap = PropertyMap.find (n - var_i, var_n) property_map in - let prop = PropertyMap.find (n - att_i, att_n) pmap in - true + let _ = PropertyMap.find (n - att_i, att_n) pmap in + true with Not_found -> false ===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml @@ -38,12 +38,20 @@ open Util type grammar = (int option * int option) SMap.t -let default_stt = - let stt = Array.make 256 false - in stt.(Char.code ';') <- true; - stt.(Char.code ',') <- true; - stt.(Char.code '(') <- true; - stt.(Char.code ')') <- true; +(* A token_end array indicates the few chars which are separate tokens, + * even if not surrounded by spaces, such as '(', ')', and ';'. + * It also indicates which chars are "inner" operators, i.e. those chars + * that make up the inner structure of structured identifiers such as + * foo.bar.baz. *) +type char_kind = | CKnormal | CKseparate | CKinner of int +type token_env = char_kind array +let default_stt : token_env = + let stt = Array.make 256 CKnormal + in stt.(Char.code ';') <- CKseparate; + stt.(Char.code ',') <- CKseparate; + stt.(Char.code '(') <- CKseparate; + stt.(Char.code ')') <- CKseparate; + stt.(Char.code '.') <- CKinner 5; stt (* default_grammar is auto-generated from typer-smie-grammar via: ===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -27,17 +27,6 @@ open Grammar (*************** The Lexer phase *********************) -(* FIXME: if we want to handle mixfix declarations such as "let _$_ x y = - toto in a+1 $ b-2" we could make the "_$_" token (i.e. a simple lexical - criteria) trigger the addition of corresponding syntax rules, but - it seems hard to extend it so the precedence can also be specified - because it is awkward to include the info in the lexical part, and as - soon as we move into the syntactical part we get bitten by the fact that - we don't know what the syntax means until we perform macroexpansion - (i.e. much later). *) - -type token_env = bool array - let digit_p char = let code = Char.code char in Char.code '0' <= code && code <= Char.code '9' @@ -84,7 +73,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos (hSymbol ({file;line;column=column+bpos}, string_sub name bpos (String.length name)), pts', 0, 0) - else if stt.(Char.code name.[bpos]) + else if stt.(Char.code name.[bpos]) = CKseparate && not (name.[bpos+1] == '_') then (hSymbol ({file;line;column=column+bpos}, string_sub name bpos (bpos + 1)), @@ -97,14 +86,17 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos pts', 0, 0) else let char = name.[bp] in - if char == '_' then + if char == '_' + && bp + 1 < String.length name + && name.[bp + 1] != '_' then (* Skip next char, in case it's a special token. *) (* For utf-8, this cp+2 is risky but actually works: _ counts - as 1 and if the input is valid utf-8 the next byte has to - be a leading byte, so it has to count as 1 as well ;-) *) + * as 1 and if the input is valid utf-8 the next byte has to + * be a leading byte, so it has to count as 1 as well ;-) *) lexsym (bp+2) (cp+2) - else if stt.(Char.code name.[bp]) && (bp + 1 >= String.length name - || not (name.[bp+1] == '_')) then + else if stt.(Char.code name.[bp]) = CKseparate + && (bp + 1 >= String.length name + || not (name.[bp+1] == '_')) then (hSymbol ({file;line;column=column+bpos}, string_sub name bpos bp), pts, bp, cp) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -448,19 +448,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = * Anonymous : lambda *) let rec infer_implicit_arg ltp largs nargs depth = - (* TODO : check arg number ?*) - (* FIXME error management *) match nosusp ltp with (* Error case *) - | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) -> - Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) Not enough arguments : \n\tltp = " - ^ Fmt_lexp.string_of_lxp ltp - ^ " ,\n\tlargs = [" - ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs) - ^ "],\n\tfun_name = " - ^ Fmt_lexp.string_of_pexp fun_name); - Debug_fun.do_debug (fun () -> prerr_newline (); ()); - assert false + | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) -> [] (* Explicit parameter *) | Arrow (Aexplicit, _, ltp_arg, _, ltp_ret) -> @@ -472,32 +462,20 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (if List.length largs >0 then let head, tail = List.hd largs, List.tl largs in (Aexplicit, head)::(infer_implicit_arg ltp_ret tail (nargs - 1) (depth - 1)) - else assert false) + else []) (* Implicit paramter not given*) | Arrow (kind, _, ltp_arg, _, ltp_ret) -> (kind, mkMetavar ())::(infer_implicit_arg ltp_ret largs nargs (depth - 1)) (* "End" of the arrow "list"*) - | _ -> Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) ltp = " - ^ Fmt_lexp.string_of_lxp ltp - ^ " ,\n\tlargs = [" - ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs) - ^ "],\n\tfun_name = " - ^ Fmt_lexp.string_of_pexp fun_name - ^ "\n"); - (* Cause the throw in builtin*) - (* [] *) - List.map (fun g -> Aexplicit, g) largs - (* cause the too many args *) + | _ -> List.map (fun g -> Aexplicit, g) largs in (* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in let ltp = nosusp ltp in let handle_named_call (loc, name) = - Debug_fun.debug_print_no_buff ("<LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ")\n"); (* Process Arguments *) - Debug_fun.do_debug (fun () -> prerr_newline (); ()); let pargs = List.map pexp_parse sargs in let largs = _lexp_parse_all pargs ctx i in let rec depth_of = function @@ -534,14 +512,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let subst, _ = !global_substitution in let ret_type = get_return_type name 0 ltp new_args subst ctx in let call = Call(vf, new_args) - in - Debug_fun.debug_print_no_buff "<LPARSE.lexp_call>(new_args) "; (* debug printing remove ASAP*) - Debug_fun.do_debug (fun () -> - List.iter (fun (_, l) -> Debug_fun.debug_print_lexp l; prerr_string ", "; ()) new_args; () - ); - Debug_fun.debug_print_lexp call; - Debug_fun.debug_print_no_buff "\n"; - call, ret_type + in call, ret_type with Not_found -> Debug_fun.debug_print_no_buff ("==== <LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ") ====\n"); @@ -1128,7 +1099,7 @@ let default_rctx = * --------------------------------------------------------- *) (* Lexp helper *) -let _lexp_expr_str (str: string) (tenv: bool array) +let _lexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) (ctx: lexp_context) = let pxps = _pexp_expr_str str tenv grm limit in lexp_parse_all pxps ctx ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -389,7 +389,7 @@ let pexp_decls_all (nodes: sexp list): pdecl list = * --------------------------------------------------------- *) (* Lexp helper *) -let _pexp_expr_str (str: string) (tenv: bool array) +let _pexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) = let sxps = _sexp_parse_str str tenv grm limit in pexp_parse_all sxps @@ -419,5 +419,3 @@ let pexp_to_string e = | Pinductive ((_,_), _, _) -> "Pinductive" | Pcons ((_,_),_) -> "Pcons" | Pcase (_, _, _) -> "Pcase" - - ===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -172,3 +172,15 @@ let pretokens_to_str pretokens = let pretokens_print p = print_string (pretokens_to_str p) +(* Prelexer comparison, ignoring source-line-number info, used for tests. *) +let rec pretokens_equal p1 p2 = match p1, p2 with + | Pretoken (_, s1), Pretoken (_, s2) -> s1 = s2 + | Prestring (_, s1), Prestring (_, s2) -> s1 = s2 + | Preblock (_, ps1, _), Preblock (_, ps2, _) -> + pretokens_eq_list ps1 ps2 + | _ -> false +and pretokens_eq_list ps1 ps2 = match ps1, ps2 with + | [], [] -> true + | (p1 :: ps1), (p2 :: ps2) -> + pretokens_equal p1 p2 && pretokens_eq_list ps1 ps2 + | _ -> false ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -231,3 +231,21 @@ let sexp_parse_all_to_list grm tokens limit = | _ -> let (sxp, rest) = sexp_parse_all grm tokens limit in sexp_parse_impl grm rest limit (sxp :: acc) in sexp_parse_impl grm tokens limit [] + +(* Sexp comparison, ignoring source-line-number info, used for tests. *) +let rec sexp_equal s1 s2 = match s1, s2 with + | Epsilon, Epsilon -> true + | Block (_, ps1, _), Block (_, ps2, _) -> pretokens_eq_list ps1 ps2 + | Symbol (_, s1), Symbol (_, s2) -> s1 = s2 + | String (_, s1), String (_, s2) -> s1 = s2 + | Integer (_, n1), Integer (_, n2) -> n1 = n2 + | Float (_, n1), Float (_, n2) -> n1 = n2 + | Node (s1, ss1), Node (s2, ss2) -> + sexp_equal s1 s2 && sexp_eq_list ss1 ss2 + | _ -> false + +and sexp_eq_list ss1 ss2 = match ss1, ss2 with + | [], [] -> true + | (s1 :: ss1), (s2 :: ss2) -> + sexp_equal s1 s2 && sexp_eq_list ss1 ss2 + | _ -> false ===================================== tests/sexp_test.ml ===================================== --- a/tests/sexp_test.ml +++ b/tests/sexp_test.ml @@ -2,38 +2,43 @@ open Sexp open Lexer open Utest_lib -let _ = (add_test "SEXP" "lambda x -> x + x" (fun () -> +let test_sexp_add dcode testfun = + add_test "SEXP" dcode (fun () -> testfun (sexp_parse_str dcode)) - let dcode = "lambda x -> x + x;" in - - let ret = sexp_parse_str dcode in +let _ = test_sexp_add "lambda x -> x + x" (fun ret -> match ret with - | [Node(lbd, [x; add])] -> (match lbd, x, add with - | (Symbol(_, "lambda_->_"), Symbol(_, "x"), - Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])) -> success () - | _ -> failure ()) - | _ -> failure () -)) - -let _ = (add_test "SEXP" "x * x * x" (fun () -> - - let dcode = "x * x * x;" in - - let ret = sexp_parse_str dcode in - match ret with - | [n] ->(match n with - | Node(Symbol(_, "_*_"), - [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")]) - -> success () - - | Node(Symbol(_, "_*_"), - [Symbol(_, "x"); Node(Symbol(_, "_*_"), [Symbol(_, "x")]); Symbol(_, "x")]) - -> success () - - | _ -> failure ()) - | _ -> failure () - -)) + | [Node(Symbol(_, "lambda_->_"), + [Symbol(_, "x"); + Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])])] + -> success () + | _ -> failure () +) + +let _ = test_sexp_add "x * x * x" (fun ret -> + match ret with + | [Node(Symbol(_, "_*_"), + [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); + Symbol(_, "x")])] + -> success () + | _ -> failure () +) + +let test_sexp_eqv dcode1 dcode2 = + add_test "SEXP" dcode1 + (fun () -> + let s1 = sexp_parse_str dcode1 in + let s2 = sexp_parse_str dcode2 in + if sexp_eq_list s1 s2 + then success () + else (sexp_print (List.hd s1); + sexp_print (List.hd s2); + failure ())) + +let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" +let _ = test_sexp_eqv "(x + y)" "_+_ x y" +let _ = test_sexp_eqv "f __; y" "(f ( __; ) y)" +let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2" + "case_ ( _|_ e ( _=>_ p1 e1) ( _=>_ p2 e2))" (* run all tests *) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/compare/80547416749c74d44c42a4b8aadfb51c90…

1 0

[Git][monnier/typer][unification] Deleted 48 commits: add global (susbtitution * constraint) variable
by BONNEVALLE Vincent 25 Aoû '16

25 Aoû '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer WARNING: The push did not contain any new commits, but force pushed to delete the commits and changes below. Deleted commits: d0a20473 by n3f4s at 2016-08-01T21:25:00+02:00 add global (susbtitution * constraint) variable - - - - - 68895a5c by n3f4s at 2016-08-01T21:44:36+02:00 add unification for default case of infer - - - - - 8a15dbf9 by n3f4s at 2016-08-01T21:46:49+02:00 add unification for lambda in check - - - - - d0a41841 by n3f4s at 2016-08-01T21:47:27+02:00 add unification for default case in check - - - - - 910c29ef by n3f4s at 2016-08-05T23:51:10+02:00 change debug print from stdout to stderr - - - - - 501fd9c5 by n3f4s at 2016-08-05T23:51:36+02:00 remove lambda case from infer - - - - - 17e17516 by n3f4s at 2016-08-05T23:53:26+02:00 add None case for Plambda in check & refactoring - - - - - 7051ef29 by n3f4s at 2016-08-05T23:54:21+02:00 add debug and idea of implicit argument in call - - - - - 0e53c1ea by n3f4s at 2016-08-05T23:55:00+02:00 add test for inference - - - - - 872b0143 by n3f4s at 2016-08-08T17:47:11+02:00 better debuging - - - - - 76ecccda by n3f4s at 2016-08-08T18:12:05+02:00 better debug printing and add mkMetavar helper - - - - - 0cb401ef by n3f4s at 2016-08-08T18:13:04+02:00 refactoring of Plambda case in check - - - - - 34c98ba5 by n3f4s at 2016-08-10T17:46:09+02:00 better output - - - - - d997582c by n3f4s at 2016-08-10T18:05:21+02:00 debug check for Plambda - - - - - 98220426 by n3f4s at 2016-08-10T18:07:23+02:00 add a case for metavar in default case in check avoid stack overflow caused by infinite recursion between infer and check - - - - - f57a7c31 by n3f4s at 2016-08-10T18:09:00+02:00 add function that create metavar for implicit arg - - - - - 284f6487 by n3f4s at 2016-08-10T18:09:45+02:00 use infer_implicit_arg to manage non Aexplicit extract the part that check for non Aexplicit arg and create metavar for implicit arg to a function - - - - - 484b86c8 by n3f4s at 2016-08-10T18:13:41+02:00 add test for non Aexplicit arg in function - - - - - 98488b1a by n3f4s at 2016-08-10T18:14:00+02:00 remove type anotation in test - - - - - 06c50bba by n3f4s at 2016-08-10T21:06:03+02:00 add mkMetavar wrapper - - - - - 7d49d849 by n3f4s at 2016-08-10T21:13:30+02:00 replace metavar construction by call to wrapper - - - - - 93ab8238 by n3f4s at 2016-08-10T21:15:00+02:00 replace metavar construction by call to wrapper - - - - - 912c40d4 by n3f4s at 2016-08-10T21:24:32+02:00 extract unification with "new" arrow in a function - - - - - 8b9efc77 by n3f4s at 2016-08-10T21:32:08+02:00 extract Lambda creation into a function - - - - - e4b8d6d2 by n3f4s at 2016-08-10T21:34:29+02:00 better output for error in default case in check - - - - - 257114e0 by n3f4s at 2016-08-10T21:59:07+02:00 default case of check return inferred_t cause eval test to fail with an error : too many argument - - - - - d16f8174 by n3f4s at 2016-08-10T22:03:55+02:00 move lambda case from infer to check makes infinite recursion pass (infinte recursion failed in previous commit) but cause errors in unfication test : change result of lexp_decls_str - - - - - a7e14366 by n3f4s at 2016-08-10T22:22:57+02:00 reduce lambda case in check (do not resolve bugs) - - - - - 8e08924e by n3f4s at 2016-08-10T23:32:06+02:00 better ouput - - - - - c379c3cc by n3f4s at 2016-08-10T23:33:48+02:00 add test for lparse - - - - - 22ffd69b by n3f4s at 2016-08-10T23:34:35+02:00 add implicit arg management - - - - - 8554fb2a by n3f4s at 2016-08-10T23:35:07+02:00 add debug output when var/fun not found - - - - - 1cb81d1c by n3f4s at 2016-08-10T23:52:21+02:00 debug infinite (mutual) recursion for check &infer - - - - - eb7ee412 by n3f4s at 2016-08-11T21:19:35+02:00 add pexp formatting - - - - - 3b603a9a by n3f4s at 2016-08-11T21:24:13+02:00 raise an error for non handled case in infer - - - - - a9d89581 by n3f4s at 2016-08-11T21:26:48+02:00 remove metavar case in default case in check - - - - - a9273fa2 by n3f4s at 2016-08-11T21:45:21+02:00 Merge branch 'tests' into unification - - - - - 6fa48187 by n3f4s at 2016-08-12T23:12:22+02:00 add name in metavar creation - - - - - eabcc167 by n3f4s at 2016-08-17T00:03:00+02:00 modify the test to make them pass - stop lparse test from always failing - change the L-exp in unify_test according to decl_str output - - - - - b520dda8 by n3f4s at 2016-08-17T00:05:28+02:00 change the output of infer_implicit_arg fix throw in conversion from typer list to ocaml list but cause error regarding number of argument - - - - - 77fef2c1 by n3f4s at 2016-08-17T00:07:32+02:00 add basic printing for metavar in _lexp_to_str - - - - - 49d6e22d by n3f4s at 2016-08-17T00:20:18+02:00 add call to lambda with implicit arg, lparse test - - - - - 5b0b03fe by n3f4s at 2016-08-17T21:45:55+02:00 remove unused code - - - - - f2751880 by n3f4s at 2016-08-17T21:46:48+02:00 remove commented code - - - - - 3172b157 by n3f4s at 2016-08-17T22:32:42+02:00 add Pmetavar case in lexp_p_infer - - - - - d4c27327 by n3f4s at 2016-08-18T18:53:22+02:00 improve implicit/explicit argument handling - - - - - 133f6fc1 by n3f4s at 2016-08-18T18:54:09+02:00 try to resolve not enough arg with metavar - - - - - 80547416 by n3f4s at 2016-08-19T06:11:22+02:00 add arg_kind in lexp printing - - - - - 8 changed files: - src/builtin.ml - src/debug_fun.ml - src/fmt_lexp.ml - src/lexp.ml - src/lparse.ml - tests/lparse_test.ml - tests/unify_test.ml - tests/utest_lib.ml Changes: ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -171,7 +171,7 @@ let rec tlist2olist acc expr = | Vcons((_, "nil"), []) -> List.rev acc | _ -> print_string (value_name expr); print_string "\n"; - value_print expr; + value_print expr; print_newline (); builtin_error dloc "List conversion failure'" ===================================== src/debug_fun.ml ===================================== --- a/src/debug_fun.ml +++ b/src/debug_fun.ml @@ -1,8 +1,8 @@ open Fmt_lexp -(* let _debug = true *) -let _debug = false +let _debug = true +(* let _debug = false *) let logs = ref [] @@ -17,18 +17,21 @@ let clear_indent () = in do_debug (fun () -> List.iter (fun (s1, s2) -> - print_string s1; - print_string (String.make (!indent * 2) '-'); - print_string s2; + prerr_string s1; + prerr_string (String.make (!indent * 2) '-'); + prerr_string s2; indent := !indent + 1; ) (!logs); logs := []; - print_newline (); + prerr_newline (); ()) +let debug_print_no_buff str = + do_debug (fun () -> prerr_string str; ()) + let debug_print_lexp lxp = let str = colored_string_of_lxp lxp str_yellow str_magenta - in do_debug (fun () -> print_string str; ()) + in do_debug (fun () -> prerr_string str; ()) let debug_print_unify fn lhs rhs str = let debug_print_unify fn lhs rhs str = ===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -1,5 +1,6 @@ open Sexp +open Pexp open Lexp open Fmt @@ -43,7 +44,7 @@ and string_of_lxp lxp = | Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")" | Let (_) -> "Let(..)" | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" - | Arrow (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (string_of_lxp b) ^ ")" + | Arrow (kind, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (string_of_lxp b) ^ ")" | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ ": " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ "))" | Metavar (value, _, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")" | Call (_) -> "Call(...)" @@ -54,6 +55,11 @@ and string_of_lxp lxp = | Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")" | _ -> "Unidentified Lexp" +and string_of_kind = function + | Aexplicit -> "Aexplicit" + | Aimplicit -> "Aimplicit" + | Aerasable -> "Aerasable" + and string_of_sort_level lvl = match lvl with | SLn i -> "SLn(" ^ string_of_int i ^ ")" @@ -65,7 +71,7 @@ and string_of_sort sort = | StypeOmega -> "StypeOmega" | StypeLevel -> "StypeLevel" -let colored_string_of_lxp lxp lcol vcol = +let rec colored_string_of_lxp lxp lcol vcol = match lxp with | Imm (Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")" | Imm (String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")" @@ -81,9 +87,9 @@ let colored_string_of_lxp lxp lcol vcol = | Call (_) -> (lcol "Call(...)" ) | Case _ -> (lcol "Case") ^ "(...)" | Inductive _ -> (lcol "Inductive") ^ "(...)" - | Sort _ -> (lcol "Sort") ^ "(...)" - | SortLevel _ -> (lcol "SortLevel") ^ "(...)" - | Susp _ -> (lcol "Susp") ^ "(...)" + | Sort (_, s) -> (lcol "Sort") ^ "(" ^ vcol (string_of_sort s)^ ")" + | SortLevel l -> (lcol "SortLevel") ^ "(" ^ vcol (string_of_sort_level l) ^ ")" + | Susp (v, s) -> (lcol "Susp") ^ "(" ^ colored_string_of_lxp v lcol vcol ^ ", " ^ vcol (string_of_subst s) ^")" | _ -> (lcol "Unidentified Lexp") let padding_right (str: string ) (dim: int ) (char_: char) : string = @@ -102,3 +108,20 @@ let center (str: string ) (dim: int ) (char_: char) : string = in (String.make lpad char_) ^ str ^ (String.make lpad char_) +let rec string_of_pexp pxp = + match pxp with + (* | Psort of location * sort *) + | Pimm (Integer (_, i)) -> "Pimm( Integer (" ^ string_of_int i ^ "))" + | Pimm (Float (_, f)) -> "Pimm( Float (" ^ string_of_float f ^ "))" + | Pimm (String (_, s)) -> "Pimm (String (" ^ s ^ "))" + | Pvar (_, s) -> "Pvar (" ^ s ^ ")" + | Phastype (_, p1, p2) -> "Phastype (" ^ string_of_pexp p1 ^ ", " ^ string_of_pexp p2 ^ ")" + | Pmetavar (_, s) -> "Pmetavar (" ^ s ^ ")" + | Plet (_, _, p) -> "Plet (_, " ^ string_of_pexp p ^ ")" + | Parrow (_, _, _, _, _) -> "Parrow (...)" + | Plambda _ -> "Plambda (...)" + | Pcall _ -> "Pcall (...)" + | Pinductive _ -> "Pinductive (...)" + | Pcons ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ s2 ^ ")" + | Pcase _ -> "Pcase (...)" + | _ -> "Pexp not handled" ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -684,6 +684,8 @@ and _lexp_to_str ctx exp = | Var ((loc, name), idx) -> name ^ (index idx) ; + | Metavar (idx, subst, (loc, name)) -> "?" ^ name ^ (index idx) (*TODO : print subst*) + | Let (_, decls, body) -> (* Print first decls without indent *) let h1, decls, idt_lvl = @@ -797,7 +799,7 @@ and _lexp_to_str ctx exp = | SortLevel (SLn v) -> "Type" ^ (string_of_int v) | _ -> "Type") - | _ -> print_string "Printing Not Implemented"; "-- --" + | _ -> print_string "Printing Not Implemented\n"; "-- --" and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -130,6 +130,13 @@ let build_var name ctx = let get_type0 ctx = build_var "Type" ctx let get_int ctx = build_var "Int" ctx +(* :-( *) +let global_substitution = ref (Unif.empty_subst, []) + +let mkMetavar () = let meta = Unif.create_metavar () + in let name = "__Metavar_" ^ (string_of_int meta) + in Metavar (meta, S.Identity, (Util.dummy_location, name)) + (* shift all variables by an offset *) let senv_lookup name ctx = senv_lookup name ctx + !_shift_glob @@ -210,22 +217,6 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let v = Inductive(tloc, label, formal, map_ctor) in v, ltp - (* This case can be inferred *) - | Plambda (kind, var, optype, body) -> - let ltp, _ = match optype with - | Some ptype -> lexp_infer ptype ctx - (* This case must have been lexp_p_check *) - | None -> lexp_error tloc "Lambda require type annotation"; - dltype, dltype in - - let nctx = env_extend ctx var Variable ltp in - let lbody, lbtp = lexp_infer body nctx in - (* We added one variable in the ctx * ) - let lbtp = _type_shift lbtp 1 in *) - - let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in - Lambda(kind, var, ltp, lbody), lambda_type - | Pcall (fname, _args) -> lexp_call fname _args ctx i @@ -250,8 +241,8 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = lexp_error loc ("Constructor \"" ^ cname ^ "\" does not exist"); [], []) - - | _ -> lexp_error loc "Not an Inductive Type"; [], [] in + | _ -> lexp_error loc "Not an Inductive Type"; [], [] + in (* build Arrow type *) let cons_type = List.fold_left (fun ltp (kind, v, tp) -> @@ -272,14 +263,17 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Pcase (loc, target, patterns) -> lexp_case None (loc, target, patterns) ctx i + | Pmetavar _ -> (let meta = mkMetavar () (*TODO *) + in lexp_warning dloc "<LEXP_P_INFER>(Pmetavar case) Check output : may be wrong lexp/type returned"; + (meta, meta) (* FIXME pretty sure that's not should be returned*)) + | Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx (i + 1)), ltp - (*FIXME right thing to do*) - | _ -> let meta = Unif.mkMetavar S.Identity (Util.dummy_location, "") (*???*) - in (meta, lexp_p_check p meta ctx) - + | Plambda _ -> (let meta = mkMetavar () + in let lxp = lexp_p_check p meta ctx + in (lxp, meta)) and lexp_let_decls decls (body: lexp) ctx i = (* build the weird looking let *) @@ -290,48 +284,71 @@ and lexp_let_decls decls (body: lexp) ctx i = and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = _lexp_p_check p t ctx 1 -(*TODO : - add substitution parameter for unification - - try to unify in default case *) and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = - let tloc = pexp_location p in + let tloc = pexp_location p + in _global_lexp_ctx := ctx; _global_lexp_trace := (i, tloc, p)::!_global_lexp_trace; + let unify_with_arrow lxp kind subst = + let arg, body = mkMetavar (), mkMetavar () + in let arrow = Arrow (kind, None, arg, Util.dummy_location, body) + in match Unif.unify arrow lxp subst with + | Some(subst) -> global_substitution := subst; arg, body + | None -> lexp_error tloc ("Type " ^ Fmt_lexp.string_of_lxp lxp + ^ " and " + ^ Fmt_lexp.string_of_lxp arrow + ^ " does not match"); dltype, dltype + + in + let infer_lambda_body kind var body subst = + (* Read var type from the provided type *) + let ltp, lbtp = match nosusp t with + | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp + | lxp -> (unify_with_arrow lxp kind subst) + in + let nctx = env_extend ctx var Variable ltp in + let lbody = _lexp_p_check body lbtp nctx (i + 1) in Lambda(kind, var, ltp, lbody) + + in + let subst, _ = !global_substitution + in + let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) + in match p with (* This case cannot be inferred *) - | Plambda (kind, var, None, body) ->( - (* Read var type from the provided type *) - let ltp, lbtp = match nosusp t with - | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp - | _ -> lexp_error tloc "Type does not match"; dltype, dltype in + | Plambda (kind, var, None, body) ->(infer_lambda_body kind var body subst) - let nctx = env_extend ctx var Variable ltp in - let lbody = _lexp_p_check body lbtp nctx (i + 1) in + (* This case can be inferred *) + | Plambda (kind, var, Some (ptype), body) -> + let ltp, _ = lexp_infer ptype ctx + in let nctx = env_extend ctx var Variable ltp + in let lbody, lbtp = lexp_infer body nctx + in Lambda(kind, var, ltp, lbody) - Lambda(kind, var, ltp, lbody)) (* This is mostly for the case where no branches are provided *) | Pcase (loc, target, patterns) -> let lxp, _ = lexp_case (Some t) (loc, target, patterns) ctx i in lxp - | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in + | _ -> (let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in (* e *) match e with (* Built-in is a dummy function with no type. We cannot check * Built-in *) | Builtin _ -> e | _ -> - (* (if TC.conv_p inferred_t t then () else debug_msg ( *) - (match Unif.unify inferred_t t Unif.empty_subst with - | Some _ -> () + (match Unif.unify inferred_t t Unif.empty_subst with (* cause eval test to fail : too many arguments *) + | Some subst -> global_substitution := subst; inferred_t | None -> debug_msg ( - print_string "1 exp "; lexp_print e; print_string "\n"; - print_string "2 inf "; lexp_print inferred_t; print_string "\n"; - print_string "3 Ann "; lexp_print t; print_string "\n"; - lexp_warning tloc "Type Mismatch inferred != Annotation")); - e + let print_lxp str = + print_string (Fmt_lexp.colored_string_of_lxp str Fmt_lexp.str_yellow Fmt_lexp.str_magenta) in + print_string "1 exp "; (print_lxp e); print_string "\n"; + print_string "2 inf "; (print_lxp inferred_t); print_string "\n"; + print_string "3 Ann susp("; (print_lxp (nosusp t)); print_string ")\n"; + lexp_warning tloc "Type Mismatch inferred != Annotation"); e )) (* Lexp.case cam be checked and inferred *) and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = @@ -409,28 +426,87 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = raise e) in (* consume Arrows and args together *) - let rec get_return_type name i ltp args = + let rec get_return_type name i ltp args subst ctx = match (nosusp ltp), args with | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) + | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl subst ctx) + (* Do a lookup to check where the var "point" to*) + (* | Var(vt), hd::args -> (let ltp = Debruijn.env_lookup_expr ctx vt in get_return_type name (i) ltp args subst ctx) *) + | Metavar _, (kind, arg)::tl -> let arr = Arrow (kind, None, mkMetavar (), Util.dummy_location, ltp) + (* in ltp *) + in (match Unif.unify ltp arr subst with + | None -> ltp (*?????*) + | Some (subst, c) -> global_substitution := (subst, c); get_return_type name (i + 1) arr tl subst ctx) | _, _ -> lexp_warning loc (name ^ " was provided with too many args. Expected: " ^ - (string_of_int i)); ltp in + (string_of_int i) ^ " got : " ^ (string_of_int (List.length args)) + ^ " for lexp : " ^ Fmt_lexp.string_of_lxp (nosusp ltp)); ltp in (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned * Constructor : a constructor is returned * Anonymous : lambda *) + let rec infer_implicit_arg ltp largs nargs depth = + (* TODO : check arg number ?*) + (* FIXME error management *) + match nosusp ltp with + (* Error case *) + | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) -> + Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) Not enough arguments : \n\tltp = " + ^ Fmt_lexp.string_of_lxp ltp + ^ " ,\n\tlargs = [" + ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs) + ^ "],\n\tfun_name = " + ^ Fmt_lexp.string_of_pexp fun_name); + Debug_fun.do_debug (fun () -> prerr_newline (); ()); + assert false + + (* Explicit parameter *) + | Arrow (Aexplicit, _, ltp_arg, _, ltp_ret) -> + (let head, tail = List.hd largs, List.tl largs + in (Aexplicit, head)::(infer_implicit_arg ltp_ret tail (nargs - 1) (depth - 1))) + + (* Implicit parameter explictly given*) + | Arrow (kind, _, ltp_arg, _, ltp_ret) when nargs = depth -> + (if List.length largs >0 + then let head, tail = List.hd largs, List.tl largs + in (Aexplicit, head)::(infer_implicit_arg ltp_ret tail (nargs - 1) (depth - 1)) + else assert false) + + (* Implicit paramter not given*) + | Arrow (kind, _, ltp_arg, _, ltp_ret) -> (kind, mkMetavar ())::(infer_implicit_arg ltp_ret largs nargs (depth - 1)) + + (* "End" of the arrow "list"*) + | _ -> Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) ltp = " + ^ Fmt_lexp.string_of_lxp ltp + ^ " ,\n\tlargs = [" + ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs) + ^ "],\n\tfun_name = " + ^ Fmt_lexp.string_of_pexp fun_name + ^ "\n"); + (* Cause the throw in builtin*) + (* [] *) + List.map (fun g -> Aexplicit, g) largs + (* cause the too many args *) + in (* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in let ltp = nosusp ltp in let handle_named_call (loc, name) = + Debug_fun.debug_print_no_buff ("<LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ")\n"); (* Process Arguments *) + Debug_fun.do_debug (fun () -> prerr_newline (); ()); let pargs = List.map pexp_parse sargs in let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in + let rec depth_of = function + Arrow (_, _, _, _, ltp) -> 1 + (depth_of ltp) + | _ -> 0 + in + let new_args = infer_implicit_arg ltp largs ((List.length largs) - 1) (depth_of ltp) + (* let new_args = List.map (fun g -> (Aexplicit, g)) largs *) + in try (* Check if the function was defined *) let idx = senv_lookup name ctx in @@ -455,10 +531,31 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = dlxp, dltype) | e -> - let ret_type = get_return_type name 0 ltp new_args in - Call(vf, new_args), ret_type + let subst, _ = !global_substitution in + let ret_type = get_return_type name 0 ltp new_args subst ctx in + let call = Call(vf, new_args) + in + Debug_fun.debug_print_no_buff "<LPARSE.lexp_call>(new_args) "; (* debug printing remove ASAP*) + Debug_fun.do_debug (fun () -> + List.iter (fun (_, l) -> Debug_fun.debug_print_lexp l; prerr_string ", "; ()) new_args; () + ); + Debug_fun.debug_print_lexp call; + Debug_fun.debug_print_no_buff "\n"; + call, ret_type with Not_found -> + Debug_fun.debug_print_no_buff ("==== <LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ") ====\n"); + Debug_fun.do_debug (fun () -> (* Some debug printing, remove ASAP*) + prerr_string "==== <LPARSE.lexp_call>(largs) "; + List.iter (fun l -> Debug_fun.debug_print_lexp l; prerr_string ", ") largs; + prerr_string " ===="; + prerr_newline (); ()); + Debug_fun.debug_print_no_buff "==== <LPARSE.lexp_call>(body) "; + Debug_fun.debug_print_lexp body; + Debug_fun.do_debug (fun () -> prerr_string " =="; prerr_newline ();() ); + Debug_fun.debug_print_no_buff "==== <LPARSE.lexp_call>(ltp) "; + Debug_fun.debug_print_lexp ltp; + Debug_fun.do_debug (fun () -> prerr_string " ===="; prerr_newline ();() ); lexp_error loc ("The function \"" ^ name ^ "\" was not defined"); let vf = (make_var name (-1) loc) in Call(vf, new_args), ltp in ===================================== tests/lparse_test.ml ===================================== --- a/tests/lparse_test.ml +++ b/tests/lparse_test.ml @@ -3,6 +3,11 @@ open Lparse open Fmt_lexp open Utest_lib +open Pexp +open Lexp + +open Builtin + let test (input_gen: (unit -> 'a list)) (fmt: 'b list -> string list) @@ -24,7 +29,9 @@ let generate_tests (name: string) (fun () -> if res then success () else failure ())) (test input_gen fmt tester) -let input = "x = lambda x -> x;" +(* let input = "y = lambda x -> x + 1;" *) +let input = "id = lambda (α : Type) ≡> lambda x : α -> x; +res = id 3;" let generate_lexp_from_str str = List.hd ((fun (lst, _) -> @@ -37,6 +44,76 @@ let _ = generate_tests "TYPECHECK" (fun () -> [generate_lexp_from_str input]) (fun x -> List.map string_of_lxp x) - (fun x -> (x, false)) + (fun x -> (x, true)) + +let lctx = default_lctx +let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () -> + + let dcode = " + sqr = lambda (x) -> x * x; + cube = lambda (x) -> x * (sqr x); + + mult = lambda (x) -> lambda (y) -> x * y; + + twice = (mult 2); + + let_fun = lambda (x) -> + let a = (twice x); b = (mult 2 x); in + a + b;" in + + let ret1, _ = lexp_decl_str dcode lctx in + + let to_str decls = + let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in + List.fold_left (fun str lxp -> str ^ lxp) "" str in + + (* Cast to string *) + let str1 = to_str ret1 in + + print_string str1; + + (* read code again *) + let ret2, _ = lexp_decl_str str1 lctx in + + (* Cast to string *) + let str2 = to_str ret2 in + + if str1 = str2 then success () else failure () +)) + +(* +let set_to_list s = + StringSet.fold (fun g a -> g::a) s [] + +let _ = (add_test "LEXP" "Free Variable" (fun () -> + + let dcode = " + a = 2; + b = 3; + f = lambda n -> (a + n); % a is a fv + g = lambda x -> ((f b) + a + x); % f,a,b are fv + " in + + let ret = pexp_decl_str dcode in + let g = match List.rev ret with + | (_, g, _)::_ -> g + | _ -> raise (Unexpected_result "Unexpected empty list") in + + let (bound, free) = free_variable g in + + let bound = set_to_list bound in + let (free, _) = free in + + match bound with + | ["x"] ->( + match free with + | ["_+_"; "f"; "b"; "a"] -> success () + | _ -> failure ()) + | _ -> failure () + +)) *) + +(* run all tests *) +let _ = run_all () let _ = run_all () ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -152,17 +152,17 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::(input_lambda2 , input_lambda3 , Constraint) ::(input_lambda3 , input_lambda3 , Equivalent) - ::(input_arrow2 , input_int_4 , Nothing) - ::(input_arrow2 , input_induct , Nothing) - ::(input_arrow2 , input_case , Constraint) + ::(input_arrow2 , input_int_4 , Unification) (* changes in lexp_p_infer & lexp_p_check *) + ::(input_arrow2 , input_induct , Unification) (* changed the "output" of lexp_decl_str*) + ::(input_arrow2 , input_case , Constraint) (* which changed the type of the Lexp*) ::(input_arrow2 , input_case2 , Constraint) ::(input_arrow2 , input_let , Constraint) - ::(input_arrow2 , input_induct , Nothing) - ::(input_arrow2 , input_lambda , Nothing) - ::(input_arrow2 , input_lambda2 , Nothing) - ::(input_arrow2 , input_arrow3 , Constraint) (* It's a constraint because we don't know yet the type *) - ::(input_arrow3 , input_arrow , Constraint) (* of the var inside the arrow *) - ::(input_arrow2 , input_arrow , Equivalent) + ::(input_arrow2 , input_induct , Unification) + ::(input_arrow2 , input_lambda , Unification) + ::(input_arrow2 , input_lambda2 , Unification) + ::(input_arrow2 , input_arrow3 , Unification) + ::(input_arrow3 , input_arrow , Unification) + ::(input_arrow2 , input_arrow , Unification) ::(input_arrow3 , input_arrow3 , Equivalent) ::(input_type , input_type_t , Equivalent) ===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -117,6 +117,12 @@ let ut_string2 = ut_string 2 let unexpected_throw sk tk e = ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); ut_string2 "[ ] UNEXPECTED THROW:\n"; + ut_string2 "[ ] ----------------------------- Callstack (20): -----------------------------------------\n"; + ut_string2 ("[ ] " ^ (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20))); + ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; + ut_string2 "[ ] ----------------------------- Backtrace: ----------------------------------------------\n"; + ut_string2 ("[ ] " ^ (Printexc.get_backtrace ()) ^ "\n"); + ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; ut_string2 "[ ] "; ut_string2 ((Printexc.to_string e) ^ "\n" ^ reset) let _expect_equal_t to_string value expect = View it on GitLab: https://gitlab.com/monnier/typer/compare/304245b63c5caed07861573d5be8e8ca89…

2 1

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Août 2016