[Git][monnier/typer][unification] 3 commits: try to undo some changes
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...
Afficher les réponses par date
participants (1)
-
BONNEVALLE Vincent