Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: d3544eba by Fallismaila at 2022-08-22T22:49:34+00:00 ignore implicit variable - - - - - 37c7447d by Fallismaila at 2022-08-22T22:49:53+00:00 ignore implicit variable - - - - - 1 changed file: - src/heuristic.ml Changes: ===================================== src/heuristic.ml ===================================== @@ -13,7 +13,8 @@ let rec heuristic_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) | Var ((loc, name), _) - -> Symbol (sexp_location loc, maybename name) + -> let s = maybename name in + if s = "ℓ" then Inverse_subst.dsinfo else Symbol (sexp_location loc, maybename name) | Proj (l,lxp,(loc,str)) -> Node (Symbol (sexp_location l, "__.__"), [(heuristic_unparse lxp);(Symbol (loc,str))]) @@ -32,15 +33,22 @@ let rec heuristic_unparse lxp = | Arrow (loc, arg_kind, (l, oname), ltp1, ltp2) -> let ut1 = heuristic_unparse ltp1 in - Node (Symbol (sexp_location loc, match arg_kind with - | Anormal -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), + if arg_kind = Aerasable then + Node (Symbol (sexp_location loc, "_≡>_"), [(match oname with - | None -> ut1 (* Inverse_subst.dsinfo *) - | Some v -> Node (Symbol (sexp_location l, "_:_"), - [Symbol (sexp_location l,v); ut1])); + | None -> ut1 + | Some _v -> Inverse_subst.dsinfo); heuristic_unparse ltp2]) + else + Node (Symbol (sexp_location loc, match arg_kind with + | Anormal -> "_->_" + | Aimplicit -> "_=>_" + | _ -> "_≡>_"), + [(match oname with + | None -> ut1 (* Inverse_subst.dsinfo *) + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); + heuristic_unparse ltp2]) | Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) @@ -117,8 +125,8 @@ let rec heuristic_unparse lxp = Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), [pexp_u_pat pat; branch])) pbranch) - (* FIXME: The cases below are all broken! *) + (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]") @@ -137,143 +145,7 @@ let rec heuristic_unparse lxp = | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [heuristic_unparse sl]) - - -(* - -(* ugly printing (sexp_print (pexp_unparse (heuristic_unparse e))) *) -let rec heuristic_unparse lxp ctx = - match lexp_lexp' lxp with - | Susp _ - -> heuristic_unparse (nosusp lxp) ctx - | Imm (sexp) - -> sexp - | Builtin ((l,name), _) - -> Symbol (l, "##" ^ name) - | Var ((loc, name), _) - -> Symbol (sexp_location loc, maybename name) - | Proj (l,lxp,(loc,str)) - -> Node (Symbol (sexp_location l, "__.__"), - [(heuristic_unparse lxp ctx);(Symbol (loc,str))]) - | Cons (t, (l, name)) - -> Node (sdatacons, - [heuristic_unparse t ctx; Symbol (l, name)]) - | Lambda (kind, vdef, ltp, body) - -> let l = lexp_location lxp in - let st = heuristic_unparse ltp ctx in - Node (Symbol (l, match kind with - | Anormal -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); - heuristic_unparse body ctx]) - - | Arrow (loc, arg_kind, (l,oname), ltp1, ltp2) - -> let ut1 = heuristic_unparse ltp1 ctx in - Node (Symbol (sexp_location loc, match arg_kind with - | Anormal -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match oname with - | None -> ut1 (* Inverse_subst.dsinfo *) - | Some v -> Node (Symbol (sexp_location l, "_:_"), - [Symbol (sexp_location l,v); ut1])); - heuristic_unparse ltp2 ctx]) - - | Let (loc, ldecls, body) - -> (* (vdef * lexp * ltype) list *) - let sdecls = List.fold_left - (fun acc (vdef, lxp, ltp) - -> Node (Symbol (lexp_location lxp, "_=_"), - [Symbol (sname vdef); heuristic_unparse ltp ctx]) - :: Node (Symbol (lexp_location lxp, "_=_"), - [Symbol (sname vdef); heuristic_unparse lxp ctx]) - :: acc) - [] ldecls in - Node (Symbol (sexp_location loc, "let_in_"), - [Node (Symbol (sexp_location loc, "_;_"), sdecls); - heuristic_unparse body ctx]) - - | Call(_, lxp, largs) - -> (* (arg_kind * lexp) list *) - let sargs = List.map (fun (_kind, elem) -> heuristic_unparse elem ctx) largs in - Node (heuristic_unparse lxp ctx, sargs) - - | Inductive(loc, label, lfargs, ctors) - -> (* (arg_kind * vdef * ltype) list *) - (* (arg_kind * pvar * pexp option) list *) - let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, sname vdef, Some (heuristic_unparse ltp ctx))) lfargs in - - Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map - (fun (name, types) - -> Node (Symbol (sexp_location loc, name), - List.map - (fun arg -> - match arg with - | (Anormal, (_,None), t) -> heuristic_unparse t ctx - | (ak, s, t) - -> let (l,_) as id = sname s in - Node (Symbol (l, match ak with - | Anormal -> "_:_" - | Aimplicit -> "_::_" - | Aerasable -> "_:::_"), - [Symbol id; heuristic_unparse t ctx])) - types)) - (SMap.bindings ctors)) - - | Case (loc, target, bltp, branches, default) - -> let bt = heuristic_unparse bltp ctx in - let pbranch = List.map (fun (str, (loc, args, bch)) -> - match args with - | [] -> Ppatsym (loc, Some str), heuristic_unparse bch ctx - | _ -> - let pat_args - = List.map (fun (_kind, ((l,oname) as name)) - -> match oname with - | Some vdef -> (Some (sexp_location l,vdef), name) - | None -> (None, name)) - args - (* FIXME: Rather than a Pcons we'd like to refer to an existing - * binding with that value! *) - in (Ppatcons (Node (sdatacons, - [bt; Symbol (sexp_location loc, str)]), - pat_args), - heuristic_unparse bch ctx) - ) (SMap.bindings branches) in - - let pbranch = match default with - | Some (v,dft) -> (Ppatsym v, - heuristic_unparse dft ctx)::pbranch - | None -> pbranch - in let e = heuristic_unparse target ctx in - Node (Symbol (sexp_location loc, "case_"), - e :: List.map - (fun (pat, branch) -> - Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), - [pexp_u_pat pat; branch])) - pbranch) - (* FIXME: The cases below are all broken! *) - - | Metavar (idx, subst, (loc, name)) - -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]") - | SortLevel (SLz) - -> Symbol (U.dummy_location, "##TypeLevel.z") - | SortLevel (SLsucc l) - -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), - [heuristic_unparse l ctx]) - | SortLevel (SLlub (l1, l2)) - -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), - [heuristic_unparse l1 ctx; heuristic_unparse l2 ctx]) - | Sort (l, StypeOmega) - -> Symbol (sexp_location l, "##Type_ω") - | Sort (l, StypeLevel) - -> Symbol (sexp_location l, "##TypeLevel.Sort") - | Sort (_l, Stype sl) - -> Node (Symbol (lexp_location sl, "##Type_"), - [heuristic_unparse sl ctx]) - -*) \ No newline at end of file + (* + [let s = heuristic_unparse sl in + if s != l then Inverse_subst.dsinfo else s]) + *) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/54debf9a7eec91f8cfdbd61557664faae... -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/54debf9a7eec91f8cfdbd61557664faae... You're receiving this email because of your account on gitlab.com.