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

Commits: 29526c1c by Soilih at 2022-01-17T16:15:35-07:00 -

- - - - - ec5e23bf by Soilih at 2022-01-19T23:30:01-07:00 fix unused var issues

- - - - -

5 changed files:

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

Changes:

===================================== src/elab.ml ===================================== @@ -1727,7 +1727,7 @@ 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 = +let sform_proj ctx loc sargs _ = match sargs with | [lxp;(Symbol (loca,str))] -> let (ret,_) = infer lxp ctx in

===================================== src/elexp.ml ===================================== @@ -140,7 +140,7 @@ 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,i) + | Proj (_,lxp,i) -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")"

===================================== src/eval.ml ===================================== @@ -467,7 +467,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> let vt = eval' e ctx in ( match vt with - | Vcons (symbol, vtl) -> List.nth vtl i + | Vcons (_, vtl) -> List.nth vtl i | _ -> error loc "Connot find a value in position %d \n" i

===================================== src/lexp.ml ===================================== @@ -985,7 +985,7 @@ and lexp_str ctx (exp : lexp) : string =

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

- | Proj (l,lxp,(loc,str)) + | Proj (_,lxp,(_,str)) -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )"

| Metavar (idx, subst, (_loc, name))

===================================== src/opslexp.ml ===================================== @@ -748,7 +748,7 @@ and check'' erased ctx e = let tct = arg_loop ctx erased args in tct | Proj (l, e, (loc, label)) - ->( let call_split e = + -> ( let call_split e = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in @@ -774,10 +774,10 @@ and check'' erased ctx e = -> if not (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 + | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with - |(l, Some n) -> mkProj (loc, e, lbl) + |(_, Some _) -> mkProj (loc, e, lbl) |_ -> Lexp.impossible in let fieldref = fvdef vdef e l (loc, label) in getfieldtype (S.cons fieldref s) fieldtypes in @@ -965,7 +965,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) - | Proj (l,lxp,lbl) -> fv lxp + | Proj (_,lxp,_) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1082,10 +1082,10 @@ and get_type ctx e = -> if not (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 + | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with - |(l, Some n) -> mkProj (loc, e, lbl) + |(_, Some _) -> mkProj (loc, e, lbl) |_ -> Lexp.impossible in let fieldref = fvdef vdef e l (loc, label) in getfieldtype (S.cons fieldref s) fieldtypes in @@ -1226,7 +1226,7 @@ let pos_of_label lctx label t : int = | _ -> (e,[]) in let it, aargs = call_split t in match lexp'_whnf it lctx, aargs with - | Inductive (_, _, fargs, constructors), aargs + | Inductive (_, _, _, constructors), _ 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 = @@ -1236,7 +1236,7 @@ let pos_of_label lctx label t : int = match l with | [] -> failwith "label not found!" | hd::tl -> match hd with - | (ak, (loc, Some vn), ltp ) + | (_, (_, Some vn), _ ) -> let (_,st) = label in if (String.equal vn st) then c else foo label tl (c + 1)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6a7a6f997f9cbaf7a28134706de2bbd48...