BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 207f7226 by Pierre Delaunay at 2016-06-06T13:40:55-04:00 added Builtin attribute type

Changes to be committed: * btl/types.typer * src/builtin.ml * new function (new_attribute)

- - - - - 11191bb7 by Pierre Delaunay at 2016-06-09T12:41:18-04:00 Remove dead code

Changes to be committed: * src/debruijn.ml: dead code removal * src/elexp.ml: fix type print * src/env.ml: modified property env * src/eval.ml: monads are lazily evaluated

- - - - - 2fb51647 by Pierre Delaunay at 2016-06-14T16:56:18-04:00 New way of merging and detecting mutually recursive definition in lexp)decls

Changes to be committed: * src/debug_util.ml * src/env.ml * src/lparse.ml * src/REPL.ml: fix typer REPL

- - - - - 641cdaa1 by n3f4s at 2016-06-17T22:39:35+02:00 debug call to unify in _unify_builtin

change first parameter of call to unify in _unify_builtin to avoid calling unify with the same lexp

- - - - - 580f6053 by n3f4s at 2016-06-17T22:41:28+02:00 Merge branch 'master' into unification

- - - - - 64417ead by n3f4s at 2016-06-20T20:53:26+02:00 remove int of substitution, and add global metavar

- - - - - 68852c47 by n3f4s at 2016-06-20T20:55:20+02:00 add doc & corrected unifyer

- - - - - 978833c3 by n3f4s at 2016-06-20T20:56:19+02:00 add _unify_inner

_unify_inner -> generalisation of _unify_inner_arrow

- - - - - 97124603 by n3f4s at 2016-06-20T21:12:28+02:00 add combine and use _unify_inner in _unify_let

- - - - - 39aded24 by n3f4s at 2016-06-20T22:17:34+02:00 correct unifyer (Let & Metavar)

- - - - - 0e633789 by n3f4s at 2016-06-20T22:59:05+02:00 add unification for Call, Call

- - - - - a93fd019 by n3f4s at 2016-06-20T23:57:24+02:00 replace Metavar(_,_,_) by Metavar(int * vdef)

- - - - - 61129132 by n3f4s at 2016-06-20T23:58:04+02:00 add case Var, Imm in _unify_var

- - - - -

14 changed files:

- + - - GNUmakefile - btl/types.typer - samples/nat.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/unification.ml

Changes:

===================================== - ===================================== --- /dev/null +++ b/-

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -9,17 +9,14 @@ OBFLAGS = -build-dir _build

all: typer debug tests-build

-ifeq ($(OS), Windows_NT) +# ifeq ($(OS), Windows_NT) # Windows need '-r' and building to native can be problematic (linking error) # So we build to byte instead -OBFLAGS = $(OBFLAGS) -r -endif +# OBFLAGS = $(OBFLAGS) -r +# endif

COMPILE_MODE = byte

- - - # debug file eval debug: # ============================

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -114,7 +114,6 @@ sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp -> (List Sexp -> Sexp) -> Sexp);

- % ----------------------------------------------------- % Monads % ----------------------------------------------------- @@ -139,5 +138,20 @@ open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String);

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

===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -1,3 +1,4 @@ +Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat);

zero = inductive-cons Nat zero;

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -122,11 +122,11 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = _pxp_parse sxps [] []

-let ierase_type (lexps: (ldecl list * lexpr list)) = +let ierase_type (lexps: (ldecl list list * lexpr list)) = let (ldecls, lexprs) = lexps in - (EL.clean_decls ldecls), (List.map EL.erase_type lexprs) + (EL.clean_toplevel ldecls), (List.map EL.erase_type lexprs)

-let ilexp_parse pexps lctx: ((ldecl list * lexpr list) * lexp_context) = +let ilexp_parse pexps lctx: ((ldecl list 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 @@ -134,7 +134,7 @@ let ilexp_parse pexps lctx: ((ldecl list * lexpr list) * lexp_context) =

let ieval lexps rctx = let (ldecls, lexprs) = lexps in - let rctx = eval_decls ldecls rctx in + let rctx = eval_decls_toplevel ldecls rctx in let vals = eval_all lexprs rctx false in vals, rctx

@@ -158,8 +158,8 @@ let _raw_eval f str lctx rctx = let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in let lxps, lctx = lexp_p_decls pxps lctx in - let elxps = EL.clean_decls lxps in - let rctx = eval_decls elxps rctx in + let elxps = EL.clean_toplevel lxps in + let rctx = eval_decls_toplevel elxps rctx in (* This is for consistency with ieval *) [], lctx, rctx

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

+let builtin_warning loc msg = + msg_warning "BUILT-IN" loc msg + type predef_table = (lexp option ref) SMap.t

let predef_name = [ @@ -264,7 +267,9 @@ let write_impl loc args_val ctx = 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

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -55,7 +55,7 @@ module StringMap = Map.Make (struct type t = string let compare = String.compare end)

(* (* rev_dbi * Var name *) => (name * lexp) *) -type property_elem = lexp StringMap.t +type property_elem = lexp PropertyMap.t type property_env = property_elem PropertyMap.t

(* easier to debug with type annotations *) @@ -203,50 +203,3 @@ let replace_by ctx name by = let nenv = List.fold_left (fun ctx elem -> cons elem ctx) nenv decls in (a, nenv, b)

-(* shift an entire expression by n *) -let rec db_shift expr n = - let db_shift lxp = db_shift lxp n in - match expr with - (* Nothing to shift *) - | Imm _ -> expr - | SortLevel _ -> expr - | Sort _ -> expr - | Builtin _ -> expr - - | Var (s, idx) -> Var(s, idx + n) - | Susp(lxp, s) -> Susp(db_shift lxp, s) - | Cons((s, idx), t) -> Cons((s, idx + n), t) - - | Let(l, decls, lxp) -> - let decls = List.map (fun (var, lxp, ltp) -> - var, db_shift lxp, db_shift ltp) decls in - Let(l, decls, db_shift lxp) - - | Arrow(kind, var, ltp, l, lxp) -> - Arrow(kind, var, db_shift ltp, l, db_shift lxp) - - | Lambda(kind, var, ltp, lxp) -> - Lambda(kind, var, db_shift ltp, db_shift lxp) - - | Call(lxp, args) -> - let args = List.map (fun (kind, lxp) -> (kind, db_shift lxp)) args in - Call(db_shift lxp, args) - - | Inductive(l, nm, fargs, ctors) -> - let fargs = List.map (fun (kind, var, ltp) -> (kind, var, db_shift ltp)) - fargs in - let ctors = SMap.map (fun args -> - List.map (fun (kind, var, ltp) -> (kind, var, db_shift ltp)) args) - ctors in - Inductive(l, nm, fargs, ctors) - - | Case(l, tlxp, tltp, retltp, branch, dflt) -> - let dflt = match dflt with - | Some lxp -> Some (db_shift lxp) - | None -> None in - - let branch = SMap.map (fun (l, args, lxp) -> - (l, args, db_shift lxp)) branch in - Case(l, db_shift tlxp, db_shift tltp, db_shift retltp, branch, dflt) - -

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -272,18 +272,55 @@ let main () = debug_pexp_decls pexps; print_string "\n"));

(* get lexp *) - let ctx = default_lctx in + let octx = default_lctx in

- print_string yellow; - let lexps, nctx = - try lexp_p_decls pexps ctx - with e -> ( - print_string reset; - print_lexp_ctx (!_global_lexp_ctx); - print_lexp_trace (); - raise e - ) in - print_string reset; + (* Debug declarations merging *) + + (** ) + let merged = lexp_detect_recursive pexps in + + 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; + + let _ = match ptp with + | Some pxp -> pexp_print pxp; + | None -> print_string " " in + + print_string "\n"; + lalign_print_string s 20; + + 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; + + ) merged in ( **) + + (* debug lexp parsing once merged *) + let lexps, nctx = _lexp_decls pexps octx 0 in + + (* + 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"; + + ) decls; *) + + (* use the new way of parsing expr *) + let ctx = nctx in let flexps = List.flatten lexps in

(* convert a lctx context into a typecheck context *)

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -205,6 +205,6 @@ and elexp_str lxp = | Inductive(_, (_, s)) -> "inductive_ " ^ s

- | _ -> "Why do you still have those ? " + | Type -> "Type "

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -61,6 +61,7 @@ type value_type = | Vdummy | Vin of in_channel | Vout of out_channel + | Vbind of elexp list

let rec value_print (vtp: value_type) = match vtp with @@ -80,6 +81,11 @@ 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" (* | _ -> print_string "debug print" *)

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

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

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -107,13 +107,13 @@ and eval_var ctx lxp v = let ((loc, name), idx) = v in try get_rte_variable (Some name) (idx) ctx with e -> - eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") + eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")

-and eval_call ctx i lname args = +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)) args in + _eval e ctx (i + 1)) eargs in let f = _eval lname ctx (i + 1) in

let rec eval_call f args ctx = @@ -128,6 +128,10 @@ and eval_call ctx i lname args = let ret = _eval lxp nctx (i + 1) in eval_call ret tl nctx

+ (* bind is lazily evaluated *) + | Vbuiltin ("bind"), _ -> + Vbind eargs + | Vbuiltin (str), args -> (* lookup the built-in implementation and call it *) (get_builtin_impl str loc) loc args ctx @@ -229,6 +233,7 @@ and typer_builtins_impl = [ ("bind" , bind_impl); ("read" , read_impl); ("write" , write_impl); + ("new-attribute" , new_attribute)

] and bind_impl loc args_val ctx = @@ -360,6 +365,7 @@ let from_lctx (ctx: lexp_context) rm: runtime_env = with e -> elexp_print lxp; print_string "\n"; raise e)

+ (* Happen once *) | None -> eval_warning dloc ("Unable to eval expr: " ^ (maybe name)); Vdummy in

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -74,7 +74,7 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * lexp option (* Default. *) - | Metavar of int * string * U.location (*idx * name * location*) + | Metavar of int * vdef (*idx * (name * location)*) (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar =

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -70,6 +70,12 @@ let _parsing_internals = ref false let _shift_glob = ref 0 let btl_folder = ref "./btl/"

+(* merged declaration, allow us to process declaration in multiple pass *) +(* first detect recursive decls then lexp decls*) +type mdecl = + | Ldecl of symbol * pexp option * pexp option + | Lmcall of symbol * sexp list + (* 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 *)

@@ -165,7 +171,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Plet(loc, decls, body) -> let decls, nctx = _lexp_decls decls ctx i in let bdy, ltp = lexp_infer body nctx in - (lexp_let_decls decls bdy nctx i), ltp + (lexp_let_decls decls bdy nctx i), ltp

(* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> @@ -271,6 +277,13 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | _ -> pexp_print p; print_string "\n"; lexp_fatal tloc "Unhandled Pexp"

+ +and lexp_let_decls decls (body: lexp) ctx i = + (* build the weird looking let *) + let decls = List.rev decls in + List.fold_left (fun lxp decls -> + Let(dloc, decls, lxp)) body decls + and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = _lexp_p_check p t ctx 1

@@ -701,12 +714,146 @@ and lexp_decls_macro (loc, mname) sargs ctx: pdecl list = (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0

-and lexp_let_decls decls (body: lexp) ctx i = - (* build the weird looking let *) - let decls = List.rev decls in - List.fold_left (fun lxp decls -> - Let(dloc, decls, lxp)) body decls +and lexp_detect_recursive pdecls = + (* Pack mutually recursive declarations *) + (* mutually recursive def must use forward declarations *) + + let decls = ref [] in + let pending = ref [] in + let merged = ref [] in + + List.iter (fun expr -> + match expr with + | Pexpr((l, s), pxp) ->( + let was_forward = (List.exists + (fun (Ldecl((_, p), _, _)) -> p = s) !pending) in + + let is_empty = (List.length !pending) = 0 in + let is_one = (List.length !pending) = 1 in + + (* This is a standard declaration: not forwarded *) + if (was_forward = false) && is_empty then( + decls := [Ldecl((l, s), Some pxp, None)]::!decls; + ) + (* This is an annotated expression + * or the last element of a mutually rec definition *) + else if (was_forward && is_one) then ( + + (* we know that names match already *) + let ptp = (match (!pending) with + | Ldecl(_, _, ptp)::[] -> ptp + (* we already checked that len(pending) == 1*) + | Ldecl(_, _, ptp)::_ -> lexp_fatal l "Unreachable" + | [] -> lexp_fatal l "Unreachable" + | Lmcall _ :: _ -> lexp_fatal l "Unreachable") in + + (* add declaration to merged decl *) + merged := Ldecl((l, s), Some pxp, ptp)::(!merged); + + (* append decls *) + decls := (List.rev !merged)::!decls; + + (* Reset State *) + pending := []; + merged := []; + ) + (* This is a mutually recursive definition *) + else ( + (* get pending element and remove it from the list *) + let elem, lst = List.partition + (fun (Ldecl((_, n), _, _)) -> n = s) !pending in + + let _ = (match elem with + (* nothing to merge *) + | [] -> + merged := Ldecl((l, s), Some pxp, None)::!merged; + + (* append new element to merged list *) + | Ldecl((l, s), _, Some ptp)::[] -> + merged := Ldecl((l, s), Some pxp, (Some ptp))::!merged; + + (* s should be unique *) + | _ -> lexp_error l "declaration must be unique") in + + (* element is not pending anymore *) + pending := lst; + )) + + | Ptype((l, s), ptp) -> + pending := Ldecl((l, s), None, Some ptp)::!pending + + (* macro will be handled later *) + | Pmcall(a, sargs) -> + decls := [Lmcall(a, sargs)]::!decls;

+ ) pdecls; + + (List.rev !decls) + + +and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = + (* detect mutually recursive def and merge definition *) + let decls = lexp_detect_recursive decls in + 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 + + (List.rev !all), ctx + +and _lexp_rec_decl decls ctx i = + (* parse a groupe of mutually recursive definition + * i.e let decl parsing *) + + (* to compute recursive offset *) + let n = (List.length decls) + 1 in + let lst = ref [] in + + (* add all elements to the environment *) + let tctx = List.fold_left (fun vctx expr -> + match expr with + | Ldecl((l, s), _, None) -> + 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 + + | Lmcall _ -> + lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in + + let i = ref 0 in + let ctx = List.fold_left (fun vctx expr -> + i := !i + 1; + match expr with + (* lexp infer *) + | Ldecl ((l, s), Some pxp, None) -> + let lxp, ltp = lexp_p_infer pxp vctx 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) + + (* 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 + lst := ((l, s), lxp, ltp)::!lst; + replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + + (* macros *) + | Lmcall (a, sargs) -> + lexp_fatal dloc "use lexp_decl_macro to parse macro decls" + + (* unused arg *) + | Ldecl ((l, s), None, _) -> + lexp_error l ("Variable "" ^ s ^ "" is unused!"); + vctx) tctx decls in + + (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 *) @@ -794,6 +941,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) | 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 @@ -818,6 +966,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) merge_list names) (List.rev !names) in

decls, ctx +*)

and lexp_decls_toplevel decls ctx = _lexp_decls decls ctx 1 @@ -1042,7 +1191,9 @@ let default_rctx = _parsing_internals := false;

let rctx = make_runtime_ctx in - eval_decls_toplevel (EL.clean_toplevel d) rctx + let rctx = eval_decls_toplevel (EL.clean_toplevel d) rctx in + _global_eval_trace := []; + rctx (* try (from_lctx (default_lctx)) with e ->( @@ -1073,7 +1224,6 @@ let lexp_decl_str str lctx = _lexp_decl_str str default_stt default_grammar (Some ";") lctx

- (* Eval String * --------------------------------------------------------- *) (* Because we cant include lparse in eval.ml *)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -4,7 +4,7 @@ open Sexp

module VMap = Map.Make (struct type t = int let compare = compare end)

-type substitution = lexp VMap.t * int +type substitution = lexp VMap.t type constraints = (lexp * lexp) list (* IMPROVEMENT For error handling : can carry location and name of type error *) type 'a expected = @@ -12,34 +12,34 @@ type 'a expected = | Error of Util.location * string (*location * type name*) | None

+let global_last_metavar = ref 0 +let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar + +let expected_to_option (e: 'a expected) : ('a option) = + match e with + | Some elt -> Some elt + | Error _ -> None + | None -> None + (* For convenience *) type return_type = (substitution * constraints) option

- (** Alias for VMap.add*) -let associate (meta: int) (lxp: lexp) ((subst, max_): substitution) +let associate (meta: int) (lxp: lexp) (subst: substitution) : substitution = - (VMap.add meta lxp subst, (max max_ meta )) - -(** Generate the next metavar by taking the highest value and - * adding it one - *) -let add_substitution (lxp: lexp) ((subst, max_): substitution) : substitution = - associate (max_ + 1) lxp (subst, max_) + (VMap.add meta lxp subst)

(** If key is in map returns the value associated * else returns None - *) -let find_or_none (value: lexp) ((map, max_): substitution) : lexp option = +*) +let find_or_none (value: lexp) (map: substitution) : lexp option = match value with - | Metavar (idx, _, _) -> (if max_ < idx (* 0 < keys <= max_ *) - then None - else (if VMap.mem idx map - then Some (VMap.find idx map) - else None)) + | Metavar (idx, _) -> (if VMap.mem idx map + then Some (VMap.find idx map) + else None) | _ -> None

-let empty_subst = (VMap.empty, 0) +let empty_subst = (VMap.empty)

(** * Imm , Imm -> if Imm =/= Imm then ERROR else OK @@ -76,24 +76,30 @@ let empty_subst = (VMap.empty, 0) * Call , Let -> ERROR * Call , Arrow -> ERROR * Call , Call -> CONSTRAINT + * Case , lexp -> ERROR

(*TODO*) * Inductive , lexp -> - * Case , case -> + * Susp , lexp -> * lexp , lexp ->

* lexp is equivalent to _ in ocaml * (Let , lexp) == (lexp , Let) - * UNIFY -> recursive call or dispatching - * OK -> add a substituion to the list of substitution + * UNIFY -> recursive call or dispatching + * OK -> add a substituion to the list of substitution + * CONSTRAINT -> returns a constraint *)

(** 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) - *) +*) + +(*FIXME : check infintie mutual recursion*) 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 | (Imm _, _) -> _unify_imm l r subst | (Cons _, Cons _) -> None | (Builtin _, _) -> _unify_builtin l r subst @@ -103,26 +109,26 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Lambda _, _) -> _unify_lambda l r subst | (Metavar _, _) -> _unify_metavar l r subst | (Call _, _) -> _unify_call l r subst + | (Case _, _) -> None | (_, _) -> None

and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (call, lxp) with - | (Call _, Imm _) -> Some ((subst, [(call, lxp)])) - | (Call _, Cons _) -> None - | (Call _, Builtin _) -> None - | (Call _, Var _) -> Some ((subst, [(call, lxp)])) - | (Call _, Let _) -> None (*¿?*) - | (Call _, Arrow _) -> None (*¿?*) - | (Call _, Call _) -> Some ((subst, [(call, lxp)])) - | (Call _, _) -> unify lxp call subst - | (_, _) -> None + let combine list1 list2 = + let l1 = List.fold_left (fun acc (_, x) -> x::acc) [] list1 + and l2 = List.fold_left (fun acc (_, x) -> x::acc) [] 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

(* maybe split unify into 2 function : is_unifyable and unify ? * cf _unify_lambda for (Lambda, Lambda) behavior*)

(** Unify a Lambda and a lexp if possible * See above for result - *) +*) and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type = match (lambda, lxp) with | (Lambda (var_kind1, _, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) @@ -131,7 +137,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type else None | (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)])) - | (Lambda _, Arrow _) -> Some ((subst, [(lambda, lxp)])) (* ?? *) + | (Lambda _, Arrow _) -> None | (Lambda _, Call _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, _) -> unify lxp lambda subst | (_, _) -> None @@ -139,17 +145,15 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type (** Unify a Metavar and a lexp if possible * See above for result * Metavar is the 'end' of the rules i.e. : it can call unify with his argument (re-ordered) - *) +*) and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type = match (meta, lxp) with - | (Metavar (val1, _, _), Metavar (val2, _, _)) -> - if val1 = val2 - then Some ((add_substitution meta subst, [])) - else None - | (Metavar (v, _, _), _) -> ( + | (Metavar (val1, _), Metavar (val2, _)) when val1 = val2 -> + Some ((subst, [])) + | (Metavar (v, _), _) -> ( match find_or_none meta subst with | None -> Some ((associate v lxp subst, [])) - | Some (lxp_) -> unify lxp_ lxp subst) (*Not sure if it's the expected behavior*) + | Some (lxp_) -> unify lxp_ lxp subst) | (_, _) -> None

(** Unify a Arrow and a lexp if possible @@ -157,16 +161,13 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type 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 (match _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst with - | Some _ -> Some ((add_substitution arrow subst, [])) - | None -> None) + then _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst else None | (Arrow _, _) -> unify lxp arrow subst | (_, _) -> None @@ -185,27 +186,28 @@ and _unify_inner_arrow (lt1: lexp) (lxp1: lexp) * (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 ((add_substitution var subst, [])) + -> if idx1 = idx2 then Some ((subst, [])) else None - | (Var _, _) -> unify r var subst (*returns to unify*) - | (_, _) -> 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 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 ((add_substitution l subst, [])) + -> if v1 = v2 then Some ((subst, [])) else None | (Imm (Integer (_, v1)), Imm (Integer (_, v2))) - -> if v1 = v2 then Some ((add_substitution l subst, [])) + -> if v1 = v2 then Some ((subst, [])) else None | (Imm (Float (_, v1)), Imm (Float (_, v2))) - -> if v1 = v2 then Some ((add_substitution l subst, [])) + -> if v1 = v2 then Some ((subst, [])) else None | (Imm _, Imm _) -> None | (Imm _, _) -> unify r l subst @@ -218,20 +220,42 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type = match (bltin, lxp) with | (Builtin ((_, name1), _), Builtin ((_, name2),_)) - -> if name1 = name2 then Some ((add_substitution lxp subst, [])) + -> if name1 = name2 then Some ((subst, [])) else None (* assuming that builtin have unique name *) - | (Builtin (_, lxp_), _) -> (match unify lxp lxp subst with - | None -> None - | Some (_, c)-> Some ((add_substitution bltin subst, c))) + | (Builtin (_, lxp_bltin), _) -> unify lxp_bltin lxp subst | (_, _) -> None

(** Unify a Let (let_) and a lexp (lxp), if possible * Unify the left lexp part of the Let (Let (_, _, lxp)) with the lexp - *) +*) and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = - match let_ with (* Discard the middle part of Let : right behavior ? *) - | Let (_, _, lxp_) -> (match unify lxp_ lxp subst with - | None -> None - | Some (_, c) -> Some ((add_substitution let_ subst, c))) - | _ -> None + match (let_, lxp) with + | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> + _unify_inner ((lxp_, lxp2)::(combine m m1)) subst + | (Let _, _) -> Some (subst, [(let_, lxp)]) + | _, _ -> None + +(** 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_left (fun acc (_, t, x) -> t::x::acc) [] list1 + and l2 = List.fold_left (fun acc (_, t, x) -> 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 = + match _unify_inner lxp_list s with + | None -> Some (s, c) + | Some (s_,c_) -> Some (s_, c@c_) + in + match lxp_l with + | (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with + | Some (s, c) -> merge (s, c) tail + | None -> None) + | [] -> None +

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