Setepenre pushed to branch master at Stefan / Typer

Commits: e314669e by Pierre Delaunay at 2016-09-25T13:39:35-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - f83ee0b4 by Pierre Delaunay at 2016-09-26T12:05:47-04:00 Merge branch 'master' of github.com:Delaunay/typer

- - - - - 12a677ab by Pierre Delaunay at 2016-09-26T19:27:11-04:00 Try to fix our Macro_ index problem. Nevertheless, it does not work as a lot of index are not computed correctly anymore

* Moved (print_lexp_ctx) from lparse.ml to debruijn.ml to help debugging * src/lparse.ml: types and expression are processed in a different context

- - - - - db617a20 by Pierre Delaunay at 2016-09-26T19:54:32-04:00 Merge with master. Indices seem to be correct. Nevertheles, Macro are still not recognized as such (back to the original issue)

- - - - -

6 changed files:

- btl/types.typer - samples/nat.typer - src/builtin.ml - src/debruijn.ml - src/lparse.ml - tests/eval_test.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -66,7 +66,7 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); % -----------------------------------------------------

List : Type -> Type; -List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); +List = inductive_ (List (a : Type)) (nil) (cons a (List a));

nil = inductive-cons List nil; cons = inductive-cons List cons; @@ -76,7 +76,7 @@ length = lambda a ≡> lambda xs -> case xs | nil => 0 - | cons hd tl => (1 + (length(a := a) tl)); + | cons hd tl => (1 + (length (a := a) tl));

head : (a : Type) ≡> List a -> a; head = lambda a ≡> @@ -92,6 +92,7 @@ tail = lambda a ≡> | nil => nil | cons hd tl => tl;

+ % ----------------------------------------------------- % Macro % ----------------------------------------------------- @@ -103,8 +104,8 @@ 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 : Type; +Macro = inductive_ (Macro) (Macro_ (List Sexp -> Sexp)); Macro_ = inductive-cons Macro Macro_ ;

expand_macro_ : Macro -> List Sexp -> Sexp; @@ -181,3 +182,6 @@ declexpr = Built-in "declexpr" Macro;

+ + +

===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -5,39 +5,31 @@ zero = inductive-cons Nat zero; succ = inductive-cons Nat succ;

to-num : Nat -> Int; -to-num = lambda (x : Nat) -> - case x - | (succ y) => (1 + (to-num y)) - | zero => 0; - -one = (succ zero); -two = (succ one); -three = (succ two); +to-num = lambda (x : Nat) -> case x + | (succ y) => (1 + (to-num y)) + | zero => 0;

plus : Nat -> Nat -> Nat; -plus = lambda (x : Nat) -> - lambda (y : Nat) -> - case x - | zero => y - | succ z => succ (plus z y); +plus = lambda (x : Nat) -> lambda (y : Nat) -> case x + | zero => y + | succ z => succ (plus z y);

+one = succ zero; +two = succ one; +three = succ two;

-odd : Nat -> Int; even : Nat -> Int; +odd : Nat -> Int; odd = lambda (n : Nat) -> case n - | zero => 0 - | succ y => (even y); + | zero => 0 + | succ y => (even y);

even = lambda (n : Nat) -> case n - | zero => 1 - | succ y => (odd y); - -%n1 = (to-num zero); -%n2 = (to-num one); -%n3 = (to-num two); + | zero => 1 + | succ y => (odd y);

-%m1 = (to-num (plus zero two)); % 2 -%m2 = (to-num (plus two zero)); % 2 -%m3 = (to-num (plus two one)); % 3

-o1 = (even two); \ No newline at end of file +a = odd one; +b = even one; +c = odd two; +d = even two; \ No newline at end of file

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -75,7 +75,7 @@ let get_predef_raw (name: string) : lexp = | None -> builtin_error dloc ("""^ name ^ "" was not predefined")

let get_predef_option (name: string) ctx = - let r = (get_size ctx) - !builtin_size - 1 in + let r = (get_size ctx) - !builtin_size - 0 in match !(SMap.find name (!predef_map)) with | Some exp -> Some (mkSusp exp (S.shift r)) | None -> None

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -46,6 +46,9 @@ let debruijn_warning = msg_warning "DEBRUIJN" (* Type definitions * ---------------------------------- *)

+let dloc = dummy_location +let type0 = Sort (dloc, Stype (SortLevel (SLn 0))) +let dltype = type0

type property_key = (int * string) (* rev_dbi * Var name *) module PropertyMap @@ -116,7 +119,8 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = lexp_ctx_cons ctx 0 (Some def) v t

-let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = + +let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env, f) = ctx in (try let _ = senv_lookup name ctx in @@ -124,9 +128,11 @@ let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = with Not_found -> ()); let nmap = StringMap.add name n map in ((n + 1, nmap), - lexp_ctx_cons env 0 (Some def) v t, + lexp_ctx_cons env r (Some def) v t, f)

+let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t + let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = let (ctx, _) = List.fold_left @@ -152,10 +158,88 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = recursion_offset - 1) (ctx, List.length defs) defs

-let _name_error loc estr str = - if estr = str then () else +let env_lookup_by_index index (ctx: elab_context): env_elem = + (Myers.nth index (_get_env ctx)) + +(* Print context *) +let print_lexp_ctx (ctx : elab_context) = + let ((n, map), env, f) = ctx in + + print_string (make_title " LEXP CONTEXT "); + + make_rheader [ + (Some ('l', 10), "NAME"); + (Some ('l', 7), "INDEX"); + (Some ('l', 10), "NAME"); + (Some ('l', 4), "OFF"); + (Some ('l', 29), "VALUE:TYPE")]; + + print_string (make_sep '-'); + + (* it is annoying to print according to StringMap order *) + (* let's use myers list order *) + let rec extract_names (lst: lexp_context) acc = + match lst with + | Mnil-> acc + | Mcons (hd, tl, _, _) -> + let name = match hd with + | (_, Some (_, name), _, _) -> name + | _ -> "" in + extract_names tl (name::acc) in + + let ord = extract_names env [] in + + let rec _print idx ord = + match ord with + | [] -> () + | hd::tl ->( + let idx2 = StringMap.find hd map in + + (if idx2 != idx then ()); + + print_string " | "; lalign_print_string hd 10; + print_string " | "; lalign_print_int (n - idx - 1) 7; + print_string " | "; + + let ptr_str = "" in (*" | | | | " in *) + + try let r, name, exp, tp = + match env_lookup_by_index (n - idx - 1) ctx with + | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp + | _ -> 0, "", None, dltype in + + (* Print env Info *) + lalign_print_string name 10; (* name must match *) + print_string " | "; + lalign_print_int r 4; + print_string " | "; + + let _ = (match exp with + | None -> print_string "<var>" + | Some exp -> lexp_print exp) + (* let str = _lexp_to_str (!debug_ppctx) exp in + let str = (match str_split str '\n' with + | hd::tl -> print_string (hd ^ "\n"); tl + | _ -> []) in + + List.iter (fun elem -> + print_string (ptr_str ^ elem ^ "\n")) str) *)in + + print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n"; + + _print (idx + 1) tl + + with Not_found -> + (print_string "Not_found |\n"; _print (idx + 1) tl)) in + + _print 0 ord; print_string (make_sep '=') + + +let _name_error loc estr str ctx = + if estr = str then () else ( + print_lexp_ctx ctx; debruijn_error loc ("DeBruijn index refers to wrong name. " ^ - "Expected: "" ^ estr ^ "" got "" ^ str ^ """) + "Expected: "" ^ estr ^ "" got "" ^ str ^ """))

(* generic lookup *) @@ -167,7 +251,7 @@ let _env_lookup ctx (v: vref): env_elem = let _ = match ret with | (_, Some (_, name), _, _) -> (* Check if names match *) - _name_error loc ename name; + _name_error loc ename name ctx; | _ -> () in

ret) @@ -187,9 +271,6 @@ let env_lookup_expr ctx (v : vref): lexp option = | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) | _ -> None

-let env_lookup_by_index index (ctx: elab_context): env_elem = - (Myers.nth index (_get_env ctx)) - (* replace an expression by another *) (* Most of the time it should be O(1) but it can be O(n) *) let replace_by ctx name by =

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -162,14 +162,15 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

(* Symbol i.e identifier *) | Pvar (loc, name) ->( - try let idx = (senv_lookup name ctx) in + try + let idx = (senv_lookup name ctx) in let lxp = (make_var name idx loc) in

(* search type *) let ltp = env_lookup_type ctx ((loc, name), idx) in lxp, ltp

- with Not_found -> + with e -> (lexp_error loc ("The variable: "" ^ name ^ "" was not declared"); (* Error recovery. The -1 index will raise an error later on *) (make_var name (-1) loc), dltype)) @@ -224,8 +225,8 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

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 *) + (* 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 @@ -401,7 +402,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = * Constructor : a constructor is returned * Anonymous : lambda *)

- (* retrieve function's body *) + (* retrieve function's body (sqr 3) sqr is a Pvar() *) let body, ltp = _lexp_p_infer func ctx (i + 1) in let ltp = nosusp ltp in

@@ -432,6 +433,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Expected non-explicit arg" | t -> lexp_print t; print_string "\n"; + print_lexp_ctx ctx; lexp_fatal (sexp_location sarg) "Explicit arg to non-function") in

@@ -493,32 +495,32 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = _lexp_p_infer pxp ctx (i + 1) in

(* This is the builtin Macro type *) - let macro_type = match get_predef_option "Macro" ctx with - | Some lxp -> lxp - (* When type.typer is being parsed and the predef is not yet - * available *) - | None -> dltype in + let macro_type, macro_disp = match get_predef_option "Macro" ctx with + | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx), true + (* When type.typer is being parsed and the predef is not yet available *) + | None -> dltype, false in + + (*print_string "\nmacro_type="; lexp_print macro_type; + print_string "\nltp="; lexp_print ltp; + print_string " (= "; lexp_print (OL.lexp_whnf ltp (ectx_to_lctx ctx)); print_string ")\n"; *)

(* determine function type *) match func, ltp with - (* This is a work around for the bug described below *) | Pvar(l, name), _ when is_builtin_macro name -> - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - (get_macro_impl loc name) loc largs ctx ltp + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx i in + (get_macro_impl loc name) loc largs ctx ltp

- (* FIXME: the branch 'builtin macro' is never used because of missing shift somewhere *) - (* while special forms have a type macro this does not recognize them as such *) - | macro, _ when OL.conv_p ltp macro_type -> ( + | macro, _ when (macro_disp && (OL.conv_p ltp macro_type))-> ( match macro with | Pvar(l, name) when is_builtin_macro name -> - print_string name; let pargs = List.map pexp_parse sargs in let largs = _lexp_parse_all pargs ctx i in (get_macro_impl loc name) loc largs ctx ltp

(* true macro *) - | _ -> handle_macro_call ()) + | _ -> + handle_macro_call ())

(* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall () @@ -813,8 +815,9 @@ and _lexp_rec_decl decls ctx i = * i.e let decl parsing *)

(* to compute recursive offset *) - let n = (List.length decls) + 1 in + let n = (List.length decls) in let lst = ref [] in + (* print_int n; print_string "\n"; *)

(* add all elements to the environment *) let tctx = List.fold_left (fun vctx decl -> @@ -823,29 +826,30 @@ and _lexp_rec_decl decls ctx i = env_extend vctx (l, s) ForwardRef dltype

| Ldecl((l, s), _, Some ptp) -> - let lxp, _ = lexp_p_infer ptp vctx in - env_extend vctx (l, s) ForwardRef lxp + let ltp, _ = lexp_p_infer ptp vctx in + env_extend vctx (l, s) ForwardRef ltp

| Lmcall _ -> lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in

+ (* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *) let i = ref 0 in let ctx = List.fold_left (fun vctx decl -> i := !i + 1; match decl with + (* +1 because we allow each definition to be recursive *) (* lexp infer *) | Ldecl ((l, s), Some pxp, None) -> - let lxp, ltp = lexp_p_infer pxp vctx in + let lxp, ltp = lexp_p_infer pxp tctx in lst := ((l, s), lxp, ltp)::!lst; - (* replace forward ref by its true value *) - replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)

(* lexp check *) | Ldecl ((l, s), Some pxp, Some ptp) -> let ltp, _ = lexp_p_infer ptp vctx in - let lxp = lexp_p_check pxp ltp vctx in + let lxp = lexp_p_check pxp ltp tctx in lst := ((l, s), lxp, ltp)::!lst; - replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)

(* macros *) | Lmcall (a, sargs) -> @@ -854,7 +858,7 @@ and _lexp_rec_decl decls ctx i = (* unused arg *) | Ldecl ((l, s), None, _) -> lexp_error l ("Variable "" ^ s ^ "" is unused!"); - vctx) tctx decls in + vctx) ctx decls in

(List.rev !lst), ctx

@@ -871,80 +875,6 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =

(loop p ctx [])

-(* Print context *) -and print_lexp_ctx (ctx : elab_context) = - let ((n, map), env, f) = ctx in - - print_string (make_title " LEXP CONTEXT "); - - make_rheader [ - (Some ('l', 10), "NAME"); - (Some ('l', 7), "INDEX"); - (Some ('l', 10), "NAME"); - (Some ('l', 4), "OFF"); - (Some ('l', 29), "VALUE:TYPE")]; - - print_string (make_sep '-'); - - (* it is annoying to print according to StringMap order *) - (* let's use myers list order *) - let rec extract_names (lst: lexp_context) acc = - match lst with - | Mnil-> acc - | Mcons (hd, tl, _, _) -> - let name = match hd with - | (_, Some (_, name), _, _) -> name - | _ -> "" in - extract_names tl (name::acc) in - - let ord = extract_names env [] in - - let rec _print idx ord = - match ord with - | [] -> () - | hd::tl ->( - let idx2 = StringMap.find hd map in - - (if idx2 != idx then ()); - - print_string " | "; lalign_print_string hd 10; - print_string " | "; lalign_print_int (n - idx - 1) 7; - print_string " | "; - - let ptr_str = "" in (*" | | | | " in *) - - try let r, name, exp, tp = - match env_lookup_by_index (n - idx - 1) ctx with - | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp - | _ -> 0, "", None, dltype in - - (* Print env Info *) - lalign_print_string name 10; (* name must match *) - print_string " | "; - lalign_print_int r 4; - print_string " | "; - - let _ = (match exp with - | None -> print_string "<var>" - | Some exp -> lexp_print exp) - (* let str = _lexp_to_str (!debug_ppctx) exp in - let str = (match str_split str '\n' with - | hd::tl -> print_string (hd ^ "\n"); tl - | _ -> []) in - - List.iter (fun elem -> - print_string (ptr_str ^ elem ^ "\n")) str) *)in - - print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n"; - - _print (idx + 1) tl - - with Not_found -> - (print_string "Not_found |\n"; _print (idx + 1) tl)) in - - _print 0 ord; - - print_string (make_sep '=')

and print_lexp_trace () = print_trace " LEXP TRACE " 50 pexp_to_string pexp_print !_global_lexp_trace

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -70,7 +70,7 @@ let _ = test_eval_eqv_named

"a = 10; b = a; c = b; d = c;"

- "d" (* == *) "10" + "d" (* == *) "10"

(* Let * ------------------------ *) @@ -92,7 +92,7 @@ let _ = test_eval_eqv_named "sqr : Int -> Int; sqr = lambda x -> x * x;"

- "(sqr 4);" (* == *) "16" + "sqr 4;" (* == *) "16"

let _ = test_eval_eqv_named "Nested Lambda" @@ -103,7 +103,7 @@ let _ = test_eval_eqv_named cube : Int -> Int; cube = lambda x -> x * (sqr x);"

- "(cube 4)" (* == *) "64" + "cube 4" (* == *) "64"

(* Cases + Inductive types @@ -130,7 +130,7 @@ let _ = test_eval_eqv_named | ctr2 l => 2 | _ => 3;"

- "(test_fun a); (test_fun b); (test_fun c)" + "test_fun a; test_fun b; test_fun c"

"1; 2; 3"

@@ -156,11 +156,11 @@ let _ = test_eval_eqv_named "Inductive::Recursive Call"

(nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two);") + one = succ zero; + two = succ one; + three = succ two;")

- "(to-num zero); (to-num one); (to-num two);" + "to-num zero; to-num one; to-num two;"

"0; 1; 2"

@@ -168,9 +168,9 @@ let _ = test_eval_eqv_named "Inductive::Nat Plus"

(nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two); + one = succ zero; + two = succ one; + three = succ two;

plus : Nat -> Nat -> Nat; plus = lambda (x : Nat) -> lambda (y : Nat) -> case x @@ -187,11 +187,13 @@ let _ = test_eval_eqv_named "Mutually Recursive Definition"

(nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two); + one = succ zero; + two = succ one; + three = succ two;

even : Nat -> Int; + odd : Nat -> Int; + odd = lambda (n : Nat) -> case n | zero => 0 | succ y => (even y); @@ -200,7 +202,7 @@ let _ = test_eval_eqv_named | zero => 1 | succ y => (odd y);")

- "(odd one); (even one); (odd two); (even two);" + "odd one; even one; odd two; even two;"

"1; 0; 0; 1"

@@ -212,9 +214,9 @@ let _ = test_eval_eqv_named add = lambda x y -> (x + y);

inc : Int -> Int; - inc = (add 1);" + inc = add 1;"

- "(inc 1); (inc 2); (inc 3);" + "inc 1; inc 2; inc 3;"

"2; 3; 4"

View it on GitLab: https://gitlab.com/monnier/typer/compare/fac6cb52949425bd38aa3e92c5b89fb2f55...