Merge pull request #15 from AthenaFoundation/list_comprehensions

Add list comprehensions and a Sudoku solver illustrating their use.

.gitignore

@@ -1,6 +1,11 @@
 .cm/
-*.grm.*
-*.lex.*
+*.grm.sig
+*.grm.sml
+*.lex.sml
+*.lex
+*.sty
+*.log
+*.pdf
 *.x86-linux
 athena
 regression_results.txt

abstract_syntax.sml

@@ -510,6 +510,7 @@ fun makeIdExpSimple(str,pos) =
         idExp({msym=msym(s),mods=[],sym=s,no_mods=true,pos=pos})
     end
 
+
 fun makeIdExpSimple'(sym,pos) = 
     let val s = sym
     in
@@ -2520,6 +2521,48 @@ fun splitApps(p) = applyPhraseFunRecursively(psplitAppExps,p)
 fun desugarPhrase(p) = applyExpFunRecursively(desugarSingleLets,(applyExpFunRecursively(desugarNestedLets,
 applyExpFunRecursively(desugarLetrecs,applyExpFunRecursively(desugarNestedTrys,p)))))
 
+fun desugarListComprehension(e1,pat,e2,guard_opt) = 
+   let val fresh_sym = Symbol.freshSymbol(SOME "v")
+       val fresh_id = idExp({msym=msym(fresh_sym),mods=[],sym=fresh_sym,no_mods=true,pos=posOfPat(pat)})
+       val match_exp = let val discriminant_phrase = exp(fresh_id)
+                           val match_clause = {pat=pat,
+					       exp=e1}
+                       in
+                         matchExp({discriminant=discriminant_phrase, 
+				   clauses=[match_clause],
+				   pos = posOfExp(e1)})
+                       end
+       val lambda_exp =  functionExp({params=[someParam({name=fresh_sym,pos=posOfPat(pat),sort_as_sym_term=NONE,op_tag=NONE,sort_as_fterm=NONE,sort_as_exp=NONE})],
+				      body=match_exp,
+				      pos=posOfExp(e1)})
+       val map_sym = S.symbol("map")
+       val map_select_sym = S.symbol("map-select-2")
+       fun guardMatchExp(g) = let val discriminant_phrase = exp(fresh_id)
+				  val match_clause = {pat=pat,
+						      exp=g}
+			      in
+				  matchExp({discriminant=discriminant_phrase, 
+					    clauses=[match_clause],
+					    pos = posOfExp(e1)})
+			      end
+       fun guardLambdaExp(g) =  functionExp({params=[someParam({name=fresh_sym,pos=posOfPat(pat),sort_as_sym_term=NONE,op_tag=NONE,sort_as_fterm=NONE,sort_as_exp=NONE})],
+					    body=guardMatchExp(g),
+					    pos=posOfExp(e1)})
+
+    in 
+      (case guard_opt of 
+          NONE => appExp({proc=exp(idExp({msym=msym(map_sym),mods=[],sym=map_sym,no_mods=true,pos=posOfExp(e1)})),
+			  args=[exp(lambda_exp),exp(e2)], 
+			  pos=posOfExp(e1),
+			  alt_exp=ref(NONE)})
+        | SOME(g) => appExp({proc=exp(idExp({msym=msym(map_select_sym),mods=[],sym=map_select_sym,no_mods=true,pos=posOfExp(e1)})),
+			     args=[exp(lambda_exp),
+				   exp(e2),
+				   exp(guardLambdaExp(g))],
+			     pos=posOfExp(e1),
+			     alt_exp=ref(NONE)}))
+    end				   
+
 fun symTermAppToExp(t) = 
       let fun printSymTermVar(sym) = (Names.sort_variable_prefix)^(Symbol.name sym)
           fun unparse(t) = (case SymTerm.isTaggedConstant(t) of  

athena.grm

@@ -25,8 +25,8 @@ fun getPos((l,p)) = {line=l,pos=p,file=(!Paths.current_file)}
        EQUAL_SIGN | ASSERT | ASSERT_CLOSE | ASSUME | ASSUME_LET | SUPPOSE_ABSURD | SUPPOSE_ABSURD_LET | ON | PROVE | 
        DMATCH | EITHER | ABSURD | MP | DN | EQUIV | LEFT_IFF | RIGHT_IFF | BOTH  | ASGN | BY_CASES | 
        META_ID | SOME_SYMBOL | LEFT_AND | RIGHT_AND | CD | VAL_OF | VAR | FUN_ARROW | DATATYPE | DATATYPES | DEFINE_SORT | 
-       SOME_LIST | SOME_CELL | SOME_SUB | SOME_TABLE | SOME_MAP | DEFINE | POUND | STRUCTURE | STRUCTURES | DOMAIN | WHERE | 
-       DECLARE | DDECLARE | DIRECTIVE_PREFIX | EGEN | BEGIN | WHILE | CLEAR | THE | DEFINE_SYMBOL | DOMAINS | 
+       SOME_LIST | SOME_CELL | SOME_SUB | SOME_TABLE | SOME_MAP | DEFINE | POUND | STRUCTURE | STRUCTURES | DOMAIN | WHERE | PROVIDED | 
+       DECLARE | DDECLARE | DIRECTIVE_PREFIX | EGEN | BEGIN | WHILE | CLEAR | THE | DEFINE_SYMBOL | DOMAINS | OVER  | 
        EGEN_UNIQUE  | LEIBNIZ | EQ_REFLEX  | SOME_QUANT | USPEC | FETCH  | RETRACT | DEFINE_FUN | ADD_DEMON | ADD_DEMONS | 
        SOME_PROP_CON | UNEQUAL_TERMS | INDUCTION | STRUCTURE_CASES | LIST | CELL | RULE  | GEN_OVER | WITH_PREDICATE | WITH_KEYS | 
        WITH_WITNESS | MAKE_CELL | REF  | USE_TERM_PARSER | USE_PROP_PARSER | END | SPECIALIZE | SET_FLAG | 
@@ -612,6 +612,10 @@ expression: any_id (let val id_pos = getPos(any_idleft)
 
           | LEFT_BRACKET phrases RIGHT_BRACKET (A.listExp({members=phrases,pos=getPos LEFT_BRACKETleft}))
 
+          | LEFT_BRACKET expression FOR pattern OVER expression RIGHT_BRACKET (A.desugarListComprehension(expression1,pattern,expression2,NONE))
+
+          | LEFT_BRACKET expression FOR pattern OVER expression PROVIDED expression RIGHT_BRACKET (A.desugarListComprehension(expression1,pattern,expression2,SOME(expression3)))
+
           |  MAP_BEGIN map_bindings MAP_END  (A.makeMapExp(map_bindings,getPos(MAP_BEGINleft)))
 
           | LPAREN METHOD LPAREN possibly_wildcard_param_list_no_dots RPAREN deduction RPAREN

athena.grm.sig

@@ -46,6 +46,7 @@ val SOME_QUANT:  'a * 'a -> (svalue,'a) token
 val EQ_REFLEX:  'a * 'a -> (svalue,'a) token
 val LEIBNIZ:  'a * 'a -> (svalue,'a) token
 val EGEN_UNIQUE:  'a * 'a -> (svalue,'a) token
+val OVER:  'a * 'a -> (svalue,'a) token
 val DOMAINS:  'a * 'a -> (svalue,'a) token
 val DEFINE_SYMBOL:  'a * 'a -> (svalue,'a) token
 val THE:  'a * 'a -> (svalue,'a) token
@@ -56,6 +57,7 @@ val EGEN:  'a * 'a -> (svalue,'a) token
 val DIRECTIVE_PREFIX:  'a * 'a -> (svalue,'a) token
 val DDECLARE:  'a * 'a -> (svalue,'a) token
 val DECLARE:  'a * 'a -> (svalue,'a) token
+val PROVIDED:  'a * 'a -> (svalue,'a) token
 val WHERE:  'a * 'a -> (svalue,'a) token
 val DOMAIN:  'a * 'a -> (svalue,'a) token
 val STRUCTURES:  'a * 'a -> (svalue,'a) token