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

Commits: 291f6c30 by Soilih BEN SOILIH at 2021-12-01T01:42:29-05:00 sform_proj

- - - - -

2 changed files:

- src/elab.ml - src/eval.ml

Changes:

===================================== src/elab.ml ===================================== @@ -1727,6 +1727,15 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

+let sform_proj ctx loc sargs ot = + match sargs with + | [Node (Symbol (l, "__.__"), [lxp;(Symbol (loca,str))])] + -> let (ret,_) = infer lxp ctx in + let e = mkProj (l,ret,(loca,str)) in + (e, Inferred e) + | _ -> sexp_error loc "Unrecognized proj expression"; + sform_dummy_ret ctx loc + let rec infer_level ctx se : lexp = match se with | Symbol (_, "z") -> mkSortLevel SLz @@ -1802,7 +1811,7 @@ let sform_load usr_elctx loc sargs _ot = let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx in elctx in - + (* read file as elab_context *) let ld_elctx = match sargs with | [String (_,file_name)] -> if !in_pervasive then @@ -1847,6 +1856,7 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("__.__", sform_proj); ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable);

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

(* Case *) | Case (loc, target, pat, dflt)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/291f6c305760ce184dcf3af6112984352a...