Ismaila FALL pushed to branch location-sinfo at Stefan / Typer

Commits: 366ff7fc by Fallismaila at 2022-08-31T20:48:52+00:00 Assertion failed line 776

- - - - -

5 changed files:

- src/REPL.ml - src/debruijn.ml - src/elab.ml - src/heuristic.ml - src/log.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -46,9 +46,7 @@ open Lexp open Prelexer open Sexp open Util -(* -open Implgenealgo -*) +

module OL = Opslexp module EL = Elexp @@ -208,8 +206,8 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) =

| "%ctx"::args | "%c"::args -> let _ = match args with - | ["all"] -> dump_un_lexp_ctx (ectx_to_lctx ectx) - | _ -> print_un_lexp_ctx (ectx_to_lctx ectx) in + | ["all"] -> Heuristic.dump_heur_ctx (ectx) + | _ -> Heuristic.print_heur_ctx (ectx) in ectx

===================================== src/debruijn.ml ===================================== @@ -435,87 +435,14 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = print_string (make_sep '=')

-let print_lexp_ctx_un (ctx : lexp_context) (ranges : (int * int) list) = - print_string (make_title " LEXP CONTEXT "); - - make_rheader - [(Some ('l', 10), "NAME"); - (Some ('l', 10), "LEXP_UNPARSE"); - (* (Some ('l', 10), "HEURISTIC_UNPARSE"); *) - (Some ('l', 42), " TYPE")]; - - print_string (make_sep '-'); - - let _ = " | | | " in - - let print i = - try - let _, name, _, ty = - match env_lookup_by_index i ctx with - | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty - | ((_, name), _, ty) -> 0, name, None, ty - in - let name' = maybename name in - let short_name = - if String.length name' > 10 - then - String.sub name' 0 9 ^ "…" - else name' - in - Printf.printf " %-10s || " short_name; - - sexp_print (Heuristic.heuristic_unparse ty); - - Printf.printf " |-->|: "; - - - (* - sexp_print (Heuristic.heuristic_unparse ty ctx); - - Printf.printf " |--> "; - *) - - lexp_print ty; - print_newline (); - print_newline () - with - | Not_found - -> print_endline " | %-7d | Not_found |" - in - - let rec print_range lower i = - let i' = i - 1 in - if i' >= lower - then - (print i'; - print_range lower i') - in - - let rec print_ranges = function - | [] -> () - | (lower, upper) :: ranges' - -> (print_range lower upper; - print_ranges ranges') - in - - print_ranges ranges; - print_string (make_sep '=') - - (* Only print user defined variables *) let print_lexp_ctx (lctx : lexp_context) : unit = print_lexp_ctx_n lctx [(0, M.length lctx - !builtin_size)]

-let print_un_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_un lctx [(0, M.length lctx - !builtin_size)] - (* Dump the whole context *) let dump_lexp_ctx (lctx : lexp_context) : unit = print_lexp_ctx_n lctx [(0, M.length lctx)]

-let dump_un_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_un lctx [(0, M.length lctx)] - let summarize_lctx (lctx : lexp_context) (at : int) : unit = let ranges = if at < 7

===================================== src/elab.ml ===================================== @@ -38,7 +38,6 @@ * -------------------------------------------------------------------------- *)

open Util - open Prelexer open Lexer

@@ -48,20 +47,18 @@ open Lexp

open Env open Debruijn +open Grammar +open Printf + module DB = Debruijn module M = Myers module EV = Eval - -open Grammar module BI = Builtin - module Unif = Unification module Inst = Instargs - module OL = Opslexp module EL = Elexp

-open Printf

(* dummies *) let dloc = dummy_location

===================================== src/heuristic.ml ===================================== @@ -1,6 +1,9 @@ open Lexp open Sexp open Pexp +open Debruijn + +module OL = Opslexp

(* ugly printing (sexp_print (pexp_unparse (heuristic_unparse e))) *) @@ -12,9 +15,11 @@ let rec heuristic_unparse lxp = -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) - | Var ((loc, 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) + if s = "ℓ" then Symbol (sexp_location loc, "") else Symbol (sexp_location loc, maybename name) + *) | Proj (l,lxp,(loc,str)) -> Node (Symbol (sexp_location l, "__.__"), [(heuristic_unparse lxp);(Symbol (loc,str))]) @@ -33,22 +38,26 @@ let rec heuristic_unparse lxp =

| Arrow (loc, arg_kind, (l, oname), ltp1, ltp2) -> let ut1 = heuristic_unparse ltp1 in - if arg_kind = Aerasable then - Node (Symbol (sexp_location loc, "_≡>_"), - [(match oname with + (match arg_kind with + | Aerasable -> Node (Symbol (sexp_location loc, "_≡>_"), + [(match oname with | 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]) + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); Symbol (sexp_location l, "?")])); + heuristic_unparse ltp2]) + | Anormal -> Node (Symbol (sexp_location loc, "_->_"), + [(match oname with + | None -> ut1 + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); + heuristic_unparse ltp2]) + | Aimplicit -> 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])); + heuristic_unparse ltp2]) + )

| Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) @@ -145,7 +154,79 @@ let rec heuristic_unparse lxp = | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [heuristic_unparse sl]) - (* - [let s = heuristic_unparse sl in - if s != l then Inverse_subst.dsinfo else s]) - *) + + +let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = + print_string (Fmt.make_title " LEXP CONTEXT "); + + Fmt.make_rheader + [(Some ('l', 10), "NAME"); + (Some ('l', 10), "LEXP_UNPARSE"); + (Some ('l', 20), "LEXP"); + (Some ('l', 42), " TYPE")]; + + print_string (Fmt.make_sep '-'); + + let _ = " | | " in + + let print i = + try + let _, name, _lexp, ty = + match env_lookup_by_index i (ectx_to_lctx ctx) with + | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty + | ((_, name), _, ty) -> 0, name, None, ty + in + let name' = maybename name in + let short_name = + if String.length name' > 10 + then + String.sub name' 0 9 ^ "…" + else name' + in + Printf.printf " %-10s || " short_name; + + let res = heuristic_unparse ty in + sexp_print res; + + + Printf.printf " |-->|: "; + + let s = fst (Elab.elaborate ctx res None) in + lexp_print s; + (* + Printf.printf " |--> "; + + lexp_print ty; + print_newline (); + *) + print_newline () + with + | Not_found + -> print_endline " | %-7d | Not_found |" + in + + let rec print_range lower i = + let i' = i - 1 in + if i' >= lower + then + (print i'; + print_range lower i') + in + + let rec print_ranges = function + | [] -> () + | (lower, upper) :: ranges' + -> (print_range lower upper; + print_ranges ranges') + in + + print_ranges ranges; + print_string (Fmt.make_sep '=') + +(* Only print user defined variables *) +let print_heur_ctx (lctx : elab_context) : unit = + print_heur_ctx_n lctx [(0, M.length (ectx_to_lctx lctx) - !builtin_size)] + +(* Dump the whole context *) +let dump_heur_ctx (lctx : elab_context) : unit = + print_heur_ctx_n lctx [(0, M.length (ectx_to_lctx lctx))]

===================================== src/log.ml ===================================== @@ -212,7 +212,7 @@ let show_error (message : string) : unit = let handle_error ~(on_error : unit -> 'a) (action : unit -> 'a) : 'a = try action () with | Stop_compilation message - -> show_error message; + -> show_error ("internal error: " ^ message); on_error () | User_error message -> show_error ("fatal user error: " ^ message);

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/366ff7fcae796b0cffcb60508c7071f8b0...