August 2018 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer][graveline] Revised comments and documentation from btl/ and samples/
by Jonathan Graveline 31 Aug '18

31 Aug '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 9fd7015b by Jonathan Graveline at 2018-08-31T21:25:07Z Revised comments and documentation from btl/ and samples/ - - - - - 10 changed files: - btl/builtins.typer - btl/case.typer - btl/do.typer - btl/plain-let.typer - btl/tuple.typer - samples/bbst.typer - samples/decltype.typer - samples/math.typer - samples/myers.typer - samples/table.typer Changes: ===================================== btl/builtins.typer ===================================== @@ -222,7 +222,7 @@ Parser_custom = Built-in "Parser.custom" : Elab_Context -> Sexp -> List Sexp; %% %% Parse an Sexp with the latest context %% -%% (I think previous top level definition should be in the context) +%% (Previous top level definition should be in the context) %% Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp; @@ -308,15 +308,34 @@ Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; %% Ref = typecons (Ref (a : Type)) (Ref a); %% +%% +%% Takes a value +%% Returns a value modifiable in the IO monad +%% and which already contain the specified value +%% Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); + +%% +%% Takes a Ref +%% Returns in the IO monad the value in the Ref +%% Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; + +%% +%% Takes a value and a Ref +%% Returns the an empty command +%% and set the Ref to contain specified value +%% Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; %% %% gensym for macro +%% %% Generate pseudo-unique symbol -%% At least they cannot be obtained outside macro -%% In macro you should NOT use symbol of the form " %gensym% ..." +%% +%% At least they cannot be obtained outside macro. +%% In macro you should NOT use symbol of the form " %gensym% ...". +%% Assume the tree dots to be anything. %% gensym = Built-in "gensym" : Unit -> IO Sexp; @@ -373,7 +392,6 @@ Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; %% %% Print message and/or fail (terminate) -%% These messages are registered like any other error %% And location is printed before the error %% ===================================== btl/case.typer ===================================== @@ -13,6 +13,10 @@ %%%% %%%% Another problem is that this macro is dependent of tuple implementation %%%% +%%%% (It is important to match every variable only once because Typer code +%%%% must always return a value. We cannot just translate to `if then else` +%%%% like construction. Otherwise what will we do if nothing match?) +%%%% %% %% Move IO outside List (from element to List) @@ -45,7 +49,8 @@ gen-vars vars = io-list (List_map %% %% Constructor for a tuple %% -%% Used in patterns +%% Used in patterns to match +%% (expand-tuple-ctor, is-tuple, ...) %% tuple-ctor : Sexp; tuple-ctor = let @@ -81,8 +86,8 @@ in Sexp_dispatch sexp %% %% Is tuple %% -is-tuple : Sexp -> Bool; -is-tuple sexp = let +tuple? : Sexp -> Bool; +tuple? sexp = let sfalse = (lambda _ -> false); @@ -99,7 +104,8 @@ in Sexp_dispatch sexp %% case ... | (expr3,expr4,...) => ... %% %% (This function is now doing nothing since there's only one -%% variable at any time: one expression or a tuple of expressions) +%% variable at any time: one expression or a tuple of expressions. +%% It used to be more useful.) %% get-tup-exprs : Sexp -> List Sexp; get-tup-exprs sexp = let @@ -132,8 +138,8 @@ Code_error = Sexp_symbol "<code error>"; dflt-var : Var; dflt-var = Sexp_symbol "_"; -is-dflt : Var -> Bool; -is-dflt v = Sexp_eq dflt-var v; +dflt? : Var -> Bool; +dflt? v = Sexp_eq dflt-var v; %% %% Takes a list of variable to match and a list of branch as "_=>_"-node @@ -278,7 +284,7 @@ renamed-pat pat names = let %% single expression %% tup : Bool; - tup = is-tuple pat; + tup = tuple? pat; %% %% Get the name of the n'th element of any tuple @@ -375,8 +381,8 @@ in Sexp_dispatch pat %% Takes two pattern and return true if the two pattern %% has the same constructor %% -is-same-ctor : Pat -> Pat -> Bool; -is-same-ctor p0 p1 = let +same-ctor? : Pat -> Pat -> Bool; +same-ctor? p0 p1 = let %% %% error used in Sexp_dispatch @@ -482,7 +488,7 @@ wrap-vars rhs lhs fun = List_fold2 (lambda fun v0 v1 -> %% %% Take a List of branches and return a List of the first pattern in each branches -%% (I must keep the order from input to ouput) +%% (The order must be kept from input to ouput) %% head-pats : List (Pair Pats Code) -> List Pat; head-pats ps = let @@ -569,7 +575,7 @@ pattern-sub-pats-vars rvars branches = let (IO_return (List_mapi (lambda c n -> let new-sym = List_nth n rvars Var_error; prev-sym = List_nth n psubs dflt-var; - in if (is-dflt c) then (prev-sym) else (new-sym) + in if (dflt? c) then (prev-sym) else (new-sym) ) subs)); }; @@ -587,7 +593,7 @@ pattern-term pat rvars = let ff : List (Pair Var Var) -> Var -> Var -> List (Pair Var Var); ff o v0 v1 = - if (is-dflt v0) then + if (dflt? v0) then (o) else (List_concat o (cons (pair v0 v1) nil)); @@ -602,10 +608,13 @@ in do { %% Type of one partition of branches (one branch with child branches) %% %% Pair of -%% Triplet of renamed pat, -%% original variable, -%% variables old/new and original pattern in each branch -%% List of next branch +%% Triplet of renamed pattern, +%% variables from renamed pattern, (list "A") +%% (old, new) variables and original pattern in each branch (list "B") +%% List of next branch (list "C") +%% +%% Take note that "renamed pattern" correspond to all pattern in list "B" +%% and list "C" is the childs of list "B" in the same order. %% part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); @@ -613,6 +622,10 @@ part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var)))) %% Takes a list of branches (pair of (patterns, body)) %% Return a list of partition %% +%% Partitioning is done according to `similar?` pattern +%% for exemple: `cons x xs` is similar to `cons y nil`, +%% even if we may later need to match `xs` or whatever to `nil`. +%% partition-branches : List (Pair Pats Code) -> IO (List part-type); partition-branches branches = let @@ -643,8 +656,10 @@ partition-branches branches = let %% %% Type for first step partition %% - %% Pair of List sorted with similar head - %% they are similar when they have the same constructor + %% Pair of List with similar head + %% they are similar when they have the same constructor. + %% + %% Pair "similar patterns" "child of similar patterns" %% pre-part-type = Pair (List Pat) (List (Pair Pats Code)); @@ -655,8 +670,8 @@ partition-branches branches = let pre-parts : List pre-part-type; pre-parts = let - is-similar : Pat -> Pat -> Bool; - is-similar p0 p1 = is-same-ctor p0 p1; + similar? : Pat -> Pat -> Bool; + similar? p0 p1 = same-ctor? p0 p1; ff : List pre-part-type -> Pair Pat (Pair Pats Code) -> List pre-part-type; ff o p = case p | pair pat tail => (case o @@ -666,13 +681,13 @@ partition-branches branches = let %% default is both equivalent and different from every pattern? %% they are merged with `merge-dflt` - if (is-dflt pat) then + if (dflt? pat) then (case part | pair pp tt => cons (pair (List_concat pp (cons pat nil)) (List_concat tt (cons tail nil))) (ff parts p)) % This line sometimes produce too many patterns else - (if (is-similar pat (List_nth 0 ps Pat_error)) then + (if (similar? pat (List_nth 0 ps Pat_error)) then (case part | pair pp tt => cons (pair (List_concat pp (cons pat nil)) (List_concat tt (cons tail nil))) @@ -685,6 +700,9 @@ partition-branches branches = let %% %% `pre-part-type` to `part-type` %% + %% We here add precomputed info about `similar?` patterns. + %% See `part-type` definition to know which information we must preserve. + %% parts : IO (List part-type); parts = let @@ -725,7 +743,7 @@ in do { %% %% There's a need to merge branch because default branch may be anywhere %% -%% (I tried to consider default branches similar to every patterns +%% (I tried to consider default branches `similar?` to every patterns %% but it failed in some way. So here we are...) %% merge-dflt : List part-type -> Option part-type -> List part-type; @@ -741,9 +759,12 @@ merge-dflt parts odflt = let %% exemple: %% | (x,_,y) => ... %% | (x,k,z) => ... + %% %% In this exemple (and in Typer) I can suppose `y != z` (or there will be warning/error) %% If we take the first case first we did not match `k` and cannot jump to the next - %% But since `y != z` we can safely take the second first + %% But since `y != z` we can safely take the second first. + %% + %% In other word, we can match (k,z) before (_,y) and fall back if k or z did not match. %% preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; @@ -758,6 +779,10 @@ merge-dflt parts odflt = let %% | (x,_,z) => ... %% | (x,_,_) => ... %% + %% Obviously (_,_) will always match so we need to test (_,z) first. + %% (Kind of thing possibly done with "_" `similar?` to everything + %% but we would need `preppend` anyway) + %% append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; append pat vars branches part = case part @@ -767,7 +792,7 @@ merge-dflt parts odflt = let in case parts | cons part parts => (case part | pair p pp => (case p | triplet pat _ vars => - if (is-dflt pat) then + if (dflt? pat) then (case odflt | some dflt => merge-dflt parts (some (append pat vars pp dflt)) | none => merge-dflt parts (some part)) @@ -783,8 +808,8 @@ in case parts %% %% Takes some branches and preppend default variable to smaller branches %% -%% (Sub-pattern introduce new variable but if -%% it fail suplementary variable must match something else) +%% (Sub-pattern introduce new variable so if +%% it fail suplementary variable must match something else (i.e. default: "_")) %% adjust-len : List (Pair Pats Code) -> List (Pair Pats Code); adjust-len branches = let @@ -875,7 +900,7 @@ compile-case subjects branches = let sub-pats-vars <- sub-pats-vars; sub-pats <- IO_return (List_fold2 (lambda o pat var -> - if (is-dflt var) then + if (dflt? var) then (o) else (List_concat o (cons pat nil)) @@ -903,7 +928,7 @@ compile-case subjects branches = let %% r <- IO_return (List_foldl (lambda o v -> - if (is-dflt v) then + if (dflt? v) then (o) else (List_concat o (cons v nil)) ===================================== btl/do.typer ===================================== @@ -98,8 +98,8 @@ in node; %% this way a-sym is defined within b-op and so on %% a-sym is now just `a` and not `IO a` %% -%% ( It could be possible to use `IO Ref` rather than a new variable -%% for each command, but will it be useful? ) +%% (It could be possible to use `IO Ref` rather than a new variable +%% for each command with same lhs symbol, but will it be useful?) %% %% ===================================== btl/plain-let.typer ===================================== @@ -20,6 +20,7 @@ %% %% Takes the plain argument of macro `plain-let` +%% Returns the `plain-let` code %% impl : List Sexp -> IO Sexp; impl args = let ===================================== btl/tuple.typer ===================================== @@ -65,7 +65,7 @@ gen-vars vars = io-list (List_map %% Reference for tuple's implicit field name %% %% Takes a list of vars (it could actually only takes a length) -%% Returns symbol `%n` with n from 0 to the length of the argument +%% Returns symbol `%n` with n in [0,length) (integer only, obviously) %% gen-tuple-names : List Sexp -> List Sexp; gen-tuple-names vars = List_mapi @@ -122,7 +122,7 @@ in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) %% syntax: %% (x, y, z) <- p; %% -%% and then `x`, `y`, `z` are defined from tuple's element 0, 1, 2 +%% and then `x`, `y`, `z` are defined as tuple's element 0, 1, 2 %% assign-tuple = macro (lambda args -> let @@ -153,7 +153,7 @@ in do { }); %% -%% Wrap the third argument (`fun`) with a `let` definition for each variables +%% Wrap the third argument `fun` with a `let` definition for each variables %% Names are taken from `rvars` and definition are taken from `ivars` %% ===================================== samples/bbst.typer ===================================== @@ -144,7 +144,9 @@ length tree = case tree empty? tree = (Int_eq (length tree) 0); %% -%% Check if two value are equal with comparison function only +%% Check if two value are equal with ordering function only +%% +%% (As stated previously: ordering function must be like "<=" or ">=") %% comp-equal : (a : Type) ≡> (a -> a -> Bool) -> a -> a -> Bool; @@ -286,8 +288,10 @@ insert elem tree = let | node-leaf => node3 d0 e k0 node-leaf node-leaf | _ => node2 d0 k0 (helper comp e k1)) + %% %% When doing a recursion I try not to call helper on a node4 %% Because we then would need the parent of this node4 + %% | node3 d0 d1 k0 k1 k2 => if (comp e d0) then @@ -371,8 +375,10 @@ insert elem tree = let | _ => node3 d0 d1 k0 k1 (helper comp e k2))) | node4 d0 d1 d2 k0 k1 k2 k3 => - %% I need the parent of "p" + %% + %% I need the parent of `p` %% But it seems to work with other branch (see above) + %% helper comp e (node2 d1 (node2 d0 k0 k1) (node2 d2 k2 k3)) | node-leaf => node2 e node-leaf node-leaf; @@ -425,7 +431,7 @@ pop-leftmost' comp tree = let in (helper tree); %% -%% Remove the smallest element +%% Remove the smallest element (when using "<=") %% pop-leftmost : (a : Type) ≡> Bbst a -> Bbst a; @@ -476,7 +482,7 @@ pop-rightmost' comp tree = let in (helper tree); %% -%% Remove the greatest element +%% Remove the greatest element (when using "<=") %% pop-rightmost : (a : Type) ≡> Bbst a -> Bbst a; @@ -526,7 +532,7 @@ get-leftmost' comp tree = let in (helper tree); %% -%% Get smallest element +%% Get smallest element (when using "<=") %% get-leftmost : (a : Type) ≡> Bbst a -> Option a; @@ -573,7 +579,7 @@ get-rightmost' comp tree = let in (helper tree); %% -%% Get greatest element +%% Get greatest element (when using "<=") %% get-rightmost : (a : Type) ≡> Bbst a -> Option a; ===================================== samples/decltype.typer ===================================== @@ -42,9 +42,10 @@ take-str : (decl-type str-var) -> (decl-type "123"); take-str s = String_concat s s; %% -%% This is the first exemple where we really need -%% type annotation (with current `##case_`) +%% Next are exemple where we really need +%% type annotation %% + take-bool : (decl-type bool-var) -> (decl-type true); take-bool b = case b | true => false ===================================== samples/math.typer ===================================== @@ -13,20 +13,22 @@ %% With this function we could remove built-in function Int->String %% +Int2String-lut : Array String; +Int2String-lut = list.List->Array + (cons "0" (cons "1" (cons "2" (cons "3" (cons "4" + (cons "5" (cons "6" (cons "7" (cons "8" (cons "9" nil) + ))))))))); + Int2String : Int -> String; Int2String x = let - lut : List String; - lut = cons "0" (cons "1" (cons "2" (cons "3" (cons "4" - (cons "5" (cons "6" (cons "7" (cons "8" (cons "9" nil) - )))))))); - helper : Int -> String; helper x = if (Int_eq x 0) then ("") else - (String_concat (helper (x / 10)) (List_nth (Int_mod x 10) lut "error")); + (String_concat (helper (x / 10)) + (Array_get "error" (Int_mod x 10) Int2String-lut)); in if (Int_eq x 0) then ("0") ===================================== samples/myers.typer ===================================== @@ -98,7 +98,7 @@ nth n l = car (nthcdr n l); set-nth : (a : Type) ≡> Int -> a -> t a -> t a; set-nth n v l = let - % I should use the new case_ macro here! + %% I should use the new case_ macro here! type Helper (a : Type) | pat1 (idx : Int) (data : a) (link1 : t a) (i : Int) (link2 : t a) @@ -229,7 +229,7 @@ map f l = let in foldr fp l mnil; %% -%% Apply all element of a Myers list to a user function +%% Apply all element of a Myers list to a user function (one by one) %% Takes a function and a list %% Returns the length of the list %% ===================================== samples/table.typer ===================================== @@ -43,9 +43,6 @@ in case t %% %% Get the number of element in the tree %% -%% (we could easily keep track of element inserted and removed) -%% (currently O(n)) -%% %% length t = let %% fold-fun len _ = len + 1; View it on GitLab: https://gitlab.com/monnier/typer/commit/9fd7015bd8c351d3a0fb5aa68a2fc6a6d56… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/9fd7015bd8c351d3a0fb5aa68a2fc6a6d56… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] Removed "debug output" in `Ref_make` from src/eval.ml
by Jonathan Graveline 30 Aug '18

30 Aug '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: a1747386 by Jonathan Graveline at 2018-08-30T20:16:35Z Removed "debug output" in `Ref_make` from src/eval.ml samples/decltype.typer: another version of `decltype` implemented in Typer samples/math.typer: a toy math library - - - - - 3 changed files: - + samples/decltype.typer - + samples/math.typer - src/eval.ml Changes: ===================================== samples/decltype.typer ===================================== @@ -0,0 +1,57 @@ +%%%% +%%%% Declaring the type of an expression +%%%% directly in Typer +%%%% + +%% +%% It mostly work as exemples below work fine +%% but I can't do somethings like: +%% y = decl-type x; +%% + +decl-type = lambda (t : Type) => lambda (_ : t) -> t; + +%% +%% Some tests and exemples +%% + +int-var : Int; +int-var = 100; + +%% +%% Error "Metavar in erase_type": +%% int = decl-type int-var; +%% + +flt-var : Float; +flt-var = 0.1; + +str-var : String; +str-var = "abc"; + +bool-var : Bool; +bool-var = true; + +take-int : (decl-type int-var) -> (decl-type 1); +take-int n = n + n; + +take-flt : (decl-type flt-var) -> (decl-type 1.0); +take-flt x = Float_+ x x; + +take-str : (decl-type str-var) -> (decl-type "123"); +take-str s = String_concat s s; + +%% +%% This is the first exemple where we really need +%% type annotation (with current `##case_`) +%% +take-bool : (decl-type bool-var) -> (decl-type true); +take-bool b = case b + | true => false + | false => true; + +rec-int : (decl-type int-var) -> (decl-type int-var); +rec-int n = if (Int_> n 0) then + (n + rec-int (n - 1)) + else + (0); ===================================== samples/math.typer ===================================== @@ -0,0 +1,244 @@ +%%%% +%%%% Sample math library. +%%%% +%%%% Basic math function, constant, etc. +%%%% +%%%% This file is only an exemple. There is probably multiple +%%%% design errors (precision lost, bad algorithm choice, etc). +%%%% + +%% +%% Get the string decimal representation of an Int +%% +%% With this function we could remove built-in function Int->String +%% + +Int2String : Int -> String; +Int2String x = let + + lut : List String; + lut = cons "0" (cons "1" (cons "2" (cons "3" (cons "4" + (cons "5" (cons "6" (cons "7" (cons "8" (cons "9" nil) + )))))))); + + helper : Int -> String; + helper x = + if (Int_eq x 0) then + ("") + else + (String_concat (helper (x / 10)) (List_nth (Int_mod x 10) lut "error")); + +in if (Int_eq x 0) then + ("0") + else + (helper x); + +%% +%% Factorial +%% +%% Shouldn't be calculated recursively but an Int isn't bigger than `fact 20;` +%% This function isn't safe +%% + +fact : Int -> Int; +fact n = + if (Int_eq 1 n) then 1 else (n * (fact (n - 1))); + +Int_abs : Int -> Int; +Int_abs n = if (Int_< n 0) then (0 - n) else n; + +Float_abs : Float -> Float; +Float_abs x = if (Float_< x 0.0) then (Float_- 0.0 x) else x; + +Float_mod : Float -> Float -> Float; +Float_mod x y = Float_- x (Float_* (Float_trunc (Float_/ x y)) y); + +%% +%% Cool math constant +%% + +pi : Float; +e : Float; + +pi = 3.141592653589793; +e = 2.718281828459045; + +%% +%% Get square root of number 'a' +%% + +sqrt : Float -> Float; +sqrt a = let + + x : Float; + x = (Float_/ a 4.0); + + sqrtp : Int -> Float -> Float; + sqrtp n x = + let xp = (Float_/ (Float_+ x (Float_/ a x)) 2.0) in + if (Int_eq n 32) then % maybe 32 isn't enough iteration ? + xp + else + (sqrtp (n + 1) xp); + +in sqrtp 0 x; + +%% +%% Power +%% +%% Only for positive integer exponent +%% +%% (Using a divide-and-conquer algorithm) +%% + +Floatpow : Float -> Int -> Float; +Floatpow x n = let + + powp : Float -> Int -> Float; + powp xp np = + if (Int_eq np 1) then + xp + else + (if (Int_eq (Int_mod np 2) 0) then + (powp (Float_* xp xp) (np / 2)) + else + (Float_* xp (powp (Float_* xp xp) ((np - 1) / 2)))); + +in powp x n; + +Intpow : Int -> Int -> Int; +Intpow x n = let + + powp : Int -> Int -> Int; + powp xp np = + if (Int_eq np 1) then + xp + else + (if (Int_eq (Int_mod np 2) 0) then + (powp (xp * xp) (np / 2)) + else + (xp * (powp (xp * xp) ((np - 1) / 2)))); + +in powp x n; + +%% +%% Sinus and Cosinus +%% +%% (Using Taylor series...) +%% +%% (Probably not the best algorithm for this) +%% + +%% +%% truncRadian keep `x` between 0 and 2pi +%% (It "trunc" all complete circle) +%% +truncRadian : Float -> Float; +truncRadian x = Float_mod x (Float_* 2.0 pi); + +%% +%% Implementation of both sinus and cosinus +%% (they just have different parameters) +%% +sinusoidaleTaylor : Int -> Float -> Float -> Float -> Float -> Float -> Float; +sinusoidaleTaylor iter y xp x n i = let + + _fact : Float -> Float; + _fact n = + if (Float_eq 1.0 n) then + 1.0 + else + (Float_* n (_fact (Float_- n 1.0))); + + ii : Float; + ii = Float_- 0.0 1.0; + + x2 : Float; + x2 = Float_* y y; + + sinusoidaleTaylorp : Int -> Float -> Float -> Float -> Float -> Float; + sinusoidaleTaylorp iter xx xp n i = + let + xxp : Float; xxp = Float_* xx x2; + np : Float; np = Float_+ n 2.0; + in if (Int_eq iter 0) then + xp + else + (sinusoidaleTaylorp (iter - 1) + xxp + (Float_+ xp (Float_* i (Float_/ xxp (_fact np)))) + np + (Float_* i ii)); + +in sinusoidaleTaylorp iter xp x n i; + +sin : Float -> Float; +sin x = let + + %% + %% I got error with value outside [0,360] + %% (It could be a precision lost or an error in sinusoidaleTaylor) + %% + xp : Float; + xp = truncRadian x; + +in sinusoidaleTaylor 20 xp xp xp 1.0 (-1.0); + +%% +%% cos is exactly like sin but start somewhere else +%% +cos : Float -> Float; +cos x = let + + %% + %% I got error with value outside [0,360] + %% (It could be a precision lost or an error in sinusoidaleTaylor) + %% + xp : Float; + xp = truncRadian x; + +in sinusoidaleTaylor 20 xp 1.0 1.0 0.0 (-1.0); + +%% +%% Random number generator +%% +%% Linear congruential +%% + +type Rand-Data + | rand-data (last : Int) (fun : (Int -> Int)); + +rand-gen : Int -> Int -> Int -> IO (Ref Rand-Data); +rand-gen min max seed = let + + a : Int; a = 1664525; + b : Int; b = 1013904223; + c : Int; c = 123456789; % probably a bad choice (reduce the period length?) + + range : Int; + range = max - min + 1; + + inrange : Int -> Int; + inrange s = min + (Int_mod (Int_abs s) range); + + randp : Int -> Int; + randp r = inrange ((a * r + b) * c); + +in Ref_make (rand-data seed randp); + +rand-next : Ref Rand-Data -> IO Int; +rand-next ref-data = do { + data <- Ref_read ref-data; + + last <- IO_return ( case data + | rand-data last _ => last ); + + f <- IO_return ( case data + | rand-data _ f => f ); + + rand <- IO_return (f last); + + Ref_write (rand-data rand f) ref-data; + + IO_return rand; +}; ===================================== src/eval.ml ===================================== @@ -723,7 +723,7 @@ let nop_fun loc _ vs = match vs with | _ -> error loc "Wrong number of argument to nop" let ref_make loc depth args_val = match args_val with - | [v] -> Vcommand (fun () -> print_string "\n\tIN REF_MAKE\n\n"; Vref (ref v)) + | [v] -> Vcommand (fun () -> Vref (ref v)) | _ -> error loc "Ref.make takes a single value as argument" let ref_read loc depth args_val = match args_val with View it on GitLab: https://gitlab.com/monnier/typer/commit/a17473862e54f2452061c3f34d688277726… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/a17473862e54f2452061c3f34d688277726… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][bosn] Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation;…
by Nathaniel 30 Aug '18

30 Aug '18

Nathaniel pushed to branch bosn at Stefan / Typer Commits: 89aecbb1 by nbos at 2018-08-30T09:05:45Z Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation; expand on guarded by destructors predicate D - - - - - 1 changed file: - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/typer_theory.tex ===================================== @@ -25,8 +25,8 @@ The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructi \begin{itemize} \renewcommand{\labelitemi}{$-$} \setlength\itemsep{-3pt} -\item An infinite hierarchy of predicative type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity; -\item A parallel hierarchy of impredicative universes +\item An infinite hierarchy of type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity; +\item Product rules that allow for both predicative and impredicative arguments and abstractions in every universe; \item Universe polymorphism allowing the parametrization of type universes; \item Erasure of propositional arguments with decidable type checking from Barras and Bernardo's variant of Miquel's Implicit Calculus of Constructions (ICC) \cite{bruno}\cite{miquel}; \item Inductive definitions as presented by Gim\'enez in \cite{gimenez}. @@ -99,7 +99,7 @@ After elaboration, implicit terms behave exactly like explicit terms so we will \caption{Extraction function $M \mapsto M^*$} \label{fig:*} \end{figure} -We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules for Typer are shown in figure \ref{fig:Typing-rules}. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms. +We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules shown in figure \ref{fig:Typing-rules} are the rules from Barras and Bernardo's ICC \cite{bruno}. \begin{figure}[h] \ \\ \ \\ \fbox{ @@ -158,7 +158,7 @@ We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \\ \end{mathpar} } - \caption{Typer's Typing Rules} + \caption{Typer's Typing Rules from ICC} \label{fig:Typing-rules} \end{figure} @@ -226,9 +226,9 @@ The typing rules for inductive definitions and case analysis are presented in fi %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq_refl : ((x : ?t) ≡> Eq x x); %% Eq_cast : (x : ?t) ≡> (y : ?t) - %% ≡> (p : Eq x y) - %% ≡> (f : ?t -> ?t') - %% ≡> f x -> f y; + %% . ≡> (p : Eq x y) + %% . ≡> (f : ?t -> ?t') + %% . ≡> f x -> f y; %% %% At run-time `Eq_cast` will be a no-op (i.e. `Eq_cast x` will reduce %% to `x`), but there is no corresponding normalization rule applied @@ -279,16 +279,18 @@ Recursion is specified through the use of a recursive operator \Letrec \todo A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP\{i,C\}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. \end{definition} \begin{definition} - The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\bigwedge_i \D_\V\{M_i\}$. The condition $\D_\V\{M\} = \D_\V\{f,k,x,M\}$ is determined by structural induction on term $M$: + The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity instead of the full $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\bigwedge_i \D_\V\{M_i\}$. By structural induction on term $M$, we describe when $\D_\V\{M\} = \D_\V\{f,k,x,M\}$ is true by assigning conjunctions of necessary conditions to each form of $M$: \begin{align*} - \D_\V\{M\} && = && \text{True} && \text{if } f \notin \fv{M}\\ - \D_\V\{\la (z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ - \D_\V\{(z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ - \D_\V\{\Letrec ?\} && = && \ ? \\ - \D_\V\{\Ind(X\:A)\<\vec{C}\>\} && = && \D_\V\{A\} \land \D_\V\{\vec{C}\} \\ - \D_\V\{f \vec{P}\} && = && (|\vec{P}| > k) \land (P_{k+1} \equiv (z\vec{Q}) \land \D_\V\{\vec{P}\} \\ - \D_\V\{\Case\ N\:S \text{ of } \<\vec{G}\>\} \todo\\ - \D_\V\{N \vec{P}\} \todo\\ + \D_\V\{M\} & = \text{True} & \text{if } f \notin \fv{M}\\ + \D_\V\{\la (z:P)\to Q\} & = \D_\V\{P\} \land \D_\V\{Q\} \\ + \D_\V\{(z:P)\to Q\} & = \D_\V\{P\} \land \D_\V\{Q\} \\ + \D_\V\{\Letrec ?\} & = \ ? \\ + \D_\V\{\Ind(X\:A)\<\vec{C}\>\} & = \D_\V\{A\} \land \D_\V\{\vec{C}\} \\ + \D_\V\{f \vec{P}\} & = (|\vec{P}| > k) \land (P_{k+1} \equiv (z\ \vec{Q})) \land \D_\V\{\vec{P}\} & \text{with $z \in \V$}\\ + \D_\V\{N \vec{P}\} & = \D_\V\{N\} \land \D_\V\{\vec{P}\} &\text{if $N \neq f$}\\ + \D_\V\{\Case\ (z\ \vec{P})\:S \text{ of } \<\vec{G}\>\} & = \D_\V\{Q\} \land \D_\V\{S\} \land \D_\V\{\vec{P}\} &\text{with $z \in \V \cup \{x\}$}\\ + & \quad \land S \equiv I\vec{R} & \text{with }I =\Ind (X:A)\<\vec{C}\> \\ + & \quad \land \text{if } \end{align*} \end{definition} @@ -388,7 +390,7 @@ In this section we will show that the erasable terms of Typer allows for a repre Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, to which we add an infinite hierarchy of predicative universes above an impredicative \Prop. Thus we have: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$ -\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,j)})$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}). +\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, where the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,j)})$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}). \subsection{Translation} \begin{figure}[h] @@ -412,7 +414,7 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \ \end{cases}\\ \rew{M \ap N} &= \begin{cases} - \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(T:\tau':\Type_i)$} \\ + \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(N:\tau':\Type_i)$} \\ \rew{M}|\rew{N} &\text{otherwise} \end{cases}\\ \rew{U\{N/x\}} &= \rew{U}\{\rew{N}/x\}\\ @@ -434,7 +436,7 @@ The translator operator \rew{\_} is defined on contexts and terms of \CC. We exp \end{align*} \end{theorem} -Before proving the correctness of the equality, we need the following lemmas: +Before proving the correctness of the equality, we show the following lemmas: \begin{lemma} \label{lem:S-equiv} $s \in \S_{CC} \iff \rew{s} \in \S$ @@ -517,6 +519,222 @@ Before proving the correctness of the equality, we need the following lemmas: \end{proof} \end{lemma} +\begin{lemma} + \label{lem:E-Lam-FV} + If we have + \begin{mathpar} + % Induction on derivations in CCω is used because induction on + % derivations of translated terms in Typer can lead to a case + % (e.g. X-App) where it is possible to insert a term absent in CCω + % (e.g. an explicit abstraction of a higher sort over a body of sort + % Type z) in the derivation tree, thus allowing variable 'y' to appear + % free in the term + + % So instead of using this lemma (in completeness, case:E-Lam) with the + % translated premises, we can use it with the initial (CCω) ones + {\Ga, y:V \CCdash P:W \\ \Ga, y:V \CCdash W : \Prop \\ \Ga \CCdash V : \Type_i} + \end{mathpar} + then the following always holds + $$y \notin \fv{\rew{P}^*}$$ + + \begin{proof} + By induction on the typing derivation $\Ga, y:V \CCdash P:W$, either a typing rule is not applicable to this derivation or we show that it satisfies $y \notin \fv{\rew{P}^*}$. + + \textbf{CC-Sort:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} + \tag{CC-Sort} + \end{mathpar} + All axioms of $\A_{CC}$ are constructed with sorts $s_1, s_2 \in \S_{CC}$. There are no sorts in $\S_{CC}$ smaller than $\Prop$. Since here $s_2$ is $W$ and by assuption $W : \Prop$, then no axiom $(s_1:s_2) \in \A_{CC}$ will match $(P:W)$ and this typing rule cannot apply. + + \textbf{CC-Var:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash \\ (x:T) \in \Ga} + {\Ga \CCdash x:T} + \tag{CC-Var} + \end{mathpar} + Considering that typing judgments are introduced in contexts exclusively by means of rule \textsc{CC-Wf-S}, we can assume + \begin{mathpar} + {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + \end{mathpar} + which all holds by the assignment $s = \Prop$. Thus, $P$ (here $x$) is a variable. The translation and extraction for the variable leaves it untouched + $$\rew{P}^* = P^* = P$$ + Because $y : V : \Type_i$ and $P : W : \Prop$, we have that $y \neq P$ because they are variables that inhabit different universes so it follows that $y \notin \fv{P}$. + + \textbf{CC-Prod:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : \s_3} + \tag{CC-Prod} + \end{mathpar} + Similarly to case \textsc{CC-Sort}, we cannot apply this rule because here $s_3 = W$ and by assumption $W : \Prop$ and \Prop\ is the smallest universe in $\S_{CC}$. So no rule $(s_1,s_2,s_3) \in \R_{CC}$ can match in this case. + + \textbf{CC-Lam:}\\ + \begin{mathpar} + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \tag{CC-Lam} + \end{mathpar} + Sort $s$ here is $\Prop$ because $(x:T) \explicit U$ is $W$ and by assumption $W : \Prop$. The construction of $(x:T) \explicit U$ reveals that $U : \Prop$ because every rule $(s_1,s_2,s_3) \in \R_{CC}$ that has $s_3 = \Prop$ also has $s_2 = \Prop$: + \begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:\Prop \\ (s_1,\Prop,\Prop) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : \Prop} + \tag{CC-Prod} + \end{mathpar} + The translation for the lambda abstraction $\la(x:T) \explicit M$ has a predicative and impredicative case. In both cases, however, the extraction erases the type annotation $\rew{T}$. Therefore $\fv{\rew{P}^*} = \fv{\rew{M}^*}$ and $y \notin \fv{\rew{M}^*}$ holds by the induction hypothesis because $M : U : \Prop$. + + \textbf{CC-App:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} + \tag{CC-App} + \end{mathpar} + Here $P = M|N$ and $W = U\{N/x\}$. $y \notin \fv{\rew{P}^*}$ will hold if we can show that $y \notin \fv{\rew{M}^*}$ and---unless $N$ is an impredicative argument---$y \notin \fv{\rew{N}^*}$. By assumption $U\{N/x\} : \Prop$ + %% Does this step really hold? + and therefore also $U : \Prop$. It follows that $(x:T)\explicit U : \Prop$ by the typing rule \textsc{CC-Prod}. Thus, by induction hypothesis, we have $y \notin \fv{\rew{M}^*}$ because $M : (x:T)\explicit U : \Prop$. If $N : T : \Prop$, then we can also apply the induction hypothesis. Otherwise, the extraction on the translation erases the impredicative argument completely. + + \end{proof} + + %% **PURGATORY** ATTEMPTED PROOF ON TYPER DERIVATIONS + %\textbf{Sort:}\\ + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} + % {\rew{\Ga, y:V} \~ \rew{s_1}:\rew{s_2}} + % \tag{Sort} + % \end{mathpar} + % \textsc{Sort} is not applicable to this derivation because $\rew{W}$ is set to have sort $\Type\ \z$ but there is no sort $\rew{s_2}$ that has sort $\Type\ \z$ because it is itself the smallest sort. + + % \textbf{Var:}\\ + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ \\ (x:\rew{T}) \in \rew{\Ga, y:V}} + % {\rew{\Ga, y:V} \~ x:\rew{T}} + % \tag{Var} + % \end{mathpar} + % It is not possible that $x = y$ because that would imply that their types satisfy $\rew{T} = \rew{V}$ (i.e. $\rew{W} = \rew{V}$) and, further, that their unverses satisfy $\Type\ (\s\ \l) = \Type\ \z$ which is false. Then, $x \neq y$ and we have that $$y \notin \fv{x^*} ~~ \equiv ~~ y \notin \fv{x}$$ because $x$ and $y$ are different variables. + + % \textbf{X-Prod \& E-Prod:}\\ + % Both \textsc{X-Prod} and \textsc{E-Prod} do not apply because both would set $\rew{W}$ to be a sort: + % $${\rew{\Ga, y:V} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}}$$ + % $$\rew{\Ga, y:V} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}$$ + + % but $\rew{W} : \Type\ \z$ and there is no sort that has sort $\Type\ \z$, because it is the smallest sort. + + % \textbf{X-Lam:}\\ + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, y:V} \~ (x:\rew{T}) \explicit \rew{U} : s} + % {\rew{\Ga, y:V} \~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} + % \tag{X-Lam} + % \end{mathpar} + + % We know that $s = \Type\ \z$ because here $\rew{W} = (x:\rew{T})\explicit \rew{U}$ and by assumption $\rew{W} : \Type\ \z$. By the construction of the explicit product $(x:\rew{T}) \explicit \rew{U}$, we have + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ \rew{T}:s_1 \\ \rew{\Ga, y:V, x:T} \~ \rew{U}:s_2 \\ (s_1,s_2,\Type\ \z) \in \R} + % {\rew{\Ga, y:V} \~ (x:\rew{T}) \explicit \rew{U} : \Type\ \z} + % \tag{X-Prod} + % \end{mathpar} + % The only rule in $\R$ that matches $(s_1,s_2,\Type\ \z)$ is $(\Type\ \z, \Type\ \z, \Type\ \z)$ where, in particular, $s_2 = \Type\ \z$ and therefore $\rew{U} : \Type\ \z$. The extraction $\rew{P}^*$ here is: + % $$(\la(x:\rew{T}) \explicit \rew{M})^* = \la (x) \explicit \rew{M}^*$$ + % Therefore, + % $$\fv{(\la(x:\rew{T}) \explicit \rew{M})^*} = \fv{\rew{M}^*}$$ + % And we have + % \begin{mathpar} + % {\rew{\Ga, y:V, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, y:V} \~ \rew{U} : \Type\ \z} + % \end{mathpar} + % so by the induction hypothesis, we can assume + % $$y \notin \fv{\rew{M}^*}$$ + + % \textbf{E-Lam:}\\ + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, y:V} \~ (x:\rew{T}) \erasable \rew{U} : s \\ x \notin \fv{\rew{M}^*}} + % {\rew{\Ga, y:V} \~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} + % \tag{E-Lam} + % \end{mathpar} + + % Similarly, here we know that $s = \Type\ \z$ because $\rew{W} : \Type\ \z$. By the construction of the erasable product $(x:\rew{T}) \erasable \rew{U}$, we have + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ \rew{T}:s_1 \\ \rew{\Ga, y:V, x:T} \~ \rew{U}:\Type\ \z \\ (s_1,\Type\ \z,\Type\ \z) \in \R_e} + % {\rew{\Ga, y:V} \~ (x:\rew{T}) \erasable \rew{U} : \Type\ \z} + % \tag{E-Prod} + % \end{mathpar} + % The extraction is + % $$(\la(x:\rew{T}) \erasable \rew{M})^* = \la (x) \erasable \rew{M}^*$$ + % Therefore, + % $$\fv{(\la(x:\rew{T}) \erasable \rew{M})^*} = \fv{\rew{M}^*}$$ + % And we have + % \begin{mathpar} + % {\rew{\Ga, y:V, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, y:V} \~ \rew{U} : \Type\ \z} + % \end{mathpar} + % so by the induction hypothesis, we can assume + % $$y \notin \fv{\rew{M}^*}$$ + + % \textbf{X-App:}\\ + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ \rew{M} : (x:T) \explicit \rew{U} \\ \rew{\Ga, y:V} \~ \rew{N}:T} + % {\rew{\Ga, y:V} \~ \rew{M}|\rew{N} : \rew{U}\{\rew{N}/x\}} + % \tag{X-App} + % \end{mathpar} + % We know that $\rew{U}\{\rew{N}/x\} : \Type\ \z$ because here $\rew{W} = \rew{U}\{\rew{N}/x\}$ and by assumption $\rew{W} : \Type\ \z$. + % %% FIXME: Does the next sentence really hold? + % Because $\rew{U}\{\rew{N}/x\} : \Type\ \z$, we also have $\rew{U} : \Type\ \z$. By the construction of the explicit product, we have + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ T:s_1 \\ \rew{\Ga, y:V}, x:T \~ \rew{U}:\Type\ \z \\ (s_1,\Type\ \z,s_3) \in \R} + % {\rew{\Ga, y:V} \~ (x:T) \explicit \rew{U} : s_3} + % \tag{X-Prod} + % \end{mathpar} + % The only rule in $\R$ that matches $(s_1,\Type\ \z,s_3)$ is $(\Type\ \z, \Type\ \z, \Type\ \z)$ where, in particular, $\rew{U} : \Type\ \z$. + + % Because $\rew{M}|\rew{N}$ is a translated term $\rew{P} = \rew{M|N}$ whose translation is not an erasable application, by the definition of the translation (figure \ref{fig:[]}): + % \begin{align*} + % \rew{M \ap N} &= + % \begin{cases} + % \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(N:\tau':\Type_i)$} \\ + % \rew{M}|\rew{N} &\text{otherwise} + % \end{cases} + % \end{align*} + % we infer that either $M$ has a type of a sort other than $\Prop$ or $N$ has a type of sort \Prop. We know that + % \begin{align*} + % sssss + % \end{align*} + + + % The extraction $\rew{P}^*$ here is: + % $$(\la(x:\rew{T}) \explicit \rew{M})^* = \la (x) \explicit \rew{M}^*$$ + % Therefore, + % $$\fv{(\la(x:\rew{T}) \explicit \rew{M})^*} = \fv{\rew{M}^*}$$ + % And we have + % \begin{mathpar} + % {\rew{\Ga, y:V, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, y:V} \~ \rew{U} : \Type\ \z} + % \end{mathpar} + % so by the induction hypothesis, we can assume + % $$y \notin \fv{\rew{M}^*}$$ + + + % \textbf{E-App:}\\ + % \begin{mathpar} + % \infer + % {\rew{\Ga, y:V} \~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \\ \rew{\Ga, y:V} \~ \rew{N}:\rew{T}} + % {\rew{\Ga, y:V} \~ \rew{M}|||\rew{N} : \rew{U}\{\rew{N}/x\}} + % \tag{E-App} + % \end{mathpar} + + % \end{proof} + +\end{lemma} \subsection{Completeness of translation} By structural induction on typing derivation, as per theorem \ref{thm:correctness-translation} ($\Rightarrow$), each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof consists in assuming the translated premises by the induction hypothesis and then showing that the translation of the conclusion from them by one of Typer's typing rules. @@ -608,6 +826,7 @@ By the induction hypothesis we can assume $$\rew{\Ga} \~$$ \begin{lemma} + \label{lem:in-ctx-equiv} The following holds: $$(x:T) \in \Ga \iff (x:\rew{T}) \in \rew{\Ga}$$ \begin{proof} @@ -685,70 +904,7 @@ The predicative product type translates to an explicit product type $(x:\rew{T}) \end{mathpar} \textbf{Impredicative subcase:}\\ -The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort $\rew{\Prop} = \Type\ \z$. To apply the corresponding Typer rule \textsc{E-Lam}, we must first show that $x \notin \fv{\rew{M}^*}$. - -\begin{lemma} - \label{lem:E-Lam-FV} - If we have - \begin{mathpar} - %% FIXME: I am limiting the proof to translated terms because - %% 1) We don't need more than this - %% 2) The lemma doesn't seem to hold otherwise; e.g. - %% M := P|Q - %% M := λ(y:T)->V | x - %% - %% where V : U : Type0 so that (λ(y:T)->V | x) : U : Type0 - %% - %% Now, I don't know where y would appear in V while respecting V : U - %% and y : T, but we still have x ∈ FV(λ(y:T)->V | x) which is enough - %% as far as I know to disprove the lemma. This is not a counterexample - %% if we limit the lemma to translated terms [M] because the rule - %% (Type₁,Type₀,Type₁) ∉ Rcc, but instead (Type₁,Type₀,Type₀) ∈ R which - %% makes the abstraction erasable in Typer and thus, x is not free - {\rew{\Ga, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, x:T} \~ \rew{U} : \Type\ \z \\ \rew{\Ga} \~ \rew{T} : \Type\ (\s\ \l)} - \end{mathpar} - then the following always holds - $$x \notin \fv{\rew{M}^*}$$ - - \begin{proof}\ \\ - By structural induction on $\rew{M}^*$: - - \textbf{Case} $\rew{M}^* = y^*$:\\ - The extraction is $y^* = y$. It cannot be that $y = x$ because $x : \rew{T} : \Type (\s\ \l)$ and $y : \rew{U} : \Type\ \z$ and equality is not defined between inhabitants of different types nor of different universes. Therefore, $x \notin \fv{y}$ because $x \neq y$. - - \textbf{Case} $\rew{M}^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\\ - $\rew{M}$ cannot be a product type since its type $\rew{U}$ inhabits the smallest universe $\Type\ \z$ . - - %% FIX\rew{M}E: This shows a problem in our presentation. We use FV(\rew{M}*) and we - %% define * but we don't define FV. Another option is to forget about * - %% and only define FV*(\rew{M}), the set of non-erasable free variables. - \textbf{Case} $\rew{M}^* = \rew{s}^*$ with $\rew{s} \in \S$:\\ - The extraction is $\rew{s}^* = \rew{s}$. All $\rew{s} \in S$ are closed constants and thus $x \notin \fv{\rew{s}}$. - - \textbf{Case} $\rew{M}^* = (\la(y:t)\explicit V)^*$:\\ - The extraction makes this $\la(y)\explicit V^*$. By the rules in $\R$, if $\rew{M}$ has sort $\Type\ \z$, then it is an upper bound for the sort of $V$. Thus, $V : U' : \Type\ \z$ and we have $x \notin \fv{V^*}$ by the induction hypothesis. - - \textbf{Case} $\rew{M}^* = (\la(y:t)\erasable V)^*$:\\ - The extraction makes this $V^*$. By the rules in $\R_e$, if $\rew{M}$ has sort $\Type\ \z$, then $V$ also has sort $\Type\ \z$. Thus, by the induction hypothesis, $x \notin \fv{V^*}$. - - \textbf{Case} $\rew{M}^* = (P \ap Q)^*$:\\ - The extraction is $(P \ap Q)^* = P^* \ap Q^*$. By the typing rule \textsc{X-App}, because $P \ap Q : \rew{U}$, then $$P : (y:t)\explicit \rew{U}\{Q/y\}$$ - %% FIXME: I'm not sure about this "reverse substitution" business - %% happening above. - %% FIXME: Also, are contexts necessary here? - for $t$ such that $Q:t$. Further, since $\rew{U} : \Type\ \z$ and because the only rules that match $(s_1,\Prop,s_3) \in R_{CC}$ have $s_3 = \Prop$ then by induction hypothesis on the completeness of the translation, we can infer $$(y:t)\explicit \rew{U}\{Q/y\} : \Type\ \z$$ -and thus assume $x \notin \fv{P^*}$ by induction hypothesis on this lemma---although only the cases of the variable, the lambda abstraction and the applications apply. Because the product type of $P$ is explicit, the sort of $Q$ is also upper bounded by $\Type\ \z$ because explicit product types occur by the application of \textsc{X-Prod} with a rule that has $s_3 = \max (s_1,s_2)$. Thus we have $x \notin \fv{Q^*}$ by the induction hypothesis. - - - \textbf{Case} $\rew{M}^* = (P \appp Q)^*$:\\ - The extraction is $(P \appp Q)^* = P^*$. Similar to the previous case, because $P$ has the same sort as $\rew{M}$, we have $x \notin \fv{P^*}$ by induction hypothesis. - \end{proof} -\end{lemma} - -By lemma \ref{lem:E-Lam-FV} above, we can infer -$$x \notin \fv{M^*}$$ - -and we have the sufficient premises to apply rule \textsc{E-Lam} and we obtain the translation of the conclusion: +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort $\rew{\Prop} = \Type\ \z$. We call upon lemma \ref{lem:E-Lam-FV} to infer that $x \notin \fv{\rew{M}^*}$ and we have the sufficient premises to apply rule \textsc{E-Lam} and we obtain the translation of the conclusion: \begin{mathpar} \infer {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \\ x \notin \fv{\rew{M}^*}} @@ -807,13 +963,22 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E} \underline{\textbf{Wf-S:}}\\ \begin{mathpar} \infer - {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} + {\rew{\Ga} \~ \rew{T}:s \\ s \in \S \\ x \notin \dv{\rew{\Ga}}} {\rew{\Ga} , x:\rew{T} \~} \tag{WF-S} \end{mathpar} +By lemma \ref{lem:S-equiv}, we can infer from $s \in \S$ that $s' \in \S_{CC}$ for some $s'$ such that $s = \rew{s'}$. We can assume +\begin{mathpar} + {\Ga \CCdash T:s'} +\end{mathpar} +by the induction hypothesis, since $s = \rew{s'}$. Finally, +\begin{mathpar} + x \notin \dv{\Ga} +\end{mathpar} +is shown by means of lemma \ref{lem:not-DV-equiv}. Thus, we can reconstruct the inference step \textsc{CC-Wf-S}: \begin{mathpar} \infer - {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + {\Ga \CCdash T:s' \\ s' \in \S_{CC} \\ x \notin \dv{\Ga}} {\Ga , x:T \CCdash} \tag{CC-Wf-S} \end{mathpar} @@ -825,6 +990,11 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E} {\rew{\Ga} \~ \rew{s_1}:\rew{s_2}} \tag{Sort} \end{mathpar} +By lemma \ref{lem:A-equiv}, we can infer from $(\rew{s_1}:\rew{s_2}) \in \A$ that $(s_1:s_2) \in \A_{CC}$. We can assume +\begin{mathpar} + {\Ga \CCdash} +\end{mathpar} +by the induction hypothesis. Therefore we have the rule: \begin{mathpar} \infer {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} @@ -839,6 +1009,11 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E} {\rew{\Ga} \~ x:\rew{T}} \tag{Var} \end{mathpar} +By lemma \ref{lem:in-ctx-equiv}, we can infer from $(x:\rew{T}) \in \rew{\Ga}$ that $(x:T) \in \Ga$ and we have +\begin{mathpar} + \Ga \CCdash +\end{mathpar} +by the induction hypothesis. We get: \begin{mathpar} \infer {\Ga \CCdash \\ (x:T) \in \Ga} @@ -847,17 +1022,18 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E} \end{mathpar} \underline{\textbf{X-Prod:}}\\ -Where $s_1 \neq \Type_1$ or $s_2 \neq \Prop$: +Where $s_1 \neq \Type_i$ or $s_2 \neq \Prop$: \begin{mathpar} \infer - {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} - {\rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}} + {\rew{\Ga} \~ \rew{T}:s_1 \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:s_2 \\ (s_1,s_2,\rew{s_3'}) \in \R} + {\rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3'}} \tag{X-Prod} \end{mathpar} +By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that $(s_1',s_2',s_3') \in \R_{CC}$ for some $s_1'$ and $s_2'$ such that $s_1 = \rew{s_1'}$ and $s_2 = \rew{s_2'}$. We can assume \begin{mathpar} \infer - {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} - {\Ga \CCdash (x:T) \explicit U : s_3} + {\Ga \CCdash T:s_1' \\ \Ga, x:T \CCdash U:s_2' \\ (s_1',s_2',s_3') \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3'} \tag{CC-Prod} \end{mathpar} @@ -870,7 +1046,7 @@ Where $s_1 \neq \Type_1$ or $s_2 \neq \Prop$: \end{mathpar} \begin{mathpar} \infer - {\Ga \CCdash T:\Type_1 \\ \Ga, x:T \CCdash U:\Prop \\ (\Type_i,\Prop,\Prop) \in \R_{CC}} + {\Ga \CCdash T:\Type_i \\ \Ga, x:T \CCdash U:\Prop \\ (\Type_i,\Prop,\Prop) \in \R_{CC}} {\Ga \CCdash (x:T) \explicit U : \Prop} \tag{CC-Prod} \end{mathpar} @@ -973,6 +1149,8 @@ However, $b$ has both an erasable and an explicit component: &\quad\leadsto\quad \rew{\Ga} \~ (y : \tau)\erasable (z : f|y)\explicit t : \Type\ \z\\ \end{align*} +In the above Typer expression, $y$ is an \emph{erasable} term applied \emph{explicitly} to the term $f$. This is not contradictory to the rule \textsc{E-Lam} because the type of + Thus, the application of $b$ to the witness and the proof will translate \todo RESULT: View it on GitLab: https://gitlab.com/monnier/typer/commit/89aecbb1547ea6467c0f8e84d2f288bbaa2… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/89aecbb1547ea6467c0f8e84d2f288bbaa2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] Revised comments; commented more function in btl/builtins.typer
by Jonathan Graveline 29 Aug '18

29 Aug '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 13cf5ad0 by Jonathan Graveline at 2018-08-29T20:49:39Z Revised comments; commented more function in btl/builtins.typer Rewrite tuple body; commented tuple unit tests (but they should work) - - - - - 6 changed files: - btl/builtins.typer - btl/case.typer - btl/do.typer - btl/tuple.typer - samples/batch_test.typer - samples/tuple_test.typer Changes: ===================================== btl/builtins.typer ===================================== @@ -157,6 +157,11 @@ String_sub = Built-in "String.sub" : String -> Int -> Int -> String; Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool; +%% +%% Takes an Sexp +%% Returns the same Sexp in the IO monad +%% but also print the Sexp to standard output +%% Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp; %% ----------------------------------------------------- @@ -200,26 +205,63 @@ Sexp_dispatch = Built-in "Sexp.dispatch" -> (block : Sexp -> a) -> a ; +%% +%% Parse an Sexp with the default context +%% default context include builtins.typer and pervasive.typer +%% but nothing else +%% +%% It was implemented to parse Sexp block in a macro +%% Parser_default = Built-in "Parser.default" : Sexp -> List Sexp; +%% +%% Same as `Parser_default` but with a custom context +%% Parser_custom = Built-in "Parser.custom" : Elab_Context -> Sexp -> List Sexp; -Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp; +%% +%% Parse an Sexp with the latest context +%% +%% (I think previous top level definition should be in the context) +%% +Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp; %%%% Array (without IO, but they could be added easily) +%% +%% Takes an index, a new value and an array +%% Returns a copy of the array with the element +%% at the specified index set to the new value %% %% Array_set is in O(N) where N is the length %% Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; +%% +%% Takes an element and an array +%% Returns a copy of the array with the new element at the end %% %% Array_append is in O(N) where N is the length %% Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a; +%% +%% Takes an Int (n) and a value +%% Returns an array containing n times the value +%% Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a; + +%% +%% Takes an array +%% Returns the number of element in the array +%% Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int; + +%% +%% Takes a default value, an index and an array +%% Returns the value in the array at the specified index or +%% the default value if the index is out of bounds +%% Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a; %% ===================================== btl/case.typer ===================================== @@ -16,8 +16,7 @@ %% %% Move IO outside List (from element to List) -%% (Was helpful for me when translating code that used to not be IO code) -%% (The function's type explain everything) +%% (The function's type explain everything) %% io-list : List (IO ?a) -> IO (List ?a); io-list l = let @@ -826,6 +825,11 @@ in List_map (preppend-dflt max-len) branches; %% Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) %% (List (Pair Pats Code)); %% + +%% +%% Takes a list of variable to match and a list of (patterns, code) +%% Returns a Sexp tree of `##case_` +%% compile-case : List Var -> List (Pair Pats Code) -> IO Code; compile-case subjects branches = let ===================================== btl/do.typer ===================================== @@ -10,9 +10,9 @@ %% print str; %% }; %% -%% str is bind by macro, +%% `str` is bind by macro, %% -%% fun is a command, +%% `fun` is a command, %% %% `do` may contain `do` because it returns a command. %% @@ -125,7 +125,10 @@ set-fun args = let in helper (Sexp_symbol "") args; % return Unit if no command given -%% Serie of command +%% +%% Macro `do` +%% Serie of command +%% do = macro (lambda args -> (IO_return (set-fun (get-decl args))) ===================================== btl/tuple.typer ===================================== @@ -35,8 +35,7 @@ %% %% Move IO outside List (from element to List) -%% (Was helpful for me when translating code that used to not be IO code) -%% (The function's type explain everything) +%% (The function's type explain everything) %% io-list : List (IO ?a) -> IO (List ?a); io-list l = let @@ -181,25 +180,40 @@ make-tuple-impl values = let %% map tuple element value mf2 : Sexp -> Sexp -> Sexp; mf2 value nth = Sexp_node (Sexp_symbol "_:=_") (cons nth (cons value nil)); + + ff1 : Sexp -> Sexp -> Sexp -> Sexp; + ff1 body arg arg-t = Sexp_node (Sexp_symbol "lambda_->_") + (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons arg-t nil))) + (cons body nil)); + + ff2 : Sexp -> Sexp -> Sexp; + ff2 body arg = Sexp_node (Sexp_symbol "lambda_≡>_") + (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons (Sexp_symbol "Type") nil))) + (cons body nil)); in do { + args-t <- gen-vars values; + args <- gen-vars values; names <- IO_return (gen-tuple-names values); - fun <- IO_return (Sexp_node (Sexp_symbol "lambda_->_") - (cons (Sexp_node (List_nth 0 args Sexp_error) (List_tail args)) (cons - (Sexp_node (Sexp_symbol "typecons") (cons (Sexp_symbol "Tuple") - (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args)) nil))) - nil)) - ); + tuple-t <- IO_return (Sexp_node (Sexp_symbol "typecons") + (cons (Sexp_symbol "Tuple") + (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args-t)) nil))); - call-fun <- IO_return (Sexp_node fun (gen-deduce values)); + tuple <- IO_return (Sexp_node (Sexp_node (Sexp_symbol "datacons") + (cons tuple-t (cons (Sexp_symbol "cons") nil))) + (List_map2 mf2 args names)); - tuple <- IO_return (Sexp_node (Sexp_symbol "##datacons") - (cons call-fun (cons (Sexp_symbol "cons") nil))); + fun <- IO_return (List_foldl ff2 + (List_fold2 ff1 tuple (List_reverse args nil) + (List_reverse args-t nil)) + (List_reverse args-t nil)); - affect <- IO_return (Sexp_node tuple (List_map2 mf2 values names)); + values <- IO_return (List_reverse values nil); + + affect <- IO_return (Sexp_node fun (List_reverse values nil)); IO_return affect; }; @@ -218,7 +232,6 @@ make-tuple = macro (lambda args -> do { %% %% Takes element's type as argument %% -%% tuple-type = macro (lambda args -> let mf : Sexp -> Sexp -> Sexp; ===================================== samples/batch_test.typer ===================================== @@ -31,7 +31,10 @@ u3 = Test_file "./samples/case_test.typer"; u4 = Test_file "./samples/polyfun_test.typer"; -u5 = Test_file "./samples/tuple_test.typer"; +%% +%% This test is currently failling due to type error in ELAB and TC +%% u5 = Test_file "./samples/tuple_test.typer"; +%% u6 = Test_file "./samples/do_test.typer"; @@ -46,15 +49,16 @@ exec-all = do { b3 <- u3; Test_info "BATCH TESTS" "\n\n\tnext file\n"; b4 <- u4; - Test_info "BATCH TESTS" "\n\n\tnext file\n"; - b5 <- u5; + %% Test_info "BATCH TESTS" "\n\n\tnext file\n"; + %% b5 <- u5; Test_info "BATCH TESTS" "\n\n\tnext file\n"; b6 <- u6; Test_info "BATCH TESTS" "\n\n\tlast file\n"; b7 <- u7; Test_info "BATCH TESTS" "\n\n\tdone\n"; - success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 (and b6 b7)))))); + %% success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 (and b6 b7)))))); + success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b6 b7))))); if success then (Test_info "BATCH TESTS" "all tests succeeded") ===================================== samples/tuple_test.typer ===================================== @@ -60,16 +60,6 @@ test-tuple = do { r2 <- Test_eq "n = false" n false; r3 <- Test_eq "o = (some false)" o (some false); - %% - %% Here is a problem with tuple's definition - %% each tuple has in fact a different type! - %% - %% r4 <- Test_eq "j = (true, some true)" j (true, some true); - %% r5 <- Test_eq "k = (false, some false)" k (false, some false); - %% - %% But those value are tested within `r0` to `r3` - %% - success <- IO_return (and r0 (and r1 (and r2 r3))); if success then View it on GitLab: https://gitlab.com/monnier/typer/commit/13cf5ad04273fec85aa4840651a68f17747… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/13cf5ad04273fec85aa4840651a68f17747… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] 3 commits: Revised comments, trying to be more clear
by Jonathan Graveline 27 Aug '18

27 Aug '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: caa73195 by Jonathan Graveline at 2018-08-24T18:33:07Z Revised comments, trying to be more clear - - - - - cd2381bc by Jonathan Graveline at 2018-08-24T19:46:34Z New unit test for `plain-let` Revision of bbst.typer and table.typer - - - - - 6ef13572 by Jonathan Graveline at 2018-08-27T19:01:33Z More comments in samples/myers.typer Basic unit tests on Myers list in samples/myers_test.typer - - - - - 16 changed files: - btl/builtins.typer - btl/case.typer - btl/do.typer - btl/list.typer - btl/pervasive.typer - btl/plain-let.typer - btl/polyfun.typer - btl/tuple.typer - samples/batch_test.typer - samples/bbst.typer - samples/bbst_test.typer - samples/myers.typer - + samples/myers_test.typer - + samples/plain_let_test.typer - samples/table.typer - samples/table_test.typer Changes: ===================================== btl/builtins.typer ===================================== @@ -208,13 +208,25 @@ Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp; %%%% Array (without IO, but they could be added easily) +%% +%% Array_set is in O(N) where N is the length +%% +Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; + +%% +%% Array_append is in O(N) where N is the length +%% Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a; + Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a; Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int; -Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a; -% let Typer deduce the value of (a : Type) +%% +%% It returns an empty array +%% +%% let Typer deduce the value of (a : Type) +%% Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a; %%%% Monads @@ -246,10 +258,13 @@ File_read = Built-in "File.read" : FileHandle -> Int -> IO String; Sys_cpu_time = Built-in "Sys.cpu_time" : Unit -> IO Float; Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; +%% %% Ref (modifiable value) - -% Ref : Type -> Type; -% Ref = typecons (Ref (a : Type)) (Ref a); +%% +%% Conceptualy: +%% Ref : Type -> Type; +%% Ref = typecons (Ref (a : Type)) (Ref a); +%% Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; @@ -259,7 +274,7 @@ Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; %% gensym for macro %% Generate pseudo-unique symbol %% At least they cannot be obtained outside macro -%% In macro you should NOT use symbol of the form ` %gensym% ...` +%% In macro you should NOT use symbol of the form " %gensym% ..." %% gensym = Built-in "gensym" : Unit -> IO Sexp; @@ -302,7 +317,7 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin %% %% Get the position of a field in a constructor -%% It return -1 in case something isn't defined +%% It return -1 in case the field isn't defined %% see pervasive.typer for a more convenient function %% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; @@ -316,12 +331,13 @@ Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; %% %% Print message and/or fail (terminate) -%% These message are registered like any other error +%% These messages are registered like any other error %% And location is printed before the error +%% %% %% Voluntarily fail -%% for exemple if next unit tests are not worth testing +%% use case: next unit tests are not worth testing %% %% Takes a "section" and a "message" as argument %% @@ -347,12 +363,33 @@ Test_info = Built-in "Test.info" : String -> String -> IO Unit; %% Test_location = Built-in "Test.location" : Unit -> String; +%%% +%%% Do some test which print a message: "[ OK]" or "[FAIL]" +%%% followed by a message passed as argument +%%% + %% -%% Do some test which print a message: "[ OK]" or "[FAIL]" +%% Takes a message and a boolean which should be true +%% Returns true if the boolean was true %% Test_true = Built-in "Test.true" : String -> Bool -> IO Bool; + +%% +%% Takes a message and a boolean which should be false +%% Returns true if the boolean was false +%% Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; + +%% +%% Takes a message and two arbitrary value of the same type +%% Returns true when the two value are equal +%% Test_eq = Built-in "Test.eq" : (a : Type) ≡> String -> a -> a -> IO Bool; + +%% +%% Takes a message and two arbitrary value of the same type +%% Returns true when the two value are not equal +%% Test_neq = Built-in "Test.neq" : (a : Type) ≡> String -> a -> a -> IO Bool; %%% builtins.typer ends here. ===================================== btl/case.typer ===================================== @@ -14,9 +14,11 @@ %%%% Another problem is that this macro is dependent of tuple implementation %%%% +%% %% Move IO outside List (from element to List) %% (Was helpful for me when translating code that used to not be IO code) %% (The function's type explain everything) +%% io-list : List (IO ?a) -> IO (List ?a); io-list l = let ff : IO (List ?a) -> IO ?a -> IO (List ?a); @@ -90,12 +92,12 @@ in Sexp_dispatch sexp sfalse sfalse sfalse sfalse sfalse; %% -%% Get matched expression (e.g. case var1 var2 ... | ...) +%% Get matched expression (e.g. case (var1,var2,...) | ...) %% -%% Expression are separated by " " (space) so it is useful for -%% case expr1 expr2 ... | ... +%% Expression are separated by "," so it is useful for +%% case (expr1,expr2,...) | ... %% but also for -%% case ... | expr3 expr4 ... => ... +%% case ... | (expr3,expr4,...) => ... %% %% (This function is now doing nothing since there's only one %% variable at any time: one expression or a tuple of expressions) @@ -308,24 +310,20 @@ renamed-pat pat names = let (lambda sym ss -> if (Sexp_eq sym (Sexp_symbol "_:=_")) then if (List_nth i kinds false) then - %% %% if client use multiple name for the same erasable args, %% I expect it to not compile... - %% (Sexp_node sym ss) else (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) else if tup then - %% %% tuples argument are all implicit so we must take special care of those - %% (Sexp_node (Sexp_symbol "_:=_") - (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) + (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else (List_nth i names Sexp_error)) (lambda _ -> if tup then (Sexp_node (Sexp_symbol "_:=_") - (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) + (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else (List_nth i names Sexp_error)) serr serr serr serr; @@ -340,7 +338,7 @@ in do { }; %% -%% Takes an Sexp as argument and IO_return `IO true` if it is a pattern +%% Takes an Sexp as argument and return `IO true` if it is a pattern %% (i.e. a constructor with or without argument) %% is-pat : Pat -> IO Bool; @@ -401,7 +399,7 @@ in Sexp_eq (ctor-of p0) (ctor-of p1); %% %% Get variable introduced by a constructor %% -%% Takes a pattern as argument and return each arguments +%% Takes a pattern as argument and returns each arguments %% of the constructor which is a variable (as opposed to a sub pattern) %% introduced-vars : Pat -> IO (List Var); @@ -422,7 +420,7 @@ introduced-vars pat = let %% Function to fold each argument of the pattern %% The Int is used internaly to keep track of argument index %% It is useful to know where is the variable in `ks` to get its kind - %% (kind is actualy only erasable or not here) + %% (kind is actualy only erasable or not) %% ff : IO (Pair Int (List Sexp)) -> Sexp -> IO (Pair Int (List Sexp)); ff p v = let @@ -473,16 +471,15 @@ in Sexp_dispatch pat %% %% Wrap the third argument (`fun`) with a `let` definition for each variables -%% Names are taken from `rvars` and definition are taken from `ivars` %% wrap-vars : List Var -> List Var -> Code -> Code; -wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> +wrap-vars rhs lhs fun = List_fold2 (lambda fun v0 v1 -> %% %% I prefer `let` definition because a lambda function would need a type %% (quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) %% (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) - fun ivars rvars; + fun rhs lhs; %% %% Take a List of branches and return a List of the first pattern in each branches @@ -603,7 +600,7 @@ in do { }; %% -%% Type of one partition of branches (one branch with some possible child branches) +%% Type of one partition of branches (one branch with child branches) %% %% Pair of %% Triplet of renamed pat, @@ -729,8 +726,8 @@ in do { %% %% There's a need to merge branch because default branch may be anywhere %% -%% (I tried to consider default branches similar to everything but it failed in some way -%% So here we are...) +%% (I tried to consider default branches similar to every patterns +%% but it failed in some way. So here we are...) %% merge-dflt : List part-type -> Option part-type -> List part-type; merge-dflt parts odflt = let ===================================== btl/do.typer ===================================== @@ -131,7 +131,9 @@ do = macro (lambda args -> (IO_return (set-fun (get-decl args))) ); +%% %% Next are example command +%% print str = (File_write (File_stdout ()) str); ===================================== btl/list.typer ===================================== @@ -45,11 +45,13 @@ length xs = case xs | cons hd tl => (1 + (length tl)); +%% %% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: %% - Provide a default value : `a -> List a -> a`; %% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error +%% head1 : (a : Type) ≡> List a -> Option a; head1 xs = case xs | nil => none @@ -102,9 +104,9 @@ in helper f 0 xs; %% map2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c) -> List a -> List b -> List c; map2 = lambda f -> lambda xs -> lambda ys -> case xs - | nil => nil + | nil => nil % may be an error | cons x xs => case ys - | nil => nil % error + | nil => nil % may be an error | cons y ys => cons (f x y) (map2 f xs ys); %% @@ -129,7 +131,7 @@ fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs | nil => o; % may or may not be an error %% -%% (Should be as any `fold right` of functional language) +%% (Should be as any `fold right` function of functional language) %% foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; foldr = lambda f -> lambda xs -> lambda i -> case xs @@ -147,7 +149,7 @@ find = lambda f -> lambda xs -> case xs | cons x xs => case f x | true => some x | false => find f xs; %% -%% Get the n'th element of a list or a default if the list is smaller +%% Get the n'th element of a list or a default if the list is smaller than n %% nth : (a : Type) ≡> Int -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs @@ -183,7 +185,8 @@ foldl = lambda f -> lambda i -> lambda xs -> case xs %% %% Takes a function and a list -%% Returns the list with element removed if the function return true on those element +%% Returns the list with element removed +%% when the user function return true on those element %% remove : (a : Type) ≡> (a -> Bool) -> List a -> List a; remove = lambda f -> lambda l -> case l @@ -243,7 +246,7 @@ empty? = lambda xs -> case xs %% Takes a comparison function and a list %% Returns the same list but sorted %% -%% If comparison is `>` then the list start with the smallest element +%% If comparison is `>` then the result start with the smallest element %% sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; sort = lambda o -> lambda l -> let @@ -278,7 +281,7 @@ in sortp (head1 l) nil nil (tail l); %% Find an element with a shortcut because the list is sorted %% Takes a comparison function, a function to match, an element and a list %% -%% (...maybe to parametric for what it does, this function is useless) +%% (...maybe too parametric for what it does, this function is useless) %% sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a; sfind = lambda o -> lambda f -> lambda a -> lambda l -> case l ===================================== btl/pervasive.typer ===================================== @@ -518,59 +518,117 @@ test3 = test4; %%%% Rewrite of some builtins to use `Option` +%% +%% If `Elab_nth-arg'` returns "_" it means: +%% A- The constructor isn't defined, or +%% B- The constructor has no n'th argument +%% +%% So in those case this function returns `none` +%% Elab_nth-arg a b c = let r = Elab_nth-arg' a b c; in case (String_eq r "_") | true => (none) | false => (some r); +%% +%% If `Elab_arg-pos'` returns (-1) it means: +%% A- The constructor isn't defined, or +%% B- The constructor has no argument named like this +%% +%% So in those case this function returns `none` +%% Elab_arg-pos a b c = let r = Elab_arg-pos' a b c; in case (Int_eq r (-1)) | true => (none) | false => (some r); -%%%% `<-` operator used in macro `do` and for tuple assignment - -define-operator "<-" 80 96; - %%%% %%%% Common library %%%% -%% `List` is the type and `list` is the module (tuple) +%% +%% `<-` operator used in macro `do` and for tuple assignment +%% + +define-operator "<-" 80 96; + +%% +%% `List` is the type and `list` is the module +%% list = load "btl/list.typer"; -%% macro `do` for easier series of IO operation +%% +%% Macro `do` for easier series of IO operation +%% +%% e.g.: +%% do { IO_return true; }; +%% do = let lib = load "btl/do.typer" in lib.do; -%% various macro for tuple -%% used by `case_` +%% +%% Module containing various macro for tuple +%% Used by `case_` +%% tuple-lib = load "btl/tuple.typer"; -%% get nth element +%% +%% Get the nth element of a tuple +%% +%% e.g.: +%% tuple-nth tup 0; +%% tuple-nth = tuple-lib.tuple-nth; -%% affectation (e.g. `(x,y,z) <- tup`) +%% +%% Affectation of tuple +%% +%% e.g.: +%% (x,y,z) <- tup; +%% _<-_ = tuple-lib.assign-tuple; -%% creation (e.g. `tup = (x,y,z)`) +%% +%% Instantiate a tuple from expressions +%% +%% e.g.: +%% tup = (x,y,z); +%% _\,_ = tuple-lib.make-tuple; Tuple = tuple-lib.tuple-type; -%% macro `case` for a little more complex pattern matching +%% +%% Macro `case` for a some more complex pattern matching +%% case_ = let lib = load "btl/case.typer" in lib.case-macro; -%%%% plain-let -%%%% Not recursive and not sequential +%% +%% plain-let +%% Not recursive and not sequential +%% +%% e.g.: +%% plain-let x = 1; in x; +%% define-operator "plain-let" () 3; + +%% +%% Already defined: %% define-operator "in" 3 67; +%% plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; -%%%% `case` at function level +%% +%% `case` at function level +%% +%% e.g.: +%% my-fun (x : Bool) +%% | true => false +%% | false => true; +%% _|_ = let lib = load "btl/polyfun.typer" in lib._|_; %%%% Unit tests function for doing file @@ -582,7 +640,7 @@ _|_ = let lib = load "btl/polyfun.typer" in lib._|_; %% A macro using `load` for unit testing purpose %% %% Takes a file name (String) as argument -%% Return variable named `exec-test` from the loaded file +%% Returns variable named `exec-test` from the loaded file %% %% `exec-test` should be a command doing unit tests %% for other purpose than that just use `load` directly! ===================================== btl/plain-let.typer ===================================== @@ -13,18 +13,18 @@ %% %% The idea is to use unique identifier in a first let -%% and then assign those first identifier to the original symbol +%% and then assign those unique identifier to the original symbol %% %% Useful for auto-generated code (macro, ...) %% %% -%% Takes the plain input of macro `plain-let` +%% Takes the plain argument of macro `plain-let` %% impl : List Sexp -> IO Sexp; impl args = let - %% error use in Sexp_dispatch + %% Error use in Sexp_dispatch serr = lambda _ -> Sexp_error; %% Takes an assignment statement and return a new @@ -37,7 +37,7 @@ impl args = let io-serr = lambda _ -> IO_return Sexp_error; %% Get a `gensym` symbol - %% I can rename a function name (not the argument) + %% It can rename a function name (not the argument) %% or just a symbol rename : Sexp -> IO Sexp; rename sexp = Sexp_dispatch sexp @@ -101,7 +101,7 @@ impl args = let }; %% Takes a list of assignment and a body (likely using those assignment) - %% Returns a `let ... in ...` construction + %% Returns a `let [assignment] in [body]` construction let-in : Sexp -> Sexp -> Sexp; let-in decls body = Sexp_node (Sexp_symbol "let_in_") (cons decls (cons body nil)); @@ -112,7 +112,7 @@ impl args = let %% Takes lists of pairs (`gensym`,definition) and (`gensym`,original symbol) %% and the body (likely using original symbol) %% Returns - %% let [gensym] = [definition] ... in let [original symbol] = [gensym] in [body] + %% let [gensym] = [definition] in let [original symbol] = [gensym] in [body] gen-code : List (Pair Sexp Sexp) -> List (Pair Sexp Sexp) -> Sexp -> Sexp; gen-code sym-def var-sym body = let ===================================== btl/polyfun.typer ===================================== @@ -5,11 +5,12 @@ %%%% (Just a `case` at function definition level) %%%% -%% error use in Sexp_dispatch +%% +%% Error use in Sexp_dispatch +%% serr : (a : Type) ≡> a -> Sexp; serr = lambda _ -> Sexp_error; -%% other error for Sexp_dispatch xserr : (a : Type) ≡> a -> List Sexp; xserr = lambda _ -> (nil : List Sexp); @@ -55,7 +56,7 @@ fun-args decl = Sexp_dispatch decl %% %% Takes a list of "_=>_"-node -%% Returns a list of pair of (pattern, body) +%% Returns a list of (pattern, body) pair %% fun-cases : List Sexp -> List (Pair Sexp Sexp); fun-cases args = let @@ -76,7 +77,7 @@ fun-cases args = let in List_map mf args; %% -%% Takes argument list and list of pair of (pattern, body) +%% Takes argument list and list of (pattern, body) pair %% Returns a function with a `case` on argument for each pattern %% cases-to-sexp : List Sexp -> List (Pair Sexp Sexp) -> Sexp; ===================================== btl/tuple.typer ===================================== @@ -33,9 +33,11 @@ %% List_map2 = list.map2; %% List_concat = list.concat; +%% %% Move IO outside List (from element to List) %% (Was helpful for me when translating code that used to not be IO code) %% (The function's type explain everything) +%% io-list : List (IO ?a) -> IO (List ?a); io-list l = let ff : IO (List ?a) -> IO ?a -> IO (List ?a); @@ -166,7 +168,7 @@ wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> fun ivars rvars; %% -%% Takes a list of values as Sexp (like 1, 1.0, "str", etc) +%% Takes a list of values (expressions) as Sexp (like a variable, 1, 1.0, "str", etc) %% Returns a tuple containing those values %% make-tuple-impl : List Sexp -> IO Sexp; @@ -216,6 +218,7 @@ make-tuple = macro (lambda args -> do { %% %% Takes element's type as argument %% +%% tuple-type = macro (lambda args -> let mf : Sexp -> Sexp -> Sexp; ===================================== samples/batch_test.typer ===================================== @@ -35,6 +35,8 @@ u5 = Test_file "./samples/tuple_test.typer"; u6 = Test_file "./samples/do_test.typer"; +u7 = Test_file "./samples/plain_let_test.typer"; + exec-all = do { Test_info "BATCH TESTS" "\n\n\tfirst file\n"; b1 <- u1; @@ -46,11 +48,13 @@ exec-all = do { b4 <- u4; Test_info "BATCH TESTS" "\n\n\tnext file\n"; b5 <- u5; - Test_info "BATCH TESTS" "\n\n\tlast file\n"; + Test_info "BATCH TESTS" "\n\n\tnext file\n"; b6 <- u6; + Test_info "BATCH TESTS" "\n\n\tlast file\n"; + b7 <- u7; Test_info "BATCH TESTS" "\n\n\tdone\n"; - success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 b6))))); + success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 (and b6 b7)))))); if success then (Test_info "BATCH TESTS" "all tests succeeded") ===================================== samples/bbst.typer ===================================== @@ -8,6 +8,8 @@ %% %% The 2-3-4 tree %% +%% (Internal representation) +%% type BbsTree (a : Type) | node2 (d : a) (l0 : BbsTree a) (l1 : BbsTree a) @@ -17,7 +19,7 @@ type BbsTree (a : Type) | node-leaf; %% -%% The tree with necessary data +%% The data structure with necessary data %% %% c is a compare function which should be similar to <= (or >=) %% @@ -139,7 +141,7 @@ length tree = case tree %% Is the tree empty? %% -is-empty tree = (Int_eq (length tree) 0); +empty? tree = (Int_eq (length tree) 0); %% %% Check if two value are equal with comparison function only @@ -212,8 +214,8 @@ in case tree %% Is elem in the tree? %% -member : (a : Type) ≡> a -> Bbst a -> Bool; -member elem tree = let +member? : (a : Type) ≡> a -> Bbst a -> Bool; +member? elem tree = let oe = find elem tree; @@ -375,7 +377,7 @@ insert elem tree = let | node-leaf => node2 e node-leaf node-leaf; -in if (member elem tree) then +in if (member? elem tree) then (case tree % we may want to replace an element (partial comparison function) | bbst s c t => bbst s c (helper c elem t)) else @@ -383,11 +385,11 @@ in if (member elem tree) then | bbst s c t => bbst (s + 1) c (helper c elem t)); %% -%% Remove the smallest element. Used in remove. +%% Internal function used in `remove` and `pop-leftmost` %% -pop-leftmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; -pop-leftmost comp tree = let +pop-leftmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; +pop-leftmost' comp tree = let four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; @@ -423,11 +425,22 @@ pop-leftmost comp tree = let in (helper tree); %% -%% Remove the biggest element. Used in remove. +%% Remove the smallest element +%% + +pop-leftmost : (a : Type) ≡> Bbst a -> Bbst a; +pop-leftmost t = case t + | bbst s c t => if (Int_eq 0 s) then + (bbst s c t) + else + (bbst (s - 1) c (pop-leftmost' c t)); + +%% +%% Internal used in `remove` and `pop-rightmost` %% -pop-rightmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; -pop-rightmost comp tree = let +pop-rightmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; +pop-rightmost' comp tree = let four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; @@ -463,11 +476,22 @@ pop-rightmost comp tree = let in (helper tree); %% -%% Get the smallest element. Used in remove. +%% Remove the greatest element +%% + +pop-rightmost : (a : Type) ≡> Bbst a -> Bbst a; +pop-rightmost t = case t + | bbst s c t => if (Int_eq 0 s) then + (bbst s c t) + else + (bbst (s - 1) c (pop-rightmost' c t)); + +%% +%% Internal used in `remove` and `get-leftmost` %% -get-leftmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; -get-leftmost comp tree = let +get-leftmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; +get-leftmost' comp tree = let four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; @@ -502,11 +526,19 @@ get-leftmost comp tree = let in (helper tree); %% -%% Get the biggest element. Used in remove. +%% Get smallest element %% -get-rightmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; -get-rightmost comp tree = let +get-leftmost : (a : Type) ≡> Bbst a -> Option a; +get-leftmost t = case t + | bbst _ c t => get-leftmost' c t; + +%% +%% Internal used in `remove` and `get-rightmost` +%% + +get-rightmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; +get-rightmost' comp tree = let four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; @@ -540,6 +572,14 @@ get-rightmost comp tree = let in (helper tree); +%% +%% Get greatest element +%% + +get-rightmost : (a : Type) ≡> Bbst a -> Option a; +get-rightmost t = case t + | bbst _ c t => get-rightmost' c t; + %% %% Remove an element from the tree %% @@ -558,14 +598,14 @@ remove elem tree = let | node-leaf => ( case l1 | node-leaf => node-leaf | _ => let - oe = get-leftmost comp l1; + oe = get-leftmost' comp l1; in case oe - | some e => node2 e l0 (pop-leftmost comp l1) + | some e => node2 e l0 (pop-leftmost' comp l1) | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l0; + oe = get-rightmost' comp l0; in case oe - | some e => node2 e (pop-rightmost comp l0) l1 + | some e => node2 e (pop-rightmost' comp l0) l1 | none => node-leaf; % May not happen too rebuild-left-three : (a -> a -> Bool) -> a -> @@ -575,14 +615,14 @@ remove elem tree = let | node-leaf => ( case l1 | node-leaf => node2 d1 node-leaf l2 | _ => let - oe = get-leftmost comp l1; + oe = get-leftmost' comp l1; in case oe - | some e => node3 e d1 l0 (pop-leftmost comp l1) l2 + | some e => node3 e d1 l0 (pop-leftmost' comp l1) l2 | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l0; + oe = get-rightmost' comp l0; in case oe - | some e => node3 e d1 (pop-rightmost comp l0) l1 l2 + | some e => node3 e d1 (pop-rightmost' comp l0) l1 l2 | none => node-leaf; % May not happen too rebuild-right-three : (a -> a -> Bool) -> a -> @@ -592,14 +632,14 @@ remove elem tree = let | node-leaf => ( case l2 | node-leaf => node2 d0 l0 node-leaf | _ => let - oe = get-leftmost comp l2; + oe = get-leftmost' comp l2; in case oe - | some e => node3 d0 e l0 l1 (pop-leftmost comp l2) + | some e => node3 d0 e l0 l1 (pop-leftmost' comp l2) | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l1; + oe = get-rightmost' comp l1; in case oe - | some e => node3 d0 e l0 (pop-rightmost comp l1) l2 + | some e => node3 d0 e l0 (pop-rightmost' comp l1) l2 | none => node-leaf; % May not happen too rebuild-left-four : (a -> a -> Bool) -> a -> a -> @@ -609,14 +649,14 @@ remove elem tree = let | node-leaf => ( case l1 | node-leaf => node3 d1 d2 node-leaf l2 l3 | _ => let - oe = get-leftmost comp l1; + oe = get-leftmost' comp l1; in case oe - | some e => node4 e d1 d2 l0 (pop-leftmost comp l1) l2 l3 + | some e => node4 e d1 d2 l0 (pop-leftmost' comp l1) l2 l3 | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l0; + oe = get-rightmost' comp l0; in case oe - | some e => node4 e d1 d2 (pop-rightmost comp l0) l1 l2 l3 + | some e => node4 e d1 d2 (pop-rightmost' comp l0) l1 l2 l3 | none => node-leaf; % May not happen too rebuild-middle-four : (a -> a -> Bool) -> a -> a -> @@ -626,14 +666,14 @@ remove elem tree = let | node-leaf => ( case l2 | node-leaf => node3 d0 d2 l0 node-leaf l3 | _ => let - oe = get-leftmost comp l2; + oe = get-leftmost' comp l2; in case oe - | some e => node4 d0 e d2 l0 l1 (pop-leftmost comp l2) l3 + | some e => node4 d0 e d2 l0 l1 (pop-leftmost' comp l2) l3 | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l1; + oe = get-rightmost' comp l1; in case oe - | some e => node4 d0 e d2 l0 (pop-rightmost comp l1) l2 l3 + | some e => node4 d0 e d2 l0 (pop-rightmost' comp l1) l2 l3 | none => node-leaf; % May not happen too rebuild-right-four : (a -> a -> Bool) -> a -> a -> @@ -643,14 +683,14 @@ remove elem tree = let | node-leaf => ( case l3 | node-leaf => node3 d0 d1 l0 l1 node-leaf | _ => let - oe = get-leftmost comp l3; + oe = get-leftmost' comp l3; in case oe - | some e => node4 d0 d1 e l0 l1 l2 (pop-leftmost comp l3) + | some e => node4 d0 d1 e l0 l1 l2 (pop-leftmost' comp l3) | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l2; + oe = get-rightmost' comp l2; in case oe - | some e => node4 d0 d1 e l0 l1 (pop-rightmost comp l2) l3 + | some e => node4 d0 d1 e l0 l1 (pop-rightmost' comp l2) l3 | none => node-leaf; % May not happen too helper : (a -> a -> Bool) -> a -> BbsTree a -> BbsTree a; @@ -705,7 +745,7 @@ remove elem tree = let | node-leaf => node-leaf; -in if (member elem tree) then +in if (member? elem tree) then (case tree | bbst s c t => bbst (s - 1) c (helper c elem t)) else @@ -745,9 +785,9 @@ odict-insert : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); odict-insert k d t = insert (pair k (some d)) t; -odict-member : (Key : Type) ≡> (Data : Type) ≡> Key -> +odict-member? : (Key : Type) ≡> (Data : Type) ≡> Key -> Bbst (Pair Key (Option Data)) -> Bool; -odict-member k t = member (pair k none) t; +odict-member? k t = member? (pair k none) t; odict-remove : (Key : Type) ≡> (Data : Type) ≡> Key -> Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); @@ -757,8 +797,8 @@ odict-update : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); odict-update k d t = insert (pair k (some d)) t; -odict-is-empty : (Key : Type) ≡> (Data : Type) ≡> Bbst (Pair Key (Option Data)) -> Bool; -odict-is-empty t = is-empty t; +odict-empty? : (Key : Type) ≡> (Data : Type) ≡> Bbst (Pair Key (Option Data)) -> Bool; +odict-empty? t = empty? t; %%% %%% Test helper ===================================== samples/bbst_test.typer ===================================== @@ -41,7 +41,7 @@ test-length = do { r3 <- Test_eq "t3" (length t3) 53; r4 <- Test_eq "t4" (length t4) 50; r5 <- Test_eq "t5" (length t5) 50; - r6 <- Test_true "e0" (is-empty e0); + r6 <- Test_true "e0" (empty? e0); r7 <- Test_eq "e1" (length e1) 1; r8 <- Test_eq "e2" (length e2) 0; @@ -70,7 +70,7 @@ test-find = do { (Test_warning "BBST" "find test failed"); }; -%% member is just a wrapped version of find so not need to test it +%% member? is just a wrapped version of find so not need to test it %% in the actual implementation test-fold = do { ===================================== samples/myers.typer ===================================== @@ -1,52 +1,77 @@ %%% %%% Adaptation of Myers list from ocaml file `myers.ml` %%% -%%% since 2018-05-14 -%%% +%% %% We could replace mnil and mcons by nil and cons %% when load and list.typer are ready +%% t : Type -> Type; type t (a : Type) | mnil | mcons (data : a) (link1 : (t a)) (i : Int) (link2 : (t a)); -% Contrary to Myers's presentation, we index from the top of the stack, -% and we don't store the total length but the "skip distance" instead. -% This makes `cons' slightly faster, and better matches our use for -% debruijn environments. +%% +%% Contrary to Myers's presentation, we index from the top of the stack, +%% and we don't store the total length but the "skip distance" instead. +%% This makes `cons' slightly faster, and better matches our use for +%% debruijn environments. +%% +%% +%% Prepend an element `x` to a Myers list `l` +%% cons : (a : Type) ≡> a -> t a -> t a; cons x l = case l | mcons _ _ s1 l1 => ( case l1 | mcons _ _ s2 l2 => ( case (Int_>= s1 s2) | true => mcons x l (s1 + s2 + 1) l2 - | false => mcons x l 1 l - ) - | _ => mcons x l 1 l - ) + | false => mcons x l 1 l ) + | _ => mcons x l 1 l ) | _ => mcons x l 1 l; +%% +%% Get the head of a Myers list `l` +%% (Get the first element) +%% Returns `some x` if the list is non-empty or `none` if it is empty +%% car : (a : Type) ≡> t a -> Option a; car l = case l | mnil => none | mcons x _ _ _ => some x; +%% +%% Get the tail of a Myers list `l` +%% (Get the same list without its first element) +%% Always returns `mnil` if the list is empty +%% cdr : (a : Type) ≡> t a -> t a; cdr l = case l | mnil => mnil | mcons _ l _ _ => l; +%% +%% Pass the first element to a user function and return the result +%% or return a default value passed as argument +%% match : (a : Type) ≡> (b : Type) ≡> t a -> b -> (a -> t a -> b) -> b; match l n c = case l | mnil => n | mcons x l _ _ => c x l; -empty : (a : Type) ≡> t a -> Bool; -empty l = case l +%% +%% Is the Myers list empty? +%% +empty? : (a : Type) ≡> t a -> Bool; +empty? l = case l | mnil => true | _ => false; +%% +%% Remove the n'th first element from the Myers list +%% (It is the same as `(cdr (cdr ...))` with `cdr` called `n` times +%% but may be faster for greater `n`) +%% nthcdr : (a : Type) ≡> Int -> t a -> t a; nthcdr n l = if_then_else_ (Int_eq n 0) l ( case l @@ -57,13 +82,21 @@ nthcdr n l = if_then_else_ (Int_eq n 0) l ) ); +%% +%% Get the n'th element of a Myers list +%% nth : (a : Type) ≡> Int -> t a -> Option a; nth n l = car (nthcdr n l); -% While `nth` is O(log N), `set_nth` is O(N)! :-( - -set_nth : (a : Type) ≡> Int -> a -> t a -> t a; -set_nth n v l = let +%% +%% Update the n'th element of a Myers list +%% Takes the index, the new value and the list +%% Returns the updated list +%% +%% (While `nth` is O(log N), `set-nth` is O(N)! :-( ) +%% +set-nth : (a : Type) ≡> Int -> a -> t a -> t a; +set-nth n v l = let % I should use the new case_ macro here! @@ -80,19 +113,24 @@ set_nth n v l = let | pat1 n vp cdr s tail => if_then_else_ (Int_eq n 0) ( mcons v cdr s tail ) - ( cons vp (set_nth (n - 1) v cdr) ) + ( cons vp (set-nth (n - 1) v cdr) ) - % We can't set_nth past the end in general because we'd need to - % magically fill the intermediate entries with something of the right type. - % But we *can* set_nth just past the end. + %% + %% We can't set-nth past the end in general because we'd need to + %% magically fill the intermediate entries with something of the right type. + %% But we *can* set-nth just past the end. + %% | pat2 n => if_then_else_ (Int_eq n 0) ( mcons v mnil 1 mnil ) ( l ); % should throw an error here! -% This operation would be more efficient using Myers's choice of keeping -% the length (instead of the skip-distance) in each node. - +%% +%% Get the element count of a Myers list +%% +%% (This operation would be more efficient using Myers's choice of keeping +%% the length (instead of the skip-distance) in each node.) +%% length : (a : Type) ≡> t a -> Int; length l = let @@ -103,10 +141,11 @@ length l = let in lengthp l 0; -% Find the first element for which the predicate `p' is true. -% "Binary" search, assuming the list is "sorted" (i.e. all elements after -% this one also return true). - +%% +%% Find the first element for which the predicate `p' is true. +%% "Binary" search, assuming the list is "sorted" (i.e. all elements after +%% this one also return true). +%% find : (a : Type) ≡> (a -> Bool) -> t a -> Option a; find p l = let @@ -129,10 +168,11 @@ find p l = let in find1 l; -% Find the last node for which the predicate `p' is false. -% "Binary" search, assuming the list is "sorted" (i.e. all elements after -% this one also return true). - +%% +%% Find the last node for which the predicate `p' is false. +%% "Binary" search, assuming the list is "sorted" (i.e. all elements after +%% this one also return true). +%% findcdr : (a : Type) ≡> (a -> Bool) -> t a -> t a; findcdr p l = let @@ -160,28 +200,43 @@ findcdr p l = let in findcdr1 none l; -fold_left : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> t a -> b; -fold_left f i l = case l +%% +%% As `fold_left` of any functional language but on Myers list +%% +foldl : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> t a -> b; +foldl f i l = case l | mnil => i - | mcons x l _ _ => fold_left f (f i x) l; + | mcons x l _ _ => foldl f (f i x) l; -fold_right : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> t a -> b -> b; -fold_right f l i = case l +%% +%% As 'fold_right` of any functional language but on Myers list +%% +foldr : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> t a -> b -> b; +foldr f l i = case l | mnil => i - | mcons x l _ _ => f x (fold_right f l i); + | mcons x l _ _ => f x (foldr f l i); +%% +%% As `map` of any functional language but on Myers list +%% (Apply a function to all element of the list) +%% map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> t a -> t b; map f l = let fp : a -> t b -> t b; fp x lp = cons (f x) lp; -in fold_right fp l mnil; +in foldr fp l mnil; +%% +%% Apply all element of a Myers list to a user function +%% Takes a function and a list +%% Returns the length of the list +%% iteri : (a : Type) ≡> (Int -> a -> Unit) -> t a -> Int; iteri f l = let fp : (Int -> a -> Int); fp i x = let _ = (f i x); in i + 1; -in fold_left fp 0 l; +in foldl fp 0 l; ===================================== samples/myers_test.typer ===================================== @@ -0,0 +1,42 @@ +%%%% +%%%% Unit tests for Myers list +%%%% + +xs = cons 1 (cons 2 (cons 3 (cons 4 mnil))); + +ys = cons 2 (cons 3 (cons 4 mnil)); + +zs = cons 4 mnil; + +ws = set-nth 1 7 ys; + +test = do { + Test_info "MYERS LIST" ""; + + r0 <- Test_eq "cdr" zs (cdr (cdr ys)); + r1 <- Test_eq "nthcdr" zs (nthcdr 2 ys); + + r2 <- Test_true "empty?" (empty? mnil); + r3 <- Test_false "empty?" (empty? zs); + + r4 <- Test_eq "car" (car xs) (some 1); + r5 <- Test_eq "car" (car zs) (some 4); + r6 <- Test_eq "car" (car mnil) none; + + r7 <- Test_eq "nth" (nth 0 zs) (some 4); + r8 <- Test_eq "nth" (nth 1 ys) (some 3); + + r9 <- Test_neq "set-nth" (nth 1 ys) (nth 1 ws); + r10 <- Test_eq "set-nth" (nth 1 ws) (some 7); + + success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 + (and r5 (and r6 (and r7 (and r8 (and r9 r10)))))))))); + + if success then + (Test_info "MYERS LIST" "test on Myers list succeeded") + else + (Test_warning "MYERS LIST" "test on Myers list failed"); + + %% IO_return success; +}; + ===================================== samples/plain_let_test.typer ===================================== @@ -0,0 +1,37 @@ +%%%% +%%%% Unit tests for `plain-let` +%%%% + +f : Int; +f = 3; + +g : Int; +g = 5; + +fun = plain-let + f x = f + x; + g = g; + a = 10; +in lambda x -> (f x) + g; + +test = do { + Test_info "PLAIN-LET" ""; + + r0 <- Test_eq "fun 0" (fun 0) 8; + r1 <- Test_eq "fun 7" (fun 7) 15; + + success <- IO_return (and r0 r1); + + if success then + (Test_info "PLAIN-LET" "test on plain-let succeeded") + else + (Test_warning "PLAIN-LET" "test on plain-let failed"); + + IO_return success; +}; + +exec-test = do { + b1 <- test; + + IO_return b1; +}; ===================================== samples/table.typer ===================================== @@ -59,7 +59,7 @@ length t = case t %% Is the tree empty? %% -is-empty t = Int_eq (length t) 0; +empty? t = Int_eq (length t) 0; %% %% Find an element in the tree and return it @@ -94,8 +94,8 @@ in case tree %% Is this element in the tree? %% -member : (a : Type) ≡> a -> Table a -> Bool; -member elem tree = case (find elem tree) +member? : (a : Type) ≡> a -> Table a -> Bool; +member? elem tree = case (find elem tree) | some _ => true | none => false; @@ -128,7 +128,7 @@ insert elem tree = let (table-node table-nil (table-leaf (Int_lsr h1 1) es)))) | table-nil => table-leaf h (cons e nil); -in if (member elem tree) then +in if (member? elem tree) then (case tree % we may want to replace a variable (partial comparison function) | table s c h t => table s c h (helper elem c (h elem) t)) else @@ -142,16 +142,16 @@ in if (member elem tree) then remove : (a : Type) ≡> a -> Table a -> Table a; remove elem tree = let - is-empty : TableTree a -> Bool; - is-empty t = case t - | table-node l r => if (is-empty l) then - (is-empty r) else + empty? : TableTree a -> Bool; + empty? t = case t + | table-node l r => if (empty? l) then + (empty? r) else (false) | table-leaf _ es => Int_eq 0 (List_length es) | table-nil => true; pop-empty : TableTree a -> TableTree a; - pop-empty t = if (is-empty t) then + pop-empty t = if (empty? t) then (table-nil) else (t); @@ -174,7 +174,7 @@ remove elem tree = let (table-leaf h1 es) % element not found | table-nil => table-nil; % element not found -in if (member elem tree) then +in if (member? elem tree) then (case tree | table s c h t => table (s - 1) c h (helper elem c (h elem) t)) else @@ -230,9 +230,9 @@ udict-insert : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); udict-insert k d t = insert (pair k (some d)) t; -udict-member : (Key : Type) ≡> (Data : Type) ≡> Key -> +udict-member? : (Key : Type) ≡> (Data : Type) ≡> Key -> Table (Pair Key (Option Data)) -> Bool; -udict-member k t = member (pair k none) t; +udict-member? k t = member? (pair k none) t; udict-remove : (Key : Type) ≡> (Data : Type) ≡> Key -> Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); @@ -242,8 +242,8 @@ udict-update : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); udict-update k d t = update (pair k (some d)) t; -udict-is-empty : (Key : Type) ≡> (Data : Type) ≡> Table (Pair Key (Option Data)) -> Bool; -udict-is-empty t = is-empty t; +udict-empty? : (Key : Type) ≡> (Data : Type) ≡> Table (Pair Key (Option Data)) -> Bool; +udict-empty? t = empty? t; %%% %%% Test helper ===================================== samples/table_test.typer ===================================== @@ -41,8 +41,8 @@ test-length = do { r3 <- Test_eq "t3" (length t3) 53; r4 <- Test_eq "t4" (length t4) 50; r5 <- Test_eq "t5" (length t5) 50; - %% r6 <- Test_eq "e0" (is-empty e0) true; - r6 <- Test_true "e0" (is-empty e0); + %% r6 <- Test_eq "e0" (empty? e0) true; + r6 <- Test_true "e0" (empty? e0); r7 <- Test_eq "e1" (length e1) 1; r8 <- Test_eq "e2" (length e2) 0; @@ -71,7 +71,7 @@ test-find = do { (Test_warning "TABLE" "find test failed"); }; -%% member is just a wrapped version of find so not need to test it +%% member? is just a wrapped version of find so not need to test it %% in the actual implementation u = (IO_run test-length) (); View it on GitLab: https://gitlab.com/monnier/typer/compare/451ead238502f3e4bde114c17a312622de… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/451ead238502f3e4bde114c17a312622de… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] Documentation, work in progress
by Jonathan Graveline 23 Aug '18

23 Aug '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 451ead23 by Jonathan Graveline at 2018-08-23T20:56:11Z Documentation, work in progress Some more tests in samples/case_test.typer - - - - - 10 changed files: - btl/builtins.typer - btl/case.typer - btl/do.typer - btl/list.typer - btl/pervasive.typer - btl/plain-let.typer - btl/polyfun.typer - btl/tuple.typer - samples/case_test.typer - tests/eval_test.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -255,44 +255,101 @@ Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; +%% %% gensym for macro - +%% Generate pseudo-unique symbol +%% At least they cannot be obtained outside macro +%% In macro you should NOT use symbol of the form ` %gensym% ...` +%% gensym = Built-in "gensym" : Unit -> IO Sexp; -%% Function on Elab_Context +%%%% Function on Elab_Context +%% +%% Get the current context of elaboration +%% Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context; +%% +%% Check if a symbol is defined in a particular context +%% Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; +%% +%% Check if a symbol is a constructor in a particular context +%% Elab_isconstructor = Built-in "Elab.isconstructor" : String -> Elab_Context -> Bool; +%% +%% Check if the n'th field of a constructor is erasable +%% If the constructor isn't defined it will always return false +%% Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_Context -> Bool; +%% +%% Check if a field of a constructor is erasable +%% If the constructor or the field aren't defined it will always return false +%% Elab_is-arg-erasable = Built-in "Elab.is-arg-erasable" : String -> String -> Elab_Context -> Bool; +%% +%% Get n'th field of a constructor +%% It return "_" in case the field isn't defined +%% see pervasive.typer for a more convenient function +%% Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String; +%% +%% Get the position of a field in a constructor +%% It return -1 in case something isn't defined +%% see pervasive.typer for a more convenient function +%% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; +%% +%% Get the docstring associated with a symbol +%% Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; %%%% Unit test helper IO +%% %% Print message and/or fail (terminate) %% These message are registered like any other error +%% And location is printed before the error +%% +%% Voluntarily fail +%% for exemple if next unit tests are not worth testing +%% +%% Takes a "section" and a "message" as argument +%% Test_fatal = Built-in "Test.fatal" : String -> String -> IO Unit; + +%% +%% Throw a warning, very similar to `Test_info` +%% but it's possible to implement a parameter for user who want it to sometimes be fatal +%% +%% Takes a "section" and a "message" as argument +%% Test_warning = Built-in "Test.warning" : String -> String -> IO Unit; + +%% +%% Just print a message with location of the call +%% +%% Takes a "section" and a "message" as argument +%% Test_info = Built-in "Test.info" : String -> String -> IO Unit; +%% %% Get a string representing location of call ("file:line:column") - +%% Test_location = Built-in "Test.location" : Unit -> String; -%% Do some test which print a message - +%% +%% Do some test which print a message: "[ OK]" or "[FAIL]" +%% Test_true = Built-in "Test.true" : String -> Bool -> IO Bool; Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; Test_eq = Built-in "Test.eq" : (a : Type) ≡> String -> a -> a -> IO Bool; ===================================== btl/case.typer ===================================== @@ -7,6 +7,12 @@ %%%% a constructor with or without argument and %%%% argument may be sub pattern or variable) %%%% +%%%% Actualy this macro instantiate tuple when there's many variables to match +%%%% but matching an already instantiated +%%%% tuple (in a variable) is more difficult... +%%%% +%%%% Another problem is that this macro is dependent of tuple implementation +%%%% %% Move IO outside List (from element to List) %% (Was helpful for me when translating code that used to not be IO code) @@ -30,14 +36,18 @@ in do { %% Takes a List of Sexp and generate a List of new name of the same length %% whatever are the element of the List %% - gen-vars : List Sexp -> IO (List Sexp); gen-vars vars = io-list (List_map (lambda _ -> gensym ()) vars); -tuple-ctor : List Sexp -> Sexp; -tuple-ctor args = let +%% +%% Constructor for a tuple +%% +%% Used in patterns +%% +tuple-ctor : Sexp; +tuple-ctor = let ctor : Sexp; ctor = Sexp_symbol "cons"; @@ -53,7 +63,6 @@ in Sexp_node (Sexp_symbol "##datacons") %% become %% `cons expr1 expr2 ... ` %% - expand-tuple-ctor : Sexp -> Sexp; expand-tuple-ctor sexp = let @@ -62,7 +71,7 @@ expand-tuple-ctor sexp = let in Sexp_dispatch sexp (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_\,_")) then - (Sexp_node (tuple-ctor ss) ss) + (Sexp_node tuple-ctor ss) else (Sexp_node s ss)) (lambda _ -> sexp) @@ -71,14 +80,13 @@ in Sexp_dispatch sexp %% %% Is tuple %% - is-tuple : Sexp -> Bool; is-tuple sexp = let sfalse = (lambda _ -> false); in Sexp_dispatch sexp - (lambda s _ -> Sexp_eq s (tuple-ctor nil)) + (lambda s _ -> Sexp_eq s tuple-ctor) sfalse sfalse sfalse sfalse sfalse; %% @@ -92,7 +100,6 @@ in Sexp_dispatch sexp %% (This function is now doing nothing since there's only one %% variable at any time: one expression or a tuple of expressions) %% - get-tup-exprs : Sexp -> List Sexp; get-tup-exprs sexp = let @@ -112,7 +119,6 @@ in Sexp_dispatch sexp %% %% Some alias to clarify type of functions %% - Var = Sexp; Pat = Sexp; Pats = List Pat; @@ -129,15 +135,16 @@ is-dflt : Var -> Bool; is-dflt v = Sexp_eq dflt-var v; %% -%% Get pattern to match as a List of pair -%% with all patterns and the user code for each branches +%% Takes a list of variable to match and a list of branch as "_=>_"-node +%% Returns pattern to match as a List of pair +%% with all patterns and user code for each branches %% - get-branches : List Sexp -> List Sexp -> List (Pair Pats Code); get-branches vars sexps = let perr = (lambda _ -> pair (cons Pat_error nil) Code_error); + %% here, sexp is a node of patterns (the lhs of a "_=>_"-node) to-case : Sexp -> Pair Pats Code; to-case sexp = let @@ -150,26 +157,37 @@ get-branches vars sexps = let in Sexp_dispatch sexp (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) - % expecting a Sexp_node as second argument to _=>_ + %% expecting a Sexp_node as second argument to _=>_ | true => pair (tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) | false => pair (cons Pat_error nil) Code_error) perr perr perr perr perr; + %% map all "_=>_"-node to (patterns, body) pair helper : List Sexp -> List (Pair Pats Code); helper sexps = List_map (lambda s -> (to-case s)) sexps; in helper sexps; +%% +%% Takes a patterns +%% Returns a list of Bool: +%% - true at n if n'th argument is erasable +%% - false at n if n'th argument is not erasable +%% kinds : Sexp -> IO (List Bool); kinds pat = let - serr = lambda _ -> Sexp_error; - + %% + %% errors used in Sexp_dispatch + %% + serr = lambda _ -> Sexp_error; strerr = lambda _ -> "< error >"; - - xserr = lambda _ -> (nil : List Sexp); + xserr = lambda _ -> (nil : List Sexp); + %% + %% Get constructor of `pat` + %% ctor : String; ctor = let ctor-name : Sexp -> String; @@ -179,12 +197,18 @@ kinds pat = let strerr strerr strerr strerr; in ctor-name pat; + %% + %% Get args from the `pat` node + %% args : List Sexp; args = Sexp_dispatch pat (lambda s ss -> ss) (lambda _ -> (nil : List Sexp)) xserr xserr xserr xserr; + %% + %% Just get a String from a symbol + %% str_of_sym : Sexp -> String; str_of_sym arg = Sexp_dispatch arg (lambda _ _ -> "< error >") @@ -194,6 +218,16 @@ kinds pat = let (lambda _ -> "< error >") (lambda _ -> "< error >"); + %% + %% map function for all pattern's variables + %% Check if each argument are erasable or not + %% It must handle 3 things (but could handle more): + %% - all arguments are in the order of the type's declaration (named or not) + %% - all arguments are without name `(_ := x)` + %% - all arguments are with a name in any order `(name := x)` + %% What I do not expect to work is a combinaison of + %% arguments with name, other without name and all this in a random order + %% mf : Elab_Context -> Sexp -> Int -> Bool; mf env arg i = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:=_")) then @@ -228,34 +262,63 @@ in ks; %% Takes a pattern and a list of new name for each argument %% It even rename sub pattern %% - renamed-pat : Sexp -> List Sexp -> IO Sexp; renamed-pat pat names = let - serr = lambda _ -> Sexp_error; - + %% + %% errors used in Sexp_dispatch + %% + serr = lambda _ -> Sexp_error; strerr = lambda _ -> "< error >"; + xserr = lambda _ -> (nil : List Sexp); - xserr = lambda _ -> (nil : List Sexp); - + %% + %% true if `pat` is a tuple, false if it is a + %% single expression + %% tup : Bool; tup = is-tuple pat; + %% + %% Get the name of the n'th element of any tuple + %% tuple-nth : Int -> Sexp; tuple-nth n = Sexp_symbol (String_concat "%" (Int->String n)); + %% + %% Get the constructor of the pattern as argument + %% + ctor : Sexp -> String; + ctor pat = Sexp_dispatch pat + (lambda s _ -> ctor s) + (lambda s -> s) + strerr strerr strerr strerr; + + %% + %% Map function to rename `pat` with symbol in `names` + %% + %% `kinds` is curried before being passed to `List_mapi` + %% and tell if an argument is erasable + %% + %% Produce code according to argument kind + %% and if it already use explicit field or not + %% mf : List Bool -> Sexp -> Int -> Sexp; mf kinds v i = Sexp_dispatch v (lambda sym ss -> if (Sexp_eq sym (Sexp_symbol "_:=_")) then if (List_nth i kinds false) then + %% %% if client use multiple name for the same erasable args, %% I expect it to not compile... + %% (Sexp_node sym ss) else (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) else if tup then + %% %% tuples argument are all implicit so we must take special care of those + %% (Sexp_node (Sexp_symbol "_:=_") (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else @@ -266,12 +329,6 @@ renamed-pat pat names = let else (List_nth i names Sexp_error)) serr serr serr serr; - - ctor : Sexp -> String; - ctor pat = Sexp_dispatch pat - (lambda s _ -> ctor s) - (lambda s -> s) - strerr strerr strerr strerr; in do { pat <- IO_return pat; @@ -286,14 +343,18 @@ in do { %% Takes an Sexp as argument and IO_return `IO true` if it is a pattern %% (i.e. a constructor with or without argument) %% - is-pat : Pat -> IO Bool; is-pat pat = let - err = lambda _ -> IO_return false; - + %% + %% errors used in Sexp_dispatch + %% + err = lambda _ -> IO_return false; serr = lambda _ -> "< error >"; + %% + %% Get a String from a Sexp_symbol + %% sym-str : Sexp -> String; sym-str sexp = Sexp_dispatch sexp (lambda _ _ -> serr ()) @@ -314,38 +375,55 @@ in Sexp_dispatch pat err err err err; %% -%% Takes two pattern and IO_return `IO true` if the two pattern -%% has the same constructor +%% Takes two pattern and return true if the two pattern +%% has the same constructor %% - is-same-ctor : Pat -> Pat -> Bool; is-same-ctor p0 p1 = let + %% + %% error used in Sexp_dispatch + %% err = lambda _ -> Pat_error; + %% + %% Get the constructor of a pattern + %% ctor-of : Pat -> Sexp; ctor-of p = Sexp_dispatch p (lambda s _ -> s) (lambda s -> Sexp_symbol s) err err err err; +%% Compare head of node of both pattern in Sexp_eq (ctor-of p0) (ctor-of p1); %% %% Get variable introduced by a constructor %% -%% Takes a pattern as argument and IO_return each arguments -%% of the constructor which is a variable (as opposed to a sub pattern) +%% Takes a pattern as argument and return each arguments +%% of the constructor which is a variable (as opposed to a sub pattern) %% - introduced-vars : Pat -> IO (List Var); introduced-vars pat = let + %% + %% error used in Sexp_dispatch + %% serr = lambda _ -> IO_return (pair 0 nil); + %% + %% List of kind of pattern argument + %% ks : IO (List Bool); ks = kinds pat; + %% + %% Function to fold each argument of the pattern + %% The Int is used internaly to keep track of argument index + %% It is useful to know where is the variable in `ks` to get its kind + %% (kind is actualy only erasable or not here) + %% ff : IO (Pair Int (List Sexp)) -> Sexp -> IO (Pair Int (List Sexp)); ff p v = let @@ -389,7 +467,7 @@ in Sexp_dispatch pat IO_return (case p | pair _ xs => xs); }) - (lambda _ -> IO_return nil) % constructor as a unique symbol (as `true`) + (lambda _ -> IO_return nil) % constructor as a unique symbol (`true`, etc) (lambda _ -> IO_return nil) (lambda _ -> IO_return nil) % error (lambda _ -> IO_return nil) (lambda _ -> IO_return nil); % error @@ -397,7 +475,6 @@ in Sexp_dispatch pat %% Wrap the third argument (`fun`) with a `let` definition for each variables %% Names are taken from `rvars` and definition are taken from `ivars` %% - wrap-vars : List Var -> List Var -> Code -> Code; wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> %% @@ -408,13 +485,15 @@ wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> fun ivars rvars; %% -%% Take a List of branches and IO_return a List of the first pattern in each branches +%% Take a List of branches and return a List of the first pattern in each branches %% (I must keep the order from input to ouput) %% - head-pats : List (Pair Pats Code) -> List Pat; head-pats ps = let + %% + %% Map function just returning the first patterns for one branch + %% mf : Pair Pats Code -> Pat; mf p = case p | pair pats _ => (List_nth 0 pats Pat_error); @@ -423,10 +502,9 @@ in List_map mf ps; %% %% Takes a pattern as argument and -%% IO_return a List of sub pattern for that branch -%% the List contain dflt-var if it has a variable which is not a pattern +%% return a List of sub pattern for that branch +%% the List contain dflt-var if it has a variable which is not a pattern %% - pattern-sub-pats : Pat -> IO (List Pat); pattern-sub-pats pat = let @@ -439,7 +517,6 @@ pattern-sub-pats pat = let %% if another branch has a sub pattern %% at this position %% - map-arg : Var -> IO Var; map-arg arg = do { b <- is-pat arg; @@ -462,11 +539,10 @@ in Sexp_dispatch pat err err err err; %% -%% Takes a List of similar pattern (i.e. a pattern of same constructor) -%% IO_return a List of gensym variable if there's is a sub pattern -%% and a default variable when there's no sub pattern +%% Takes a List of similar pattern (i.e. patterns with same constructor) +%% Returns a List of gensym variable if there is a sub pattern +%% and a default variable when there is no sub pattern %% - pattern-sub-pats-vars : List Var -> List (Pair Pat (List (Pair Var Var))) -> IO (List Var); pattern-sub-pats-vars rvars branches = let @@ -504,13 +580,12 @@ pattern-sub-pats-vars rvars branches = let in List_foldl ff (IO_return nil) pats; %% -%% IO_return a List of old/new variables names +%% Return a List of old/new variables names %% -%% new variable should be identical for each branches -%% but old variable (from user code) are arbitrary -%% (except for explicit field pattern...) +%% New variable should be identical for each branches +%% but old variable (from user code) are arbitrary +%% (except for explicit field pattern...) %% - pattern-term : Pat -> List Var -> IO (List (Pair Var Var)); pattern-term pat rvars = let @@ -530,22 +605,24 @@ in do { %% %% Type of one partition of branches (one branch with some possible child branches) %% -%% pair of renamed pat, variables old/new in each branch and List of next branch -%% a branch with a pattern with old/new variables for each next branches -%% and each next branches from this branch +%% Pair of +%% Triplet of renamed pat, +%% original variable, +%% variables old/new and original pattern in each branch +%% List of next branch %% - part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); %% -%% IO_return a pair of renamed and partitioned pattern -%% (i.e. a Pair of renamed pattern, introduced variables, old pattern and tail of branches) -%% (Yeah, I need old pattern to get sub pattern at some point) +%% Takes a list of branches (pair of (patterns, body)) +%% Return a list of partition %% - partition-branches : List (Pair Pats Code) -> IO (List part-type); partition-branches branches = let + %% + %% Remove the first pattern of all `branches` + %% tl-branches : List (Pair Pats Code); tl-branches = let @@ -555,6 +632,9 @@ partition-branches branches = let in List_map mf branches; + %% + %% Pull the first patterns of all branches and keep the tails + %% hd-pair : List (Pair Pat (Pair Pats Code)); hd-pair = let @@ -567,11 +647,15 @@ partition-branches branches = let %% %% Type for first step partition %% - %% Pair of List sorted with similar head (head as in first) + %% Pair of List sorted with similar head + %% they are similar when they have the same constructor %% - pre-part-type = Pair (List Pat) (List (Pair Pats Code)); + %% + %% First step partition (see `pre-part-type`) + %% from `branches` + %% pre-parts : List pre-part-type; pre-parts = let @@ -602,6 +686,9 @@ partition-branches branches = let in List_foldl ff nil hd-pair; + %% + %% `pre-part-type` to `part-type` + %% parts : IO (List part-type); parts = let @@ -633,24 +720,48 @@ in do { %% %% reminder -%% part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); +%% +%% part-type = Pair +%% (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) +%% (List (Pair Pats Code)); %% +%% +%% There's a need to merge branch because default branch may be anywhere +%% +%% (I tried to consider default branches similar to everything but it failed in some way +%% So here we are...) +%% merge-dflt : List part-type -> Option part-type -> List part-type; merge-dflt parts odflt = let + %% %% It must be bugged in one way or another... - - %% preppend child branches in case we see a default branch before a normal branch - + %% + + %% + %% Preppend child branches if we see a default branch before a normal branch + %% + %% exemple: + %% | (x,_,y) => ... + %% | (x,k,z) => ... + %% In this exemple (and in Typer) I can suppose `y != z` (or there will be warning/error) + %% If we take the first case first we did not match `k` and cannot jump to the next + %% But since `y != z` we can safely take the second first + %% preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; preppend pat vars branches part = case part | pair p b => (case p | triplet _ lv v => pair (triplet pat lv (List_concat vars v)) (List_concat branches b)); - %% append child branches in case we see more than one default branches - + %% + %% Append child branches if we see more than one default branches + %% + %% exemple: + %% | (x,_,z) => ... + %% | (x,_,_) => ... + %% append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; append pat vars branches part = case part @@ -674,9 +785,11 @@ in case parts | none => nil); %% -%% takes some branches and preppend default variable to smaller branches +%% Takes some branches and preppend default variable to smaller branches +%% +%% (Sub-pattern introduce new variable but if +%% it fail suplementary variable must match something else) %% - adjust-len : List (Pair Pats Code) -> List (Pair Pats Code); adjust-len branches = let @@ -710,27 +823,38 @@ in List_map (preppend-dflt max-len) branches; %% %% reminder +%% %% part-type = Pair %% (Triplet %% Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) %% (List (Pair Pats Code)); %% - compile-case : List Var -> List (Pair Pats Code) -> IO Code; compile-case subjects branches = let subject = (List_nth 0 subjects Var_error); + %% + %% Get partition of branches + %% parts : IO (List part-type); parts = do { ps <- partition-branches branches; IO_return (merge-dflt ps none); }; + %% + %% Takes a decomposed `part-type` and generate code from it + %% translate-sub-pats : List Var -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> IO Code; translate-sub-pats rvars pats-vars branches = let - + + %% + %% Here we consider sub-pattern with necessary suplementary variable, + %% append them to branches and generate code + %% + recursion : List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> IO Code; recursion pats-vars branches = let @@ -772,8 +896,10 @@ compile-case subjects branches = let sub-pats-vars <- sub-pats-vars; r <- IO_return (List_concat sub-pats-vars (List_tail subjects)); + %% %% As for constructor we remove variable if it is always a default %% variable without any corresponding sub pattern + %% r <- IO_return (List_foldl (lambda o v -> if (is-dflt v) then @@ -801,6 +927,9 @@ compile-case subjects branches = let in recursion pats-vars branches; + %% + %% Generate code from one `part-type` + %% translate-part : part-type -> IO Code; translate-part branch = case branch | pair patterns branches => (case patterns @@ -809,6 +938,9 @@ compile-case subjects branches = let IO_return (quote (_=>_ (uquote pat) (uquote sub-cases))); }); + %% + %% Generate code from all partition + %% translate : List part-type -> IO Code; translate parts = do { branches <- io-list (List_map translate-part parts); @@ -827,8 +959,8 @@ in do { %%% The macro we want. %%% -rec-case : List Sexp -> IO Sexp; -rec-case args = let +case-impl : List Sexp -> IO Sexp; +case-impl args = let case0 : List Sexp -> IO Sexp; case0 args = let @@ -876,4 +1008,4 @@ rec-case args = let in (Sexp_dispatch (List_nth 0 args Sexp_error) case1 err err err err err); -case-macro = macro rec-case; +case-macro = macro case-impl; ===================================== btl/do.typer ===================================== @@ -14,11 +14,21 @@ %% %% fun is a command, %% -%% do may contain do because it returns a command. +%% `do` may contain `do` because it returns a command. %% +%% +%% Operator of assignment in `do` block +%% assign = Sexp_symbol "_<-_"; +%% +%% Takes one of `;`-separated command in `do` block +%% Returns the left-hand side symbol +%% or a default symbol +%% +%% `lhs <- rhs;` +%% get-sym : Sexp -> Sexp; get-sym sexp = let @@ -32,6 +42,13 @@ get-sym sexp = let dflt-sym dflt-sym dflt-sym dflt-sym dflt-sym; % there must be a command +%% +%% Takes one of `;`-separated command in `do` block +%% Returns the right-hand side command +%% `lhs <- rhs;` +%% or +%% `rhs;` +%% get-op : Sexp -> Sexp; get-op sexp = let @@ -52,17 +69,22 @@ get-op sexp = let in if (Sexp_eq op (Sexp_symbol "")) then Sexp_error else op; +%% +%% Takes a block (`{...}`) +%% Parse the block and returns the list of command inside the block +%% get-decl : List Sexp -> List Sexp; get-decl args = let err = lambda _ -> cons Sexp_error nil; - % Expecting a Block of command separated by ";" + %% Expecting a Block of command separated by ";" node = Sexp_dispatch (List_nth 0 args Sexp_error) (lambda _ _ -> cons Sexp_error nil) err err err err + %% `Parser_newest` use the most recent environment (lambda l -> Parser_newest l); in node; @@ -76,7 +98,14 @@ in node; %% this way a-sym is defined within b-op and so on %% a-sym is now just `a` and not `IO a` %% +%% ( It could be possible to use `IO Ref` rather than a new variable +%% for each command, but will it be useful? ) +%% +%% +%% Takes the list of command inside `do` block +%% This is the `main` of macro `do` +%% set-fun : List Sexp -> Sexp; set-fun args = let ===================================== btl/list.typer ===================================== @@ -11,6 +11,8 @@ %%%% List type +%% +%% List's type is currently in pervasive.typer %% %% FIXME: "List : ?" should be sufficient but triggers %% macro `type` isn't actually defined where this file is included @@ -24,6 +26,19 @@ %%%% List functions +%% +%% Get the length of a list in O(N) times where N is the length +%% +%% Alternative (tail recursive): +%% +%% length xs = let +%% helper : (a : Type) ≡> Int -> List a -> Int; +%% helper len xs = case xs +%% | nil => len +%% | cons hd tl => helper (len + 1) tl; +%% in helper 0 xs; +%% +%% length : (a : Type) ≡> List a -> Int; length xs = case xs | nil => 0 @@ -40,21 +55,39 @@ head1 xs = case xs | nil => none | cons hd tl => some hd; +%% +%% Takes a list +%% Returns `some x` where x is the first element of the list +%% or none if the list is empty +%% head : (a : Type) ≡> List a -> Option a; head xs = case xs | cons x _ => some x | nil => none; +%% +%% Takes a list +%% Returns the same list without it's first element +%% The tail of `nil` is still `nil` +%% tail : (a : Type) ≡> List a -> List a; tail xs = case xs | nil => nil | cons hd tl => tl; +%% +%% Apply a function to all element of a list +%% +%% (Should be as `map` of every functional language) +%% map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (map f xs); +%% +%% As `map` but user's function also takes element index as last argument +%% mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; mapi = lambda f -> lambda xs -> let helper : (a -> Int -> b) -> Int -> List a -> List b; @@ -63,6 +96,10 @@ mapi = lambda f -> lambda xs -> let | cons x xs => cons (f x i) (helper f (i + 1) xs); in helper f 0 xs; +%% +%% As `map` but with 2 list at the same time +%% If they are not of the same length the result is just as long as the smallest +%% map2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c) -> List a -> List b -> List c; map2 = lambda f -> lambda xs -> lambda ys -> case xs | nil => nil @@ -70,6 +107,9 @@ map2 = lambda f -> lambda xs -> lambda ys -> case xs | nil => nil % error | cons y ys => cons (f x y) (map2 f xs ys); +%% +%% As `foldl` but user's function also takes element index as last argument +%% foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> List b -> a; foldli = lambda f -> lambda o -> lambda xs -> let helper : (a -> b -> Int -> a) -> Int -> a -> List b -> a; @@ -78,7 +118,9 @@ foldli = lambda f -> lambda o -> lambda xs -> let | cons x xs => helper f (i + 1) (f o x i) xs; in helper f 0 o xs; +%% %% Fold 2 List as long as both List are non-empty +%% fold2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c -> a) -> a -> List b -> List c -> a; fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs | cons x xs => ( case ys @@ -86,16 +128,27 @@ fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs | nil => o ) % may be an error | nil => o; % may or may not be an error +%% +%% (Should be as any `fold right` of functional language) +%% foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; foldr = lambda f -> lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (foldr f xs i); +%% +%% Takes a function and a list +%% Returns `some x` if x is the first element on the list to return true +%% when applied to the function or `none` if there was no such element +%% find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; find = lambda f -> lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => find f xs; +%% +%% Get the n'th element of a list or a default if the list is smaller +%% nth : (a : Type) ≡> Int -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d @@ -104,19 +157,34 @@ nth = lambda n -> lambda xs -> lambda d -> case xs | true => x | false => nth (n - 1) xs d; +%% +%% Reverse the element of a list +%% Common usage is `reverse ll nil` which reverse the list ll +%% reverse : (a : Type) ≡> List a -> List a -> List a; reverse = lambda l -> lambda t -> case l | nil => t | cons hd tl => reverse tl (cons hd t); +%% +%% Concat two list with first argument first +%% concat : (a : Type) ≡> List a -> List a -> List a; concat = lambda l -> lambda t -> reverse (reverse l nil) t; +%% +%% Apply all element of the list to an object through a function +%% (Should be as `fold-left` of any functional language) +%% foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; foldl = lambda f -> lambda i -> lambda xs -> case xs | nil => i | cons x xs => foldl f (f i x) xs; +%% +%% Takes a function and a list +%% Returns the list with element removed if the function return true on those element +%% remove : (a : Type) ≡> (a -> Bool) -> List a -> List a; remove = lambda f -> lambda l -> case l | nil => nil @@ -125,8 +193,10 @@ remove = lambda f -> lambda l -> case l | false => cons x (remove f xs) ); +%% %% Merge two List to a List of Pair %% Both List must be of same length +%% merge : (a : Type) ≡> (b : Type) ≡> List a -> List b -> List (Pair a b); merge = lambda xs -> lambda ys -> case xs | cons x xs => ( case ys @@ -134,8 +204,11 @@ merge = lambda xs -> lambda ys -> case xs | nil => nil ) % error | nil => nil; +%% %% `Unmerge` a List of Pair -%% The two functions name said it all +%% The two functions' name say it all +%% + map-fst : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List a; map-fst = lambda xs -> let mf : Pair a b -> a; @@ -148,12 +221,30 @@ map-snd = lambda xs -> let mf p = case p | pair _ y => y; in map mf xs; +%% %% Is argument List empty -empty : (a : Type) ≡> List a -> Bool; -empty = lambda xs -> Int_eq (length xs) 0; +%% +empty? : (a : Type) ≡> List a -> Bool; +%% +%% O(N): +%% empty? = lambda xs -> Int_eq (length xs) 0; +%% +%% O(1): +empty? = lambda xs -> case xs + | nil => true + | _ => false; +%%%% %%%% Sorting List +%%%% +%% +%% Using Quicksort but not in-place +%% Takes a comparison function and a list +%% Returns the same list but sorted +%% +%% If comparison is `>` then the list start with the smallest element +%% sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; sort = lambda o -> lambda l -> let @@ -161,12 +252,19 @@ sort = lambda o -> lambda l -> let sortp = lambda p -> lambda lt -> lambda gt -> lambda l -> case p | none => nil | some (pp) => ( case l - | nil => ( let + | nil => ( let + + %% Sort the two sub-list + %% With the head as pivot ltp : List a; ltp = sortp (head1 lt) nil nil (tail lt); gtp : List a; gtp = sortp (head1 gt) nil nil (tail gt); + + %% concatenate because we can't do it in-place in concat ltp (cons pp gtp) ) | cons x xs => ( case (o x pp) + + %% partition with `p` as pivot | true => sortp p lt (cons x gt) xs | false => sortp p (cons x lt) gt xs ) @@ -176,6 +274,12 @@ in sortp (head1 l) nil nil (tail l); %%%% Some algo on sorted list +%% +%% Find an element with a shortcut because the list is sorted +%% Takes a comparison function, a function to match, an element and a list +%% +%% (...maybe to parametric for what it does, this function is useless) +%% sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a; sfind = lambda o -> lambda f -> lambda a -> lambda l -> case l | nil => none @@ -187,6 +291,10 @@ sfind = lambda o -> lambda f -> lambda a -> lambda l -> case l ) ); +%% +%% Takes a function and a list +%% Returns all element which return true when applied to the function +%% sall : (a : Type) ≡> (a -> Bool) -> List a -> List a; sall = lambda f -> lambda l -> case l | nil => nil @@ -195,11 +303,18 @@ sall = lambda f -> lambda l -> case l | false => sall f xs ); -sexist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool; -sexist = lambda o -> lambda f -> lambda a -> lambda l -> case (sfind o f a l) +%% +%% Is some element member of the list? +%% +sexist? : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool; +sexist? = lambda o -> lambda f -> lambda a -> lambda l -> case (sfind o f a l) | none => false | some _ => true; +%% +%% Insert an element into an already sorted list +%% Takes a comparison function, an element to insert and a list +%% sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; sinsert = lambda o -> lambda a -> lambda l -> case l | nil => cons a l @@ -208,6 +323,12 @@ sinsert = lambda o -> lambda a -> lambda l -> case l | false => cons x (sinsert o a xs) ); +%% +%% Takes a comparison function, a pivot and a list +%% Returns the sub-list with all element "greater" than pivot +%% (For exemple if the comparison function is `>` then it returns +%% all element greater or equal to pivot) +%% ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; ssup = lambda o -> lambda a -> lambda l -> case l | nil => nil @@ -216,6 +337,12 @@ ssup = lambda o -> lambda a -> lambda l -> case l | false => ssup o a xs ); +%% +%% Takes a comparison function, a pivot and a list +%% Returns the sub-list with all element "smaller" than pivot +%% (For exemple if the comparison function is `>` then it returns +%% all element smaller than pivot) +%% sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; sinf = lambda o -> lambda a -> lambda l -> case l | nil => nil @@ -228,6 +355,9 @@ sinf = lambda o -> lambda a -> lambda l -> case l %%%% Array from List %%%% +%% +%% Takes a list and returns an array with the same element in the same order +%% List->Array : (a : Type) ≡> List a -> Array a; List->Array xs = let ===================================== btl/pervasive.typer ===================================== @@ -362,12 +362,6 @@ type-impl = lambda (x : List Sexp) -> type_ = macro type-impl; -%%%% Backward compatibility - -length = List_length; -head = List_head1; -tail = List_tail; - %%%% Tuples %% Sample tuple: a module holding Bool and its constructors. @@ -585,10 +579,10 @@ _|_ = let lib = load "btl/polyfun.typer" in lib._|_; %% because of circular dependency... %% -%% A macro using `load` for testing purpose +%% A macro using `load` for unit testing purpose %% -%% takes a file name (String) as argument -%% return variable named `exec-test` from the loaded file +%% Takes a file name (String) as argument +%% Return variable named `exec-test` from the loaded file %% %% `exec-test` should be a command doing unit tests %% for other purpose than that just use `load` directly! ===================================== btl/plain-let.typer ===================================== @@ -11,16 +11,34 @@ %% List_reverse = list.reverse; %% List_tail = list.tail; +%% +%% The idea is to use unique identifier in a first let +%% and then assign those first identifier to the original symbol +%% +%% Useful for auto-generated code (macro, ...) +%% + +%% +%% Takes the plain input of macro `plain-let` +%% impl : List Sexp -> IO Sexp; impl args = let + %% error use in Sexp_dispatch serr = lambda _ -> Sexp_error; + %% Takes an assignment statement and return a new + %% symbol for the resulting variable + %% For function it only rename the function name and not the argument gen-sym : Sexp -> IO Sexp; gen-sym arg = let + %% error use in Sexp_dispatch io-serr = lambda _ -> IO_return Sexp_error; + %% Get a `gensym` symbol + %% I can rename a function name (not the argument) + %% or just a symbol rename : Sexp -> IO Sexp; rename sexp = Sexp_dispatch sexp (lambda _ ss -> do { @@ -36,6 +54,7 @@ impl args = let (IO_return Sexp_error)) io-serr io-serr io-serr io-serr io-serr; + %% Takes an assignment statement and return the right-hand side get-def : Sexp -> Sexp; get-def arg = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then @@ -43,6 +62,7 @@ impl args = let (Sexp_error)) serr serr serr serr serr; + %% Takes an assignment statement and return the left-hand side get-var : Sexp -> Sexp; get-var arg = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then @@ -50,6 +70,7 @@ impl args = let (Sexp_error)) serr serr serr serr serr; + %% Takes a list of assignment and return a list of pair of `gensym` and definition (rhs) get-sym-def : List Sexp -> IO (List (Pair Sexp Sexp)); get-sym-def args = do { r <- List_foldl (lambda o arg -> do { @@ -61,6 +82,8 @@ impl args = let IO_return r; }; + %% Takes a list of assignment and the output of `get-sym-def` + %% Returns a list of pair of `gensym` and original symbol get-var-sym : List Sexp -> List (Pair Sexp Sexp) -> IO (List (Pair Sexp Sexp)); get-var-sym args syms = let @@ -77,12 +100,19 @@ impl args = let IO_return r; }; + %% Takes a list of assignment and a body (likely using those assignment) + %% Returns a `let ... in ...` construction let-in : Sexp -> Sexp -> Sexp; let-in decls body = Sexp_node (Sexp_symbol "let_in_") (cons decls (cons body nil)); + %% Takes a list of assignment and separate them with `;` let-decls : List Sexp -> Sexp; let-decls decls = Sexp_node (Sexp_symbol "_;_") decls; + %% Takes lists of pairs (`gensym`,definition) and (`gensym`,original symbol) + %% and the body (likely using original symbol) + %% Returns + %% let [gensym] = [definition] ... in let [original symbol] = [gensym] in [body] gen-code : List (Pair Sexp Sexp) -> List (Pair Sexp Sexp) -> Sexp -> Sexp; gen-code sym-def var-sym body = let @@ -96,6 +126,7 @@ impl args = let in let-in (let-decls decls0) (let-in (let-decls decls1) body); + %% Returns a list of assignment from a "_;_"-node get-decls : Sexp -> List Sexp; get-decls sexp = let @@ -108,6 +139,8 @@ impl args = let xserr xserr xserr xserr xserr; in do { + %% get list of pair and use it to generate `plain-let` + defs <- IO_return (get-decls (List_nth 0 args Sexp_error)); body <- IO_return (List_nth 1 args Sexp_error); sym-def <- get-sym-def defs; @@ -116,7 +149,9 @@ in do { IO_return (gen-code sym-def var-sym body); }; +%% just calling the `impl` function in a macro plain-let-macro = macro (lambda args -> do { r <- impl args; + %% Sexp_debug_print r; IO_return r; }); ===================================== btl/polyfun.typer ===================================== @@ -1,12 +1,15 @@ %%%% %%%% Polymorphic function %%%% +%%%% ( ^ I'm not sure about the name) %%%% (Just a `case` at function definition level) %%%% +%% error use in Sexp_dispatch serr : (a : Type) ≡> a -> Sexp; serr = lambda _ -> Sexp_error; +%% other error for Sexp_dispatch xserr : (a : Type) ≡> a -> List Sexp; xserr = lambda _ -> (nil : List Sexp); @@ -14,15 +17,25 @@ xserr = lambda _ -> (nil : List Sexp); %% List_map = list.map; %% List_tail = list.tail; +%% +%% Takes a function node with its argument and the body as a second argument +%% Returns a definition with a `;` +%% fun-decl : Sexp -> Sexp -> Sexp; fun-decl decl body = Sexp_node (Sexp_symbol "_;_") (cons (quote ( (uquote decl) = (uquote body) )) nil); +%% +%% Sexp_node (Sexp_symbol "_;_") (cons +%% (Sexp_node (Sexp_symbol "_=_") (cons decl (cons body nil))) +%% nil); +%% -%% Sexp_node (Sexp_symbol "_;_") (cons -%% (Sexp_node (Sexp_symbol "_=_") (cons decl (cons body nil))) -%% nil); - +%% +%% Takes a function node with it's argument (`f x y`) +%% Returns a list of the symbol of every argument +%% (for `f (x : Int) y` it returns a list containing symbol "x" and "y") +%% fun-args : Sexp -> List Sexp; fun-args decl = Sexp_dispatch decl (lambda s ss -> let @@ -40,6 +53,10 @@ fun-args decl = Sexp_dispatch decl in List_map mf ss) xserr xserr xserr xserr xserr; +%% +%% Takes a list of "_=>_"-node +%% Returns a list of pair of (pattern, body) +%% fun-cases : List Sexp -> List (Pair Sexp Sexp); fun-cases args = let @@ -58,6 +75,10 @@ fun-cases args = let in List_map mf args; +%% +%% Takes argument list and list of pair of (pattern, body) +%% Returns a function with a `case` on argument for each pattern +%% cases-to-sexp : List Sexp -> List (Pair Sexp Sexp) -> Sexp; cases-to-sexp vars cases = let @@ -77,14 +98,22 @@ in Sexp_node (Sexp_symbol "case_") (cons (List_nth 0 vars Sexp_error)) (List_map mf cases))) nil); +%% +%% The macro we want +%% +%% I expect a function node and then "_=>_"-nodes +%% _|_ = macro (lambda args -> let + %% function with argument (e.g. `f x y`) decl : Sexp; decl = List_nth 0 args Sexp_error; + %% symbol to match fargs : List Sexp; fargs = fun-args decl; + %% pattern for argument match cases : List (Pair Sexp Sexp); cases = fun-cases (List_tail args); ===================================== btl/tuple.typer ===================================== @@ -2,6 +2,8 @@ %%%% macro '_,_' for tuple %%%% +%% +%% Here's an exemple similar to tuple from `load` %% %% Sample tuple: a module holding Bool and its constructors. %% @@ -53,17 +55,26 @@ in do { %% Takes a List of Sexp and generate a List of new name of the same length %% whatever are the element of the List %% - gen-vars : List Sexp -> IO (List Sexp); gen-vars vars = io-list (List_map (lambda _ -> gensym ()) vars); +%% +%% Reference for tuple's implicit field name +%% +%% Takes a list of vars (it could actually only takes a length) +%% Returns symbol `%n` with n from 0 to the length of the argument +%% gen-tuple-names : List Sexp -> List Sexp; gen-tuple-names vars = List_mapi (lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i))) vars; +%% +%% Takes a list +%% Returns a list of the same length with every element set to "?" symbol +%% gen-deduce : List Sexp -> List Sexp; gen-deduce vars = List_map (lambda _ -> Sexp_symbol "?") @@ -73,12 +84,17 @@ gen-deduce vars = List_map %%% Access one tuple's element %%% -%% tuple-nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type; - +%% +%% This is a macro with conceptualy this signature: +%% tuple-nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type; +%% +%% Returns the n'th element of the tuple +%% tuple-nth = macro (lambda args -> let nerr = lambda _ -> (Int->Integer (-1)); + %% argument `n` of this macro n : Integer; n = Sexp_dispatch (List_nth 1 args Sexp_error) (lambda _ _ -> nerr ()) @@ -86,9 +102,11 @@ tuple-nth = macro (lambda args -> let (lambda n -> n) nerr nerr; + %% implicit tuple field name elem-sym : Sexp; elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); + %% tuple, argument of this macro tup : Sexp; tup = List_nth 0 args Sexp_error; @@ -99,10 +117,18 @@ in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) %%% Affectation, unwraping tuple %%% +%% +%% syntax: +%% (x, y, z) <- p; +%% +%% and then `x`, `y`, `z` are defined from tuple's element 0, 1, 2 +%% assign-tuple = macro (lambda args -> let xserr = lambda _ -> (nil : List Sexp); + %% Expect a ","-node + %% Returns variables get-tup-elem : Sexp -> List Sexp; get-tup-elem sexp = Sexp_dispatch sexp (lambda s ss -> @@ -112,6 +138,8 @@ assign-tuple = macro (lambda args -> let (nil)) xserr xserr xserr xserr xserr; + %% map every tuple's variable + %% using `tuple-nth` to assign element to variable mf : Sexp -> Sexp -> Int -> Sexp; mf t arg i = Sexp_node (Sexp_symbol "_=_") (cons arg (cons (Sexp_node (Sexp_symbol "tuple-nth") @@ -137,12 +165,18 @@ wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) fun ivars rvars; +%% +%% Takes a list of values as Sexp (like 1, 1.0, "str", etc) +%% Returns a tuple containing those values +%% make-tuple-impl : List Sexp -> IO Sexp; make-tuple-impl values = let + %% map tuple element declaration mf1 : Sexp -> Sexp -> Sexp; mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil)); + %% map tuple element value mf2 : Sexp -> Sexp -> Sexp; mf2 value nth = Sexp_node (Sexp_symbol "_:=_") (cons nth (cons value nil)); @@ -168,6 +202,9 @@ in do { IO_return affect; }; +%% +%% Macro to instantiate a tuple +%% make-tuple = macro (lambda args -> do { r <- make-tuple-impl args; r <- IO_return r; @@ -175,7 +212,10 @@ make-tuple = macro (lambda args -> do { }); %% - +%% Macro returning the type of a tuple +%% +%% Takes element's type as argument +%% tuple-type = macro (lambda args -> let mf : Sexp -> Sexp -> Sexp; ===================================== samples/case_test.typer ===================================== @@ -49,6 +49,12 @@ dflt2 a b c = case (a,b,c) | (true,false,_) => 1 | (_,_,_) => 0; +dflt3 : Bool -> Bool -> Bool -> Int; +dflt3 a b c = case (a,b,c) + | (_,_,true) => 777 + | (_,false,false) => 888 + | (_,_,_) => 999; + nand : Bool -> Bool -> Bool; nand b0 b1 = case (b0,b1) | (true,true) => false @@ -80,6 +86,10 @@ test-dflt = do { r18 <- Test_true "nand" (nand false true); r19 <- Test_true "nand" (nand false false); + r20 <- Test_eq "dflt3" (dflt3 true false false) 888; + r21 <- Test_eq "dflt3" (dflt3 true true false) 999; + r22 <- Test_eq "dflt3" (dflt3 true false true) 777; + part1 <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 r7))))))); @@ -88,7 +98,9 @@ test-dflt = do { part3 <- IO_return (and r16 (and r17 (and r18 r19))); - success <- IO_return (and part1 (and part2 part3)); + part4 <- IO_return (and r20 (and r21 r22)); + + success <- IO_return (and part1 (and part2 (and part3 part4))); if success then (Test_info "MACRO CASE" "test on default succeeded") ===================================== tests/eval_test.ml ===================================== @@ -264,9 +264,9 @@ let _ = test_eval_eqv_named nil' = datacons List' nil; my_list' = (cons' 1 nil');" - "length my_list; - head my_list; - head (tail my_list)" + "list.length my_list; + list.head my_list; + list.head (list.tail my_list)" "4; some 1; some 2" View it on GitLab: https://gitlab.com/monnier/typer/commit/451ead238502f3e4bde114c17a312622de7… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/451ead238502f3e4bde114c17a312622de7… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][bosn] Restructure sections and figures; correct some awkward phrasing
by Nathaniel 23 Aug '18

23 Aug '18

Nathaniel pushed to branch bosn at Stefan / Typer Commits: 57ed864b by nbos at 2018-08-22T22:36:04Z Restructure sections and figures; correct some awkward phrasing - - - - - 1 changed file: - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/typer_theory.tex ===================================== @@ -17,49 +17,24 @@ \maketitle -\section{Introduction} -We here formalize the Typer language and prove some of its properties. The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructions (CC) \cite{CC} enriched with the following features: +We here formalize the Typer language and prove some of its properties. + +\section{Typer's Type Theory} +The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructions (CC) \cite{CC} enriched with the following features: \begin{itemize} \renewcommand{\labelitemi}{$-$} \setlength\itemsep{-3pt} -\item An infinite hierarchy of type universes \`a la Russell similar to the one found in Luo's Extended Calculus of Constructions (ECC) \cite{luo}, but without cumulativity; +\item An infinite hierarchy of predicative type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity; +\item A parallel hierarchy of impredicative universes \item Universe polymorphism allowing the parametrization of type universes; \item Erasure of propositional arguments with decidable type checking from Barras and Bernardo's variant of Miquel's Implicit Calculus of Constructions (ICC) \cite{bruno}\cite{miquel}; \item Inductive definitions as presented by Gim\'enez in \cite{gimenez}. \end{itemize} -\section{Typer's Type Theory} -\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga \~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon (;) and enriched with additional declarations with a comma (,). We write the empty context as a dot ($\cdot$) and the set of declared variables in a context $\Ga$ as $\dv{\Ga}$. The set of free (i.e. unbound) variables in a term $T$ is written $\fv{T}$. The expression $M\{N/x\}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$. - -\begin{figure}[h] - \ \\ \ \\ \fbox{ - \begin{mathpar} - \\ - \infer - {\ } - {\emptyctx \~} - \textsc{ (Wf-E)} - \and %-------------------- - \infer - {\Ga \~ T:s \\ s \in \S \\ x \notin \dv{\Ga}} - {\Ga , x:T \~} - \textsc{ (Wf-S)} - \\ - \end{mathpar} - } - \caption{Typer's Well-Formed Context Rules} -\end{figure} - \subsection{Universes and Universe Polymorphism} -Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \s\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ -%% FIXME: We'll need somewhere to clarify that those `l`s have to be present -%% in the Γ environment with type TypeLevel. -All type levels $\l$ inhabit the type \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. Sometimes we write $\s^i$ to abbreviate the application of the successor $i$ times. We define a set $\mathbb{L}$ which is closed under those two constructs. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. - -We have that \Sortw\ is the unique sort of all the types of universe polymorphic functions. We can now describe the explicit subset of Typer as a Pure Type System \cite{barendregt}: - -\begin{figure}[h] +\begin{figure} + \label{fig:PTS} \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \\ \S = \{ & \SortL;\ \Sortw;\ \Type\ \l\} &\forall\l \in \mathbb{L} \\[9pt] @@ -73,8 +48,7 @@ We have that \Sortw\ is the unique sort of all the types of universe polymorphic \caption{Typer's Pure Type System} \end{figure} -Because of the impredicativity of the erasable part of Typer, we need to define a separate set of rules, written $\R_e$, some of which will be referred as $(s_1,s_2)$ as an abbreviation for $(s_1,s_2,s_2)$. -\begin{figure}[h] +\begin{figure} \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \\ \R_e = \{ &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \\ @@ -85,10 +59,18 @@ Because of the impredicativity of the erasable part of Typer, we need to define \caption{Typer's Impredicative Rules} \end{figure} -\subsection{ICC in Typer} -Typer manipulates three separate kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, participate in type checking and are then erased before execution. +Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \s\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ +%% FIXME: We'll need somewhere to clarify that those `l`s have to be present +%% in the Γ environment with type TypeLevel. +The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ which is closed under those two constructs. We write $\s^i$ to abbreviate the application of the successor $i$ times. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. All type levels $\l$ inhabit the type \TypeLevel\ which belongs to the sort \SortL. + +\Sortw\ is the unique sort of all the universe polymorphic function types. We describe the explicit part of Typer as a Pure Type System \cite{barendregt} in figure \ref{fig:PTS}. % FIXME: PDF prints 1.1 instead of 1 +Because of the erasable part of Typer allows for impredicative definitions, we define a separate set of rules $\R_e$. + +\subsection{Erasure in Typer} +Typer manipulates three separate kinds of terms to simplify the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and executed. \emph{Implicit} terms are also used during execution, but Typer can infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, provide type information during checking and are erased before execution. -\textbf{Notation:} The notation we adopt in this document is meant to both allow for the distinction between the three kinds of terms and to evoke actual Typer source code. The traditional explicit lambda term $\la(x\:A).b$ will here be written $\la(x\:A)\explicit b$ and similarly the product type $\Pi(x\:A).B$ will be written $(x\:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms: +\textbf{Notation:} The notation we adopt in this document is meant to allow for the distinction between the three kinds of terms and also to evoke actual Typer code. The traditional explicit lambda term $\la(x\:A).b$ will here be written $\la(x\:A)\explicit b$ and similarly the product type $\Pi(x\:A).B$ will be written $(x\:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms: \begin{center} \begin{tabular}[h]{rclll} @@ -99,7 +81,10 @@ Typer manipulates three separate kinds of terms to simplify both the writing and \end{tabular} \end{center} -After elaboration, implicit terms behave exactly like explicit terms so we will not explicitly include them in our calculus; they will be assumed to be a subset of the explicit terms. We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. +After elaboration, implicit terms behave exactly like explicit terms so we will not explicitly include them in our calculus; they will be assumed to be a subset of the explicit terms. + +\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga \~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon (;) and enriched with an additional declarations with a comma (,). We write the empty context as a dot ($\cdot$). The set of declared variables in a context $\Ga$ is written $\dv{\Ga}$ and the set of free (i.e. unbound) variables in a term $T$ is written $\fv{T}$. The expression $M\{N/x\}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$. + \begin{figure}[h] \centering \fbox{\begin{minipage}{0.9\linewidth} @@ -114,13 +99,23 @@ After elaboration, implicit terms behave exactly like explicit terms so we will \caption{Extraction function $M \mapsto M^*$} \label{fig:*} \end{figure} -The typing rules for explicit and erasable terms are shown in figure \ref{fig:X-E-rules}. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms. +We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules for Typer are shown in figure \ref{fig:Typing-rules}. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms. \begin{figure}[h] \ \\ \ \\ \fbox{ \begin{mathpar} \\ \infer + {\ } + {\emptyctx \~} + \textsc{ (Wf-E)} + \and %-------------------- + \infer + {\Ga \~ T:s \\ s \in \S \\ x \notin \dv{\Ga}} + {\Ga , x:T \~} + \textsc{ (Wf-S)} + \and %-------------------- + \infer {\Ga \~ \\ (s_1:s_2) \in \A} {\Ga \~ s_1:s_2} \textsc{ (Sort)} @@ -163,22 +158,19 @@ The typing rules for explicit and erasable terms are shown in figure \ref{fig:X- \\ \end{mathpar} } - \caption{Typer's Typing Judgment Rules} - \label{fig:X-E-rules} + \caption{Typer's Typing Rules} + \label{fig:Typing-rules} \end{figure} - There are two notable differences between explicit and erasable typing rules: \begin{enumerate} \item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$ -\item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with incoherent terms. +\item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with free terms after erasure. \end{enumerate} - - \subsection{Inductive Definitions} -\textbf{Notation:} We use a vector notation to refer to a series of finitely many term, i.e. $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the term vector $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to an $i$ member of the set $\{1,2,3,...,n\}$ for $n = |\vec{N}|$. - +\textbf{Notation:} We abbreviate a list of terms $N_i$ as $\vec{N}$. For example, $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the list of terms $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to a member $i$ of the set $\{1,2,3,...,n\}$ for $n = |\vec{N}|$. +\\ \begin{definition} We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} @@ -189,16 +181,16 @@ There are two notable differences between explicit and erasable typing rules: Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} -We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are: +We extend our abstract syntax with four terms from Gim\'enez's inductive definitions \cite{gimenez}: \begin{itemize} \renewcommand{\labelitemi}{$-$} \setlength\itemsep{-3pt} -\item $\Ind(X:A) \<\vec{C}\>$ which is an inductively defined type recursively bound to $X$. $\vec{C}$ is the list of constructor signatures which must be a \emph{form of constructor} w.r.t. $X$. +\item $\Ind(X:A) \<\vec{C}\>$ is an inductively defined type recursively bound to $X$. $\vec{C}$ is the list of constructor signatures which must be a \emph{form of constructor} w.r.t. $X$. \item $\Constr(i:I)$ stands for the $i$th constructor of an inductive type $I$. -\item $\Case\ M\: S \text{ of } \<\vec{G}\>$ which is the function by case analysis on the expression $M$ of type $S$ and where $\<\vec{G}\>$ is the list of cases, represented as abstractions of the respective patterns of constructions. +\item $\Case\ M\: S \text{ of } \<\vec{G}\>$ is the function by case analysis on the expression $M$ of type $S$ and where $\<\vec{G}\>$ is the list of cases, represented as abstractions of the respective patterns of constructions. \end{itemize} -The typing rules for inductive definitions and case analysis are presented in figure \ref{IND-rules}. +The typing rules for inductive definitions and case analysis are presented in figure \ref{fig:IND-rules}. \begin{figure}[h] \ \\ \ \\ \fbox{ @@ -329,7 +321,7 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \end{figure} \section{Typer as an Extension of a Calculus of Constructions} -In this section we will prove that the erasable terms of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an impredicative $\mathsf{Prop}$ and an infinite hierarchy of predicative universes (\CC). +In this section we will show that the erasable terms of Typer allows for a representation of all typing derivations from a Calculus of Constructions with an impredicative $\mathsf{Prop}$ and an infinite hierarchy of predicative universes (\CC). This will be demonstrated through a translation and its proof of correctness. \subsection{Definition of \CC} @@ -394,9 +386,9 @@ In this section we will prove that the erasable terms of Typer allow for a repre \label{fig:CC-rules} \end{figure} -Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, with an infinite hierarchy of universes above an impredicative \Prop. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$ +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, to which we add an infinite hierarchy of predicative universes above an impredicative \Prop. Thus we have: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$ -\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,j)})$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than other definitions of \CC\ (see for example \cite{miquel}). +\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,j)})$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}). \subsection{Translation} \begin{figure}[h] @@ -442,7 +434,7 @@ The translator operator \rew{\_} is defined on contexts and terms of \CC. We exp \end{align*} \end{theorem} -Before proving the correctness of the equality, we will need the following lemmas: +Before proving the correctness of the equality, we need the following lemmas: \begin{lemma} \label{lem:S-equiv} $s \in \S_{CC} \iff \rew{s} \in \S$ View it on GitLab: https://gitlab.com/monnier/typer/commit/57ed864b2272654ddc7041f5e882ccf4b80… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/57ed864b2272654ddc7041f5e882ccf4b80… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] New character '@' introducing docstring
by Jonathan Graveline 22 Aug '18

22 Aug '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 3981eea1 by Jonathan Graveline at 2018-08-22T23:29:34Z New character '@' introducing docstring New primitive `Elab.debug-doc` mostly for testing docstring Replaced `load_` by `load` - - - - - 8 changed files: - btl/builtins.typer - btl/pervasive.typer - btl/tuple.typer - src/elab.ml - src/eval.ml - src/lexer.ml - src/prelexer.ml - src/util.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -276,6 +276,8 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; +Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; + %%%% Unit test helper IO %% Print message and/or fail (terminate) ===================================== btl/pervasive.typer ===================================== @@ -545,14 +545,14 @@ define-operator "<-" 80 96; %%%% %% `List` is the type and `list` is the module (tuple) -list = load_ "btl/list.typer"; +list = load "btl/list.typer"; %% macro `do` for easier series of IO operation -do = let lib = load_ "btl/do.typer" in lib.do; +do = let lib = load "btl/do.typer" in lib.do; %% various macro for tuple %% used by `case_` -tuple-lib = load_ "btl/tuple.typer"; +tuple-lib = load "btl/tuple.typer"; %% get nth element tuple-nth = tuple-lib.tuple-nth; @@ -566,7 +566,7 @@ _\,_ = tuple-lib.make-tuple; Tuple = tuple-lib.tuple-type; %% macro `case` for a little more complex pattern matching -case_ = let lib = load_ "btl/case.typer" in lib.case-macro; +case_ = let lib = load "btl/case.typer" in lib.case-macro; %%%% plain-let %%%% Not recursive and not sequential @@ -574,10 +574,10 @@ case_ = let lib = load_ "btl/case.typer" in lib.case-macro; define-operator "plain-let" () 3; %% define-operator "in" 3 67; -plain-let_in_ = let lib = load_ "btl/plain-let.typer" in lib.plain-let-macro; +plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %%%% `case` at function level -_|_ = let lib = load_ "btl/polyfun.typer" in lib._|_; +_|_ = let lib = load "btl/polyfun.typer" in lib._|_; %%%% Unit tests function for doing file @@ -604,8 +604,8 @@ Test_file = macro (lambda args -> let in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) (lambda _ _ -> ret) (lambda _ -> ret) - %% `load_` is a special form and takes a Sexp rather than a real `String` - (lambda s -> quote (let lib = load_ (uquote (Sexp_string s)); in lib.exec-test)) + %% `load` is a special form and takes a Sexp rather than a real `String` + (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) (lambda _ -> ret) (lambda _ -> ret) (lambda _ -> ret)) ===================================== btl/tuple.typer ===================================== @@ -174,6 +174,8 @@ make-tuple = macro (lambda args -> do { IO_return r; }); +%% + tuple-type = macro (lambda args -> let mf : Sexp -> Sexp -> Sexp; ===================================== src/elab.ml ===================================== @@ -1069,8 +1069,14 @@ and lexp_decls_1 [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, ctx_define nctx var lexp ltp - | [Symbol ((l, vname) as v); sexp] + | [Symbol (l, vname); sexp] -> if SMap.mem vname pending_decls then + let decl_loc = SMap.find vname pending_decls in + let v = ({file = l.file; + line = l.line; + column = l.column; + docstr = String.concat "\n" [decl_loc.docstr; l.docstr]}, + vname) in let pending_decls = SMap.remove vname pending_decls in let pending_defs = ((v, sexp) :: pending_defs) in if SMap.is_empty pending_decls then @@ -1621,7 +1627,7 @@ let register_special_forms () = ("case_", sform_case); ("let_in_", sform_letin); ("Type_", sform_type); - ("load_", sform_load); + ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ("new-attribute", sform_new_attribute); ===================================== src/eval.ml ===================================== @@ -746,6 +746,16 @@ let getenv loc depth args_val = match args_val with | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context) | _ -> error loc "getenv takes a single Unit as argument" +let debug_doc loc depth args_val = match args_val with + | [Vstring name; Velabctx ectx] + -> (try let idx = senv_lookup name ectx in + let elem = lctx_lookup (ectx_to_lctx ectx) + (((dummy_location, Some name), idx)) in + match elem with + | ((l,_),_,_) -> Vstring (l.docstr) + with _ -> Vstring "element not found") + | _ -> error loc "Elab.debug_doc takes a String and an Elab_Context as arguments" + let is_bound loc depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (try (ignore (senv_lookup name ectx); true) @@ -994,6 +1004,7 @@ let register_builtin_functions () = ("Ref.write" , ref_write, 2); ("gensym" , gensym, 1); ("Elab.getenv" , getenv, 1); + ("Elab.debug-doc", debug_doc, 2); ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); ("Elab.is-nth-erasable", is_nth_erasable, 3); ===================================== src/lexer.ml ===================================== @@ -48,7 +48,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos | [] -> (internal_error "No next token!") | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) - | (Pretoken ({file;line;column}, name) :: pts') + | (Pretoken ({file;line;column;docstr}, name) :: pts') -> let char = name.[bpos] in if digit_p char || (char = '-' (* FIXME: Handle '+' as well! *) @@ -57,10 +57,10 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos let rec lexnum bp cp (np : num_part) = if bp >= String.length name then ((if np == NPint then - Integer ({file;line;column=column+cpos}, + Integer ({file;line;column=column+cpos;docstr=docstr}, int_of_string (string_sub name bpos bp)) else - Float ({file;line;column=column+cpos}, + Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))), pts', 0, 0) else @@ -74,28 +74,28 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos -> lexnum (bp+1) (cp+1) NPexp | _ -> ((if np == NPint then - Integer ({file;line;column=column+cpos}, + Integer ({file;line;column=column+cpos;docstr=docstr}, int_of_string (string_sub name bpos bp)) else - Float ({file;line;column=column+cpos}, + Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))), pts, bp, cp) in lexnum (bpos+1) (cpos+1) NPint else if bpos + 1 >= String.length name then - (hSymbol ({file;line;column=column+cpos}, + (hSymbol ({file;line;column=column+cpos;docstr=docstr}, string_sub name bpos (String.length name)), pts', 0, 0) else if stt.(Char.code name.[bpos]) = CKseparate then - (hSymbol ({file;line;column=column+cpos}, + (hSymbol ({file;line;column=column+cpos;docstr=docstr}, string_sub name bpos (bpos + 1)), pts, bpos+1, cpos+1) else let rec lexsym bpos cpos = let mksym epos escaped - = if epos = bpos then epsilon {file;line;column=column+cpos} else + = if epos = bpos then epsilon {file;line;column=column+cpos;docstr=docstr} else let rawstr = string_sub name bpos epos in let str = if escaped then unescape rawstr else rawstr in - hSymbol ({file;line;column=column+cpos}, str) in + hSymbol ({file;line;column=column+cpos;docstr=docstr}, str) in let rec lexsym' prec lf bp cp escaped = if bp >= String.length name then (lf (mksym (String.length name) escaped), pts', 0, 0) @@ -122,7 +122,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos && CKseparate != (stt.(Char.code name.[bp']))) || not (lf dummy_epsilon = dummy_epsilon) -> let left = mksym bp escaped in - let op = hSymbol ({file;line;column=column+cp}, + let op = hSymbol ({file;line;column=column+cp;docstr=docstr}, "__" ^ String.sub name bp 1 ^ "__") in let bpos = bp' in let cpos = inc_cp cp char in ===================================== src/prelexer.ml ===================================== @@ -50,90 +50,92 @@ let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp -let rec prelex (file : string) (getline : unit -> string) ln ctx acc +let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : string) : pretoken list = try (* let fin = open_in file in *) let line = getline () in let limit = String.length line in let nextline = prelex file getline (ln + 1) in - let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc = + let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc doc = let nexttok = prelex' ctx in - if bpos >= limit then nextline ctx acc else + if bpos >= limit then nextline ctx acc doc else match line.[bpos] with - | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc - | '%' -> nextline ctx acc (* A comment. *) + | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc doc + | '%' -> nextline ctx acc doc (* A comment. *) + (* line's bounds seems ok: String.sub line 1 0 == "" *) + | '@' -> nextline ctx acc (String.concat "\n" [doc; (String.sub line 1 (limit - 1))]) | '"' (* A string. *) -> let rec prestring bp cp chars = if bp >= limit then - (prelexer_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} "Unterminated string"; nextline ctx - (Prestring ({file=file; line=ln; column=cpos}, "") - :: acc)) + (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") + :: acc) "") else match line.[bp] with | '"' -> nexttok (bp+1) (cp+1) - (Prestring ({file=file; line=ln; column=cpos}, + (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, string_implode (List.rev chars)) - :: acc) + :: acc) "" | '\\' -> (if bpos + 1 >= limit then - (prelexer_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} "Unterminated string"; nextline ctx - (Prestring ({file=file; line=ln; column=cpos}, + (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") - :: acc)) + :: acc) "") else match line.[bp + 1] with | 't' -> prestring (bp+2) (cp+2) ('\t' :: chars) | 'n' -> prestring (bp+2) (cp+2) ('\n' :: chars) | 'r' -> prestring (bp+2) (cp+2) ('\r' :: chars) | ('u' | 'U') -> - prelexer_error {file=file; line=ln; column=cp} + prelexer_error {file=file; line=ln; column=cp; docstr=doc} "Unimplemented unicode escape"; prestring (bp+2) (cp+2) chars | char -> prestring (bp+2) (cp+2) (char :: chars)) | char -> prestring (bp+1) (inc_cp cp char) (char :: chars) in prestring (bpos+1) (cpos+1) [] - | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] + | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] doc | '}' -> (match ctx with | ((sln, scpos, sbpos, sacc) :: ctx) -> prelex' ctx (bpos+1) (cpos+1) - (Preblock ({file=file; line=sln; column=scpos}, + (Preblock ({file=file; line=sln; column=scpos; docstr=doc}, List.rev acc, - {file=file; line=ln; column=(cpos + 1)}) - :: sacc) - | _ -> (prelexer_error {file=file; line=ln; column=cpos} + {file=file; line=ln; column=(cpos + 1); docstr=doc}) + :: sacc) "" + | _ -> (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} "Unmatched closing brace"; - prelex' ctx (bpos+1) (cpos+1) acc)) + prelex' ctx (bpos+1) (cpos+1) acc doc)) | char (* A pretoken. *) -> let rec pretok bp cp = if bp >= limit then - nextline ctx (Pretoken ({file=file; line=ln; column=cpos}, + nextline ctx (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, string_sub line bpos bp) - :: acc) + :: acc) "" else match line.[bp] with | (' '|'\t'|'\n'|'\r'|'%'|'"'|'{'|'}' ) -> nexttok bp cp - (Pretoken ({file=file; line=ln; column=cpos}, + (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, string_sub line bpos bp) - :: acc) + :: acc) "" | '\\' when bp+1 < limit -> let char = line.[bp + 1] in pretok (bp + 2) (1 + inc_cp cp char) | char -> pretok (bp+1) (inc_cp cp char) in pretok (bpos+1) (inc_cp cpos char) - in prelex' ctx 0 1 acc (* Traditionally, column numbers start at 1 :-( *) + in prelex' ctx 0 1 acc doc (* Traditionally, column numbers start at 1 :-( *) with End_of_file -> match ctx with | [] -> List.rev acc | ((ln, cpos, _, _) :: ctx) -> - (prelexer_error {file=file; line=ln; column=cpos} + (prelexer_error {file=file; line=ln; column=cpos; docstr=""} "Unmatched opening brace"; List.rev acc) @@ -141,7 +143,7 @@ let prelex_file file = let fin = open_in file in prelex file (fun _ -> input_line fin) (* Traditionally, line numbers start at 1 :-( *) - 1 [] [] + 1 [] [] "" let prelex_string str = let pos = ref 0 in @@ -155,7 +157,7 @@ let prelex_string str = let line = string_sub str start npos in (* print_string ("Read line: " ^ line); *) line - in prelex "<string>" getline 1 [] [] + in prelex "<string>" getline 1 [] [] "" let pretoken_name pretok = match pretok with ===================================== src/util.ml ===================================== @@ -25,8 +25,8 @@ module IMap = Map.Make (struct type t = int let compare = compare end) type charpos = int type bytepos = int -type location = { file : string; line : int; column : charpos } -let dummy_location = {file=""; line=0; column=0} +type location = { file : string; line : int; column : charpos; docstr : string; } +let dummy_location = {file=""; line=0; column=0; docstr=""} (*************** DeBruijn indices for variables *********************) View it on GitLab: https://gitlab.com/monnier/typer/commit/3981eea1c7632db58f0d21ddd7a63734169… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/3981eea1c7632db58f0d21ddd7a63734169… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][bosn] Finish fix lem:FV-E-Lam
by Nathaniel 22 Aug '18

22 Aug '18

Nathaniel pushed to branch bosn at Stefan / Typer Commits: c52700fd by nbos at 2018-08-22T21:29:36Z Finish fix lem:FV-E-Lam - - - - - 1 changed file: - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/typer_theory.tex ===================================== @@ -433,7 +433,7 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \ \label{fig:[]} \end{figure} -The translator operator \rew{\ } is defined on contexts and terms of \CC. We expose the translation on figure \ref{fig:[]}. We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC: +The translator operator \rew{\_} is defined on contexts and terms of \CC. We expose the translation on figure \ref{fig:[]}. We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC: \begin{theorem} \label{thm:correctness-translation} \begin{align*} @@ -699,48 +699,57 @@ The impredicative product type translates to an erasable product type $(x:\rew{T \label{lem:E-Lam-FV} If we have \begin{mathpar} - %% TODO: Check if the condition `T:Type (s ℓ)` is really necessary - %% (If not, also fix on last case of completeness proof) - {\Ga, x:T \~ M:U \\ \Ga, x:T \~ U : \Type\ \z \\ \Ga \~ T : \Type\ (\s\ \l)} + %% FIXME: I am limiting the proof to translated terms because + %% 1) We don't need more than this + %% 2) The lemma doesn't seem to hold otherwise; e.g. + %% M := P|Q + %% M := λ(y:T)->V | x + %% + %% where V : U : Type0 so that (λ(y:T)->V | x) : U : Type0 + %% + %% Now, I don't know where y would appear in V while respecting V : U + %% and y : T, but we still have x ∈ FV(λ(y:T)->V | x) which is enough + %% as far as I know to disprove the lemma. This is not a counterexample + %% if we limit the lemma to translated terms [M] because the rule + %% (Type₁,Type₀,Type₁) ∉ Rcc, but instead (Type₁,Type₀,Type₀) ∈ R which + %% makes the abstraction erasable in Typer and thus, x is not free + {\rew{\Ga, x:T} \~ \rew{M}:\rew{U} \\ \rew{\Ga, x:T} \~ \rew{U} : \Type\ \z \\ \rew{\Ga} \~ \rew{T} : \Type\ (\s\ \l)} \end{mathpar} then the following always holds - $$x \notin \fv{M^*}$$ + $$x \notin \fv{\rew{M}^*}$$ \begin{proof}\ \\ - By structural induction on extracted terms (figure \ref{fig:*}), either $M^*$ cannot be equal to it, or $x$ cannot be free within it, thus showing that $x \notin \fv{M^*}$. + By structural induction on $\rew{M}^*$: - \textbf{Case} $M^* = y^*$:\\ - The extraction is $y^* = y$. It cannot be that $y = x$ because $x : T : \Type (\s\ \l)$ and $y : U : \Type\ \z$ and equality is not defined between inhabitants of different types nor different universe. Therefore, $x \notin \fv{y}$ because $x \neq y$. + \textbf{Case} $\rew{M}^* = y^*$:\\ + The extraction is $y^* = y$. It cannot be that $y = x$ because $x : \rew{T} : \Type (\s\ \l)$ and $y : \rew{U} : \Type\ \z$ and equality is not defined between inhabitants of different types nor of different universes. Therefore, $x \notin \fv{y}$ because $x \neq y$. - \textbf{Case} $M^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\\ - $M$ cannot be a product type since its type $U$ inhabits the smallest universe $\Type\ \z$ . + \textbf{Case} $\rew{M}^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\\ + $\rew{M}$ cannot be a product type since its type $\rew{U}$ inhabits the smallest universe $\Type\ \z$ . - %% FIXME: This shows a problem in our presentation. We use FV(M*) and we + %% FIX\rew{M}E: This shows a problem in our presentation. We use FV(\rew{M}*) and we %% define * but we don't define FV. Another option is to forget about * - %% and only define FV*(M), the set of non-erasable free variables. - \textbf{Case} $M^* = (s)^*$ with $s \in \S$:\\ - The extraction is $s^* = s$. All $s \in S$ are closed constants and thus $x \notin \fv{s}$. + %% and only define FV*(\rew{M}), the set of non-erasable free variables. + \textbf{Case} $\rew{M}^* = \rew{s}^*$ with $\rew{s} \in \S$:\\ + The extraction is $\rew{s}^* = \rew{s}$. All $\rew{s} \in S$ are closed constants and thus $x \notin \fv{\rew{s}}$. - \textbf{Case} $M^* = (\la(y:t)\explicit V)^*$:\\ - The extraction makes this $\la(y)\explicit V^*$. By the rules in $\R$, if $M$ has sort $\Type\ \z$, then it is an upper bound for the sort of $V$. Thus, $V : U' : \Type\ \z$ and we have $x \notin \fv{V^*}$ by the induction hypothesis. - - \textbf{Case} $M^* = (\la(y:t)\erasable V)^*$:\\ - The extraction makes this $V^*$. By the rules in $\R_e$, if $M$ has sort $\Type\ \z$, then $V$ also has sort $\Type\ \z$. Thus, by the induction hypothesis, $x \notin \fv{V^*}$. - - %% FIXME: - \textbf{Case} $M^* = (P \ap Q)^*$:\\ - The extraction is $(P \ap Q)^* = P^* \ap Q^*$. - %% FIXME: $P$ can be something else than an abstraction (e.g. it can be - %% a simple variable). What we can know is that P : T : Prop, because we - %% know that it returns something in Prop, so we can - %% apply the induction hypothesis to it. - $P$ can only expand to an abstraction such that $P^* \ap Q^* = (\la (x:t) \explicit V)^* | Q^*$. We have shown that $x$ is not free in the explicit abstraction. - %% FIXME: We can only use the induction hypothesis if Q : T : Prop! - By the induction hypothesis, $x$ is not free in $Q^*$. - - %% FIXME: Again, $P$ can be something else than an abstraction. - \textbf{Case} $M^* = (P \appp Q)^*$:\\ - The extraction is $(P \appp Q)^* = P^*$. $P$ can only expand to an abstraction $(\la (\iota:t) \erasable V)^*$ and we have shown that $x$ is not free in the erasable abstraction. + \textbf{Case} $\rew{M}^* = (\la(y:t)\explicit V)^*$:\\ + The extraction makes this $\la(y)\explicit V^*$. By the rules in $\R$, if $\rew{M}$ has sort $\Type\ \z$, then it is an upper bound for the sort of $V$. Thus, $V : U' : \Type\ \z$ and we have $x \notin \fv{V^*}$ by the induction hypothesis. + + \textbf{Case} $\rew{M}^* = (\la(y:t)\erasable V)^*$:\\ + The extraction makes this $V^*$. By the rules in $\R_e$, if $\rew{M}$ has sort $\Type\ \z$, then $V$ also has sort $\Type\ \z$. Thus, by the induction hypothesis, $x \notin \fv{V^*}$. + + \textbf{Case} $\rew{M}^* = (P \ap Q)^*$:\\ + The extraction is $(P \ap Q)^* = P^* \ap Q^*$. By the typing rule \textsc{X-App}, because $P \ap Q : \rew{U}$, then $$P : (y:t)\explicit \rew{U}\{Q/y\}$$ + %% FIXME: I'm not sure about this "reverse substitution" business + %% happening above. + %% FIXME: Also, are contexts necessary here? + for $t$ such that $Q:t$. Further, since $\rew{U} : \Type\ \z$ and because the only rules that match $(s_1,\Prop,s_3) \in R_{CC}$ have $s_3 = \Prop$ then by induction hypothesis on the completeness of the translation, we can infer $$(y:t)\explicit \rew{U}\{Q/y\} : \Type\ \z$$ +and thus assume $x \notin \fv{P^*}$ by induction hypothesis on this lemma---although only the cases of the variable, the lambda abstraction and the applications apply. Because the product type of $P$ is explicit, the sort of $Q$ is also upper bounded by $\Type\ \z$ because explicit product types occur by the application of \textsc{X-Prod} with a rule that has $s_3 = \max (s_1,s_2)$. Thus we have $x \notin \fv{Q^*}$ by the induction hypothesis. + + + \textbf{Case} $\rew{M}^* = (P \appp Q)^*$:\\ + The extraction is $(P \appp Q)^* = P^*$. Similar to the previous case, because $P$ has the same sort as $\rew{M}$, we have $x \notin \fv{P^*}$ by induction hypothesis. \end{proof} \end{lemma} View it on GitLab: https://gitlab.com/monnier/typer/commit/c52700fd91d2133021fd0e04a737fc5429b… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/c52700fd91d2133021fd0e04a737fc5429b… You're receiving this email because of your account on gitlab.com.

1 0