marcoonroad

{-# LANGUAGE GADTs #-}

module Dependent (
    Nat,     O,       S,
    Z,       Zero,    SuccPos, SuccNeg,
    Prop,    V,       X,
    List,    Nil,     Cons,
    Vector,  Exist,   Times,
    Option,  Some,    None,
    Coprod,  OnLeft,  OnRight,

marcoonroad

Require Import Utf8.

Section Existence.

  (* a simple list that says if a given element is inhabitant *)

  Inductive exst { T } (x : T) : bool -> Type :=
  | Here    :      exst x false -> exst x true
  | There   : T -> exst x true  -> exst x true
  | NoSuch  : T -> exst x false -> exst x false

marcoonroad

-- begin of test --

local option = require 'option'

local hash = { a = 15, b = 2, c = 7 }
local list = { 4, 8, 2, 3 }

local function test (label)
	local first  = option.bind (hash[ label ])
	local second = option.bind (list[ first ])

marcoonroad

(*
	Exercise: 2 stars (andb_eq_orb)
	Prove the following theorem. (You may want to first prove a
 subsidiary lemma or two. Alternatively, remember that you do not have
 to introduce all hypotheses at the same time.)

 Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> b = c.

*)

marcoonroad

#ifndef MACROSH
#define MACROSH

#define super(self)           (& self -> __parent)
#define context(self)         (self -> __hidden)
#define send(self, slot, ...) (self -> slot (self, ## __VA_ARGS__))
#define bless(type)           malloc (sizeof (struct __##type##__))
#define method(type, name)    __##name##__##type##__
#define as                    /* */
#define extends(type)         struct __##type##__ __parent

marcoonroad

-- an exampleof "dynamic inheritance" --
-- changing lookup prototypes (parent objects) --

local Object = { }

-- primitive methods --

function Object : bless (struct) return setmetatable (struct, { __index = self }) end

function Object : clone ( )

marcoonroad

#ifndef FAILUREH
#	define FAILUREH

#include <setjmp.h>

static jmp_buf hook;

void raise (char * reason) {
	longjmp (hook, (int) reason); // cast the address into a int number
}

marcoonroad

-- readonly test --

local function readonly (hash)
  return setmetatable ({ }, {
    __index = hash,
    __newindex = function (self, key, value)
      if rawget (getmetatable (self).__index, key) then
        key = tostring (key)
        value = tostring (value)
        return error ("Attempt to rewrite the field <" .. key .. "> with <" .. value .. "> on given hashtable...")

marcoonroad

[Dica] Lista de links com documentação das seguintes linguagens:

• PHP - http://php.net/docs.php
• JavaScript - https://developer.mozilla.org/en-US/docs/Web/JavaScript
• Python - https://www.python.org/doc/versions/ ( escolha a versão ).
• Java - http://docs.oracle.com/javase/7/docs/api/
• Ruby - http://ruby-doc.org/
• Perl - http://www.perl.org/docs.html
• C/C++ - http://en.cppreference.com/w/
• Haskell - http://www.haskell.org/haddock/doc/html/index.html

marcoonroad

#!/usr/bin/perl6

use v6;

# reactive programming per se is turing complete?


#         --------------[ y, x + y ]--------------
#         |                                      |
#         |         ------                       |