BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 969e81a9 by n3f4s at 2016-10-07T09:58:56+02:00 try to undo some changes

- - - - - 6d9ca990 by n3f4s at 2016-10-07T10:01:53+02:00 try to undo bad changes to lparse.ml

- - - - - 4692b07f by n3f4s at 2016-10-07T10:03:42+02:00 add missing package for the report title

- - - - -

3 changed files:

- + doc/rapport/title.sty - src/lparse.ml - tests/unify_test.ml

Changes:

===================================== doc/rapport/title.sty ===================================== --- /dev/null +++ b/doc/rapport/title.sty @@ -0,0 +1,50 @@ + +\ProvidesPackage{title} + +\RequirePackage{graphicx} + +\newcommand*{\subtitle}[1]{\gdef@subtitle{#1}% +} +\newcommand*{@subtitle}{} + +\newcommand*{\tuteurPoly}[1]{\gdef@tuteurPoly{#1}} +\newcommand*{\tuteurEntr}[1]{\gdef@tuteurEntr{#1}} + +\newcommand*{\logo}[3]{\gdef@logo{#1\hfill#2\hfill#3}% +} +\newcommand*{@logo}{} + +\newcommand*{\scolaryear}[1]{\gdef@scolaryear{#1}} + +\newcommand*{\thisyear}[1]{\gdef@thisyear{#1}} + +\renewcommand*{\maketitle}{% +\begin{titlepage} +\parindent 0pt +INFO @thisyear \hfill Tuteur de stage : @tuteurEntr\ +Année @scolaryear \hfill Enseignant responsable : @tuteurPoly\ + +\vfill + +\begin{flushleft} + \usefont{OT1}{ptm}{m}{n} + \Large @title\ :\ + \Huge @subtitle +\end{flushleft} + +\par +\hrule height 4pt +\par + +\begin{flushright} + \usefont{OT1}{phv}{m}{n} + \Large @author + \par +\end{flushright} + +\vfill + +@logo +\end{titlepage} +} +\endinput

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -77,16 +77,32 @@ type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list

-let elab_check_def (ctx : lexp_context) var lxp ltype = - if OL.conv_p ltype (OL.check ctx lxp) then - () (* FIXME: Check ltype as well! *) + +let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = + match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with + | Sort (_, _) -> () (* All clear! *) + | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_to_str ltp) + +let elab_check_proper_type (ctx : elab_context) ltp v = + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp + with e -> print_string ("Exception while checking type `" + ^ lexp_to_str ltp ^ "` of var `" ^ + (let (_, name) = v in name) ^"`\n"); + print_lexp_ctx (ectx_to_lctx ctx); + raise e + +let elab_check_def (ctx : elab_context) var lxp ltype = + let lctx = ectx_to_lctx ctx in + if OL.conv_p ltype (OL.check lctx lxp) then + elab_check_proper_type ctx ltype var else (print_string "¡¡ctx_define error!!\n"; lexp_print lxp; print_string " !: "; lexp_print ltype; print_string "\nbecause\n"; - lexp_print (OL.check ctx lxp); + lexp_print (OL.check lctx lxp); print_string " != "; lexp_print ltype; print_string "\n";

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -18,8 +18,7 @@ open Str open Debug

open Fmt_lexp - -open Log +open Debug_fun

type result = | Constraint

View it on GitLab: https://gitlab.com/monnier/typer/compare/fdf96490b143816ed5dd0ca22fba464cc99...