gdeest

import stdlib.themes.bootstrap
import stdlib.widgets.bootstrap
import stdlib.widgets.completion
import stdlib.web.client

WB = WBootstrap

function array_completion(options, on_select) {
    config = { 
	WCompletion.default_config with 

gdeest

import stdlib.apis.twitter

twitter_config = Twitter({ consumer_key: "XXX",
			   consumer_secret: "XXX" });

function user_tweets(user) {
    twitter_config.get_user_timeline(
	user, 
	twitter_config.default_timeline, {none})
}

gdeest

varTerm = do
  char <- noneOf ['.', '\\', '(', ')']
  return $ Var char

appTerm = do
  app <- char '(' *> lambdaTerm <* char ')'
  arg <- lambdaTerm
  return $ App app arg

absTerm = do

gdeest

grammar fr.irisa.cairn.interproc.simple.Simple	with org.eclipse.xtext.common.Terminals

import "http://www.eclipse.org/emf/2002/Ecore" as ecore
//import "http://gecosinterproc" as interproc
import "platform:/plugin/fr.irisa.cairn.interproc.simple/src/fr/irisa/cairn/interproc/gecos/extensions/gecosexts.ecore" as interproc
import "platform:/plugin/fr.irisa.cairn.gecos.model/model/gecos.cdfg.ecore#//core" as core
import "platform:/plugin/fr.irisa.cairn.gecos.model/model/gecos.cdfg.ecore#//instrs" as instrs
import "platform:/plugin/fr.irisa.cairn.gecos.model/model/gecos.cdfg.ecore#//types" as types
import "platform:/plugin/fr.irisa.cairn.gecos.model/model/gecos.cdfg.ecore#//blocks" as blocks
import "platform:/plugin/fr.irisa.cairn.gecos.model/model/gecos.cdfg.ecore#//annotations" as annot

gdeest

{-# LANGUAGE OverloadedStrings #-}

import Data.ByteString.Char8 hiding (putStrLn)
import Network.SimpleIRC
import System.IO.Error

joinEvent :: EventFunc
joinEvent m msg = case mNick msg of
                    Just "gawelBot" -> sendCmd m $ MQuit "Bye !"
                    _ -> return ()

gdeest

require 'icalendar'
require 'camping'
require 'net/http'
require 'uri'


Camping.goes :IcalFilter

module IcalFilter::Controllers
  class Index < R '/'

gdeest

(* Construit un enregistrement à partir d'une liste de paires clé/valeur. *)
(* En cas de doublons, la première valeur associée au champ prime. *)

Fixpoint build_rec (l: list (rec_field*option val)): option (rec_field -> option val) := 
  match l with
    | nil => Some (fun _ => None)
    | (f,v)::l => match (v, build_rec l) with
                    | (Some v', Some r) => Some (update_rec r f v')
                    | _ => None
                  end

gdeest

    (* case_eq v0. case_eq v1. *)
    (* intros. *)
    (* rewrite H2 in H1. rewrite H3 in H0. *)
    (* rewrite H0 in H. rewrite H1 in H. discriminate. *)
    (* intros. rewrite H2 in H1. rewrite H3 in H0. *)
    (* rewrite H0 in H. rewrite H1 in H. *)
    (* injection H. intro. rewrite <- H4. *)
    (* eapply IHe1 *)
Admitted

gdeest

Lemma star_red_lookup: forall s f e e', star_red_exp s e e' ->
                                        star_red_exp s (Elookup e f) (Elookup e' f).
Proof.
  intros.
  induction H.
  - apply star_refl.
  - eapply star_step.
    apply red_lookup_simpl.
    apply H. apply IHstar.
Qed.

gdeest

Theorem nat_to_red: forall s e v, nat_expr s e (Econst v) -> star_red_exp s e (Econst v).
Proof.
  intros s e.
  induction e; intros v' H; inversion H; subst.
  - constructor.
  - eapply star_step. constructor. apply star_refl.
  - eapply star_step. constructor. apply H3. apply star_refl.
  - apply IHe1 in H4. apply IHe2 in H5.
    inversion H4; subst.
    + (* e1 = (Econst (Vint i1)) *)