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

Commits: 9d4d090d by Soilih BEN SOILIH at 2021-11-21T21:35:01-05:00 -

- - - - - 91edf98c by Soilih BEN SOILIH at 2021-11-23T23:58:29-05:00 Proj in check

- - - - - 4f5c69fc by Soilih BEN SOILIH at 2021-11-24T18:54:10-05:00 -

- - - - - f609101d by Soilih BEN SOILIH at 2021-11-25T09:37:14-05:00 -

- - - - - 1f077559 by Soilih BEN SOILIH at 2021-11-25T13:49:08-05:00 get_type, check''

- - - - -

3 changed files:

- src/elexp.ml - src/eval.ml - src/opslexp.ml

Changes:

===================================== src/elexp.ml ===================================== @@ -52,7 +52,7 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref

- | Proj of U.location * elexp * symbol + | Proj of U.location * elexp * int

(* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp @@ -140,8 +140,8 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" - | Proj (l,lxp,(loc,str)) - -> "( _._ " ^ elexp_string lxp ^ " " ^ str ^ " )" + | Proj (l,lxp,i) + -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")"

| Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)

===================================== src/eval.ml ===================================== @@ -462,6 +462,9 @@ 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 (l, e, i) + -> failwith ""

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

===================================== src/opslexp.ml ===================================== @@ -747,6 +747,45 @@ and check'' erased ctx e = args) in let tct = arg_loop ctx erased args in tct + | Proj (l, e, (loc, label)) + ->( let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (check erased ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors != 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -761,7 +800,7 @@ and check'' erased ctx e = | Sort (_, Stype l) -> l | _ -> Log.log_error ~loc:(lexp_location ekind) "Target lexp's kind is not a sort"; DB.level0 in - let it, aargs = call_split etype in + let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = @@ -1015,7 +1054,45 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v - | Proj (l,lxp,lbl) -> mkProj (l,lxp,lbl) + | Proj (l, e, (loc, label)) + -> ( (*check'' DB.set_empty ctx e*) + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (get_type ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors != 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let fieldtypes = SMap.find label constructors in + let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1147,7 +1224,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) - | L.Proj (l,lxp,lbl) -> E.Proj (l, erase_type lctx lxp,lbl) + | L.Proj (l,lxp,lbl) -> failwith "cannot convert a lexp to elexp" | 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/13cf6a0ec06b3e4b6ec0a99ebb81bd82c...