Setepenre pushed to branch master at Stefan / Typer

Commits: ca0b6e8d by Pierre Delaunay at 2016-05-15T08:57:03-04:00 Builtin now takes two arguments: function_name and function_type

Changes to be committed: * btl/types.typer: reflect "Builtin" change * src/elexp.ml: unsusp susp * src/REPL.ml: - reflected change linked to elexp.ml - file reading is now done with eval_file * src/builtin.ml - add predefined_table and get_predefine * src/lparse.ml: - simplified handle_call as it had a lot of legacy code - constructor now inherit inductive's formal_args as Aerasable arguments cons : (a : Type) ≡> (v : a) -> List a -> List - predef_table is populated in default_ctx right after builtin type definition were read * src/debug_util.ml: - added: -typecheck argument

- - - - -

11 changed files:

- .travis.yml - GNUmakefile - btl/types.typer - samples/quote.typer - src/REPL.ml - src/builtin.ml - src/debug_util.ml - src/elexp.ml - src/eval.ml - src/lparse.ml - src/typecheck.ml

Changes:

===================================== .travis.yml ===================================== --- a/.travis.yml +++ b/.travis.yml @@ -6,7 +6,7 @@ env: addons: apt: packages: - - ocaml + - opam

before_script: - opam config setup -a

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -66,9 +66,11 @@ clean:

.PHONY: typer debug tests

+run/typecheck: + @./_build/debug_util ./samples/test__.typer -typecheck

run/debug_util: - @./_build/debug_util ./samples/test__.typer -fmt-type=off + @./_build/debug_util ./samples/test__.typer -fmt-type=on -fmt-index=off -fmt-pretty=on

run/typer: @./_build/typer

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -41,11 +41,8 @@ String = Built-in "String"; Sexp = Built-in "Sexp";

% Basic operators -_+_ : Int -> Int -> Int; -_+_ = Built-in "_+_"; - -_*_ : Int -> Int -> Int; -_*_ = Built-in "_*_"; +_+_ = Built-in "_+_" (Int -> Int -> Int); +_*_ = Built-in "_*_" (Int -> Int -> Int);

Bool = inductive_ (Boolean) (True) (False); True = inductive-cons Bool True; @@ -56,14 +53,9 @@ Option = inductive_ (Option (a : Type)) (None) (Some a); Some = inductive-cons Option Some; None = inductive-cons Option None;

-string_eq : String -> String -> Bool; -string_eq = Built-in "string_eq"; - -int_eq : Int -> Int -> Bool; -int_eq = Built-in "int_eq"; - -sexp_eq : Sexp -> Sexp -> Bool; -sexp_eq = Built-in "sexp_eq"; +string_eq = Built-in "string_eq" (String -> String -> Bool); +int_eq = Built-in "int_eq" (Int -> Int -> Bool); +sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool);

% ----------------------------------------------------- % List @@ -100,32 +92,25 @@ tail = lambda a => % Macro % -----------------------------------------------------

-block_ : (List Sexp) -> Sexp; -block_ = Built-in "block_"; - -symbol_ : String -> Sexp; -symbol_ = Built-in "symbol_"; - -string_ : String -> Sexp; -string_ = Built-in "string_"; - -node_ : Sexp -> (List Sexp) -> Sexp; -node_ = Built-in "node_"; - -integer_ : Int -> Sexp; -integer_ = Built-in "integer_"; - -float_ : Float -> Sexp; -float_ = Built-in "float_"; +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-cons Macro Macro_ ;

-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_"; +sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp + -> (Sexp -> List Sexp -> Sexp) + -> (String -> Sexp) + -> (String -> Sexp) + -> (Int -> Sexp) + -> (Float -> Sexp) + -> (List Sexp -> Sexp) + -> Sexp);

===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -11,7 +11,10 @@ node = (lambda (op : Sexp) -> lambda (y : List Sexp) -> case y | nil => node_ op nil - | _ => node_ op (quote' y)); + | _ => node_ (quote' (cons op nil)) (quote' y)); + | _ => node_ (symbol_ "node_") (cons (quote' op) + (cons (reconstruire la liste en sexp) nil)) + | uquote => y

% tree traversal quote' : List Sexp -> List Sexp; @@ -32,10 +35,26 @@ quote' = lambda (x : List Sexp) -> % quote definition quote = Macro_ (lambda (x : List Sexp) -> head Sexp (quote' x));

+fun n = + let x = 2 in + % Should it return % (node_ (symbol_ "_*_") (cons (symbol_ x) (cons (symbol_ x) nil)))

% OR % x * x (Lexp, donc Call(_*_, [x x])

-%main = quote (x * x); \ No newline at end of file +%main = quote (x * x); + + +Quelque chose comme: + + Nat = inductive Nat + | zero + | succ Nat; + +est parsé comme: + + Call(op=_|_, args=[(inductive Nat), zero, (succ Nat)]) + +for it to work, we could define _|_ as a Macro

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -55,6 +55,7 @@ open Builtin open Env open Debruijn module TC = Typecheck +module EL = Elexp

(* how to handle arrow keys ? *) let _history = ref [] @@ -118,7 +119,12 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = | _ -> _pxp_parse tl dacc ((pexp_parse sxp)::pacc) in _pxp_parse sxps [] []

-let ilexp_parse pexps lctx = + +let ierase_type (lexps: (ldecl list * lexpr list)) = + let (ldecls, lexprs) = lexps in + (EL.clean_decls ldecls), (List.map EL.erase_type lexprs) + +let ilexp_parse pexps lctx: ((ldecl list * lexpr list) * lexp_context) = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_p_decls pdecls lctx in let lexprs = lexp_parse_all pexprs lctx in @@ -140,12 +146,27 @@ let _ieval f str lctx rctx = (* Different from usual typer *) let pxps = ipexp_parse nods in let lxps, lctx = ilexp_parse pxps lctx in - let v, rctx = ieval lxps rctx in + let elxps = ierase_type lxps in + let v, rctx = ieval elxps rctx in v, lctx, rctx

+let _raw_eval f str lctx rctx = + let pres = (f str) 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 + let lxps, lctx = lexp_p_decls pxps lctx in + let elxps = EL.clean_decls lxps in + let rctx = eval_decls elxps rctx in + (* This is for consistency with ieval *) + [], lctx, rctx + let ieval_string = _ieval prelex_string let ieval_file = _ieval prelex_file

+let eval_string = _raw_eval prelex_string +let eval_file = _raw_eval prelex_file +

let _welcome_msg = " Typer 0.0.0 - Interpreter - (c) 2016 @@ -172,9 +193,7 @@ let readfiles files (i, lctx, rctx) prt = print_string " In["; ralign_print_int i 2; print_string "] >> "; print_string ("%readfile " ^ file); print_string "\n";));

- (* FIXME: This should not use the "ieval" but the "eval" syntax, - * i.e. only accept a sequence of declarations at top-level. *) - try let (ret, lctx, rctx) = ieval_file file lctx rctx in + try let (ret, lctx, rctx) = eval_file file lctx rctx in (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with Sys_error _ -> ( @@ -232,8 +251,8 @@ let parse_args () = let main () = parse_args ();

- let lctx = default_lctx () in - let rctx = default_rctx () in + let lctx = default_lctx in + let rctx = default_rctx in

print_string (make_title " TYPER REPL "); print_string _welcome_msg;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -44,6 +44,26 @@ let builtin_error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg)

+type predef_table = (lexp option ref) SMap.t + +let predef_name = [ + "cons"; + "nil" +] + +let predef_map : predef_table = + (* add predef name, expr will be populated when parsing *) + List.fold_left (fun m name -> + SMap.add name (ref None) m) SMap.empty predef_name + +let get_predef name = + match !(SMap.find name predef_map) with + | Some exp -> exp + | None -> builtin_error dloc "Try to access an empty predefined" + +let set_predef name lexp = + SMap.find name predef_map := lexp + (* Builtin types *) let dloc = dummy_location let slevel0 = SortLevel (SLn 0)

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -46,6 +46,7 @@ open Lexer open Lparse open Eval module EL = Elexp +module TC = Typecheck

(* definitions *) open Grammar @@ -89,6 +90,7 @@ let _format_mode = ref false let _ppctx = ref (true , 0, true, false, true, 2, true) let _format_dest = ref "" let _write_file = ref false +let _typecheck = ref false

let _set_print_pretty ctx v = @@ -113,7 +115,7 @@ let set_print_index v () = mod_ctx _set_print_index v let set_print_indent_size v = mod_ctx _set_print_indent_size v let set_highlight v () = mod_ctx _set_highlight v let set_print_pretty v () = mod_ctx _set_print_pretty v - +let set_typecheck v () = _typecheck := v

let output_to_file str = _write_file := true; @@ -146,6 +148,9 @@ let arg_defs = [ ("-fmt-file", Arg.String output_to_file, " Output formatted code to a file");

+ ("-typecheck", + Arg.Unit (add_p_option "typecheck"), " Enable type checking"); + (* Debug *) ("-pretok", Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); @@ -280,6 +285,28 @@ let main () = ) in print_string reset;

+ (* convert a lctx context into a typecheck context *) + (* they will be the same in the future *) + let lctx_to_cctx (lctx: lexp_context): TC.tc_ctx = + let (_, env, _) = lctx in + let n = Myers.length env in + + let rec loop i env cctx = + if i = (-1) then cctx else ( + let i, v, olxp, ltp = !(Myers.nth i env) in + let vlxp = match olxp with + | Some lxp -> TC.LetDef lxp + | None -> TC.ForwardRef in + let cctx = Myers.cons (i, Some v, vlxp, ltp) cctx in + loop (i - 1) env cctx) in + loop n env Myers.nil in + + (if (get_p_option "typecheck") then( + let cctx = lctx_to_cctx ctx in + (* run type check *) + List.iter (fun (_, lxp, _) -> + let _ = TC.check cctx lxp in ()) lexps)); + (if (get_p_option "lexp") then( print_string (make_title " Lexp "); debug_lexp_decls lexps; print_string "\n"));

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -57,11 +57,8 @@ type elexp = | Cons of symbol | Case of U.location * elexp * (U.location * (vdef option) list * elexp) SMap.t * elexp option - - (* Type definition *) - | Arrow - | SortLevel - | Sort + (* Type place-holder just in case *) + | Type (* Inductive takes a slot in the env that is why it need to be here *) | Inductive of U.location * label

@@ -89,12 +86,12 @@ 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) + (* To be thrown out *) - | L.Arrow _ -> Arrow - | L.SortLevel _ -> SortLevel - | L.Sort _ -> Sort - (* FIXME: This one is wrong: eliminate it with `unsusp`. *) - | L.Susp _ -> Arrow + | L.Arrow _ -> Type + | L.SortLevel _ -> Type + | L.Sort _ -> Type (* Still useful to some extend *) | L.Inductive(l, label, _, _) -> Inductive(l, label)

@@ -140,11 +137,8 @@ let rec elexp_location e = | Call (f,_) -> elexp_location f | Cons ((l,_)) -> l | Case (l,_,_,_) -> l - - | Arrow _ -> U.dummy_location - | Inductive _ -> U.dummy_location - | Sort _ -> U.dummy_location - | SortLevel _ -> U.dummy_location + | Inductive(l, _) -> l + | Type -> U.dummy_location

let rec elexp_print lxp = print_string (elexp_str lxp) and elexp_to_string lxp = elexp_str lxp

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -258,7 +258,8 @@ and sexp_dispatch loc args ctx =

let sxp = match sxp with | Vsexp(sxp) -> sxp - | _ -> debug_msg (value_print sxp); + | _ -> debug_msg ( print_string "\n"; + value_print sxp; print_string "\n"); eval_error loc "sexp_dispatch expects a Sexp as 1st arg" in

match sxp with

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -68,6 +68,13 @@ let _global_lexp_trace = ref [] let _parsing_internals = ref false let btl_folder = ref "./btl/"

+(* This is used to make Type annotation and inferred type having the same index *) +(* since inferred type might need to parse a lambda var to infer the type *) +let _type_shift tp i = + match tp with + | Var(v, idx) -> Var(v, idx) + | expr -> expr + (* The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable * @@ -157,11 +164,13 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> let ltp, _ = lexp_infer tp ctx in - let ctx = match ovar with - | None -> ctx - | Some var -> env_extend ctx var None ltp in + let nctx, sh = match ovar with + | None -> ctx, 0 + | Some var -> (env_extend ctx var None ltp), 1 in + + let lxp, _ = lexp_infer expr nctx in + let lxp = _type_shift lxp sh in

- let lxp, _ = lexp_infer expr ctx in let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, (get_type0 ctx)

@@ -197,6 +206,8 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

let nctx = env_extend ctx var None 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 @@ -218,20 +229,24 @@ 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 args = match idt with - | Some Inductive(_, _, _, ctor_def) -> ( - try (SMap.find cname ctor_def) + let formal, args = match idt with + | Some Inductive(_, _, formal, ctor_def) -> ( + try formal, (SMap.find cname ctor_def) with Not_found -> 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) -> Arrow(kind, v, tp, loc, ltp)) inductive_type (List.rev args) in

+ (* Add Aerasable argument *) + let cons_type = List.fold_left (fun ltp (kind, v, tp) -> + Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in + Cons((vr, idx), sym), cons_type

with Not_found -> @@ -274,7 +289,8 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = 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 *) @@ -285,7 +301,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = 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) + e*)

(* Lexp.case cam be checked and inferred *) and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = @@ -315,15 +331,18 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =

(* make a list of all branches return type *) let texp = ref [] in + let ctx_len = get_size ctx in

(* Read patterns one by one *) let fold_fun (merged, dflt) (pat, exp) = (* Create pattern context *) let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in + let nctx_len = get_size nctx in

(* parse using pattern context *) let exp, ltp = lexp_infer exp nctx in - texp := ltp::!texp; + (* we added len(arg) variable int the context *) + texp := (_type_shift ltp (nctx_len - ctx_len))::!texp;

(* Check ltp type. Must be similar to rtype *) (if type_check ltp then () @@ -385,34 +404,27 @@ 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

- (* Replace a built-in name by builtin so they can be recognized - * during eval *) - if (is_lbuiltin idx ctx) then ( match env_lookup_expr ctx ((loc, name), idx) with - | None -> lexp_error loc "Unknown builtin"; - let ret_type = get_return_type name 0 ltp new_args in - Call(vf, new_args), ret_type + | Some Builtin((_, "Built-in"), _) ->( + (* ------ SPECIAL ------ *) + match !_parsing_internals, largs with + | true, [Imm(String (_, str))] -> + Builtin((loc, str), ltp), ltp

- | Some Builtin((_, "Built-in"), ltp) ->( - match !_parsing_internals with - | false -> lexp_error loc "Use of Built-in in user code"; - dlxp, dlxp - | _ ->( - match largs with - | [Imm (String (_, str)) ] -> + | true, [Imm(String (_, str)); ltp] -> Builtin((loc, str), ltp), ltp - | _ -> typer_unreachable "cannot be reached"))

- (* a builtin functions *) - | Some Builtin((_, name), ltp) -> - (* We keep loc info *) - Call(Builtin((loc, name), ltp), new_args), ltp + | true, _ -> + lexp_error loc "Wrong Usage of "Built-in""; + dlxp, dltype

- | _ -> typer_unreachable "ill formed Builtin" - ) - else - let ret_type = get_return_type name 0 ltp new_args in - Call(vf, new_args), ret_type + | false, _ -> + lexp_error loc "Use of "Built-in" in user code"; + dlxp, dltype) + + | _ -> + 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"); @@ -801,12 +813,20 @@ let default_lctx = 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 _, lctx = lexp_p_decls pxps lctx in - _parsing_internals := false; - lctx + + _parsing_internals := true; + let _, lctx = lexp_p_decls pxps lctx in + _parsing_internals := false; + + (* Once default builtin are set we can populate the predef table *) + List.iter (fun name -> + let idx = senv_lookup name lctx in + let v = Var((dloc, name), idx) in (* + let value = (env_lookup_expr lctx v) in *) + set_predef name (Some v)) predef_name; + (* -- DONE -- *) + lctx

(* Make runtime context with built-in types *) let default_rctx = @@ -853,3 +873,4 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (EL.clean_decls lxps) in (eval_decls elxps rctx), lctx +

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -106,6 +106,10 @@ type varbind = | ForwardRef | LetDef of lexp

+(* easier to debug with type annotations *) +type tc_elem = int * vdef option * varbind * lexp +type tc_ctx = tc_elem Myers.myers + let lookup_type ctx vref = let (_, i) = vref in let (_, _, _, t) = Myers.nth i ctx in

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