diff options
| author | Gabriel Kerneis | 2014-03-18 13:32:21 +0000 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-03-18 13:32:21 +0000 |
| commit | ef17899571edf9f937c0c9397ece277f99540e55 (patch) | |
| tree | fc1b12b7631cfa23324ffca9d64395586217325a /src | |
| parent | 0e5d48a091c847d773e2305359a7d959f8fac19e (diff) | |
More library functions for Power
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser.mly | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 7 |
2 files changed, 9 insertions, 0 deletions
diff --git a/src/parser.mly b/src/parser.mly index 8672704f..4fef21f7 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -181,6 +181,8 @@ id: { idl (DeIid($3)) } | Lparen Deinfix Div Rparen { idl (DeIid($3)) } + | Lparen Deinfix Quot Rparen + { idl (DeIid("quot")) } | Lparen Deinfix Eq Rparen { Id_aux(DeIid($3),loc ()) } | Lparen Deinfix Excl Lparen diff --git a/src/type_internal.ml b/src/type_internal.ml index 795971e3..67021cc9 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -205,6 +205,7 @@ let initial_typ_env = ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e)); ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e)); ("mod",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e)); + ("quot",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e)); (*Type incomplete*) (":",Some(([("a",{k=K_Typ});("b",{k=K_Typ});("c",{k=K_Typ})], {t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "b"}])},{t=Tvar "c"},pure_e)}),External (Some "vec_concat"),[],pure_e)); @@ -214,11 +215,17 @@ let initial_typ_env = ("to_vec_dec",Some(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e)); ("==",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "eq"),[],pure_e)); ("!=",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "neq"),[],pure_e)); + ("<",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "lt"),[],pure_e)); + (">",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gt"),[],pure_e)); + ("<_u",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "ltu"),[],pure_e)); + (">_u",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gtu"),[],pure_e)); ("is_one",Some(([],{t= Tfn (bit_t,bool_t,pure_e)}),External (Some "is_one"),[],pure_e)); ("~",Some((["a",{k=K_Typ}],{t= Tfn ({t=Tvar "a"},{t=Tvar "a"},pure_e)}),External (Some "bitwise_not"),[],pure_e)); ("|",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_or"),[],pure_e)); ("^",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_xor"),[],pure_e)); ("&",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_and"),[],pure_e)); + ("^^",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([bit_t;nat_typ])},{t=Tvar "a"},pure_e)}),External (Some "duplicate"),[],pure_e)); + ("<<<",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};nat_typ])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_rightshift"),[],pure_e)); ] let initial_abbrev_env = |