BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 29ba9a05 by Pierre Delaunay at 2016-06-14T17:05:37-04:00 remove dead code

- - - - - 1bf06575 by Pierre Delaunay at 2016-06-14T17:56:19-04:00 Handle macro decls

Changes to be committed: * src/debug_util.ml : added some debug options * src/lparse.ml : Handle macro decls * src/eval.ml : - added (run-io) - new function (get_predef_eval) retuns a evaluated predef * btl/types.typer : added (run-io)

- - - - - 7d78d71b by Pierre Delaunay at 2016-06-14T20:00:25-04:00 delete dead code + add macro decls test

Changes to be committed: * src/eval.ml : remove dead code * tests/macro_test.ml: new test * btl/types.typer : added properties * src/lparse.ml : added properties * src/debruijn.ml : * new function (add_property) * new function (dump_properties) * src/debug_util.ml: * new debug option (dump-prop)

- - - - - 642376ae by Pierre Delaunay at 2016-06-25T18:16:01-04:00 Context accessors and Monad handling. modified travis script

Changes to be committed: *.travis.yml * src/debruijn.ml: - new function (get_attribute) - new function (has_attribute) - modify calling convention of (add_attribute) (better consistency) * btl/types.typer - added builtin context accessors (decltype) and (declexpr) * src/eval.ml - fix monad handling * src/lparse.ml - added context accessor as builtin macro

- - - - - d5da7869 by Pierre Delaunay at 2016-06-25T18:35:09-04:00 new calling convention for builtin functions (location -> int -> value_type list -> runtime_env -> value_type) ^~~~^ new

This allows us to have a more accurate call trace when eval is called inside a builtin-function.

Changes to be committed: * btl/types.typer * src/builtin.ml * src/eval.ml

- - - - - f530a2dd by Pierre Delaunay at 2016-06-26T11:23:25-04:00 Moved builtin macro implementation

Changes to be committed: * btl/types.typer: change type of some accessors * src/builtin.ml : - fix predef shifting - moved builtin macro implementation there * src/debruijn.ml: remove dead code * src/lparse.ml - builtin macro are now recognized inside (handle_macro_call)

- - - - - e0141d3f by n3f4s at 2016-06-27T16:38:38+02:00 Merge branch 'master' into unification

- - - - - 716e4d39 by n3f4s at 2016-06-27T16:42:20+02:00 add naive unification for Sort & SortLevel

- - - - - c2f914ab by n3f4s at 2016-06-27T17:48:41+02:00 re-ordering code for readability

- - - - - 1a8f1f70 by n3f4s at 2016-06-27T17:49:21+02:00 add _unify_sort* to top level unify function

- - - - - 4e00bcc5 by n3f4s at 2016-06-27T22:54:55+02:00 add unification case for _unify_sort

- - - - - d50e1e6a by n3f4s at 2016-06-27T23:47:55+02:00 correct _unify_induct

- - - - - 8757daba by n3f4s at 2016-06-27T23:48:44+02:00 add unification for Var & Susp with Sort

- - - - - ba72e9be by n3f4s at 2016-06-28T16:22:56+02:00 Add Case, Let, and Susp to the first unifyed types

- - - - - b4776a7e by n3f4s at 2016-06-28T16:25:18+02:00 correct case unification

Unification with Case returns a constraint Check result of unification of the 'inside' of the Case for unification Case, Case

- - - - - 86e66e31 by n3f4s at 2016-06-28T16:27:39+02:00 Correct _unify_induct & _unify_sort

- - - - -

13 changed files:

- − - - .travis.yml - btl/types.typer - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/env.ml - src/eval.ml - src/lparse.ml - src/unification.ml - tests/macro_test.ml - tests/unify_test.ml - − w_file

Changes:

===================================== - deleted ===================================== --- a/- +++ /dev/null

===================================== .travis.yml ===================================== --- a/.travis.yml +++ b/.travis.yml @@ -3,16 +3,12 @@ language: ocaml env: - OCAML_VERSION=4.02

-addons: - apt: - packages: - - opam - -before_script: - - opam config setup -a - - opam config env +sudo: true

before_script: + - sudo apt-get -qq update + - sudo apt-get install opam + - opam init --auto-setup - opam config setup -a - opam config env

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -27,6 +27,7 @@ %* %* Description: %* Define builtin types and functions +%* This file MUST be correctly typed %* %* ---------------------------------------------------------------------------

@@ -34,12 +35,14 @@ % Base Types % -----------------------------------------------------

-Type = Built-in "Type"; -Int = Built-in "Int"; -Float = Built-in "Float"; -String = Built-in "String"; -Sexp = Built-in "Sexp"; -Unit = Built-in "Unit"; +Type = Built-in "Type"; +Int = Built-in "Int"; +Float = Built-in "Float"; +String = Built-in "String"; +Sexp = Built-in "Sexp"; + +Unit = Built-in "Unit"; % Nothing +Context = Built-in "Context"; % Lexp Context

% Basic operators _+_ = Built-in "_+_" (Int -> Int -> Int); @@ -134,6 +137,11 @@ bind = Built-in "bind" ( FileHandle = Built-in "FileHandle";

% define operation on file handle +run-io = Built-in "run-io" ( + (a : Type) ≡> + (b : Type) ≡> + IO a -> (a -> IO b) -> (IO b) -> Unit); + open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String); @@ -143,15 +151,20 @@ read = Built-in "read" (FileHandle -> Int -> IO String); % -----------------------------------------------------

Attribute = Built-in "Attribute"; -new-attribute = Built-in "new-attribute" (Type -> Attribute); - - - - +new-attribute = Built-in "new-attribute" (Macro);

+add-attribute = Built-in "add-attribute" (Macro); +attribute = Macro_ add-attribute;

+get-attribute = Built-in "get-attribute" Macro; +has-attribute = Built-in "has-attribute" (Macro);

+% ----------------------------------------------------- +% Context Accessors +% -----------------------------------------------------

+decltype = Built-in "decltype" Macro; +declexpr = Built-in "declexpr" Macro;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -51,19 +51,31 @@ type predef_table = (lexp option ref) SMap.t

let predef_name = [ "cons"; - "nil" + "nil"; + "Unit"; + "True"; + "False"; + "Bool"; ]

+let builtin_size = ref 0 + 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 = +let get_predef_raw (name: string) : lexp = match !(SMap.find name predef_map) with | Some exp -> exp | None -> builtin_error dloc "Try to access an empty predefined"

+let get_predef name ctx = + let r = (get_size ctx) - !builtin_size in + let v = mkSusp (get_predef_raw name) (S.shift r) in + v + + let set_predef name lexp = SMap.find name predef_map := lexp

@@ -94,7 +106,7 @@ let type_float = Builtin((dloc, "Float"), type0) let type_string = Builtin((dloc, "String"), type0)

(* Builtin of builtin * string * ltype *) -let _generic_binary_iop name f loc (args_val: value_type list) +let _generic_binary_iop name f loc (depth: int) (args_val: value_type list) (ctx: runtime_env) =

let l, r = match args_val with @@ -114,11 +126,11 @@ let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b)

(* loc is given by the compiler *) -let none_fun : (location -> value_type list -> runtime_env -> value_type) +let none_fun : (location -> int -> value_type list -> runtime_env -> value_type) = (fun loc args_val ctx -> builtin_error loc "Requested Built-in was not implemented")

-let make_symbol loc args_val ctx = +let make_symbol loc depth args_val ctx = (* symbol is a simple string *) let lxp = match args_val with | [r] -> r @@ -158,10 +170,12 @@ let rec tlist2olist acc expr = tlist2olist (hd::acc) tl | Vcons((_, "nil"), []) -> List.rev acc | _ -> + print_string (value_name expr); print_string "\n"; value_print expr; + builtin_error dloc "List conversion failure'"

-let make_node loc args_val ctx = +let make_node loc depth args_val ctx =

let op, tlist = match args_val with | [Vsexp(op); lst] -> op, lst @@ -185,7 +199,7 @@ let make_node loc args_val ctx =

Vsexp(Node(op, s))

-let make_string loc args_val ctx = +let make_string loc depth args_val ctx = let lxp = match args_val with | [r] -> r | _ -> builtin_error loc ("string_ expects 1 argument") in @@ -194,7 +208,7 @@ let make_string loc args_val ctx = | Vstring(str) -> Vsexp(String(loc, str)) | _ -> builtin_error loc ("string_ expects one string as argument")

-let make_integer loc args_val ctx = +let make_integer loc depth args_val ctx = let lxp = match args_val with | [r] -> r | _ -> builtin_error loc ("integer_ expects 1 argument") in @@ -203,24 +217,24 @@ let make_integer loc args_val ctx = | Vint(str) -> Vsexp(Integer(loc, str)) | _ -> builtin_error loc ("integer_ expects one string as argument")

-let make_float loc args_val ctx = Vdummy -let make_block loc args_val ctx = Vdummy +let make_float loc depth args_val ctx = Vdummy +let make_block loc depth args_val ctx = Vdummy

let ttrue = Vcons((dloc, "True"), []) let tfalse = Vcons((dloc, "False"), []) let btyper b = if b then ttrue else tfalse

-let string_eq loc args_val ctx = +let string_eq loc depth args_val ctx = match args_val with | [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2) | _ -> builtin_error loc "string_eq expects 2 strings"

-let int_eq loc args_val ctx = +let int_eq loc depth args_val ctx = match args_val with | [Vint(s1); Vint(s2)] -> btyper (s1 = s2) | _ -> builtin_error loc "int_eq expects 2 integer"

-let sexp_eq loc args_val ctx = +let sexp_eq loc depth args_val ctx = match args_val with | [Vsexp(s1); Vsexp(s2)] -> ( match s1, s2 with @@ -232,54 +246,41 @@ let sexp_eq loc args_val ctx = | _ -> builtin_error loc "int_eq expects 2 sexp"

-let open_impl loc args_val ctx = +let open_impl loc depth args_val ctx =

let file, mode = match args_val with | [Vstring(file_name); Vstring(mode)] -> file_name, mode | _ -> builtin_error loc "open expects 2 strings" in

- (* open file *) (* return a file handle *) - match mode with - | "r" -> Vin(open_in file) - | "w" -> Vout(open_out file) - | _ -> builtin_error loc "wrong open mode" - + (* open file *) (* return a file handle *) + Vcommand(fun () -> + match mode with + | "r" -> Vin(open_in file) + | "w" -> Vout(open_out file) + | _ -> builtin_error loc "wrong open mode")

-let read_impl loc args_val ctx = +let read_impl loc depth args_val ctx =

let channel = match args_val with | [Vin(c); _] -> c | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - builtin_error loc "read expects a in_channel" in + builtin_error loc "read expects an in_channel" in

let line = input_line channel in Vstring(line)

-let write_impl loc args_val ctx = +let write_impl loc depth args_val ctx =

let channel, msg = match args_val with | [Vout(c); Vstring(msg)] -> c, msg | _ -> List.iter (fun v -> value_print v) args_val; - builtin_error loc "read expects a out_channel" in + builtin_error loc "read expects an out_channel" in

fprintf channel "%s" msg; Vdummy

-let new_attribute loc args_val ctx = - builtin_warning loc "new-attributes to be implemented"; - Vdummy - -(* - * Should we have a function that - * -> returns a new context inside typer ? (So we need to add a ctx type too) - * -> returns current context ? - * -> pexp_eval expr - * -> lexp_eval expr - * -> ou seulement: 'eval expr ctx' - *) - let is_lbuiltin idx ctx = let bsize = 1 in let csize = get_size ctx in @@ -288,3 +289,85 @@ let is_lbuiltin idx ctx = true else false + +(* -------------------------------------------------------------------------- + * Built-in Macro + * -------------------------------------------------------------------------- *) + +(* Those are function that are evaluated during lexp_parse *) + +let get_attribute_impl loc largs ctx ftype = + + let (vi, vn), (ai, an) = match largs with + | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) + | _ -> 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 + lxp, ltype + +let new_attribute_impl loc largs ctx ftype = + + let eltp = match largs with + | [eltp] -> eltp + | _ -> builtin_warning loc "new-attribute expects one argument"; type0 in + + eltp, ftype + +let has_attribute_impl loc largs ctx ftype = + + let (vi, vn), (ai, an) = match largs with + | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) + | _ -> builtin_error loc "has-attribute expects two arguments" in + + let b = has_property ctx (vi, vn) (ai, an) in + + let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in + rvar, (get_predef "Bool" ctx) + +let declexpr_impl loc largs ctx ftype = + + let (vi, vn) = match largs with + | [Var((_, vn), vi)] -> (vi, vn) + | _ -> builtin_error loc "declexpr expects one argument" in + + let lxp = env_lookup_expr ctx ((loc, vn), vi) in + let ltp = env_lookup_type ctx ((loc, vn), vi) in + lxp, ftype + + +let decltype_impl loc largs ctx ftype = + + let (vi, vn) = match largs with + | [Var((_, vn), vi)] -> (vi, vn) + | _ -> builtin_error loc "decltype expects one argument" in + + let ltype = env_lookup_type ctx ((loc, vn), vi) in + (* mkSusp prop (S.shift (var_i + 1)) *) + ltype, type0 + +let builtin_macro = [ + ("decltype", decltype_impl); + ("declexpr", declexpr_impl); + ("get-attribute", get_attribute_impl); + ("new-attribute", new_attribute_impl); + ("has-attribute", has_attribute_impl); +] + +type macromap = + (location -> lexp list -> lexp_context -> lexp -> (lexp * lexp)) SMap.t + +let macro_impl_map : macromap = + List.fold_left (fun map (name, funct) -> + SMap.add name funct map) SMap.empty builtin_macro + +let get_macro_impl loc name = + try SMap.find name macro_impl_map + with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found") + +let is_builtin_macro name = + try SMap.find name macro_impl_map; true + with Not_found -> false + + +

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -123,20 +123,6 @@ let _name_error loc estr str = debruijn_error loc ("DeBruijn index refers to wrong name. " ^ "Expected: "" ^ estr ^ "" got "" ^ str ^ """)

-(* -let env_set_var_info ctx (def: vref) (v: lexp option) (t: lexp) = - let ((dv_size, _), info_env, _) = ctx in - let ((loc, ename), dbi) = def in - - try(let rf = (Myers.nth dbi info_env) in - let (_, (_, name), _, _) = !rf in - - (* Check if names match *) - _name_error loc ename name; - - rf := (0, (loc, ename), v, t)) - with - Not_found -> debruijn_error loc "DeBruijn index out of bounds!" *)

(* generic lookup *) let _env_lookup ctx (v: vref): env_elem = @@ -158,7 +144,7 @@ let _env_lookup ctx (v: vref): env_elem = let env_lookup_type ctx (v : vref): lexp = let (_, idx) = v in let (_, _, _, ltp) = _env_lookup ctx v in - mkSusp ltp (S.shift (idx + 1)) + mkSusp ltp (S.shift (idx + 0))

let env_lookup_expr ctx (v : vref): lexp = let (_, idx) = v in @@ -203,3 +189,84 @@ let replace_by ctx name by = let nenv = List.fold_left (fun ctx elem -> cons elem ctx) nenv decls in (a, nenv, b)

+(* -------------------------------------------------------------------------- *) +(* PropertyMap *) +(* -------------------------------------------------------------------------- *) + + +let add_property ctx (var_i, var_n) (att_i, att_n) (prop: lexp) + : lexp_context = + + let (a, b, property_map) = ctx in + let n = get_size ctx in + + (* get_var properties *) + let vmap = try PropertyMap.find (var_i, var_n) property_map + with Not_found -> PropertyMap.empty in + + (* add property *) + let nvmap = PropertyMap.add (n - att_i, att_n) prop vmap in + + (* update properties *) + let property_map = PropertyMap.add (n - var_i, var_n) nvmap property_map in + + (a, b, property_map) + +let get_property ctx (var_i, var_n) (att_i, att_n): lexp = + let (a, b, property_map) = ctx in + let n = get_size ctx in + + (* /!\ input index are reversed or not ? I think not so I shift them *) + let pmap = try PropertyMap.find (n - var_i, var_n) property_map + with Not_found -> + debruijn_error dummy_location ("Variable "" ^ var_n ^ "" does not have any properties") in + + let prop = try PropertyMap.find (n - att_i, att_n) pmap + with Not_found -> + debruijn_error dummy_location ("Property "" ^ att_n ^ "" not found") in + mkSusp prop (S.shift (var_i + 1)) + + +let has_property ctx (var_i, var_n) (att_i, att_n): bool = + let (a, b, property_map) = ctx in + let n = get_size ctx in + + 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 + with Not_found -> false + + +let dump_properties ctx = + let (a, b, property_map) = ctx in + print_string (make_title " Properties "); + + make_rheader [ + (Some ('l', 10), "V-NAME"); + (Some ('l', 4), "RIDX"); + (Some ('l', 10), "P-NAME"); + (Some ('l', 4), "RIDX"); + (Some ('l', 32), "LEXP")]; + + print_string (make_sep '-'); + + PropertyMap.iter (fun (var_i, var_n) pmap -> + print_string " | "; + lalign_print_string var_n 10; print_string " | "; + ralign_print_int var_i 4; print_string " | "; + let first = ref true in + + PropertyMap.iter (fun (att_i, att_n) lxp -> + (if (!first = false) then + print_string (make_line ' ' 20) + else + first := false); + + lalign_print_string att_n 10; print_string " | "; + ralign_print_int att_i 4; print_string " : "; + lexp_print lxp; print_string "\n") pmap) property_map; + + print_string (make_sep '-'); + +

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -275,71 +275,59 @@ let main () = let octx = default_lctx in

(* Debug declarations merging *) + (if (get_p_option "merge-debug") then( + let merged = lexp_detect_recursive pexps in

- (** ) - let merged = lexp_detect_recursive pexps in + List.iter (fun lst -> + print_string (make_line '-' 80); + print_string "\n";

- let _ = List.iter (fun lst -> - print_string (make_line '-' 80); - print_string "\n"; + List.iter (fun v -> + match v with + | Ldecl((l, s), pxp, ptp) -> ( + lalign_print_string s 20;

- List.iter (fun v -> - match v with - | Ldecl((l, s), pxp, ptp) -> ( - lalign_print_string s 20; + let _ = match ptp with + | Some pxp -> pexp_print pxp; + | None -> print_string " " in

- let _ = match ptp with - | Some pxp -> pexp_print pxp; - | None -> print_string " " in + print_string "\n"; + lalign_print_string s 20;

- print_string "\n"; - lalign_print_string s 20; + let _ = match pxp with + | Some pxp -> pexp_print pxp; + | None -> print_string " " in

- let _ = match pxp with - | Some pxp -> pexp_print pxp; - | None -> print_string " " in + print_string "\n") + | Lmcall((l, s), _ ) -> + print_string s; print_string "\n" + ) lst;

- print_string "\n") - | Lmcall((l, s), _ ) -> - print_string s; print_string "\n" - ) lst; - - ) merged in ( **) + ) merged));

(* debug lexp parsing once merged *) let lexps, nctx = _lexp_decls pexps octx 0 in + (* use the new way of parsing expr *) + let ctx = nctx in + let flexps = List.flatten lexps in

- (* - List.iter (fun ((l, s), lxp, ltp) -> - lalign_print_string s 20; - lexp_print ltp; print_string "\n"; + (if (get_p_option "lexp-merge-debug") then( + List.iter (fun ((l, s), lxp, ltp) -> + lalign_print_string s 20; + lexp_print ltp; print_string "\n";

- lalign_print_string s 20; - lexp_print lxp; print_string "\n"; + lalign_print_string s 20; + lexp_print lxp; print_string "\n";

- ) decls; *) + ) flexps));

- (* use the new way of parsing expr *) - let ctx = nctx in - let flexps = List.flatten lexps in + (if (get_p_option "dump-prop") then( + dump_properties ctx; + print_string "\n"));

- (* convert a lctx context into a typecheck context *) - (* they will be the same in the future *) + (* get typecheck context *) let lctx_to_cctx (lctx: lexp_context) = let (_, env, _) = ctx in env in - (* - 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( print_string (make_title " TYPECHECK "); @@ -349,9 +337,8 @@ let main () = List.iter (fun (_, lxp, _) -> let _ = TC.check cctx lxp in ()) flexps;

- print_string (make_line '-' 76); - - )); + print_string (" " ^ (make_line '-' 76)); + print_string "\n";));

(if (get_p_option "lexp") then( print_string (make_title " Lexp "); @@ -360,20 +347,8 @@ let main () = (if (get_p_option "lctx") then( print_lexp_ctx nctx; print_string "\n"));

- - (* - List.iter (fun ((_, n), lxp, _) -> - print_string n; print_string "\n") - (List.flatten lexps); *) - let clean_lxp = EL.clean_toplevel lexps in

- (* - List.iter (fun ((_, n), lxp) -> - print_string n; print_string "\n"; - ) (List.flatten clean_lxp); - *) - (* Eval declaration *) let rctx = default_rctx in print_string yellow;

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -49,6 +49,7 @@ let env_error loc msg =

let str_idx idx = "[" ^ (string_of_int idx) ^ "]"

+ type value_type = | Vint of int | Vstring of string @@ -61,7 +62,8 @@ type value_type = | Vdummy | Vin of in_channel | Vout of out_channel - | Vbind of elexp list + | Vcommand of (unit -> value_type) +

let rec value_print (vtp: value_type) = match vtp with @@ -81,11 +83,7 @@ let rec value_print (vtp: value_type) = | Vdummy -> print_string "value_print_dummy" | Vin _ -> print_string "in_channel" | Vout _ -> print_string "out_channel" - | Vbind [a; b] -> print_string "bind ("; - elexp_print a; print_string ") ("; - elexp_print b; print_string ")"; - - | Vbind _ -> print_string "bind" + | Vcommand _ -> print_string "command" (* | _ -> print_string "debug print" *)

let value_location (vtp: value_type) = @@ -108,7 +106,7 @@ let value_name v = | Vdummy -> "Vdummy" | Vin _ -> "Vin" | Vout _ -> "Vout" - | Vbind _ -> "Vbind" + | Vcommand _ -> "Vcommand"

(* Runtime Environ *) type env_cell = (string option * value_type) ref

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -61,6 +61,7 @@ let _eval_max_recursion_depth = ref 255 let reset_eval_trace () = _global_eval_trace := [] let _builtin_lookup = ref SMap.empty

+ (* This is an internal definition * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp ctx i: (value_type) = @@ -83,7 +84,7 @@ let rec _eval lxp ctx i: (value_type) = | Lambda ((_, n), lxp) -> Closure(n, lxp, ctx) | Builtin ((_, str)) -> Vbuiltin(str)

- (* Return a value stored in env *) + (* Return a value stored in env *) | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx)

@@ -100,8 +101,13 @@ let rec _eval lxp ctx i: (value_type) = | Case (loc, target, pat, dflt) -> (eval_case ctx i loc target pat dflt)

- | _ -> print_string "debug catch-all eval: "; - elexp_print lxp; print_string "\n"; Vstring("eval Not Implemented") + | Type -> Vcons((tloc, "Unit"), []) + + +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

and eval_var ctx lxp v = let ((loc, name), idx) = v in @@ -111,38 +117,34 @@ and eval_var ctx lxp v =

and eval_call ctx i lname eargs = let loc = elexp_location lname in - let args = List.map (fun e -> - (* elexp_print e; print_string "\n"; *) - _eval e ctx (i + 1)) eargs in let f = _eval lname ctx (i + 1) in

+ (* standard function *) let rec eval_call f args ctx = - match f, args with - | Vcons (n, []), _ -> - let e = Vcons(n, args) in - (* value_print e; print_string "\n"; *) e - - (* we add an argument to the closure *) - | Closure (n, lxp, ctx), hd::tl -> - let nctx = add_rte_variable (Some n) hd ctx in - let ret = _eval lxp nctx (i + 1) in - eval_call ret tl nctx + match f, args with + | Vcons (n, []), _ -> + let e = Vcons(n, args) in + (* value_print e; print_string "\n"; *) e

- (* bind is lazily evaluated *) - | Vbuiltin ("bind"), _ -> - Vbind eargs + (* we add an argument to the closure *) + | Closure (n, lxp, ctx), hd::tl -> + let nctx = add_rte_variable (Some n) hd ctx in + let ret = _eval lxp nctx (i + 1) in + eval_call ret tl nctx

- | Vbuiltin (str), args -> - (* lookup the built-in implementation and call it *) - (get_builtin_impl str loc) loc args ctx + | Vbuiltin (str), args -> + (* lookup the built-in implementation and call it *) + (get_builtin_impl str loc) loc (i + 1) args ctx

- (* return result of eval *) - | _, [] -> f + (* return result of eval *) + | _, [] -> f

- | _ -> debug_msg (value_print f); - eval_error loc "Cannot eval function" in + | _ -> debug_msg (value_print f); + eval_error loc "Cannot eval function" in

- eval_call f args ctx + (* eval function here *) + let args = List.map (fun e -> _eval e ctx (i + 1)) eargs in + eval_call f args ctx

and eval_case ctx i loc target pat dflt = (* Eval target *) @@ -231,36 +233,62 @@ and typer_builtins_impl = [ ("eval_" , typer_eval); ("open" , open_impl); ("bind" , bind_impl); + ("run-io" , run_io); ("read" , read_impl); ("write" , write_impl); - ("new-attribute" , new_attribute) - ] -and bind_impl loc args_val ctx = + +and bind_impl loc depth args_val ctx =

let io, cb = match args_val with | [io; callback] -> io, callback | _ -> builtin_error loc "bind expects two arguments" in

+ (* build Vcommand from io function *) + let cmd = match io with + | Vcommand (cmd) -> cmd + | _ -> builtin_error loc "bind first arguments must be a monad" in + + (* bind returns another Vcommand *) + Vcommand (fun () -> (* get callback *) - let body, ctx = match cb with - | Closure(_, body, ctx) -> body, ctx - | _ -> builtin_error loc "A Closure was expected" in + let body, ctx = match cb with + | Closure(_, body, ctx) -> body, ctx + | _ -> builtin_error loc "A Closure was expected" in + + (* run given command *) + let underlying = cmd () in

(* add evaluated IO to arg list *) - let nctx = add_rte_variable None io ctx in + let nctx = add_rte_variable None underlying ctx in

(* eval callback *) - _eval body nctx 0 + _eval body nctx depth) + +and run_io loc depth args_val ctx = + + let io, ltp = match args_val with + | [io; ltp] -> io, ltp + | _ -> builtin_error loc "run-io expects 2 arguments" in + + let cmd = match io with + | Vcommand (cmd) -> cmd + | _ -> builtin_error loc "run-io expects a monad as first argument" in + + (* run given command *) + let _ = cmd () in + + (* return given type *) + ltp

-and typer_eval loc args ctx = +and typer_eval loc depth args ctx = let arg = match args with | [a] -> a | _ -> eval_error loc "eval_ expects a single argument" in (* I need to be able to lexp sexp but I don't have lexp ctx *) match arg with (* Nodes that can be evaluated *) - | Closure (_, body, ctx) -> _eval body ctx 1 + | Closure (_, body, ctx) -> _eval body ctx depth (* Leaf *) | _ -> arg

@@ -279,7 +307,7 @@ and get_builtin_impl str loc = (* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) -> (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) -and sexp_dispatch loc args ctx = +and sexp_dispatch loc depth args ctx = let eval a b = _eval a b 1 in let sxp, nd, sym, str, it, flt, blk, rctx = match args with | [sxp; Closure(_, nd, rctx); Closure(_, sym, _); @@ -373,45 +401,3 @@ let from_lctx (ctx: lexp_context) rm: runtime_env = done;

!rctx - - (* let ((n, _), env, _) = ctx in - let rctx = ref make_runtime_ctx in - - let bsize = 0 in - let csize = n - 1 in - - (* add all variables * ) - for i = bsize to csize do - let name = match (Myers.nth (csize - i) env) with - | (_, Some (_, name), _, _) -> Some name - | _ -> None in - - rctx := add_rte_variable name Vdummy (!rctx) - done; *) - - let diff = csize - bsize in - - (* process all of them *) - for i = 0 to diff do - try - let j = diff - i (* - 1 *) in - let name, exp = match Myers.nth (csize - i) env with - | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp - | _ -> None, None in - - let vxp = match exp with - | Some lxp -> - let lxp = (erase_type lxp) in - (try (eval lxp !rctx) - with e -> elexp_print lxp; - print_string "\n"; raise e) - - | None -> Vdummy in - rctx := add_rte_variable name vxp (!rctx) - - with Not_found -> - print_int n; print_string " "; - print_int (csize - i); print_string "\n "; - raise Not_found - done; - !rctx *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -456,102 +456,60 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = Call(vf, new_args), ltp in

let handle_macro_call (loc, name) = - (* look up for definition *) - let idx = try senv_lookup name ctx + (* check for builtin *) + match is_builtin_macro name with + | true -> + 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 + + (* 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 ("Could not find Variable: " ^ name) in - - (* Get the macro *) - let lxp = try env_lookup_expr ctx ((loc, name), idx) (* with - | e -> e - | _ -> lexp_fatal loc "The macro cannot be expanded"; *) - with Not_found -> - lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ - " is not a correct index.") in - - let lxp = match unsusp_all lxp with - | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | _ -> - 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 - - (* Build function to be called *) - let arg = olist2tlist_lexp sargs ctx in - - let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = EL.erase_type lxp in - let rctx = (from_lctx ctx 0) in - - (* - let rargs = eval (EL.erase_type arg) rctx in - let rctx = add_rte_variable None rargs rctx in - - let lxp = Susp(lxp, (SU.shift 1)) in - let body = eval (EL.erase_type lxp) rctx in - - print_string "HERE2\n"; - value_print body; *) - (* - - print_string "\n\n"; - lexp_print lxp; print_string "\n\n"; *) - - (* print_string "DH: "; - value_print (eval (EL.erase_type arg) rctx); print_string "\n"; *) - (* - print_rte_ctx rctx; print_string "\n"; - print_lexp_ctx ctx; print_string "\n";*) - - _global_eval_trace := []; - - let vxp = try eval elexp rctx - with e -> - print_eval_trace (); - raise e in - - let sxp = match vxp with - | Vsexp(sxp) -> sxp - (* Those are sexp converted by the eval function *) - | Vint(i) -> Integer(dloc, i) - | Vstring(s) -> String(dloc, s) - | Vfloat(f) -> Float(dloc, f) - (* I have vdum here WHY *) - | v -> debug_msg (value_print v); - lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in - - - let pxp = pexp_parse sxp in - _lexp_p_infer pxp ctx (i + 1) in - - (* - let handle_qq loc = - (* In quasi quote we need to traverse the sexp tree and evaluate - * (uq) calls *) - - let rec seek_n_replace sxp = - match sxp with - (* Unquote *) - | Node (Symbol(_, "uquote"), [arg]) ->( - let parg = pexp_parse arg in - let larg, _ = _lexp_p_infer parg ctx i in - let vsxp = eval larg (from_lctx ctx) in - match vsxp with - | Vint (i) -> Integer(loc, i) - | Vstring (s) -> String (loc, s) - | Vsexp(sxp) -> sxp - | _ -> - value_print vsxp; - lexp_warning loc "Sexp was expected"; Epsilon) - - | Node (op, lst) -> Node(op, (List.map seek_n_replace lst)) - | _ -> sxp in - - let sxp = match sargs with - | [sxp] -> seek_n_replace sxp - | _ -> lexp_error loc "qquote expects a sexp"; Epsilon in - Imm(sxp), type_sexp in *) + lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ + " is not a correct index.") in + + let lxp = match unsusp_all lxp with + | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct + | _ -> + 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 + + (* Build function to be called *) + let arg = olist2tlist_lexp sargs ctx in + + let lxp = Call(lxp, [(Aexplicit, arg)]) in + let elexp = EL.erase_type lxp in + let rctx = (from_lctx ctx 0) in + + _global_eval_trace := []; + + let vxp = try eval elexp rctx + with e -> + print_eval_trace (); + raise e in + + let sxp = match vxp with + | Vsexp(sxp) -> sxp + (* Those are sexp converted by the eval function *) + | Vint(i) -> Integer(dloc, i) + | Vstring(s) -> String(dloc, s) + | Vfloat(f) -> Float(dloc, f) + (* I have vdum here WHY *) + | v -> debug_msg (value_print v); + lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in + + let pxp = pexp_parse sxp in + _lexp_p_infer pxp ctx (i + 1)) in

(* determine function type *) match fun_name, ltp with @@ -564,7 +522,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = Call(body, new_args), ltp

| (Pvar (l, n), Var((_, "Macro"), _)) -> - (* FIXME: check db_idx points too a Macro type *) + (* FIXME: check db_idx points to a Macro type *) handle_macro_call (l, n)

(* Call to Vanilla or constructor *) @@ -581,9 +539,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = 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" + pexp_print e; print_string "\n"; + print_string ((pexp_to_string e) ^ "\n"); + lexp_fatal (pexp_location e) "This expression cannot be called"

(* Read a pattern and create the equivalent representation *) @@ -670,7 +628,7 @@ and lexp_parse_inductive ctors ctx i =

(* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_decls_macro (loc, mname) sargs ctx: pdecl list = +and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* lookup for mname_ *) let idx = try senv_lookup mname ctx with Not_found -> @@ -690,26 +648,43 @@ and lexp_decls_macro (loc, mname) sargs ctx: pdecl list = lexp_print lxp; print_string "\n"; lexp_fatal loc "Macro is ill formed" in

- (* 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 rctx = (from_lctx ctx 0) in + match lxp with + | Var((_, "add-attribute"), _) ->( + (* Builtin macro *) + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx 0 in + + (* extract info *) + let var, att, fn = match largs with + | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn + | _ -> lexp_fatal loc "add-attribute expects 3 args" in

- (* get a list of declaration *) - let decls = eval elexp rctx in + let ctx = add_property ctx var att fn in + + [], ctx + ) + (* Standard Macro *) + | _ -> ( + (* 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 rctx = (from_lctx ctx 0) in

- (* convert typer list to ocaml *) - let decls = tlist2olist [] decls in + (* get a list of declaration *) + let decls = eval elexp rctx in

- (* extract sexp from result *) - let decls = List.map (fun g -> - match g with - | Vsexp(sxp) -> sxp - | _ -> lexp_fatal loc "Macro expects sexp list") decls in + (* convert typer list to ocaml *) + let decls = tlist2olist [] decls in

- (* read as pexp_declaraton *) - pexp_decls_all decls + (* extract sexp from result *) + let decls = List.map (fun g -> + match g with + | Vsexp(sxp) -> sxp + | _ -> lexp_fatal loc "Macro expects sexp list") decls in + + (* read as pexp_declaraton *) + pexp_decls_all decls, ctx)

(* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 @@ -797,9 +772,19 @@ and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = let all = ref [] in

let ctx = List.fold_left (fun ctx decl -> - let d, ctx = _lexp_rec_decl decl ctx i in - all := d::!all; - ctx) ctx decls in + match decl with + (* Special case *) + | [Lmcall ((l, s), sargs)] -> + (* get pexp decls *) + let pdecls, ctx = lexp_decls_macro (l, s) sargs ctx in + let decls, ctx = _lexp_decls pdecls ctx i in + all := (List.append (List.rev decls) !all); + ctx + + | _ -> + let d, ctx = _lexp_rec_decl decl ctx i in + all := d::!all; + ctx) ctx decls in

(List.rev !all), ctx

@@ -853,171 +838,9 @@ and _lexp_rec_decl decls ctx i =

(List.rev !lst), ctx

- (* -and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) = - - let names = ref [] in (* decls name in correct order *) - let glob = ref SMap.empty in - let mut = ref [] in - let offset = ref 1 in - let last_decls = ref "" in - let recursive_mode = ref false in - - let ctx = List.fold_left (fun vctx expr -> - _global_lexp_trace := []; - match expr with - | Pexpr((l, s), pxp) ->( - try let idx = senv_lookup s vctx in - let ltp = env_lookup_type vctx ((l, s), idx) in - let lxp = lexp_p_check pxp ltp vctx in - (* update declaration *) - glob := SMap.add s (l, s, Some lxp, ltp) !glob; - - (* check if recursive definition *) - (if !last_decls = s && !recursive_mode then - ( - (* print_string "RECURSIVE END\n"; *) - (* push every variable with the correct offset *) - let d = List.rev !mut in - let length = (List.length d) + 1 in - let j = ref 0 in - - let vctx = - List.fold_left (fun vctx n -> - let (l, s, lxp, ltp) = SMap.find n !glob in - let lxp = match lxp with - | Some lxp -> LetDef lxp - | None -> lexp_warning dloc "ForwardRef are not allowed"; - ForwardRef in - - j := !j + 1; - replace_by vctx s (length - !j, Some (l, s), lxp, ltp)) vctx d - - in - - (* Clean everything *) - mut := []; - last_decls := ""; - recursive_mode := false; - vctx - ) - else - ( - (if !recursive_mode then offset := !offset + 1); - (* update context *) - replace_by vctx s (1, Some (l, s), (LetDef lxp), ltp); - )); - - with Not_found -> - (* Add dummy first *) - let tctx = env_extend vctx (l, s) ForwardRef dltype in - let lxp, ltp = lexp_p_infer pxp tctx in - - names := [s]::!names; - - (if !recursive_mode then ( - offset := !offset + 1; - mut := s::!mut)); - - glob := SMap.add s (l, s, Some lxp, ltp) !glob; - - env_extend vctx (l, s) (LetDef lxp) ltp) - - | Ptype((l, s), ptp) -> - (if !recursive_mode then () else - last_decls := s; - offset := 1); - - recursive_mode := true; - names := [s]::!names; - mut := s::!mut; - - (* get type *) - let ltp, _ = lexp_p_infer ptp vctx in - (* push *) - glob := SMap.add s (l, s, None, ltp) !glob; - env_extend vctx (l, s) ForwardRef ltp - - | Pmcall((l, n), sargs) -> ( - let pdecls = lexp_decls_macro (l, n) sargs vctx in - let _, _ =_lexp_decls pdecls vctx (i + 1) in - - vctx) - - (* | _ -> vctx*)) ctx decls in - - (* - (if List.length !mut != 0 then names := !mut::!names); *) - - (* return a list containing mutually recursive def *) - let merge_list names = - List.fold_left (fun acc key -> - let (l, s, lxp, ltp) = SMap.find key !glob in - let lxp = match lxp with - | Some lxp -> lxp - | None -> dltype in - - (* - let ltp = unsusp_all ltp in - let lxp = unsusp_all lxp in *) - ((l, s), lxp, ltp)::acc) [] names in - - let decls = List.map (fun names -> - merge_list names) (List.rev !names) in - - decls, ctx -*) - and lexp_decls_toplevel decls ctx = _lexp_decls decls ctx 1

- (* let names = ref [] in - let offset = ref 0 in - let merged = ref SMap.empty in - let acc = ref [] in - - let ctx = List.fold_left (fun vctx expr -> - match expr with - | Pexpr ((l, s), pxp) ->( - try let idx = senv_lookup s vctx in - let ltp = env_lookup_type vctx ((l, s), idx) in - let lxp = lexp_p_check pxp ltp vctx in - let (_, _, _, ltp) = SMap.find s !merged in - merged := SMap.add s (l, s, Some lxp, ltp) !merged; - let r = !offset in - let r = if r = 0 then 1 else r in - offset := 0; - replace_by vctx s (r, Some (l, s), (LetDef lxp), ltp); - - with Not_found -> - (* Add dummy first *) - let tctx = env_extend vctx (l, s) ForwardRef dltype in - let lxp, ltp = lexp_p_infer pxp tctx in - names := s::!names; - merged := SMap.add s (l, s, Some lxp, ltp) !merged; - env_extend vctx (l, s) (LetDef lxp) ltp) - - | Ptype ((l, s), ptp) -> - offset := !offset + 1; - let ltp, _ = lexp_p_infer ptp vctx in - names := s::!names; - merged := SMap.add s (l, s, None, ltp) !merged; - env_extend vctx (l, s) ForwardRef ltp - - | _ -> vctx) ctx decls in - - (* merge type and expr *) - let decls = List.fold_left (fun acc key -> - let (l, s, lxp, ltp) = SMap.find key !merged in - let lxp = match lxp with - | Some lxp -> lxp - | None -> dltype in - let ltp = unsusp_all ltp in - let lxp = unsusp_all lxp in - ((l, s), lxp, ltp)::acc) [] !names in - - decls, ctx *) - and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list =

let rec loop (plst: pexp list) ctx (acc: lexp list) = @@ -1160,12 +983,13 @@ let default_lctx = List.iter (fun ((_, s), _, _) -> print_string (s ^ ", ")) decls; print_string "] \n") d; *)

+ builtin_size := get_size lctx; + (* Once default builtin are set we can populate the predef table *) try 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 *) + let v = Var((dloc, name), idx) in set_predef name (Some v)) predef_name; (* -- DONE -- *) lctx @@ -1194,13 +1018,6 @@ let default_rctx = let rctx = eval_decls_toplevel (EL.clean_toplevel d) rctx in _global_eval_trace := []; rctx - (* - try (from_lctx (default_lctx)) - with e ->( - print_eval_trace (); - lexp_error dloc "Could not convert lexp context into rte context"; - raise e) *) -

(* String Parsing * --------------------------------------------------------- *)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -91,6 +91,8 @@ let empty_subst = (VMap.empty) * CONSTRAINT -> returns a constraint *)

+(****************************** Top level unify *************************************) + (** Dispatch to the right unifyer. * If (_unify_X X Y) don't handle the case (X, Y), it call (unify Y X) * The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) @@ -100,6 +102,9 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = match (l, r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst + | (_, Case _) -> _unify_case r l subst + | (_, Susp _) -> _unify_susp r l subst + | (_, Let _) -> _unify_let r l subst | (Imm _, _) -> _unify_imm l r subst | (Cons _, _) -> _unify_cons l r subst | (Builtin _, _) -> _unify_builtin l r subst @@ -112,107 +117,32 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Susp _, _) -> _unify_susp l r subst | (Case _, _) -> _unify_case l r subst | (Inductive _, _) -> _unfiy_induct l r subst - | (_, _) -> None + | (Sort _, _) -> _unify_sort l r subst + | (SortLevel _, _) -> _unify_sortlvl l r subst +(*| (_, _) -> None*)

-(** Check arg_king in (arg_kind * vdef option) list in Case *) -and is_same arglist arglist2 = - match arglist, arglist2 with - | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2 - | [], [] -> true - | _, _ -> false +(********************************* Type specific unify *******************************)

-(** try to unify the SMap part of the case *) -and _unify_inner_case l s = - let rec _unify_inner_case l s = - match l with - | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::t when key = key2 -> - (if is_same arglist arglist2 then ( match unify lxp lxp2 s with - | Some (s', c) -> (match _unify_inner_case l s' with - | Some (s_, c_) -> Some (s_, c@c_) - | None -> None) - | None -> None) - else None) - | [] -> Some (s, []) - | _ -> None - in _unify_inner_case l s - -(** Unify a Case with a lexp - * Case, Var -> constraint (if the variable type and the type of the return value is equivalent, it should be unifiable) - * Case, Case -> try to unify - * Case, _ -> None - *) -and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = -(* Maybe Constraint instead ?*) - match case, lxp with - | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2)) - -> ( match lxpopt, lxopt2 with - | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with - | Some (s, c) -> _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s (* TODO match on result *) - | None -> None) - | _, _ -> None) - | (Case _, Var _) -> Some (subst, [(case, lxp)]) (* ??? *) - | (_, _) -> None - -(* - Those part of Inductive : - * ((arg_kind * vdef * ltype) list) (* formal Args *) - * ((arg_kind * vdef option * ltype) list) - are almost identical except for the 'vdef option' (which is ignored) so the same function (_unify_inner_induct) should - work for those part, but it don't work because of 'vdef option' +(** Unify two Imm if they match <=> Same type and same value + * Add one of the Imm (the first arguement) to the substitution + * Imm, Imm -> if Imm =/= Imm then ERROR else OK + * Imm, lexp -> unify lexp Imm *) -(** for _unfiy_induct_sub_list*) -and _unify_inner_induct_2 lst subst : return_type = - let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2 - then unify l1 l2 subst +and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = + match (l, r) with + | (Imm (String (_, v1)), Imm (String (_, v2))) + -> if v1 = v2 then Some ((subst, [])) else None - in - List.fold_left (fun a e -> (match a with - | Some (s, c) -> (match test e s with - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c)) - | None -> test e subst) - ) None lst - -(** for _unify_induct : unify the formal arg*) -and _unify_inner_induct_1 lst subst : return_type = - let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2 - then unify l1 l2 subst + | (Imm (Integer (_, v1)), Imm (Integer (_, v2))) + -> if v1 = v2 then Some ((subst, [])) else None - in - List.fold_left (fun a e -> (match a with - | Some (s, c) -> (match test e s with - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c)) - | None -> test e subst) - ) None lst - -(** unify the SMap of list in Inductive *) -and _unify_induct_sub_list l1 l2 subst = - let test l1 l2 subst = match l1, l2 with - | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct_2 (List.combine v1 v2) subst with - | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c)) - | None -> (_unify_induct_sub_list t1 t2 subst)) - | _, _ -> None - in test l1 l2 subst - -(** Unify a Inductive and a lexp - * Inductive, Inductive -> try t unify - * Inductive, _ -> None*) -and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (induct, lxp) with - | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> - (match _unify_inner_induct_1 (List.combine farg1 farg2) subst with - | None -> None - | Some (s, c) -> _unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) + | (Imm (Float (_, v1)), Imm (Float (_, v2))) + -> if v1 = v2 then Some ((subst, [])) + else None + | (Imm _, Imm _) -> None + | (Imm _, _) -> unify r l subst | (_, _) -> None

-and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = - match susp_ with - | Susp _ -> unify (unsusp_all susp_) lxp subst - | _ -> None - and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = (* symbol = (location * string)*) match (cons, lxp) with @@ -223,16 +153,67 @@ and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = else None | (_, _) -> None

-and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = - let combine list1 list2 = - let l1 = List.fold_right (fun (_, x) acc -> x::acc) list1 [] - and l2 = List.fold_right (fun (_, x) acc -> x::acc) list2 [] +(** Unify a builtin (bltin) and a lexp (lxp) if it is possible + * If the two arguments are builtin, unify based on name + * If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp +*) +and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type = + match (bltin, lxp) with + | (Builtin ((_, name1), _), Builtin ((_, name2),_)) + -> if name1 = name2 then Some ((subst, [])) + else None (* assuming that builtin have unique name *) + | (Builtin (_, lxp_bltin), _) -> unify lxp_bltin lxp subst + | (_, _) -> None + +(** Unify a Let (let_) and a lexp (lxp), if possible + * Let , Let -> check the 'inside' of the let + * Let , lexp -> constraint +*) +and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = + let combine list1 list2 f = + let l1 = List.fold_right (f) list1 [] + and l2 = List.fold_right (f) list2 [] in List.combine l1 l2 - in match (call, lxp) with - | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> - _unify_inner ((lxp1, lxp2)::(combine lxp_list1 lxp_list2)) subst - | (Call _, _) -> Some ((subst, [(call, lxp)])) - | (_, _) -> None + in match (let_, lxp) with + | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> + let f = (fun (_, t, x) acc -> t::x::acc) + in _unify_inner ((lxp_, lxp2)::(combine m m1 f)) subst + | (Let _, _) -> Some (subst, [(let_, lxp)]) + | _, _ -> None + +(** Unify a Var and a lexp, if possible + * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes + * (Var, Metavar) -> unify_metavar Metavar var subst + * (_, _) -> None +*) +and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = + match (var, r) with + | (Var (_, idx1), Var (_, idx2)) + -> if idx1 = idx2 then Some ((subst, [])) + else None + | (Var _, Imm _) -> Some (subst, [(var, r)])(*FIXME : check for the value of Var -> need context ?*) + | (Var _, _) -> unify r var subst (*returns to unify*) + | (_, _) -> None + +(** Unify a Arrow and a lexp if possible + * (Arrow, Arrow) -> if var_kind = var_kind + then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) + else None + * (_, _) -> None +*) +and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) + : return_type = + match (arrow, lxp) with + | (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) + -> if var_kind1 = var_kind2 + then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst + (* _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst *) + else None + | (Arrow _, Imm _) -> None + | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) (* FIXME Var can contain type ???*) + | (Arrow _, _) -> unify lxp arrow subst + (*| (Arrow _, Call _) -> None*) (* Call can return type (?) *) + | (_, _) -> None

(** Unify a Lambda and a lexp if possible * See above for result @@ -266,100 +247,152 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type | Some (lxp_) -> unify lxp_ lxp subst) | (_, _) -> None

-(** Unify a Arrow and a lexp if possible - * (Arrow, Arrow) -> if var_kind = var_kind - then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) - else None - * (_, _) -> None +and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = + let combine list1 list2 f = + let l1 = List.fold_right (f) list1 [] + and l2 = List.fold_right (f) list2 [] + in List.combine l1 l2 + in match (call, lxp) with + | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> + let f = (fun (_, x) acc -> x::acc) + in _unify_inner ((lxp1, lxp2)::(combine lxp_list1 lxp_list2 f)) subst + | (Call _, _) -> Some ((subst, [(call, lxp)])) + | (_, _) -> None + +and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = + match susp_ with + | Susp _ -> unify (unsusp_all susp_) lxp subst + | _ -> None + +(** Unify a Case with a lexp + * Case, Case -> try to unify + * Case, _ -> Constraint *) -and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) - : return_type = - match (arrow, lxp) with - | (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) - -> if var_kind1 = var_kind2 - then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst - (* _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst *) - else None - | (Arrow _, Imm _) -> None - | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) (* FIXME Var can contain type ???*) - | (Arrow _, _) -> unify lxp arrow subst - (*| (Arrow _, Call _) -> None*) (* Call can return type (?) *) +and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = + match case, lxp with + | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2)) + -> ( match lxpopt, lxopt2 with + | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with + | Some (s, c) -> (match _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s with + | Some (s', c') -> Some (s', c@c') + | None -> None) + | None -> None) + | _, _ -> None) + | (Case _, _) -> Some (subst, [(case, lxp)]) + | (_, _) -> None + +(** Unify a Inductive and a lexp + * Inductive, Inductive -> try unify + * Inductive, Var -> constraint + * Inductive, Call/Metavar/Case/Let -> constraint + * Inductive, _ -> None*) +and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = + match (induct, lxp) with + | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> + (match _unify_inner_induct_1 (List.combine farg1 farg2) subst with + | None -> None + | Some (s, c) -> (match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with + | Some (s', c') -> Some (s', c@c') + | None -> None)) + | (Inductive _, Var _) -> Some (subst, [(induct, lxp)]) | (_, _) -> None

-(** Unify lexp & ltype (Arrow (_,_,ltype, lexp)) of two Arrow*) -and _unify_inner_arrow (lt1: lexp) (lxp1: lexp) - (lt2: lexp) (lxp2: lexp) (subst: substitution): return_type = - match unify lt1 lt2 subst with - | Some (subst_, const) -> ( (*bracket for formating*) - match unify lxp1 lxp2 subst_ with - | Some (s, c) -> Some(s, const@c) - | None -> None ) - | None -> None +and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type = + match sortlvl, lxp with + | (SortLevel s, SortLevel s2) -> (match s, s2 with + | SLn i, SLn j when i = j -> Some (subst, []) + | SLsucc l1, SLsucc l2 -> unify l1 l2 subst (* Is SLsucc some kind of linked list ? *) + | _, _ -> None) + | _, _ -> None

-(** Unify a Var and a lexp, if possible - * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes - * (Var, Metavar) -> unify_metavar Metavar var subst - * (_, _) -> None +and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = + match sort_, lxp with + | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with + | Stype lxp1, Stype lxp2 -> unify lxp1 lxp2 subst + | StypeOmega, StypeOmega -> Some (subst, []) + | StypeLevel, StypeLevel -> Some (subst, []) + | _, _ -> None) + | Sort _, Var _ -> Some (subst, [(sort_, lxp)]) + | _, _ -> None + +(************************ Helper function **************************************) + +(***** for Case *****) +(** Check arg_king in (arg_kind * vdef option) list in Case *) +and is_same arglist arglist2 = + match arglist, arglist2 with + | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2 + | [], [] -> true + | _, _ -> false + +(** try to unify the SMap part of the case *) +and _unify_inner_case l s = + let rec _unify_inner_case l s = + match l with + | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::t when key = key2 -> + (if is_same arglist arglist2 then ( match unify lxp lxp2 s with + | Some (s', c) -> (match _unify_inner_case l s' with + | Some (s_, c_) -> Some (s_, c@c_) + | None -> None) + | None -> None) + else None) + | [] -> Some (s, []) + | _ -> None + in _unify_inner_case l s + + +(***** for Inductive *****) +(* + Those part of Inductive : + * ((arg_kind * vdef * ltype) list) (* formal Args *) + * ((arg_kind * vdef option * ltype) list) + are almost identical except for the 'vdef option' (which is ignored) so the same function (_unify_inner_induct) should + work for those part, but it don't work because of 'vdef option' *) -and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = - match (var, r) with - | (Var (_, idx1), Var (_, idx2)) - -> if idx1 = idx2 then Some ((subst, [])) +(** for _unfiy_induct_sub_list*) +and _unify_inner_induct_2 lst subst : return_type = + let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2 + then unify l1 l2 subst else None - | (Var _, Imm _) -> Some (subst, [(var, r)])(*FIXME : check for the value of Var -> need context ?*) - | (Var _, _) -> unify r var subst (*returns to unify*) - | (_, _) -> None + in + List.fold_left (fun a e -> (match a with + | Some (s, c) -> (match test e s with + | Some (s1, c1) -> Some (s1, c1@c) + | None -> Some (s, c)) + | None -> test e subst) + ) None lst

-(** Unify two Imm if they match <=> Same type and same value - * Add one of the Imm (the first arguement) to the substitution *) -and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = - match (l, r) with - | (Imm (String (_, v1)), Imm (String (_, v2))) - -> if v1 = v2 then Some ((subst, [])) - else None - | (Imm (Integer (_, v1)), Imm (Integer (_, v2))) - -> if v1 = v2 then Some ((subst, [])) - else None - | (Imm (Float (_, v1)), Imm (Float (_, v2))) - -> if v1 = v2 then Some ((subst, [])) +(** for _unify_induct : unify the formal arg*) +and _unify_inner_induct_1 lst subst : return_type = + let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2 + then unify l1 l2 subst else None - | (Imm _, Imm _) -> None - | (Imm _, _) -> unify r l subst - | (_, _) -> None + in + List.fold_left (fun a e -> (match a with + | Some (s, c) -> (match test e s with + | Some (s1, c1) -> Some (s1, c1@c) + | None -> Some (s, c)) + | None -> test e subst) + ) None lst

-(** Unify a builtin (bltin) and a lexp (lxp) if it is possible - * If the two arguments are builtin, unify based on name - * If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp -*) -and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (bltin, lxp) with - | (Builtin ((_, name1), _), Builtin ((_, name2),_)) - -> if name1 = name2 then Some ((subst, [])) - else None (* assuming that builtin have unique name *) - | (Builtin (_, lxp_bltin), _) -> unify lxp_bltin lxp subst - | (_, _) -> None +(** unify the SMap of list in Inductive *) +and _unify_induct_sub_list l1 l2 subst = + let test l1 l2 subst = match l1, l2 with + | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct_2 (List.combine v1 v2) subst with + | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with + | Some (s1, c1) -> Some (s1, c1@c) + | None -> Some (s, c)) + | None -> (_unify_induct_sub_list t1 t2 subst)) + | _, _ -> None + in test l1 l2 subst

-(** Unify a Let (let_) and a lexp (lxp), if possible - * Let , Let -> check the 'inside' of the let - * Let , lexp -> constraint -*) -and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (let_, lxp) with - | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> - _unify_inner ((lxp_, lxp2)::(combine m m1)) subst - | (Let _, _) -> Some (subst, [(let_, lxp)]) - | _, _ -> None +(***** general *****)

(** take two list [(vdef * ltype * lexp), (vdef2 * ltype2 * lexp2)...] map them to [ltype, lexp, ltype2, lexp2, ...] and zip them to [(ltype * ltype), (lexp * lexp), (ltype2 * ltype2), (lexp2 * lexp2), ...] *) -and combine list1 list2 = - let l1 = List.fold_right (fun (_, t, x) acc -> t::x::acc) list1 [] - and l2 = List.fold_right (fun (_, t, x) acc -> t::x::acc) list2 [] - in List.combine l1 l2 - and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type = let merge ((s, c): (substitution * constraints)) (lxp_list: (lexp * lexp) list) : return_type =

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -66,5 +66,33 @@ let _ = (add_test "MACROS" "macros base" (fun () -> )

+let _ = (add_test "MACROS" "macros decls" (fun () -> + reset_eval_trace (); + + 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); + + my-decls = Macro_ decls-impl; + + my-decls Nat;" in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let ecode = "a; b;" in + + let ret = eval_expr_str ecode lctx rctx in + + match ret with + | [Vint(a); Vint(b)] -> + if (a = 1 && b = 2) then success () else failure () + + | _ -> failure ()) +) + + (* run all tests *) let _ = run_all ()

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -71,7 +71,7 @@ let colored_string_of_lxp lxp lcol vcol = | Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")" | Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")" | Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl)) - ^ " => (" ^ (vcol (string_of_lxp body)) ^ ") )" + ^ " => (" ^ (vcol (string_of_lxp body)) ^ "))" | Metavar (value, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")" | Call (_) -> (lcol "Call(...)" ) | Case _ -> (lcol "Case") ^ "(...)"

===================================== w_file deleted ===================================== --- a/w_file +++ /dev/null

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