Skip to content

Commit

Permalink
Replace externals with a more robust implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
@matijapretnar
matijapretnar committed Oct 18, 2021
1 parent 564650f commit 3288298
Show file tree
Hide file tree
Showing 25 changed files with 378 additions and 499 deletions.
1 change: 0 additions & 1 deletion docs/try/effmode.js
View file
Expand Up @@ -9,7 +9,6 @@ CodeMirror.defineMIME('text/x-eff', {
'effect' : 'keyword',
'else' : 'keyword',
'end' : 'keyword',
'external' : 'keyword',
'false' : 'builtin',
'finally' : 'keyword',
'fun' : 'keyword',
Expand Down
1 change: 0 additions & 1 deletion etc/eff-mode.el
View file
Expand Up @@ -20,7 +20,6 @@
"else"
"end"
"effect"
"external"
"finally"
"for"
"fun"
Expand Down
96 changes: 1 addition & 95 deletions etc/eff.tmbundle/eff.tmLanguage
View file
Expand Up @@ -1462,7 +1462,7 @@
</dict>
</dict>
<key>end</key>
<string>(?=\b(type|val|external|class|module|end)\b)|^\s*$</string>
<string>(?=\b(type|val|class|module|end)\b)|^\s*$</string>
<key>name</key>
<string>meta.module.signature.val.eff</string>
<key>patterns</key>
Expand Down Expand Up @@ -1530,100 +1530,6 @@
</dict>
</array>
</dict>
<dict>
<key>begin</key>
<string>(external)\s+([a-z_][a-zA-Z0-9_']*)\s*(:)</string>
<key>beginCaptures</key>
<dict>
<key>1</key>
<dict>
<key>name</key>
<string>keyword.other.eff</string>
</dict>
<key>2</key>
<dict>
<key>name</key>
<string>entity.name.type.external-signature.eff</string>
</dict>
<key>3</key>
<dict>
<key>name</key>
<string>punctuation.separator.type-constraint.eff</string>
</dict>
</dict>
<key>end</key>
<string>(?=\b(type|val|external|class|module|let|end)\b)|^\s*$</string>
<key>name</key>
<string>meta.module.signature.external.eff</string>
<key>patterns</key>
<array>
<dict>
<key>captures</key>
<dict>
<key>1</key>
<dict>
<key>name</key>
<string>punctuation.definition.optional-parameter.eff</string>
</dict>
<key>2</key>
<dict>
<key>name</key>
<string>entity.name.tag.label.optional.eff</string>
</dict>
<key>3</key>
<dict>
<key>name</key>
<string>punctuation.separator.optional-parameter.eff</string>
</dict>
</dict>
<key>match</key>
<string>(\?)([a-z][a-zA-Z0-9_]*)\s*(:)</string>
<key>name</key>
<string>variable.parameter.optional.eff</string>
</dict>
<dict>
<key>begin</key>
<string>(~)([a-z][a-zA-Z0-9'_]*)\s*(:)\s*</string>
<key>beginCaptures</key>
<dict>
<key>1</key>
<dict>
<key>name</key>
<string>punctuation.definition.labeled-parameter.eff</string>
</dict>
<key>2</key>
<dict>
<key>name</key>
<string>entity.name.tag.label.eff</string>
</dict>
<key>3</key>
<dict>
<key>name</key>
<string>punctuation.separator.label.eff</string>
</dict>
</dict>
<key>end</key>
<string>\s</string>
<key>name</key>
<string>variable.parameter.labeled.eff</string>
<key>patterns</key>
<array>
<dict>
<key>include</key>
<string>#variables</string>
</dict>
</array>
</dict>
<dict>
<key>include</key>
<string>#strings</string>
</dict>
<dict>
<key>include</key>
<string>#typedefs</string>
</dict>
</array>
</dict>
</array>
</dict>
<key>moduleref</key>
Expand Down
6 changes: 3 additions & 3 deletions src/01-language/backendSignature.ml
View file
Expand Up @@ -6,6 +6,9 @@ module type T = sig

val initial_state : state

val load_primitive :
state -> CoreTypes.Variable.t -> Primitives.primitive -> state

val process_computation :
state ->
CoreSyntax.computation ->
Expand Down Expand Up @@ -33,9 +36,6 @@ module type T = sig
(CoreSyntax.variable * Type.ty_scheme) list ->
state

val process_external :
state -> CoreTypes.Variable.t * Type.ty * string -> state

val process_tydef :
state ->
(CoreTypes.TyName.t, CoreTypes.TyParam.t list * Type.tydef) Assoc.t ->
Expand Down
129 changes: 129 additions & 0 deletions src/01-language/primitives.ml
View file
@@ -0,0 +1,129 @@
type primitive =
| CompareEq
| CompareGe
| CompareGt
| CompareLe
| CompareLt
| CompareNe
| FloatAcos
| FloatAdd
| FloatAsin
| FloatAtan
| FloatCos
| FloatDiv
| FloatExp
| FloatExpm1
| FloatInfinity
| FloatLog
| FloatLog1p
| FloatMul
| FloatNaN
| FloatNeg
| FloatNegInfinity
| FloatOfInt
| FloatSin
| FloatSqrt
| FloatSub
| FloatTan
| IntegerAdd
| IntegerDiv
| IntegerMod
| IntegerMul
| IntegerNeg
| IntegerPow
| IntegerSub
| IntOfFloat
| StringConcat
| StringLength
| StringOfFloat
| StringOfInt
| StringSub
| ToString

(* Keep this list up to date with the type above, otherwise the missing primitives will not be loaded *)
let primitives =
[
CompareEq;
CompareGe;
CompareGt;
CompareLe;
CompareLt;
CompareLt;
CompareNe;
FloatAcos;
FloatAdd;
FloatAsin;
FloatAtan;
FloatCos;
FloatDiv;
FloatExp;
FloatExpm1;
FloatInfinity;
FloatLog;
FloatLog1p;
FloatMul;
FloatNaN;
FloatNeg;
FloatNegInfinity;
FloatOfInt;
FloatSin;
FloatSqrt;
FloatSub;
FloatTan;
IntegerAdd;
IntegerDiv;
IntegerMod;
IntegerMul;
IntegerNeg;
IntegerPow;
IntegerSub;
IntOfFloat;
StringConcat;
StringLength;
StringOfFloat;
StringOfInt;
StringSub;
ToString;
]

let primitive_name = function
| CompareEq -> "="
| CompareGe -> ">="
| CompareGt -> ">"
| CompareLe -> "<="
| CompareLt -> "<"
| CompareNe -> "<>"
| FloatAcos -> "acos"
| FloatAdd -> "+."
| FloatAsin -> "asin"
| FloatAtan -> "atan"
| FloatCos -> "cos"
| FloatDiv -> "/."
| FloatExp -> "exp"
| FloatExpm1 -> "expm1"
| FloatInfinity -> "infinity"
| FloatLog -> "log"
| FloatLog1p -> "log1p"
| FloatMul -> "*."
| FloatNaN -> "nan"
| FloatNeg -> "~-."
| FloatNegInfinity -> "neg_infinity"
| FloatOfInt -> "float_of_int"
| FloatSin -> "sin"
| FloatSqrt -> "sqrt"
| FloatSub -> "-."
| FloatTan -> "tan"
| IntegerAdd -> "+"
| IntegerDiv -> "/"
| IntegerMod -> "mod"
| IntegerMul -> "*"
| IntegerNeg -> "~-"
| IntegerPow -> "**"
| IntegerSub -> "-"
| IntOfFloat -> "int_of_float"
| StringConcat -> "^"
| StringLength -> "string_length"
| StringOfFloat -> "string_of_float"
| StringOfInt -> "string_of_int"
| StringSub -> "sub"
| ToString -> "to_string"
2 changes: 0 additions & 2 deletions src/02-parser/commands.ml
View file
Expand Up @@ -11,8 +11,6 @@ and plain_command =
(** [let p1 = t1 and ... and pn = tn] *)
| TopLetRec of (Sugared.variable * Sugared.term) list
(** [let rec f1 p1 = t1 and ... and fn pn = tn] *)
| External of (Sugared.variable * Sugared.ty * Sugared.variable)
(** [external x : t = "ext_val_name"] *)
| DefEffect of (Sugared.effect * (Sugared.ty * Sugared.ty))
(** [effect Eff : ty1 -> t2] *)
| Term of Sugared.term
Expand Down
10 changes: 5 additions & 5 deletions src/02-parser/desugarer.ml
View file
Expand Up @@ -641,11 +641,11 @@ let desugar_top_let_rec state defs =
let defs' = List.fold_right desugar_defs (List.combine ns defs) [] in
(state', defs')

let desugar_external state (x, t, f) =
let n = fresh_var (Some x) in
let ts = syntax_to_core_params (free_type_params t) in
let _state', t' = desugar_type ts state t in
({ state with context = Assoc.update x n state.context }, (n, t', f))
let load_primitive state x prim =
{
state with
context = Assoc.update (Primitives.primitive_name prim) x state.context;
}

let desugar_def_effect state (eff, (ty1, ty2)) =
let state', eff' = effect_to_symbol state eff in
Expand Down
8 changes: 3 additions & 5 deletions src/02-parser/desugarer.mli
View file
Expand Up @@ -5,6 +5,9 @@ type state

val initial_state : state

val load_primitive :
state -> UntypedSyntax.variable -> Primitives.primitive -> state

val desugar_computation :
state -> SugaredSyntax.term -> state * UntypedSyntax.computation

Expand All @@ -13,11 +16,6 @@ val desugar_def_effect :
SugaredSyntax.effect * (SugaredSyntax.ty * SugaredSyntax.ty) ->
state * (CoreTypes.Effect.t * (Type.ty * Type.ty))

val desugar_external :
state ->
SugaredSyntax.variable * SugaredSyntax.ty * string ->
state * (CoreTypes.Variable.t * Type.ty * string)

val desugar_top_let :
state ->
(SugaredSyntax.pattern * SugaredSyntax.term) list ->
Expand Down
3 changes: 0 additions & 3 deletions src/02-parser/grammar.mly
View file
Expand Up @@ -37,7 +37,6 @@
%token <SugaredSyntax.label> UNAME
%token <SugaredSyntax.typaram> PARAM
%token TYPE ARROW HARROW OF EFFECT PERFORM
%token EXTERNAL
%token MATCH WITH FUNCTION HASH
%token LET REC AND IN
%token FUN BAR BARBAR
Expand Down Expand Up @@ -107,8 +106,6 @@ plain_topdef:
{ Commands.TopLet defs }
| LET REC defs = separated_nonempty_list(AND, let_rec_def)
{ Commands.TopLetRec defs }
| EXTERNAL x = ident COLON t = ty EQUAL n = STRING
{ Commands.External (x, t, n) }
| EFFECT eff = effect COLON t1 = prod_ty ARROW t2 = ty
{ Commands.DefEffect (eff, (t1, t2))}
| EFFECT eff = effect COLON t = prod_ty
Expand Down
1 change: 0 additions & 1 deletion src/02-parser/lexer.mll
View file
Expand Up @@ -11,7 +11,6 @@
("effect", EFFECT);
("else", ELSE);
("end", END);
("external", EXTERNAL);
("false", BOOL false);
("finally", FINALLY);
("fun", FUN);
Expand Down

0 comments on commit 3288298

Please sign in to comment.