Re: [Typer] [Git][monnier/typer][master] 2 commits: finished type_ macro

finished type_ macro

Merci.

Changes to be committed:

• samples/inductive.typer
  • finished the type_ macro
• samples/int_index_inconsistency.typer
  • type index are inconsistent
• src/builtin.ml
  • improved error message

Au fait, pourrais-tu mettre des commit-message un peu plus détaillés?

• let sexp_nil = nil (a := Sexp) in

• let sexp_nil = (nil (a := Sexp)) in

Pourquoi?

• let type-name = get-name name in

À quoi sert ce get-name?

+type Nat t

• | succ Nat
• | zero;

C'est quoi le "t"?

+let _ = (add_test "EVAL" "Monads" (fun () ->

• reset_eval_trace ();
• let dcode = "

•  c = bind (a := Type) (b := Type) (open \"./_build/w_file.txt\" \"w\")
  

•    (lambda (f : FileHandle) ->
  

•      write f \"Hello2\");
  

• " in
• let rctx, lctx = eval_decl_str dcode lctx rctx in
• let rcode = "run-io (a := Type) (b := Unit) c Unit" in
• (* Eval defined lambda *)
• let ret = eval_expr_str rcode lctx rctx in

•    (* Expect a 3 results *)
  

•    match ret with
  

•        | [v] -> success ()
  

•        | _ -> failure ()
  

+))

Pour les eval_test, ça serait bien de faire qqch comme j'ai fait pour les sexp, i.e. de pouvoir simplement écrire quelques tests où tu donnes 2 expressions Typer et le test vérifie qu'elles renvoient la même valeur. Comme ça on peut ajouter des tests sans avoir à recopier un gros boilerplate de code Ocaml.

Stefan