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

Commits: 5b74723c by “falismai@iro.umontreal.ca” at 2022-05-31T22:18:07+00:00 Suppression du module Int

- - - - -

5 changed files:

- − Int - src/debug.ml - src/elab.ml - src/eval.ml - src/pexp.ml

Changes:

===================================== Int deleted ===================================== @@ -1,28 +0,0 @@ -btl/builtins.typer:Integer->Int = Built-in "Integer->Int" : Integer -> Int; -btl/builtins.typer:Integer->String = Built-in "Integer->String" : Integer -> String; -btl/pervasive.typer: | nil => (Integer->Int 0) -btl/pervasive.typer: (Int_+ (Integer->Int 1) (List_length tl)); -btl/pervasive.typer: => case Int_<= n (Integer->Int 0) -btl/pervasive.typer: | false => List_nth (Int_- n (Integer->Int 1)) xs d; -btl/pervasive.typer: | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); -btl/pervasive.typer:in helper f (Integer->Int 0) xs; -btl/pervasive.typer:List_empty xs = Int_eq (List_length xs) (Integer->Int 0); -btl/pervasive.typer: (cons (List_nth (Integer->Int 1) ss Sexp_error) nil))); -btl/pervasive.typer: head = List_nth (Integer->Int 0) head-pair Sexp_error; -btl/pervasive.typer: type-type = List_nth (Integer->Int 1) head-pair Sexp_error; -btl/pervasive.typer: | vnil (p ::: Eq n (Integer->Int 0)) -btl/pervasive.typer: | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1))); -btl/pervasive.typer: let e1 = List_nth (Integer->Int 0) args Sexp_error; -btl/pervasive.typer: e2 = List_nth (Integer->Int 1) args Sexp_error; -btl/pervasive.typer: e3 = List_nth (Integer->Int 2) args Sexp_error; -btl/pervasive.typer:in case (Int_eq r (Integer->Int -1)) -btl/poly-lits.typer:IntFromInteger = mkFromInteger Integer->Int; -btl/tuple.typer: elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); -samples/nats.typer:Integer->Nat : Integer -> Nat; -samples/nats.typer:Integer->Nat i = -samples/nats.typer: S (Integer->Nat (Integer_- i 1)) -samples/nats.typer:NatFromInteger = mkFromInteger Integer->Nat; -src/eval.ml: let name = "Integer->Int" in -src/eval.ml: | _ -> error loc "Integer->String expects one Integer argument" -src/eval.ml: ("Integer->String", integer_to_string, 1); -tests/eval_test.ml:intFromIntegerCoercion = mkCoercible (Integer->Int);

===================================== src/debug.ml ===================================== @@ -121,7 +121,8 @@ let debug_lexp_decls decls = List.iter (fun e -> let ((loc, _name), lxp, _ltp) = e in

- printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc)); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string + (sexp_location loc));

let str = lexp_str_decls (!debug_ppctx) [e] in

===================================== src/elab.ml ===================================== @@ -1114,7 +1114,7 @@ and lexp_parse_inductive ctors ctx = acc impossible in let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t _l e - -> mkArrow (lexp_sinfo altacc, Aerasable, vname, t, e)) + -> mkArrow (lexp_sinfo e, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1334,7 +1334,8 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (Symbol(loc, ""), Some vname) in + -> let ltp = infer_and_generalize_type nctx stp (stp, + Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1355,7 +1356,7 @@ and lexp_decls_1 pending_defs then (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (Symbol(loc, ""), Some vname) ForwardRef ltp) + else recur [] (ectx_extend nctx (stp, Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ @@ -1367,13 +1368,13 @@ and lexp_decls_1 | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((_l, vname)); sexp] + | [Symbol ((l, vname)); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (sexp, Some vname) in + let var = (epsilon (l), Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks,

===================================== src/eval.ml ===================================== @@ -717,7 +717,7 @@ and print_eval_trace trace = print_trace " EVAL TRACE " trace a

let io_bind loc depth args_val = - let trace_dum = (Var ((Symbol(loc, ""), None), -1)) in + let trace_dum = (Var ((epsilon loc, None), -1)) in

match args_val with | [Vcommand cmd; callback]

===================================== src/pexp.ml ===================================== @@ -20,9 +20,6 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-(* -*open Util -*) open Sexp (* Symbol *)

let pexp_error loc = Log.log_error ~section:"PEXP" ~loc

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5b74723c05d49bbca4f84c67b6eaf384ad...