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.