From 5cf1b36e5f6bb93e5faec49bd37d2aa6cb1b7d91 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sun, 14 May 2017 01:23:14 -0400 Subject: - WIP: Function analysis. --- new-luxc/source/luxc/analyser/lux.lux | 144 +++++++++++++++++++++++++++++++++- new-luxc/source/luxc/base.lux | 38 +++++++++ 2 files changed, 181 insertions(+), 1 deletion(-) (limited to 'new-luxc/source') diff --git a/new-luxc/source/luxc/analyser/lux.lux b/new-luxc/source/luxc/analyser/lux.lux index e215412c6..7bce8ed8d 100644 --- a/new-luxc/source/luxc/analyser/lux.lux +++ b/new-luxc/source/luxc/analyser/lux.lux @@ -114,7 +114,7 @@ (TC;check expected actual)) =value (&;with-expected-type Top (analyse eval value))] - (wrap (&common;replace-type actual =value)))) + (wrap (&common;replace-type expected =value)))) (def: (analyse-typed-tuple analyse cursor members) (-> (-> Code (Lux Analysis)) Cursor @@ -253,3 +253,145 @@ (TC;check expected (la;get-type =variant)))] (wrap (&common;replace-type expected =variant))) (&;fail (format "Invalid type for variant: " (%type expected))))))) + +## Functions +(def: (maybe-to-lux input) + (All [a] (-> (Maybe a) (Lux a))) + (case input + #;None + (&;fail "") + + (#;Some value) + (:: Monad wrap value))) + +(def: (with-var body) + (All [a] (-> (-> [Nat Type] (Lux a)) (Lux a))) + (do Monad + [[id var] (&;within-type-env TC;create-var) + output (body [id var]) + _ (&;within-type-env (TC;delete-var id))] + (wrap output))) + +(def: (bind-var var-id bound-idx type) + (-> Nat Nat Type Type) + (case type + (#;Host name params) + (#;Host name (L/map (bind-var var-id bound-idx) params)) + + (^template [] + ( left right) + ( (bind-var var-id bound-idx left) + (bind-var var-id bound-idx right))) + ([#;Sum] + [#;Product] + [#;Function] + [#;App]) + + (#;Var id) + (if (n.= var-id id) + (#;Bound bound-idx) + type) + + (^template [] + ( env quantified) + ( (L/map (bind-var var-id bound-idx) env) + (bind-var var-id (n.+ +2 bound-idx) quantified))) + ([#;UnivQ] + [#;ExQ]) + + (#;Named name unnamed) + (#;Named name + (bind-var var-id bound-idx unnamed)) + + _ + type)) + +(def: #export (analyse-function analyse cursor func-name arg-name body) + (-> (-> Code (Lux Analysis)) Cursor + Text Text Code + (Lux Analysis)) + (do Monad + [expected macro;expected-type] + (&;with-try + (function [error] + (let [raw (format "Functions require function types: " (type;to-text expected))] + (&;fail (if (T/= "" error) + raw + (format error "\n" raw))))) + (case expected + (#;Named name unnamed) + (do @ + [=function (&;with-expected-type unnamed + (analyse-function analyse cursor func-name arg-name body))] + (wrap (&common;replace-type expected =function))) + + (#;App funT argT) + (do @ + [fully-applied (maybe-to-lux (type;apply-type funT argT)) + =function (&;with-expected-type fully-applied + (analyse-function analyse cursor func-name arg-name body))] + (wrap (&common;replace-type expected =function))) + + (#;UnivQ _) + (do @ + [[var-id var] (&;within-type-env + TC;existential) + expected' (maybe-to-lux (type;apply-type expected var)) + =function (&;with-expected-type expected' + (analyse-function analyse cursor func-name arg-name body))] + (wrap (&common;replace-type expected =function))) + + (#;ExQ _) + (with-var + (function [[var-id var]] + (do @ + [expected' (maybe-to-lux (type;apply-type expected var)) + =function (&;with-expected-type expected' + (analyse-function analyse cursor func-name arg-name body))] + (&common;clean var =function)))) + + (#;Var id) + (do @ + [? (&;within-type-env + (TC;bound? id))] + (if ? + (do @ + [expected' (&;within-type-env + (TC;read-var id))] + (&;with-expected-type expected' + (analyse-function analyse cursor func-name arg-name body))) + ## Inference + (with-var + (function [[input-id inputT]] + (with-var + (function [[output-id outputT]] + (do @ + [#let [funT (#;Function inputT outputT)] + =function (&;with-expected-type funT + (analyse-function analyse cursor func-name arg-name body)) + funT' (&;within-type-env + (TC;clean output-id funT)) + concrete-input? (&;within-type-env + (TC;bound? input-id)) + funT'' (if concrete-input? + (&;within-type-env + (TC;clean input-id funT')) + (wrap (#;UnivQ (list) (bind-var input-id +1 funT')))) + _ (&;within-type-env + (TC;check expected funT''))] + (wrap (&common;replace-type expected =function))) + )))))) + + (#;Function inputT outputT) + (do @ + [[=scope =body] (&;with-scope + (&env;with-local [func-name expected] + (&env;with-local [arg-name inputT] + (&;with-expected-type outputT + (analyse body)))))] + (wrap [[expected cursor] + (#la;Function =scope =body)])) + + _ + (&;fail "") + )))) diff --git a/new-luxc/source/luxc/base.lux b/new-luxc/source/luxc/base.lux index 3a085e07e..74e316b3c 100644 --- a/new-luxc/source/luxc/base.lux +++ b/new-luxc/source/luxc/base.lux @@ -99,3 +99,41 @@ (#E;Success [compiler' output]) (#E;Success [(set@ #;source old-source compiler') output]))))) + +(def: #export (with-try handler action) + (All [a] (-> (-> Text (Lux a)) (Lux a) (Lux a))) + (function [compiler] + (case (action compiler) + (#E;Success [compiler' output]) + (#E;Success [compiler' output]) + + (#E;Error error) + ((handler error) compiler)))) + +(def: fresh-bindings + (All [k v] (Bindings k v)) + {#;counter +0 + #;mappings (list)}) + +(def: fresh-scope + Scope + {#;name (list) + #;inner +0 + #;locals fresh-bindings + #;captured fresh-bindings}) + +(def: #export (with-scope action) + (All [a] (-> (Lux a) (Lux [Scope a]))) + (function [compiler] + (case (action (update@ #;scopes (|>. (#;Cons fresh-scope)) compiler)) + (#E;Success [compiler' output]) + (case (get@ #;scopes compiler') + #;Nil + (#E;Error "Impossible error: Drained scopes!") + + (#;Cons head tail) + (#E;Success [(set@ #;scopes tail compiler') + [head output]])) + + (#E;Error error) + (#E;Error error)))) -- cgit v1.2.3