Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer

Commits: f4662f03 by Soilih BEN SOILIH at 2021-12-02T09:55:19-05:00 +

- - - - - 02545ba2 by Soilih BEN SOILIH at 2021-12-02T14:46:37-05:00 lexp to elexp

- - - - -

4 changed files:

- btl/pervasive.typer - src/elab.ml - src/eval.ml - src/opslexp.ml

Changes:

===================================== btl/pervasive.typer ===================================== @@ -428,7 +428,7 @@ pair = datacons Pair pair;

__.__ = let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") + let constructor = Sexp_node (Sexp_symbol "##__.__") (cons (Sexp_symbol "?") (cons (Sexp_symbol "cons") nil));

===================================== src/elab.ml ===================================== @@ -1732,7 +1732,7 @@ let sform_proj ctx loc sargs ot = | [Node (Symbol (l, "__.__"), [lxp;(Symbol (loca,str))])] -> let (ret,_) = infer lxp ctx in let e = mkProj (l,ret,(loca,str)) in - (e, Inferred e) + (e, Lazy) | _ -> sexp_error loc "Unrecognized proj expression"; sform_dummy_ret ctx loc

===================================== src/eval.ml ===================================== @@ -462,7 +462,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> eval_call (elexp_location f) f trace (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) - (* TODO: Proj *) + (* Proj *) | Proj (l, e, i) -> eval' e ctx

===================================== src/opslexp.ml ===================================== @@ -1219,12 +1219,44 @@ let arity_of_cons ^^ {|because it is not an inductive type: %s|}) name (lexp_string ty)

+let pos_of_label lctx label t : int = + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let it, aargs = call_split t in + match lexp'_whnf it lctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors != 1 + -> let bindings = SMap.bindings constructors in + let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c = + match lst with + | [ls] -> let (_,l) = ls in + let rec foo label (l : (arg_kind * vname * ltype) list) c = + match l with + | [] -> failwith "label not found!" + | hd::tl -> match hd with + | (ak, (loc, Some vn), ltp ) + -> let (_,st) = label in + if (String.equal vn st) then c + else foo label tl (c + 1) + | _ -> foo label tl (c + 1) + in + foo label l c + | _ -> failwith "More than one element!" + in find_the_pos label bindings 0 + | Inductive _, _ + -> failwith "Proj on an inductive type that's not a tuple!" + | _,_ -> failwith "Proj on a non-inductive type!" + let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) - | L.Proj (l,lxp,lbl) -> failwith "cannot convert a lexp to elexp" + | L.Proj (l, exp, label) + -> let t = get_type lctx exp in + E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/291f6c305760ce184dcf3af6112984352...