Typer Février 2021

typer@iro.umontreal.ca

1 participants
4 discussions

[Git][monnier/typer][master] * src/elab.ml (lexp_check_decls): Fix broken odd/even example.
by Stefan 09 Fév '21

09 Fév '21

Stefan pushed to branch master at Stefan / Typer Commits: 77981fd4 by Stefan Monnier at 2021-02-09T18:04:24-05:00 * src/elab.ml (lexp_check_decls): Fix broken odd/even example. * src/REPL.ml (main): Re-raise internal error, so OCAMLRUNPARAM=b gives a proper backtrace. * samples/nat.typer (even1): Make it trickier to catch the previous error. - - - - - 4 changed files: - samples/nat.typer - src/REPL.ml - src/debruijn.ml - src/elab.ml Changes: ===================================== samples/nat.typer ===================================== @@ -18,8 +18,14 @@ one = succ zero; two = succ one; three = succ two; +%% `even1` is added just to have a more complex mutual-recursion, +%% where the order of declarations and definitions don't match at all. +even1 : Nat -> Int; even : Nat -> Int; odd : Nat -> Int; +even1 = lambda (n : Nat) -> case n + | zero => 1 + | succ y => (odd y); odd = lambda (n : Nat) -> case n | zero => 0 | succ y => (even y); @@ -29,6 +35,7 @@ even = lambda (n : Nat) -> case n | succ y => (odd y); + a = odd one; b = even one; c = odd two; ===================================== src/REPL.ml ===================================== @@ -1,6 +1,6 @@ (* REPL.ml --- Read Eval Print Loop (REPL) -Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2021 Free Software Foundation, Inc. Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> @@ -315,8 +315,9 @@ let main () = with | Log.Stop_Compilation msg -> handle_stopped_compilation msg; exit 1 - | Log.Internal_error msg -> - handle_stopped_compilation ("Internal error: " ^ msg); exit 1 + | (Log.Internal_error msg) as e -> + handle_stopped_compilation ("Internal error: " ^ msg); + raise e | Log.User_error msg -> handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 ) in ===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2021 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2021 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -1131,21 +1131,25 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let ectx = let (_, a, b, c) = ectx in let (grm, _, _, _) = nctx in (grm, a, b, c) in - let (declmap, nctx) + let (declmap) = List.fold_right - (fun ((l, vname), pexp) (map, nctx) -> + (fun ((l, vname), sexp) (map) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in - let e = check pexp adjusted_t nctx in - let (grm, ec, lc, sl) = nctx in + (* We elab `sexp` within the original `nctx`, i.e. + * the context where the other vars don't have + * a definition yet. This is because we can't yet + * build the proper `nctx`: a partially filled + * mutually-recursive block would not have the + * proper format, e.g. for `lctx_view`! *) + let e = check sexp adjusted_t nctx in let d = (v', LetDef (i + 1, e), t) in - (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + (IMap.add i ((l, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") - defs (IMap.empty, nctx) in + defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls View it on GitLab: https://gitlab.com/monnier/typer/-/commit/77981fd4dc8bc6af20e1db5148a9fb14f… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/77981fd4dc8bc6af20e1db5148a9fb14f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 4 commits: construction d'un objet json avec yojson
by Soilihi BEN SOILIHI BOINA 05 Fév '21

05 Fév '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 4bc5738f by Soilih BEN SOILIH at 2021-02-05T08:44:41-07:00 construction d'un objet json avec yojson - - - - - cbb623a9 by Soilih BEN SOILIH at 2021-02-05T08:58:17-07:00 construire un serveur en ocaml - - - - - 3831b442 by Soilih BEN SOILIH at 2021-02-05T09:34:50-07:00 lire un fichier json avec yojson - - - - - 5dee08c0 by Soilih BEN SOILIH at 2021-02-05T09:51:07-07:00 manipulation d'un objet json lu avec yojson - - - - - 8 changed files: - + LSP_Server/Yojson_exemple/examples/book.json - + LSP_Server/Yojson_exemple/examples/construire.ml - + LSP_Server/Yojson_exemple/examples/dune - + LSP_Server/Yojson_exemple/examples/dune-project - + LSP_Server/Yojson_exemple/examples/lire_un_fichier_json.ml - + LSP_Server/Yojson_exemple/examples/manipulation_du_fichier_lu.ml - + LSP_Server/Yojson_exemple/examples/server.ml - − test.txt Changes: ===================================== LSP_Server/Yojson_exemple/examples/book.json ===================================== @@ -0,0 +1,11 @@ +{ + "title": "Real World OCaml", + "tags" : [ "functional programming", "ocaml", "algorithms" ], + "pages": 450, + "authors": [ + { "name": "Jason Hickey", "affiliation": "Google" }, + { "name": "Anil Madhavapeddy", "affiliation": "Cambridge"}, + { "name": "Yaron Minsky", "affiliation": "Jane Street"} + ], + "is_online": true +} \ No newline at end of file ===================================== LSP_Server/Yojson_exemple/examples/construire.ml ===================================== @@ -0,0 +1,50 @@ +(* + ******commandes******* + $ eval $(opam env) + $ dune build construire.exe + $ ./_build/default/construire.exe + + <<EOF + + Construire un objet Json avec Yojson + Soit l'exemple suivant comme étant celui qu'on + souhaite construire: + +{ + "id": "09031996", + "name": "Soilih Ben Soilih", + "education": [ + { + "university": "UdeM", + "level": "master", + "last_year": 2021, + "finished": false + } + ], + "married":false, + "research_keys": ["LSP", "Ocaml", "Typer"] +} +EOF +*) + +open Yojson.Basic.Util + +let json_output = + `Assoc + [ + ("id", `String "09031996"); + ("name", `String "Soilih Ben Soilih"); + ( "education", + `Assoc + [ ("university", `String "UdeM"); ("level", `String "master");("last_year", `Int 2021);("finished", `Bool false) ] ); + ("married", `Bool false) + ] + +let main () = + let oc = stdout in + Yojson.Basic.pretty_to_channel oc json_output; + output_string oc "\n" + +let a = main () + +(* On peut ensuite utiliser la variable a pour écrire dans un fichier.json*) ===================================== LSP_Server/Yojson_exemple/examples/dune ===================================== @@ -0,0 +1,28 @@ +(executable + (name filtering) + (modules filtering) + (flags (-safe-string)) + (libraries yojson)) + +(executable + (name construire) + (modules construire) + (flags (-safe-string)) + (libraries yojson)) + + (executable + (name server) + (modules server) + (libraries yojson lwt cohttp cohttp-lwt-unix)) + + (executable + (name lire_un_fichier_json) + (modules lire_un_fichier_json) + (libraries yojson core core_kernel lwt cohttp cohttp-lwt-unix)) + + (executable + (name manipulation_du_fichier_lu) + (modules manipulation_du_fichier_lu) + (libraries core yojson)) + + ===================================== LSP_Server/Yojson_exemple/examples/dune-project ===================================== @@ -0,0 +1 @@ +(lang dune 2.8) ===================================== LSP_Server/Yojson_exemple/examples/lire_un_fichier_json.ml ===================================== @@ -0,0 +1,24 @@ +open Core_kernel;; +open Yojson;; +open Core + +(* + taper les commandes suivantes pour tester : + $ eval $(opam env) + $ dune build lire_un_fichier_json.exe --profile release + $ ./_build/default/lire_un_fichier_json.exe + + On remarque que ça affiche "ok", ce qui veut dire qu'il a réussi + à lire le fichier à partir de Yojson comme avec le In_channel + basique d'ocaml pour lire une fichier. +*) + +let () = + (* Read JSON file into an OCaml string *) + let buf = In_channel.read_all "book.json" in + (* Use the string JSON constructor *) + let json1 = Yojson.Basic.from_string buf in + (* Use the file JSON constructor *) + let json2 = Yojson.Basic.from_file "book.json" in + (* Test that the two values are the same *) + print_endline (if Yojson.Basic.equal json1 json2 then "OK" else "FAIL") \ No newline at end of file ===================================== LSP_Server/Yojson_exemple/examples/manipulation_du_fichier_lu.ml ===================================== @@ -0,0 +1,38 @@ +open Core + +(* + *** manipulation d'un fichier json lu *** + Taper les commandes suivantes: + $ eval $(opam env) + $ dune build manipulation_du_fichier_lu.exe + $ ./_build/default/manipulation_du_fichier_lu.exe + + On voit donc qu'on peut lire tout le fichier, tout comme + chaque clé qu'on veut et la manipuler comme on veut. +*) + +let () = + (* Read the JSON file *) + let json = Yojson.Basic.from_file "book.json" in + + (* Locally open the JSON manipulation functions *) + let open Yojson.Basic.Util in + let title = json |> member "title" |> to_string in + let tags = json |> member "tags" |> to_list |> filter_string in + let pages = json |> member "pages" |> to_int in + let is_online = json |> member "is_online" |> to_bool_option in + let is_translated = json |> member "is_translated" |> to_bool_option in + let authors = json |> member "authors" |> to_list in + let names = List.map authors ~f:(fun json -> member "name" json |> to_string) in + + (* Print the results of the parsing *) + printf "Title: %s (%d)\n" title pages; + printf "Authors: %s\n" (String.concat ~sep:", " names); + printf "Tags: %s\n" (String.concat ~sep:", " tags); + let string_of_bool_option = + function + | None -> "<unknown>" + | Some true -> "yes" + | Some false -> "no" in + printf "Online: %s\n" (string_of_bool_option is_online); + printf "Translated: %s\n" (string_of_bool_option is_translated) \ No newline at end of file ===================================== LSP_Server/Yojson_exemple/examples/server.ml ===================================== @@ -0,0 +1,30 @@ +open Cohttp_lwt_unix +open Yojson +open Printf +open Lwt + +(* taper les commandes suivantes: + $ dune build server.exe --profile release + $ ./_build/default/server.exe + et le serveur sera en ligne. + Ensuite, il faut ouvrir un autre terminal + et taper la commande qui suit pour ajouter + des informations au serveur: + $ curl 127.0.0.1:2021 --data "information" + +*) + +let server = begin + let callback conn req body = + body |> Cohttp_lwt.Body.to_string >|= (fun data -> + eprintf "Body: %s\n" data ;flush stderr; + sprintf "I'm a server" + ) + >>= (fun body -> Server.respond_string ~status:`OK ~body ()) + in begin + eprintf "Server is online\n";flush stderr; + Server.create ~mode:(`TCP (`Port 2021)) (Server.make ~callback ()) + end +end + +let _ = Lwt_main.run server \ No newline at end of file ===================================== test.txt deleted ===================================== @@ -1 +0,0 @@ -test !!! View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5f41573014ed1e572ea99cb5183e5ba6… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5f41573014ed1e572ea99cb5183e5ba6… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] essai
by Soilihi BEN SOILIHI BOINA 03 Fév '21

03 Fév '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 5f415730 by Soilih BEN SOILIH at 2021-02-03T23:06:43-07:00 essai - - - - - 1 changed file: - + test.txt Changes: ===================================== test.txt ===================================== @@ -0,0 +1 @@ +test !!! View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5f41573014ed1e572ea99cb5183e5ba64… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5f41573014ed1e572ea99cb5183e5ba64… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch soilih
by Soilihi BEN SOILIHI BOINA 03 Fév '21

03 Fév '21

Soilihi BEN SOILIHI BOINA pushed new branch soilih at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/soilih You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Février 2021