<commit_before>(library
  (harlan front typecheck)
  (export typecheck)
  (import
    (rnrs)
    (util cKanren mk)
    (util cKanren ck)
    (util cKanren typecomp)
    (only (chezscheme) printf pretty-print)
    (harlan compile-opts)
    (util color))

(define-syntax (define-mk x)
  (define trace-mk #f)
  (syntax-case x ()
    ((_ name (lambda (a* ...) body))
     (if trace-mk
         #`(define name
             (lambda (a* ...)
               (fresh ()
                 (project (a* ...)
                   (begin
                     (printf "~s\n" (list 'name a* ...))
                     succeed))
                 body)))
         #`(define name (lambda (a* ...) body))))))

(define-mk pairo
  (lambda (x)
    (fresh (a d)
      (== `(,a . ,d) x))))

(define-mk lookup
  (lambda (env x type)
    (fresh (env^)
      (conde
        ((== `((,x . ,type) . ,env^) env))
        ((fresh (y t)
           (=/= x y)
           (== `((,y . ,t) . ,env^) env)
           (lookup env^ x type)))))))

(define-mk infer-exprs
  (lambda (exprs env type exprso)
    (fresh (expr expro expr* expro*)
      (conde
        ((== exprs '())
         (== exprso '()))
        ((== exprs `(,expr . ,expr*))
         (== exprso `(,expro . ,expro*))
         (infer-expr expr env type expro)
         (infer-exprs expr* env type expro*))))))

(define-mk infer-expr
  (lambda (expr env type expro)
    (conde
      ((fresh (c)
         (== expr `(char ,c))
         (== expro `(char ,c))
         (== type 'char)))
      ((fresh (n)
         (== expr `(num ,n))
         (prefo type '(int float u64))
         (== expro `(,type ,n))))
      ((fresh (n)
         (== expr `(float ,n))
         (== expro `(float ,n))
         (== type 'float)))
      ((fresh (str)
         (== expr `(str ,str))
         (== expro `(str ,str))
         (== type 'str)))
      ((fresh (b)
         (== expr `(bool ,b))
         (== expro `(bool ,b))
         (== type `bool)))
      ((fresh (x)
         (== expr `(var ,x))
         (== expro `(var ,type ,x))
         (lookup env x type)))
      ((fresh (test test^ conseq conseq^ alt alt^)
         (== expr `(if ,test ,conseq ,alt))
         (== expro `(if ,test^ ,conseq^ ,alt^))
         (infer-expr test env 'bool test^)
         (infer-expr conseq env type conseq^)
         (infer-expr alt env type alt^)))
      ((fresh (e* e^* t n)
         (== expr `(vector . ,e*))
         (== expro `(vector ,type . ,e^*))
         (report-backtrack `(vector . ,e*) env)
         (== type `(vec ,n ,t))
         (infer-exprs e* env t e^*)
         (project (e*) (== (length e*) n))))
      ((fresh (c t)
         (== expr `(make-vector (num ,c)))
         (== expro `(make-vector ,t (int ,c)))
         (== type `(vec ,c ,t))))
      ((fresh (op e e^ t n)
         (== expr `(reduce ,op ,e))
         (== expro `(reduce ,type ,op ,e^))
         (report-backtrack `(reduce ,op ,e) env)
         (conde
           ((== op '+))
           ((== op '*)))
         (prefo type '(int float u64))
         (== `(vec ,n ,type) t)
         (infer-expr e env t e^)))
      ((fresh (e e^ t n)
         (== expr `(length ,e))
         (report-backtrack `(length ,e) env)
         (== expro `(length ,e^))
         (== type 'int)
         (infer-expr e env `(vec ,n ,t) e^)))
      ((fresh (c arg)
         (== expr `(iota ,arg))
         (== expro `(iota (int ,c)))
         (conde
           ((== arg `(num ,c)))
           ((fresh (e e^ t)
              (== arg `(length ,e))
              (infer-expr e env `(vec ,c ,t) e^))))
         (== type `(vec ,c int))))
      ((fresh (op e1 e2 e1^ e2^ t)<commit_msg>The type inside a reduce now refers to the type of the inner expression, not the return type.<commit_after>(library
  (harlan front typecheck)
  (export typecheck)
  (import
    (rnrs)
    (util cKanren mk)
    (util cKanren ck)
    (util cKanren typecomp)
    (only (chezscheme) printf pretty-print)
    (harlan compile-opts)
    (util color))

(define-syntax (define-mk x)
  (define trace-mk #f)
  (syntax-case x ()
    ((_ name (lambda (a* ...) body))
     (if trace-mk
         #`(define name
             (lambda (a* ...)
               (fresh ()
                 (project (a* ...)
                   (begin
                     (printf "~s\n" (list 'name a* ...))
                     succeed))
                 body)))
         #`(define name (lambda (a* ...) body))))))

(define-mk pairo
  (lambda (x)
    (fresh (a d)
      (== `(,a . ,d) x))))

(define-mk lookup
  (lambda (env x type)
    (fresh (env^)
      (conde
        ((== `((,x . ,type) . ,env^) env))
        ((fresh (y t)
           (=/= x y)
           (== `((,y . ,t) . ,env^) env)
           (lookup env^ x type)))))))

(define-mk infer-exprs
  (lambda (exprs env type exprso)
    (fresh (expr expro expr* expro*)
      (conde
        ((== exprs '())
         (== exprso '()))
        ((== exprs `(,expr . ,expr*))
         (== exprso `(,expro . ,expro*))
         (infer-expr expr env type expro)
         (infer-exprs expr* env type expro*))))))

(define-mk infer-expr
  (lambda (expr env type expro)
    (conde
      ((fresh (c)
         (== expr `(char ,c))
         (== expro `(char ,c))
         (== type 'char)))
      ((fresh (n)
         (== expr `(num ,n))
         (prefo type '(int float u64))
         (== expro `(,type ,n))))
      ((fresh (n)
         (== expr `(float ,n))
         (== expro `(float ,n))
         (== type 'float)))
      ((fresh (str)
         (== expr `(str ,str))
         (== expro `(str ,str))
         (== type 'str)))
      ((fresh (b)
         (== expr `(bool ,b))
         (== expro `(bool ,b))
         (== type `bool)))
      ((fresh (x)
         (== expr `(var ,x))
         (== expro `(var ,type ,x))
         (lookup env x type)))
      ((fresh (test test^ conseq conseq^ alt alt^)
         (== expr `(if ,test ,conseq ,alt))
         (== expro `(if ,test^ ,conseq^ ,alt^))
         (infer-expr test env 'bool test^)
         (infer-expr conseq env type conseq^)
         (infer-expr alt env type alt^)))
      ((fresh (e* e^* t n)
         (== expr `(vector . ,e*))
         (== expro `(vector ,type . ,e^*))
         (report-backtrack `(vector . ,e*) env)
         (== type `(vec ,n ,t))
         (infer-exprs e* env t e^*)
         (project (e*) (== (length e*) n))))
      ((fresh (c t)
         (== expr `(make-vector (num ,c)))
         (== expro `(make-vector ,t (int ,c)))
         (== type `(vec ,c ,t))))
      ((fresh (op e e^ t n)
         (== expr `(reduce ,op ,e))
         (== expro `(reduce ,t ,op ,e^))
         (report-backtrack `(reduce ,op ,e) env)
         (conde
           ((== op '+))
           ((== op '*)))
         (prefo type '(int float u64))
         (== `(vec ,n ,type) t)
         (infer-expr e env t e^)))
      ((fresh (e e^ t n)
         (== expr `(length ,e))
         (report-backtrack `(length ,e) env)
         (== expro `(length ,e^))
         (== type 'int)
         (infer-expr e env `(vec ,n ,t) e^)))
      ((fresh (c arg)
         (== expr `(iota ,arg))
         (== expro `(iota (int ,c)))
         (conde
           ((== arg `(num ,c)))
           ((fresh (e e^ t)
              (== arg `(length ,e))
              (infer-expr e env `(vec ,c ,t) e^))))
         (== type `(vec ,c int))))
      ((fresh (op e1 e2 e1^ e2^ t)
{'fraction_non_alphanumeric': 0.208955223880597, 'fraction_numerical': 0.0021908804600848965, 'mean_word_length': 1.5601121626358219, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7360413', 'n_tokens_mistral': 2669, 'n_tokens_neox': 2571, 'n_words': 772}