diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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 diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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" diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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 } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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{} = "_" diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 diff --git a/test/data/levenshtein.dats b/test/data/levenshtein.dats new file mode 100644 --- /dev/null +++ b/test/data/levenshtein.dats @@ -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 : 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: 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 : int(i)) => + (i := sz2i(s1_l) ; i > 0 ; i := i - 1) + (column[i] := i) + + fun loop2 { i : nat | i > 0 && i <= n+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 } .. (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(p1) + var s2 = $UN.ptr0_get(p2) + in + levenshtein(s1, s2) + end diff --git a/test/data/levenshtein.out b/test/data/levenshtein.out new file mode 100644 --- /dev/null +++ b/test/data/levenshtein.out @@ -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 : 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 : 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 : int(i)) => + (i := sz2i(s1_l) ; i > 0 ; i := i - 1) + (column[i] := i) + + fun loop2 { i : nat | i > 0 && i <= n+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 } .. ( 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(p1) + var s2 = $UN.ptr0_get(p2) + in + levenshtein(s1, s2) + end