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/291f6c305760ce184dcf3af6112984352…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/291f6c305760ce184dcf3af6112984352…
You're receiving this email because of your account on gitlab.com.
