language-ats 1.2.0.14 → 1.2.0.15

raw patch · 7 files changed

+262/−83 lines, 7 filesPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

API changes (from Hackage documentation)

Files

• language-ats.cabal +1/−1
• src/Language/ATS/Lexer.x +9/−0
• src/Language/ATS/Parser.y +6/−0
• src/Language/ATS/PrettyPrint.hs +4/−2
• src/Language/ATS/Types.hs +92/−80
• test/data/levenshtein.dats +73/−0
• test/data/levenshtein.out +77/−0

@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.2.0.14+version: 1.2.0.15 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale

@@ -220,6 +220,9 @@     <0> local                    { tok (\p _ -> alex $ Keyword p KwLocal) }     <0> praxi                    { tok (\p _ -> alex $ Keyword p KwPraxi) }     <0> while                    { tok (\p _ -> alex $ Keyword p KwWhile) }+    <0> "while*"                 { tok (\p _ -> alex $ Keyword p KwWhileStar) }+    <0> for                      { tok (\p _ -> alex $ Keyword p KwFor) }+    <0> "for*"                   { tok (\p _ -> alex $ Keyword p KwForStar) }     <0> where                    { tok (\p _ -> alex $ Keyword p KwWhere) }     <0> begin                    { tok (\p _ -> alex $ Keyword p KwBegin) }     <0> overload                 { tok (\p _ -> alex $ Keyword p KwOverload) }@@ -365,6 +368,9 @@              | KwStadef              | KwPraxi              | KwWhile+             | KwWhileStar+             | KwFor+             | KwForStar              | KwWhere              | KwBegin              | KwOverload@@ -488,6 +494,9 @@     pretty KwStadef = "stadef"     pretty KwPraxi = "praxi"     pretty KwWhile = "while"+    pretty KwWhileStar = "while*"+    pretty KwFor = "for"+    pretty KwForStar = "for*"     pretty KwOverload = "overload"     pretty KwWith = "with"     pretty KwDataview = "dataview"

@@ -102,6 +102,9 @@     dataview { Keyword $$ KwDataview }     datavtype { Keyword $$ KwDatavtype }     while { Keyword $$ KwWhile }+    whileStar { Keyword $$ KwWhileStar }+    for { Keyword $$ KwFor }+    forStar { Keyword $$ KwForStar }     of { Keyword $$ KwOf }     exception { Keyword $$ KwException }     include { Keyword $$ KwInclude }@@ -477,6 +480,9 @@               | Name { NamedVal $1 }               | lbrace ATS rbrace { Actions $2 }               | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }+              | for openParen PreExpression closeParen PreExpression { For $1 $3 $5 }+              | whileStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $8 $9 }+              | forStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { ForStar $1 $2 (snd $3) $5 $8 $9 }               | lineComment PreExpression { CommentExpr (to_string $1) $2 }               | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }               | PreExpression where lbrace ATS rbrace { WhereExp $1 $4 }

@@ -79,7 +79,6 @@ splits Mult       = True splits Add        = True splits Div        = True-splits Sub        = True splits LogicalAnd = True splits LogicalOr  = True splits _          = False@@ -137,7 +136,7 @@         a (BinaryF op e e')             | splits op = e </> pretty op <+> e'             | otherwise = e <+> pretty op <+> e'-        a (IndexF _ n e)                = pretty n <> "[" <> e <> "]"+        a (IndexF _ n e)                = pretty n <> brackets e         a (NamedValF nam)              = pretty nam         a (CallF nam [] [] Nothing []) = pretty nam <> "()"         a (CallF nam [] [] e xs) = pretty nam <> prettyArgsProof e xs@@ -169,6 +168,9 @@         a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (reverse es))         a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (reverse es)) <> ")"         a (WhileF _ e e')              = "while" <> parens e <> e'+        a (ForF _ e e')                = "for" <> parens e <> e'+        a (WhileStarF _ us t as e e')  = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'+        a (ForStarF _ us t as e e')    = "for*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'         a (ActionsF (ATS [d]))         = "{" <+> pretty d <+> "}"         a (ActionsF as)                = "{" <$> indent 2 (pretty as) <$> "}"         a UnderscoreLitF{}             = "_"

@@ -515,6 +515,9 @@                   | TupleEx a [Expression a]                   | BoxTupleEx a [Expression a]                   | While a (Expression a) (Expression a)+                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @while@ loop that is guaranteed to terminate.+                  | For a (Expression a) (Expression a)+                  | ForStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @for@ loop that is guaranteed to terminate.                   | Actions (ATS a)                   | Begin a (Expression a)                   | BinList { _op :: BinOp a, _exprs :: [Expression a] }@@ -557,6 +560,9 @@                      | TupleExF a [x]                      | BoxTupleExF a [x]                      | WhileF a x x+                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x+                     | ForF a x x+                     | ForStarF a [Universal a] (StaticExpression a) [Arg a] x x                      | ActionsF (ATS a)                      | BeginF a x                      | BinListF (BinOp a) [x]@@ -571,88 +577,94 @@ type instance Base (Expression a) = ExpressionF a  instance Recursive (Expression a) where-    project (Let l ds me)            = LetF l ds me-    project (VoidLiteral l)          = VoidLiteralF l-    project (Call n is us mps as)    = CallF n is us mps as-    project (NamedVal n)             = NamedValF n-    project (ListLiteral l s t es)   = ListLiteralF l s t es-    project (If e e' me)             = IfF e e' me-    project (UintLit u)              = UintLitF u-    project (FloatLit f)             = FloatLitF f-    project (IntLit i)               = IntLitF i-    project (HexLit s)               = HexLitF s-    project (UnderscoreLit l)        = UnderscoreLitF l-    project (Lambda l lt p e)        = LambdaF l lt p e-    project (LinearLambda l lt p e)  = LinearLambdaF l lt p e-    project (Index l n e)            = IndexF l n e-    project (Access l e n)           = AccessF l e n-    project (StringLit s)            = StringLitF s-    project (CharLit c)              = CharLitF c-    project (AddrAt l e)             = AddrAtF l e-    project (ViewAt l e)             = ViewAtF l e-    project (Binary op e e')         = BinaryF op e e'-    project (Unary op e)             = UnaryF op e-    project (IfCase l arms)          = IfCaseF l arms-    project (Case l k e arms)        = CaseF l k e arms-    project (RecordValue l recs mty) = RecordValueF l recs mty-    project (Precede e e')           = PrecedeF e e'-    project (ProofExpr a e e')       = ProofExprF a e e'-    project (TypeSignature e ty)     = TypeSignatureF e ty-    project (WhereExp e ds)          = WhereExpF e ds-    project (TupleEx l es)           = TupleExF l es-    project (BoxTupleEx l es)        = BoxTupleExF l es-    project (While l e e')           = WhileF l e e'-    project (Actions ds)             = ActionsF ds-    project (Begin l e)              = BeginF l e-    project (BinList op es)          = BinListF op es-    project (PrecedeList es)         = PrecedeListF es-    project (FixAt a s sfun)         = FixAtF a s sfun-    project (LambdaAt a sfun)        = LambdaAtF a sfun-    project (ParenExpr l e)          = ParenExprF l e-    project (CommentExpr s e)        = CommentExprF s e-    project (MacroVar l s)           = MacroVarF l s+    project (Let l ds me)              = LetF l ds me+    project (VoidLiteral l)            = VoidLiteralF l+    project (Call n is us mps as)      = CallF n is us mps as+    project (NamedVal n)               = NamedValF n+    project (ListLiteral l s t es)     = ListLiteralF l s t es+    project (If e e' me)               = IfF e e' me+    project (UintLit u)                = UintLitF u+    project (FloatLit f)               = FloatLitF f+    project (IntLit i)                 = IntLitF i+    project (HexLit s)                 = HexLitF s+    project (UnderscoreLit l)          = UnderscoreLitF l+    project (Lambda l lt p e)          = LambdaF l lt p e+    project (LinearLambda l lt p e)    = LinearLambdaF l lt p e+    project (Index l n e)              = IndexF l n e+    project (Access l e n)             = AccessF l e n+    project (StringLit s)              = StringLitF s+    project (CharLit c)                = CharLitF c+    project (AddrAt l e)               = AddrAtF l e+    project (ViewAt l e)               = ViewAtF l e+    project (Binary op e e')           = BinaryF op e e'+    project (Unary op e)               = UnaryF op e+    project (IfCase l arms)            = IfCaseF l arms+    project (Case l k e arms)          = CaseF l k e arms+    project (RecordValue l recs mty)   = RecordValueF l recs mty+    project (Precede e e')             = PrecedeF e e'+    project (ProofExpr a e e')         = ProofExprF a e e'+    project (TypeSignature e ty)       = TypeSignatureF e ty+    project (WhereExp e ds)            = WhereExpF e ds+    project (TupleEx l es)             = TupleExF l es+    project (BoxTupleEx l es)          = BoxTupleExF l es+    project (While l e e')             = WhileF l e e'+    project (WhileStar l us t as e e') = WhileStarF l us t as e e'+    project (For l e e')               = ForF l e e'+    project (ForStar l us t as e e')   = ForStarF l us t as e e'+    project (Actions ds)               = ActionsF ds+    project (Begin l e)                = BeginF l e+    project (BinList op es)            = BinListF op es+    project (PrecedeList es)           = PrecedeListF es+    project (FixAt a s sfun)           = FixAtF a s sfun+    project (LambdaAt a sfun)          = LambdaAtF a sfun+    project (ParenExpr l e)            = ParenExprF l e+    project (CommentExpr s e)          = CommentExprF s e+    project (MacroVar l s)             = MacroVarF l s  instance Corecursive (Expression a) where-    embed (LetF l ds me)            = Let l ds me-    embed (VoidLiteralF l)          = VoidLiteral l-    embed (CallF n is us mps as)    = Call n is us mps as-    embed (NamedValF n)             = NamedVal n-    embed (ListLiteralF l s t es)   = ListLiteral l s t es-    embed (IfF e e' me)             = If e e' me-    embed (UintLitF u)              = UintLit u-    embed (IntLitF i)               = IntLit i-    embed (FloatLitF f)             = FloatLit f-    embed (HexLitF s)               = HexLit s-    embed (UnderscoreLitF l)        = UnderscoreLit l-    embed (LambdaF l lt p e)        = Lambda l lt p e-    embed (LinearLambdaF l lt p e)  = LinearLambda l lt p e-    embed (IndexF l n e)            = Index l n e-    embed (AccessF l n e)           = Access l n e-    embed (StringLitF s)            = StringLit s-    embed (CharLitF c)              = CharLit c-    embed (AddrAtF l e)             = AddrAt l e-    embed (ViewAtF l e)             = ViewAt l e-    embed (BinaryF op e e')         = Binary op e e'-    embed (UnaryF op e)             = Unary op e-    embed (IfCaseF l arms)          = IfCase l arms-    embed (CaseF l k e arms)        = Case l k e arms-    embed (RecordValueF l recs mty) = RecordValue l recs mty-    embed (PrecedeF e e')           = Precede e e'-    embed (ProofExprF a e e')       = ProofExpr a e e'-    embed (TypeSignatureF e ty)     = TypeSignature e ty-    embed (WhereExpF e ds)          = WhereExp e ds-    embed (TupleExF l es)           = TupleEx l es-    embed (BoxTupleExF l es)        = BoxTupleEx l es-    embed (WhileF l e e')           = While l e e'-    embed (ActionsF ds)             = Actions ds-    embed (BeginF l e)              = Begin l e-    embed (BinListF op es)          = BinList op es-    embed (PrecedeListF es)         = PrecedeList es-    embed (FixAtF a s sfun)         = FixAt a s sfun-    embed (LambdaAtF a sfun)        = LambdaAt a sfun-    embed (ParenExprF l e)          = ParenExpr l e-    embed (CommentExprF s e)        = CommentExpr s e-    embed (MacroVarF l s)           = MacroVar l s+    embed (LetF l ds me)              = Let l ds me+    embed (VoidLiteralF l)            = VoidLiteral l+    embed (CallF n is us mps as)      = Call n is us mps as+    embed (NamedValF n)               = NamedVal n+    embed (ListLiteralF l s t es)     = ListLiteral l s t es+    embed (IfF e e' me)               = If e e' me+    embed (UintLitF u)                = UintLit u+    embed (IntLitF i)                 = IntLit i+    embed (FloatLitF f)               = FloatLit f+    embed (HexLitF s)                 = HexLit s+    embed (UnderscoreLitF l)          = UnderscoreLit l+    embed (LambdaF l lt p e)          = Lambda l lt p e+    embed (LinearLambdaF l lt p e)    = LinearLambda l lt p e+    embed (IndexF l n e)              = Index l n e+    embed (AccessF l n e)             = Access l n e+    embed (StringLitF s)              = StringLit s+    embed (CharLitF c)                = CharLit c+    embed (AddrAtF l e)               = AddrAt l e+    embed (ViewAtF l e)               = ViewAt l e+    embed (BinaryF op e e')           = Binary op e e'+    embed (UnaryF op e)               = Unary op e+    embed (IfCaseF l arms)            = IfCase l arms+    embed (CaseF l k e arms)          = Case l k e arms+    embed (RecordValueF l recs mty)   = RecordValue l recs mty+    embed (PrecedeF e e')             = Precede e e'+    embed (ProofExprF a e e')         = ProofExpr a e e'+    embed (TypeSignatureF e ty)       = TypeSignature e ty+    embed (WhereExpF e ds)            = WhereExp e ds+    embed (TupleExF l es)             = TupleEx l es+    embed (BoxTupleExF l es)          = BoxTupleEx l es+    embed (WhileF l e e')             = While l e e'+    embed (WhileStarF l us t as e e') = WhileStar l us t as e e'+    embed (ForF l e e')               = For l e e'+    embed (ForStarF l us t as e e')   = ForStar l us t as e e'+    embed (ActionsF ds)               = Actions ds+    embed (BeginF l e)                = Begin l e+    embed (BinListF op es)            = BinList op es+    embed (PrecedeListF es)           = PrecedeList es+    embed (FixAtF a s sfun)           = FixAt a s sfun+    embed (LambdaAtF a sfun)          = LambdaAt a sfun+    embed (ParenExprF l e)            = ParenExpr l e+    embed (CommentExprF s e)          = CommentExpr s e+    embed (MacroVarF l s)             = MacroVar l s  -- | An 'implement' or 'primplmnt' declaration data Implementation a = Implement { pos            :: a

@@ -0,0 +1,73 @@+staload UN = "prelude/SATS/unsafe.sats"++// Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C+fn levenshtein {m:nat}{n:nat}(s1 : string(m), s2 : string(n)) : int =+  let+    val s1_l: size_t(m) = length(s1)+    val s2_l: size_t(n) = length(s2)+    val column: arrayref(int, m+1) = arrayref_make_elt(s1_l + 1, 0)+    var i: int = sz2i(s1_l)+    +    fun loop1 { i : nat | i <= m } .<i>. (i : int(i)) : void =+      case+ i of+        | 0 => ()+        | i =>> {+          val () = column[i] := i+          val () = loop1(i - 1)+        }+    +    val () = loop1(sz2i(s1_l))+    +    val () = while* {i:nat} .<i>. (i: int(i)) => (i > 0)(column[i] := i ; i := i - 1)+    val () = while(i > 0)(column[i] := i ; i := i - 1)+    val () = for* { i : nat | i <= m }  .<i>. (i : int(i)) =>+        (i := sz2i(s1_l) ; i > 0 ; i := i - 1)+        (column[i] := i)+    +    fun loop2 { i : nat | i > 0 && i <= n+1 } .<n-i+1>. (x : int(i)) : void =+      if x <= sz2i(s2_l) then+        {+          val () = column[0] := x+          val () = let+            fun inner_loop { j : nat | j > 0 && j <= m+1 } .<m-j+1>. (y : int(j), last_diag : int) :+              void =+              if y <= sz2i(s1_l) then+                let+                  var old_diag = column[y]+                  +                  fun min_3(x : int, y : int, z : int) : int =+                    min(x, (min(y, z)))+                  +                  fun bool2int(c0 : char, c1 : char) : int =+                    if c0 = c1 then+                      0+                    else+                      1+                  +                  val () = column[y] := min_3( column[y] + 1+                                             , column[y - 1] + 1+                                             , last_diag + bool2int(s1[y - 1], s2[x - 1])+                                             )+                in+                  inner_loop(y + 1, old_diag)+                end+          in+            inner_loop(1, x - 1)+          end+          val () = loop2(x + 1)+        }+    +    val () = loop2(1)+  in+    column[s1_l]+  end++fn levenshtein_vt {m:nat}{n:nat}(s1 : !strnptr(m), s2 : !strnptr(n)) : int =+  let+    var p1 = strnptr2ptr(s1)+    var p2 = strnptr2ptr(s2)+    var s1 = $UN.ptr0_get<string(m)>(p1)+    var s2 = $UN.ptr0_get<string(n)>(p2)+  in+    levenshtein(s1, s2)+  end

@@ -0,0 +1,77 @@+staload UN = "prelude/SATS/unsafe.sats"++// Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C+fn levenshtein {m:nat}{n:nat}(s1 : string(m), s2 : string(n)) : int =+  let+    val s1_l: size_t(m) = length(s1)+    val s2_l: size_t(n) = length(s2)+    val column: arrayref(int, m+1) = arrayref_make_elt(s1_l + 1, 0)+    var i: int = sz2i(s1_l)+    +    fun loop1 { i : nat | i <= m } .<i>. (i : int(i)) : void =+      case+ i of+        | 0 => ()+        | i =>> {+          val () = column[i] := i+          val () = loop1(i - 1)+        }+    +    val () = loop1(sz2i(s1_l))+    val () = while* {i:nat}  .<i>. (i : int(i)) =>+        ((i > 0))+        (column[i] := i ; i := i - 1)+    val () = while(i > 0)(column[i] := i ; i := i - 1)+    val () = for* { i : nat | i <= m }  .<i>. (i : int(i)) =>+        (i := sz2i(s1_l) ; i > 0 ; i := i - 1)+        (column[i] := i)+    +    fun loop2 { i : nat | i > 0 && i <= n+1 } .<n-i+1>. (x : int(i)) :+      void =+      if x <= sz2i(s2_l) then+        {+          val () = column[0] := x+          val () = let+            fun inner_loop { j : nat | j > 0 && j <= m+1 } .<m-j+1>. ( y : int(j)+                                                                     , last_diag : int+                                                                     ) : void =+              if y <= sz2i(s1_l) then+                let+                  var old_diag = column[y]+                  +                  fun min_3(x : int, y : int, z : int) : int =+                    min(x, (min(y, z)))+                  +                  fun bool2int(c0 : char, c1 : char) : int =+                    if c0 = c1 then+                      0+                    else+                      1+                  +                  val () = column[y] := min_3( column[y] + 1+                                             , column[y - 1] + 1+                                             , last_diag + bool2int(s1[y - 1], s2[x - 1])+                                             )+                in+                  inner_loop(y + 1, old_diag)+                end+          in+            inner_loop(1, x - 1)+          end+          val () = loop2(x + 1)+        }+    +    val () = loop2(1)+  in+    column[s1_l]+  end++fn levenshtein_vt {m:nat}{n:nat}(s1 : !strnptr(m), s2 : !strnptr(n)) :+  int =+  let+    var p1 = strnptr2ptr(s1)+    var p2 = strnptr2ptr(s2)+    var s1 = $UN.ptr0_get<string(m)>(p1)+    var s2 = $UN.ptr0_get<string(n)>(p2)+  in+    levenshtein(s1, s2)+  end