[Git][monnier/typer][master] Use strings to specify operators
Stefan pushed to branch master at Stefan / Typer Commits: 1def0013 by Stefan Monnier at 2017-09-19T16:53:25Z Use strings to specify operators - - - - - 3 changed files: - btl/pervasive.typer - src/elab.ml - tests/eval_test.ml Changes: ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -346,9 +346,9 @@ Decidable = typecons (Decidable (prop : Type)) %%%% If -define-operator if () 2; -define-operator then 2 1; -define-operator else 1 66; +define-operator "if" () 2; +define-operator "then" 2 1; +define-operator "else" 1 66; if_then_else_ = macro (lambda args -> ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -253,7 +253,7 @@ let mkDummy_infer ctx loc = let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = match sargs with - | [Symbol (_, name); l; r] + | [String (_, name); l; r] -> let level s = match s with | Symbol (_, "") -> None | Integer (_, n) -> Some n @@ -261,7 +261,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = let (grm, a, b, c) = ctx in (SMap.add name (level l, level r) grm, a, b, c) | [o; _; _] - -> sexp_error (sexp_location o) "Expecting a symbol"; ctx + -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ -> sexp_error loc "define-operator expects 3 argument"; ctx ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -410,9 +410,9 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "define-operator" - "define-operator IF () 2; - define-operator THEN 2 1; - define-operator ELSE 1 66; + "define-operator \"IF\" () 2; + define-operator \"THEN\" 2 1; + define-operator \"ELSE\" 1 66; IF_THEN_ELSE_ = if_then_else_;" "{IF true THEN 2 ELSE 3};" View it on GitLab: https://gitlab.com/monnier/typer/commit/1def001319dfae6c055552d3f5b8fac4958a... --- View it on GitLab: https://gitlab.com/monnier/typer/commit/1def001319dfae6c055552d3f5b8fac4958a... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan