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

Commits: 0da98bd3 by Soilih at 2022-01-24T20:00:19-05:00 -

- - - - - 67425c5d by Soilih at 2022-01-27T10:01:08-05:00 -

- - - - - b773be88 by Soilih at 2022-01-27T10:01:52-05:00 -

- - - - - 8fba06f7 by Soilih at 2022-01-27T10:14:07-05:00 -

- - - - - e276f7e8 by Soilih at 2022-02-01T18:28:14-05:00 -

- - - - - 7558d398 by Soilih at 2022-02-01T22:04:39-05:00 -

- - - - -

1 changed file:

- src/opslexp.ml

Changes:

===================================== src/opslexp.ml ===================================== @@ -1055,7 +1055,8 @@ and get_type ctx e = | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v | 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) @@ -1219,35 +1220,41 @@ 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 pos_of_label lctx label e : int = let call_split e = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let it, aargs = call_split t in + + let it, aargs = call_split (lexp_whnf e lctx) in match lexp'_whnf it lctx, aargs with | 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 = - 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 - | (_, (_, Some vn), _ ) - -> 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 + -> + (match SMap.bindings constructors with + | [(_,l)] -> let rec foo label (l : (arg_kind * vname * ltype) list) (c: int) : int= + match l with + | [] + -> let (loc,st) = label in + Log.log_error ~loc:loc "Label: %s Not Found!" st; 0 + | hd::tl -> match hd with + | (_, (_, Some vn), _ ) + -> 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 0 + | _ -> let (loc,_) = label in + Log.log_fatal ~loc:loc "Wrong arg number to inductive type!" + ) | Inductive _, _ - -> failwith "Proj on an inductive type that's not a tuple!" - | _,_ -> failwith "Proj on a non-inductive type!" + -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on an inductive type that's not a tuple!"; 0 + | _,_ -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on a non-inductive type: %s" (Lexp.lexp_string it) ; 0 +

let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with

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