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/304245b63c5caed07861573d5be8e8ca896...