language-ats 1.2.0.15 → 1.2.0.16
raw patch · 9 files changed
+358/−94 lines, 9 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ Language.ATS: KwPrvar :: Keyword
+ Language.ATS: PrVar :: Pattern a -> Maybe (Expression a) -> Maybe (Type a) -> Declaration a
+ Language.ATS: [$sel:_prVarExpr:Func] :: Declaration a -> Maybe (Expression a)
+ Language.ATS: [$sel:prVarType:Func] :: Declaration a -> Maybe (Type a)
+ Language.ATS: [$sel:prvarPat:Func] :: Declaration a -> Pattern a
- Language.ATS: WhileStar :: a -> [Universal a] -> (StaticExpression a) -> [Arg a] -> (Expression a) -> (Expression a) -> Expression a
+ Language.ATS: WhileStar :: a -> [Universal a] -> (StaticExpression a) -> [Arg a] -> (Expression a) -> (Expression a) -> (Maybe [Arg a]) -> Expression a
Files
- language-ats.cabal +1/−1
- src/Language/ATS/Lexer.x +3/−0
- src/Language/ATS/Parser.y +6/−1
- src/Language/ATS/PrettyPrint.hs +11/−1
- src/Language/ATS/Types.hs +89/−88
- test/data/concurrency.out +2/−2
- test/data/levenshtein.out +1/−1
- test/data/levenshtein2.dats +124/−0
- test/data/levenshtein2.out +121/−0
language-ats.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.2.0.15+version: 1.2.0.16 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale
src/Language/ATS/Lexer.x view
@@ -155,6 +155,7 @@ <0> fnx { tok (\p _ -> alex $ Keyword p KwFnx) } <0> and { tok (\p _ -> alex $ Keyword p KwAnd) } <0> prval { tok (\p _ -> alex $ Keyword p KwPrval) }+ <0> prvar { tok (\p _ -> alex $ Keyword p KwPrvar) } <0> prfn { tok (\p _ -> alex $ Keyword p KwPrfn) } <0> prfun { tok (\p _ -> alex $ Keyword p KwPrfun) } <0> datatype { tok (\p _ -> alex $ Keyword p KwDatatype) }@@ -365,6 +366,7 @@ | KwOf | KwAbsprop | KwPrval+ | KwPrvar | KwStadef | KwPraxi | KwWhile@@ -491,6 +493,7 @@ pretty KwOf = "of" pretty KwAbsprop = "absprop" pretty KwPrval = "prval"+ pretty KwPrvar = "prvar" pretty KwStadef = "stadef" pretty KwPraxi = "praxi" pretty KwWhile = "while"
src/Language/ATS/Parser.y view
@@ -77,6 +77,7 @@ stadef { Keyword $$ KwStadef } val { $$@(Keyword _ (KwVal _)) } prval { Keyword $$ KwPrval }+ prvar { Keyword $$ KwPrvar } var { Keyword $$ KwVar } then { Keyword $$ KwThen } let { Keyword $$ KwLet }@@ -481,7 +482,8 @@ | 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 }+ | whileStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $8 $9 Nothing }+ | whileStar Universals Termetric openParen Args closeParen colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $12 $13 (Just $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) }@@ -850,6 +852,9 @@ StaticDeclaration : prval Pattern eq Expression { PrVal $2 (Just $4) Nothing } | prval Pattern colon Type { PrVal $2 Nothing (Just $4) } | prval Pattern colon Type eq Expression { PrVal $2 (Just $6) (Just $4) }+ | prvar Pattern eq Expression { PrVar $2 (Just $4) Nothing }+ | prvar Pattern colon Type { PrVar $2 Nothing (Just $4) }+ | prvar Pattern colon Type eq Expression { PrVar $2 (Just $6) (Just $4) } | praxi PreFunction { Func $1 (Praxi $2) } | primplmnt FunArgs StaticImplementation { ProofImpl $2 $3 } | StafunDecl { $1 }
src/Language/ATS/PrettyPrint.hs view
@@ -141,11 +141,15 @@ a (CallF nam [] [] Nothing []) = pretty nam <> "()" a (CallF nam [] [] e xs) = pretty nam <> prettyArgsProof e xs a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us+ a (CallF nam [] us Nothing [x])+ | startsParens x = pretty nam <> prettyArgsU "{" "}" us <> pretty x a (CallF nam [] us e xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs a (CallF nam is [] Nothing []) = pretty nam <> prettyImplicits is a (CallF nam is [] Nothing [x]) | startsParens x = pretty nam <> prettyImplicits is <> pretty x a (CallF nam is [] e xs) = pretty nam <> prettyImplicits is <> prettyArgsProof e xs+ a (CallF nam is us Nothing [x])+ | startsParens x = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> pretty x a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs a (CaseF _ add' e cs) = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs) a (IfCaseF _ cs) = "ifcase" <$> indent 2 (prettyIfCase cs)@@ -169,7 +173,8 @@ 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 (WhileStarF _ us t as e e' Nothing) = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'+ a (WhileStarF _ us t as e e' (Just ty)) = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> ":" <+> prettyArgs ty <+> "=>" <$> 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) <$> "}"@@ -349,6 +354,7 @@ isVal Val{} = True isVal Var{} = True isVal PrVal{} = True+isVal PrVar{} = True isVal _ = False glue :: Declaration a -> Declaration a -> Bool@@ -559,6 +565,10 @@ pretty (PrVal p Nothing (Just t)) = "prval" <+> pretty p <+> ":" <+> pretty t pretty (PrVal p (Just e) (Just t)) = "prval" <+> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e pretty PrVal{} = undefined+ pretty (PrVar p (Just e) Nothing) = "prvar" <+> pretty p <+> "=" <+> pretty e+ pretty (PrVar p Nothing (Just t)) = "prvar" <+> pretty p <+> ":" <+> pretty t+ pretty (PrVar p (Just e) (Just t)) = "prvar" <+> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e+ pretty PrVar{} = undefined pretty (AndDecl t p e) = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e pretty (Val a t p e) = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e pretty (Var t p Nothing (Just e)) = "var" <+> pretty p <> valSig t <+> "with" <+> pretty e
src/Language/ATS/Types.hs view
@@ -143,6 +143,7 @@ | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a } | StaVal [Universal a] String (Type a) | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (Expression a), prValType :: Maybe (Type a) }+ | PrVar { prvarPat :: Pattern a, _prVarExpr :: Maybe (Expression a), prVarType :: Maybe (Type a) } | Var { varT :: Maybe (Type a), varPat :: Pattern a, _varExpr1 :: Maybe (Expression a), _varExpr2 :: Maybe (Expression a) } | AndDecl { andT :: Maybe (Type a), andPat :: Pattern a, _andExpr :: Expression a } | Include String@@ -515,7 +516,7 @@ | 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.+ | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Maybe [Arg 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)@@ -560,7 +561,7 @@ | TupleExF a [x] | BoxTupleExF a [x] | WhileF a x x- | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x+ | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Maybe [Arg a]) | ForF a x x | ForStarF a [Universal a] (StaticExpression a) [Arg a] x x | ActionsF (ATS a)@@ -577,94 +578,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 (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+ 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' ty) = WhileStarF l us t as e e' ty+ 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 (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+ 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' ty) = WhileStar l us t as e e' ty+ 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
test/data/concurrency.out view
@@ -212,7 +212,7 @@ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan val mutex = unsafe_mutex_vt2t(ch.mutex) val (prf | ()) = mutex_lock(mutex)- val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val xs = $UN.castvwtp0{queue(a)}(prf | ch.queue) val () = channel_insert_helper<a>(chan, xs, x) prval prf = $UN.castview0{locked_v(l1)}(xs) val () = mutex_unlock(prf | mutex)@@ -223,7 +223,7 @@ { val+ CHANNEL{l0,l1,l2,l3}(ch) = chan val mutex = unsafe_mutex_vt2t(ch.mutex) val (prf | ()) = mutex_lock(mutex)- val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val xs = $UN.castvwtp0{queue(a)}(prf | ch.queue) val x = channel_remove_helper<a>(chan, xs) prval prf = $UN.castview0{locked_v(l1)}(xs) val () = mutex_unlock(prf | mutex) }
test/data/levenshtein.out view
@@ -18,7 +18,7 @@ val () = loop1(sz2i(s1_l)) val () = while* {i:nat} .<i>. (i : int(i)) =>- ((i > 0))+ (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)) =>
+ test/data/levenshtein2.dats view
@@ -0,0 +1,124 @@+staload UN = "prelude/SATS/unsafe.sats"++// Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C+fn min_3(x : int, y : int, z : int) : int =+ min(x, (min(y, z)))++fn bool2int(c0 : char, c1 : char) : int =+ if c0 = c1 then+ 0+ else+ 1++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)+ + fun loop1() : arrayref(int, m+1) =+ let+ val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<int>(succ(s1_l))+ + //+ val p1_arr = ptr1_succ<int>(p_arr)+ prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr)+ val () = ptr_set<int>(pf1_at | p_arr, 0)+ + //+ var i: int = 0+ prval [larr:addr]EQADDR () = eqaddr_make_ptr(p1_arr)+ var p = p1_arr+ + prvar pf0 = array_v_nil{int}(())+ + prvar pf1 = pf_arr+ + //+ val () = while* { i : nat | i <= m } .<m-i>. ( i : int(i)+ , p : ptr(larr+i*sizeof(int))+ , pf0 : array_v(int, larr, i)+ , pf1 : array_v(int?, larr+i*sizeof(int), m-i)+ ) : ( pf0 : array_v(int, larr, m)+ , pf1 : array_v(int?, larr+i*sizeof(int), 0)+ ) =>+ (i < sz2i(s1_l))+ {+ //+ prval (pf_at, pf1_res) = array_v_uncons{int?}(pf1)+ prval () = pf1 := pf1_res+ + //+ val c = g0ofg1(i)+ val () = ptr_set<int>(pf_at | p, c)+ val () = p := ptr1_succ<int>(p)+ + //+ prval () = pf0 := array_v_extend{int}(pf0, pf_at)+ val () = i := i + 1+ + //+ }+ + // end of [val]+ //+ prval () = pf_arr := pf0+ prval () = array_v_unnil{int?}(pf1)+ prval pf_arr = array_v_cons{int}(pf1_at, pf_arr)+ + //+ val res = arrayptr_encode(pf_arr, pf_gc | p_arr)+ in+ arrayptr_refize(res)+ end+ + val column = loop1(())+ + 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]+ 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_(s1 : string, s2 : string) : int =+ let+ fn witness(s : string) : [m:nat] string(m) =+ $UN.cast(s)+ in+ levenshtein(witness(s1), witness(s2))+ 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+
+ test/data/levenshtein2.out view
@@ -0,0 +1,121 @@+staload UN = "prelude/SATS/unsafe.sats"++// Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C+fn min_3(x : int, y : int, z : int) : int =+ min(x, (min(y, z)))++fn bool2int(c0 : char, c1 : char) : int =+ if c0 = c1 then+ 0+ else+ 1++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)+ + fun loop1() : arrayref(int, m+1) =+ let+ val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<int>(succ(s1_l))+ + //+ val p1_arr = ptr1_succ<int>(p_arr)+ prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr)+ val () = ptr_set<int>(pf1_at | p_arr, 0)+ + //+ var i: int = 0+ prval [larr:addr]EQADDR () = eqaddr_make_ptr(p1_arr)+ var p = p1_arr+ prvar pf0 = array_v_nil{int}()+ prvar pf1 = pf_arr+ + //+ val () = while* { i : nat | i <= m } .<m-i>. ( i : int(i)+ , p : ptr(larr+i*sizeof(int))+ , pf0 : array_v(int, larr, i)+ , pf1 : array_v(int?, larr+i*sizeof(int), m-i)+ ) : ( pf0 : array_v(int, larr, m)+ , pf1 : array_v(int?, larr+i*sizeof(int), 0)+ ) =>+ (i < sz2i(s1_l))+ {+ //+ prval (pf_at, pf1_res) = array_v_uncons{int?}(pf1)+ prval () = pf1 := pf1_res+ + //+ val c = g0ofg1(i)+ val () = ptr_set<int>(pf_at | p, c)+ val () = p := ptr1_succ<int>(p)+ + //+ prval () = pf0 := array_v_extend{int}(pf0, pf_at)+ val () = i := i + 1+ + //+ }+ + // end of [val]+ //+ prval () = pf_arr := pf0+ prval () = array_v_unnil{int?}(pf1)+ prval pf_arr = array_v_cons{int}(pf1_at, pf_arr)+ + //+ val res = arrayptr_encode(pf_arr, pf_gc | p_arr)+ in+ arrayptr_refize(res)+ end+ + val column = loop1(())+ + 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]+ 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_(s1 : string, s2 : string) : int =+ let+ fn witness(s : string) : [m:nat] string(m) =+ $UN.cast(s)+ in+ levenshtein(witness(s1), witness(s2))+ 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