Commits

Thomas Williams committed 6588d22 Merge with conflicts

Merge remote-tracking branch 'origin/inderl_change'

Conflicts:
src/coq_backend.ml

Comments (0)

Files changed (25)

   | x l						:: :: X_l
   | ( ix ) l					:: :: PreX_l
     {{ com Remove infix status }}
+  | name_t -> x_l					:: M :: extract
+    {{ com Extract x from a name\_t }}
+    {{ lem (match [[name_t]] with | Name (x,l) -> (x,l) | Nt _ (x,l) _ _ -> (x,l) }}
+    {{ hol TODO }}
+    {{ ocaml (assert false) }}
 
 ix_l {{ tex \ottnt{ix}^{l} }} :: '' ::=
   {{ com Location-annotated infix names }}
   {{ com Location-annotated function clauses }}
   | funcl_aux l						:: :: Rec_l
 
-x_l_opt {{ tex \ottnt{id}^? }} :: 'X_l_' ::=
-  {{ com Optional name for inductively defined relation clauses }}
-  |              :: :: none
-  | x_l :        :: :: some
+name_t :: 'name_t_' ::=
+  {{ com Name or name with type for inductively defined relation clauses }}
+  | x_l	      	 :: :: name
+  | ( x_l : typ ) :: :: nt
+
+name_ts :: '' ::=
+  {{ com Names with optional types for inductively defined relation clauses }}
+  | name_t0 .. name_tn :: :: NameTs
 
 rule_aux :: '' ::=
   {{ com Inductively defined relation clauses }}
-  | x_l_opt forall x_l1 .. x_ln . exp ==> x_l exp1 .. expi	:: :: Rule
+  | x_l : forall name_t1 .. name_ti . exp ==> x_l1 exp1 .. expn	:: :: Rule
 
 rule :: '' ::=
   {{ com Location-annotated inductively defined relation clauses }}
   | rule_aux l						:: :: Rule_l
 
+witness_opt {{ tex \ottnt{witness}^? }} :: 'witness_' ::=
+  {{ com Optional witness type name declaration. Must be present for a witness type to be generated. }}  
+  |  	 	  :: :: none
+  | witness type x_l ; :: :: some
+
+check_opt {{ tex \ottnt{check}^? }} :: 'check_' ::=
+  {{ com Option check name declaration }}
+  |  	 	      :: :: none
+  | check x_l ;	      :: :: some
+
+functions_opt {{ tex \ottnt{functions}^? }} :: 'functions_' ::=
+  {{ com Optional names and types for functions to be generated. Types should use only in, out, unit, or the witness type }}
+  |  	 	  	:: :: none
+  | x_l : typ		:: :: one
+  | x_l : typ ;	functions_opt	:: :: some
+
+indreln_name_aux :: 'inderln_name_' ::=
+  {{ com Name for inductively defined relation }}
+  | [ x_l : typschm witness_opt check_opt functions_opt ] :: :: Name
+
+indreln_name :: '' ::=
+  {{ com Location-annotated name for inductively defined relations }}
+  | indreln_name_aux l	    	     		 	 :: :: Name_l
+
 parsing
 
 P_app right Let_val
     {{ com Opening modules }}
 %  | include id							:: :: Include
 %    {{ com Including modules }}
-  | indreln targets_opt rule1 and ... and rulen			:: :: Indreln
+  | indreln targets_opt indreln_name1 and ... and indreln_namei rule1 and ... and rulen			:: :: Indreln
     {{ com Inductively defined relations }}
   | val_spec 							:: :: Spec_def
     {{ com Top-level type constraints }}
   | { x1 |-> t1 , .. , xn |-> tn }				:: :: concrete
     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }}
     {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} 
+  | { x_l1 |-> t1 , .. , x_ln |-> tn }	    	       	    	 :: :: concrete_loc
+    {{ hol TODO }}
+    {{ lem (List.fold_right (fun ((x,l),t) m -> Pmap.add x t m) [[x_l1 t1 .. x_ln tn]] Pmap.empty) }}
   | E_l1 u+ .. u+ E_ln						:: M :: union
     {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }}
     {{ lem (List.fold_right union_map [[E_l1..E_ln]] Pmap.empty) }}
 
 TD |- t ok
 ------------------------------------------------------------ :: wild
-TD,E,E_l |- _ : t gives {}
+TD,E,E_l |- _ : t gives :E_l_concrete: {}
 
 TD,E,E_l1 |- pat : t gives E_l2
 x NOTIN dom(E_l2)
 ------------------------------------------------------------ :: as
-TD,E,E_l1 |- (pat as x l) : t gives E_l2 u+ {x|->t}
+TD,E,E_l1 |- (pat as x l) : t gives E_l2 u+ :E_l_concrete: {x|->t}
 
 TD,E,E_l1 |- pat : t gives E_l2
 TD,E |- typ ~> t
 TD |- t ok
 E,E_l |- x not ctor
 ------------------------------------------------------------ :: var
-TD,E,E_l |- x l1 l2 : t gives {x|->t}
+TD,E,E_l |- x l1 l2 : t gives :E_l_concrete: {x|->t}
 
 </TD,E |- field idi : p t_args -> ti gives (xi of names) // i />
 </TD,E,E_l |- pati : ti gives E_li//i/>
 
 |- lit : t
 ------------------------------------------------------------ :: lit
-TD,E,E_l |- lit : t gives {}
+TD,E,E_l |- lit : t gives :E_l_concrete: {}
 
 E,E_l |- x not ctor
 ------------------------------------------------------------ :: num_add
-TD,E,E_l |- x l + num : __num gives {x|->__num}
+TD,E,E_l |- x l + num : __num gives :E_l_concrete: {x|->__num}
 
 
 defns
 ------------------------------------------------------------ :: typed
 TD,E,E_l |- (exp : typ) : t gives S_c,S_N
 
-%KATHYCOMMENT: where does E_l1 come from?
 TD,E,E_l1 |- letbind gives E_l2, S_c1,S_N1
 TD,E,E_l1 u+ E_l2 |- exp : t gives S_c2,S_N2
 ------------------------------------------------------------ :: let
-TD,E,E_l |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2
+TD,E,E_l1 |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2
 
 TD,E,E_l |- exp1 : t1 gives S_c1,S_N1 .... TD,E,E_l |- expn : tn gives S_cn,S_Nn
 ------------------------------------------------------------ :: tup
 ------------------------------------------------------------ :: begin
 TD,E,E_l |- begin exp end : t gives S_c,S_N
 
-%TODO t might need different index constraints
 TD,E,E_l |- exp1 : __bool gives S_c1,S_N1
 TD,E,E_l |- exp2 : t gives S_c2,S_N2
 TD,E,E_l |- exp3 : t gives S_c3,S_N3
 ------------------------------------------------------------ :: if
 TD,E,E_l |- if exp1 then exp2 else exp3 : t gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
 
-%TODO t might need different index constraints
 TD,E,E_l |- exp1 : t gives S_c1,S_N1
 TD,E,E_l |- exp2 : __list t gives S_c2,S_N2
 ------------------------------------------------------------ :: cons
 
 % TODO: should require that each xi actually appears free in exp1
 </TD |- ti ok//i/>
-TD,E,E_l u+ {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1
-TD,E,E_l u+ {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2
-disjoint doms(E_l, {</xi|->ti//i/>})
+TD,E,E_l u+ :E_l_concrete: {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1
+TD,E,E_l u+ :E_l_concrete: {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2
+disjoint doms(E_l, :E_l_concrete: {</xi|->ti//i/>})
 E = <E_m,E_p,E_f,E_x>
 </xi NOTIN dom(E_x)//i/>
 ------------------------------------------------------------ :: set_comp
  by
 
 ------------------------------------------------------------ :: empty
-TD,E,E_l |- gives {},{}
+TD,E,E_l |- gives :E_l_concrete:{},{}
 
 TD |- t ok
-TD,E,E_l1 u+ {x |-> t} |- </qbindi//i/> gives E_l2,S_c1
-disjoint doms({x |-> t}, E_l2)
+TD,E,E_l1 u+ :E_l_concrete: {x |-> t} |- </qbindi//i/> gives E_l2,S_c1
+disjoint doms(:E_l_concrete: {x |-> t}, E_l2)
 ------------------------------------------------------------ :: var
-TD,E,E_l1 |- x l </qbindi//i/> gives {x |-> t} u+ E_l2,S_c1
+TD,E,E_l1 |- x l </qbindi//i/> gives :E_l_concrete: {x |-> t} u+ E_l2,S_c1
 
 TD,E,E_l1 |- pat : t gives E_l3
 TD,E,E_l1 |- exp : __set t gives S_c1,S_N1
  by
 
 ------------------------------------------------------------ :: empty
-TD,E,E_l |- list gives {},{}
+TD,E,E_l |- list gives :E_l_concrete:{},{}
 
 TD,E,E_l1 |- pat : t gives E_l3
 TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
 
 :check_funcl:TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N
 ------------------------------------------------------------ :: fn
-TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N
+TD,E,E_l1 |- funcl_aux l gives :E_l_concrete: {x|->t},S_c,S_N
 
 defns
 check_rule :: '' ::=
 by
 
 </TD |- ti ok//i/>
-E_l2 = {</yi|->ti//i/>} 
+E_l2 = {</name_ti->x|->ti//i/>} 
 TD,E,E_l1 u+ E_l2 |- exp' : __bool gives S_c',S_N'
 TD,E,E_l1 u+ E_l2 |- exp1 : u1 gives S_c1,S_N1 .. TD,E,E_l1 u+ E_l2 |- expn : un gives S_cn,S_Nn
 ------------------------------------------------------------ :: rule
-TD,E,E_l1 |- x_l_opt forall </yi li//i/> . exp' ==> x l exp1 .. expn l' gives {x|->curry((u1 * .. * un) , __bool)}, S_c' union S_c1 union .. union S_cn,S_N' union S_N1 union .. union S_Nn
+TD,E,E_l1 |- x_l1 : forall </name_ti//i/> . exp' ==> x l exp1 .. expn l' gives {x|->curry((u1 * .. * un) , __bool)}, S_c' union S_c1 union .. union S_cn,S_N' union S_N1 union .. union S_Nn
 
 defns
 check_texp_tc :: '' ::=
 {{ com Check a value definition }}
 by
 
-TD,E,{} |- letbind gives {</xi|->ti//i/>},S_c,S_N
+TD,E,:E_l_concrete: {} |- letbind gives :E_l_concrete: {</xi|->ti//i/>},S_c,S_N
 %TODO, check S_N constraints
 I |- S_c gives semC
 </FV(ti) SUBSET tnvs//i/>
 </FV(ti) SUBSET tnvs//i/>
 FV(semC) SUBSET tnvs
 compatible overlap(</xi|->ti//i/>)
-E_l = {</xi|->ti//i/>}
+E_l = :E_l_concrete: {</xi|->ti//i/>}
 ------------------------------------------------------------ :: recfun
 TD,I,E |- let rec targets_opt </funcli//i/> gives {</xi|-><forall tnvs. semC => ti,let>//i/>}
 
 </zj//j/>,<TD,TC,I>,E |- val_def l gives empty,<{},{},{},E_x>
 
 </TD,E1,E_l |- rulei gives {xi|->ti},S_ci,S_Ni//i/>
-%TODO Check S_N constraints
+%TODO Check S_N constraints Check indreln_names
 I |- </S_ci//i/> gives semC
 </FV(ti) SUBSET tnvs//i/>
 FV(semC) SUBSET tnvs
 compatible overlap(</xi|->ti//i/>)
-E_l = {</xi|->ti//i/>}
+E_l = :E_l_concrete: {</xi|->ti//i/>}
 E2 = <{},{},{},{</xi |-><forall tnvs. semC => ti,let>//i/>}>
 ------------------------------------------------------------ :: indreln
-</zj//j/>,<TD,TC,I>,E1 |- indreln targets_opt </rulei//i/> l gives empty,E2
+</zj//j/>,<TD,TC,I>,E1 |- indreln targets_opt indreln_names </rulei//i/> l gives empty,E2
 
 </zj//j/> x,D1,E1 |- defs gives D2,E2
 ------------------------------------------------------------ :: module

language/lem.pdf

Binary file modified.
 
 
 type
-a = terminal * text
-
-
-type
 n = terminal * text
 
 
-type 
-a_l =  (* Location-annotated type variables *)
-   A_l of a * l
-
-
-type 
-n_l =  (* Location-annotated numeric variables *)
-   N_l of n * l
+type
+a = terminal * text
 
 
 type 
 
 
 type 
+n_l =  (* Location-annotated numeric variables *)
+   N_l of n * l
+
+
+type 
+a_l =  (* Location-annotated type variables *)
+   A_l of a * l
+
+
+type 
+nexp_constraint_aux =  (* Whether a vector is bounded or fixed size *)
+   Fixed of nexp * terminal * nexp
+ | Bounded of nexp * terminal * nexp
+
+
+type 
+tnvar =  (* Union of type variables and Nexp type variables, with locations *)
+   Avl of a_l
+ | Nvl of n_l
+
+
+type 
 id =  (* Long identifers *)
    Id of ((x_l * terminal)) list * x_l * l
 
 
 type 
+nexp_constraint =  (* Location-annotated Nexp range *)
+   Range_l of nexp_constraint_aux * l
+
+
+type 
+c =  (* Typeclass constraints *)
+   C of id * tnvar
+
+
+type 
 lit_aux =  (* Literal constants *)
    L_true of terminal
  | L_false of terminal
 
 
 type 
-tnvar =  (* Union of type variables and Nexp type variables, with locations *)
-   Avl of a_l
- | Nvl of n_l
-
-
-type 
-nexp_constraint_aux =  (* Whether a vector is bounded or fixed size *)
-   Fixed of nexp * terminal * nexp
- | Bounded of nexp * terminal * nexp
-
-
-type 
 p =  (* Unique paths *)
    Path_def of ((x * terminal)) list * x
  | Path_list of terminal
 
 
 type 
-lit = 
-   Lit_l of lit_aux * l (* Location-annotated literal constants *)
-
-
-type 
-c =  (* Typeclass constraints *)
-   C of id * tnvar
+cs =  (* Typeclass and length constraint lists *)
+   Cs_empty
+ | Cs_classes of (c * terminal) list * terminal (* Must have $>0$ constraints *)
+ | Cs_lengths of (nexp_constraint * terminal) list * terminal (* Must have $>0$ constraints *)
+ | Cs_both of (c * terminal) list * terminal * (nexp_constraint * terminal) list * terminal (* Must have $>0$ of both form of constraints *)
 
 
 type 
-nexp_constraint =  (* Location-annotated Nexp range *)
-   Range_l of nexp_constraint_aux * l
+lit = 
+   Lit_l of lit_aux * l (* Location-annotated literal constants *)
 
 
 type 
 
 
 type 
-tannot_opt =  (* Optional type annotations *)
-   Typ_annot_none
- | Typ_annot_some of terminal * typ
+target =  (* Backend target names *)
+   Target_hol of terminal
+ | Target_isa of terminal
+ | Target_ocaml of terminal
+ | Target_coq of terminal
+ | Target_tex of terminal
+ | Target_html of terminal
 
 
 type 
-q =  (* Quantifiers *)
-   Q_forall of terminal
- | Q_exists of terminal
+c_pre =  (* Type and instance scheme prefixes *)
+   C_pre_empty
+ | C_pre_forall of terminal * (tnvar) list * terminal * cs (* Must have $>0$ type variables *)
 
 
 type 
 
 
 type 
-cs =  (* Typeclass and length constraint lists *)
-   Cs_empty
- | Cs_classes of (c * terminal) list * terminal (* Must have $>0$ constraints *)
- | Cs_lengths of (nexp_constraint * terminal) list * terminal (* Must have $>0$ constraints *)
- | Cs_both of (c * terminal) list * terminal * (nexp_constraint * terminal) list * terminal (* Must have $>0$ of both form of constraints *)
+q =  (* Quantifiers *)
+   Q_forall of terminal
+ | Q_exists of terminal
 
 
 type 
-target =  (* Backend target names *)
-   Target_hol of terminal
- | Target_isa of terminal
- | Target_ocaml of terminal
- | Target_coq of terminal
- | Target_tex of terminal
- | Target_html of terminal
+tannot_opt =  (* Optional type annotations *)
+   Typ_annot_none
+ | Typ_annot_some of terminal * typ
 
 
 type 
 
 
 type 
+targets =  (* Backend target name lists *)
+   Targets_concrete of terminal * (target * terminal) list * terminal
+
+
+type 
+functions_opt =  (* Optional names and types for functions to be generated. Types should use only in, out, unit, or the witness type *)
+   Functions_none
+ | Functions_one of x_l * terminal * typ
+ | Functions_some of x_l * terminal * typ * terminal * functions_opt
+
+
+type 
+typschm =  (* Type schemes *)
+   Ts of c_pre * typ
+
+
+type 
+witness_opt =  (* Optional witness type name declaration. Must be present for a witness type to be generated. *)
+   Witness_none
+ | Witness_some of terminal * terminal * x_l * terminal
+
+
+type 
+check_opt =  (* Option check name declaration *)
+   Check_none
+ | Check_some of terminal * x_l * terminal
+
+
+type 
 exp_aux =  (* Expressions *)
    Ident of id (* Identifiers *)
  | Nvar of n (* Nexp var, has type num *)
 
 
 type 
-x_l_opt =  (* Optional name for inductively defined relation clauses *)
-   X_l_none
- | X_l_some of x_l * terminal
-
-
-type 
-c_pre =  (* Type and instance scheme prefixes *)
-   C_pre_empty
- | C_pre_forall of terminal * (tnvar) list * terminal * cs (* Must have $>0$ type variables *)
-
-
-type 
-targets =  (* Backend target name lists *)
-   Targets_concrete of terminal * (target * terminal) list * terminal
+name_t =  (* Name or name with type for inductively defined relation clauses *)
+   Name_t_name of x_l
+ | Name_t_nt of terminal * x_l * terminal * typ * terminal
 
 
 type 
 
 
 type 
-rule_aux =  (* Inductively defined relation clauses *)
-   Rule of x_l_opt * terminal * (x_l) list * terminal * exp * terminal * x_l * (exp) list
-
-
-type 
-typschm =  (* Type schemes *)
-   Ts of c_pre * typ
-
-
-type 
 lemma_typ =  (* Types of Lemmata *)
    Lemma_assert of terminal
  | Lemma_lemma of terminal
 
 
 type 
+indreln_name_aux =  (* Name for inductively defined relation *)
+   Inderln_name_Name of terminal * x_l * terminal * typschm * witness_opt * check_opt * functions_opt * terminal
+
+
+type 
 funcl =  (* Location-annotated function clauses *)
    Rec_l of funcl_aux * l
 
 
 type 
+rule_aux =  (* Inductively defined relation clauses *)
+   Rule of x_l * terminal * terminal * (name_t) list * terminal * exp * terminal * x_l * (exp) list
+
+
+type 
 nec =  (* Numeric expression constraints *)
    Lessthan of ne * terminal * nec
  | Eq of ne * terminal * nec
 
 
 type 
-rule =  (* Location-annotated inductively defined relation clauses *)
-   Rule_l of rule_aux * l
+instschm =  (* Instance schemes *)
+   Is of c_pre * terminal * id * typ * terminal
 
 
 type 
-instschm =  (* Instance schemes *)
-   Is of c_pre * terminal * id * typ * terminal
+lemma_decl =  (* Lemmata and Tests *)
+   Lemma_named of lemma_typ * targets option * x_l * terminal * terminal * exp * terminal
+ | Lemma_unnamed of lemma_typ * targets option * terminal * exp * terminal
 
 
 type 
 
 
 type 
-lemma_decl =  (* Lemmata and Tests *)
-   Lemma_named of lemma_typ * targets option * x_l * terminal * terminal * exp * terminal
- | Lemma_unnamed of lemma_typ * targets option * terminal * exp * terminal
+indreln_name =  (* Location-annotated name for inductively defined relations *)
+   Name_l of indreln_name_aux * l
 
 
 type 
 
 
 type 
+rule =  (* Location-annotated inductively defined relation clauses *)
+   Rule_l of rule_aux * l
+
+
+type 
 def_aux =  (* Top-level definitions *)
    Type_def of terminal * (td * terminal) list (* Type definitions *)
  | Val_def of val_def (* Value definitions *)
  | Module of terminal * x_l * terminal * terminal * defs * terminal (* Module definitions *)
  | Rename of terminal * x_l * terminal * id (* Module renamings *)
  | Open of terminal * id (* Opening modules *)
- | Indreln of terminal * targets option * (rule * terminal) list (* Inductively defined relations *)
+ | Indreln of terminal * targets option * (indreln_name * terminal) list * (rule * terminal) list (* Inductively defined relations *)
  | Spec_def of val_spec (* Top-level type constraints *)
  | Class of terminal * terminal * x_l * tnvar * terminal * ((terminal * x_l * terminal * typ * l)) list * terminal (* Typeclass definitions *)
  | Instance of terminal * instschm * ((val_def * l)) list * terminal (* Typeclass instantiations *)
 
 
 type 
+name_ts =  (* Names with optional types for inductively defined relation clauses *)
+   NameTs of (name_t) list
+
+
+type 
 env_tag =  (* Tags for the (non-constructor) value descriptions *)
    Method of terminal (* Bound to a method *)
  | Spec of terminal (* Specified with val *)
 
 
 type 
-f_desc = 
-   F_field of terminal * terminal * tnv list * terminal * p * terminal * t * terminal * terminal * x * terminal * Set.Make(String).t * terminal * terminal (* Fields *)
-
-
-type 
 v_desc =  (* Value descriptions *)
    V_constr of terminal * terminal * tnv list * terminal * t list * terminal * p * terminal * terminal * x * terminal * Set.Make(String).t * terminal * terminal (* Constructors *)
  | V_val of terminal * terminal * tnv list * terminal * semC * terminal * t * terminal * env_tag * terminal (* Values *)
 
 
 type 
-tc_def =  (* Type and class constructor definitions *)
-   Tc_def of tnv list * t option (* Type constructors *)
+f_desc = 
+   F_field of terminal * terminal * tnv list * terminal * p * terminal * t * terminal * terminal * x * terminal * Set.Make(String).t * terminal * terminal (* Fields *)
 
 
 type 
 inst =  (* A typeclass instance, t must not contain nested types *)
    Inst of semC * terminal * terminal * p * t * terminal
 
+
+type 
+tc_def =  (* Type and class constructor definitions *)
+   Tc_def of tnv list * t option (* Type constructors *)
+
 (** definitions *)
 (** definitions *)
 (** definitions *)
   val reln_start : t
   val reln_end : t
   val reln_sep : t
+  val reln_name_start : t
+  val reln_name_end : t
   val reln_clause_start : t
   val reln_clause_quant : t
   val reln_clause_show_empty_quant : bool
   val reln_clause_show_name : bool
+  val reln_clause_quote_name : bool
   val reln_clause_add_paren : bool
   val reln_clause_end : t
 
   let reln_start = kwd "indreln"
   let reln_end = emp
   let reln_sep = kwd "and"
+  let reln_name_start = kwd "["
+  let reln_name_end = kwd "]"
   let reln_clause_quant = kwd "forall"
   let reln_clause_show_empty_quant = true
-  let reln_clause_show_name = false
+  let reln_clause_show_name = true
+  let reln_clause_quote_name = false
   let reln_clause_add_paren = false
   let reln_clause_start = emp
   let reln_clause_end = emp
   let setcomp_binding_start = kwd "&forall;"
   let reln_clause_quant = kwd "&forall;"
   let reln_clause_show_empty_quant = true
-  let reln_clause_show_name = false
+  let reln_clause_show_name = true
+  let reln_clause_quote_name = false
   let reln_clause_add_paren = false
   let reln_clause_start = emp
 
   let reln_start = tkwdl "indreln"
   let reln_end = emp
   let reln_sep = tkwdm "and"
+  let reln_name_start = kwd "["
+  let reln_name_end = kwd "]"
   let reln_clause_start = emp
   let reln_clause_quant = kwd "\\forall"
   let reln_clause_show_empty_quant = true
-  let reln_clause_show_name = false
+  let reln_clause_show_name = true
+  let reln_clause_quote_name = false
   let reln_clause_add_paren = false
   let reln_clause_end = emp
 
   let reln_start = kwd "inductive"
   let reln_end = emp
   let reln_sep = kwd "|"
+  let reln_name_start = emp (*TODO Indreln fix up for isabelle*)
+  let reln_name_end = emp
   let reln_clause_start = kwd "\""
   let reln_clause_quant = kwd "!!"
   let reln_clause_show_empty_quant = false
   let reln_clause_show_name = true
+  let reln_clause_quote_name = true
   let reln_clause_add_paren = false
   let reln_clause_end = kwd "\""
 
   let reln_start = meta "val _ = Hol_reln `"
   let reln_end = meta "`;"
   let reln_sep = kwd "/\\"
+  let reln_name_start = emp (*TODO Inderln fixup for Hol*)
+  let reln_name_end = emp
   let reln_clause_start = kwd "("
   let reln_clause_quant = kwd "!"
   let reln_clause_show_empty_quant = false
   let reln_clause_show_name = false
+  let reln_clause_quote_name = false
   let reln_clause_add_paren = true
   let reln_clause_end = kwd ")"
 
                                                 | Tn_N (x, y, z) -> kwd (Ulib.Text.to_string y))) tvs in
     tdef_tctor false tvs n regexp ^ tyexp true n' tvs' texp 
 
-let indreln_clause (name_opt, s1, qnames, s2, e_opt, s3, rname, es) =
+let range = function
+  | GtEq(_,n1,s,n2) -> nexp n1 ^ ws s ^ kwd ">=" ^ nexp n2
+  | Eq(_,n1,s,n2) -> nexp n1 ^ ws s ^ kwd "=" ^ nexp n2
+
+let constraints = function
+  | None -> emp
+  | Some(Cs_list(l_c,op_s,l_r,s)) ->
+      flat (Seplist.to_sep_list
+              (fun (id,tv) ->
+                 Ident.to_output T.infix_op_format Type_var T.path_sep id ^
+                 tyvar tv)
+              (sep (kwd","))
+              l_c) ^
+      (match op_s with
+        | None -> emp
+        | Some s1 -> ws s1 ^ kwd ";") ^
+      flat (Seplist.to_sep_list range (sep (kwd",")) l_r) ^
+      ws s ^
+      kwd "=>"
+
+let constraint_prefix (Cp_forall(s1,tvs,s2,constrs)) =
+  ws s1 ^
+  T.forall ^
+  flat (List.map tyvar tvs) ^
+  ws s2 ^
+  kwd "." ^
+  constraints constrs
+
+let indreln_name (RName(s1,name,s2,(constraint_pre,t),witness,checks,functions,s3)) =
+  ws s1 ^
+  T.reln_name_start ^ 
+  (Name.to_output T.infix_op_format Term_method name) ^ ws s2 ^
+  T.typ_sep ^
+      begin
+        match constraint_pre with
+          | None -> emp
+          | Some(cp) -> constraint_prefix cp
+      end ^
+      typ t ^  
+  ws s3 ^
+  T.reln_name_end
+
+let indreln_clause (Rule(name, s0, s1, qnames, s2, e_opt, s3, rname, es)) =
   (if T.reln_clause_show_name then (
-    (match name_opt with None -> emp | Some name ->
-      Name.to_output_quoted T.infix_op_format Term_method name ^
+    ((if T.reln_clause_quote_name then Name.to_output_quoted else Name.to_output) T.infix_op_format Term_method name ^
+      ws s0 ^
       kwd ":"
     )
   ) else emp) ^
   ws s1 ^ T.reln_clause_start ^
+  (*Indreln TODO does not print format annotated variables with their types find*)
   (if (T.reln_clause_show_empty_quant || List.length qnames > 0) then (
     T.reln_clause_quant ^
-    flat (interspace (List.map (fun n -> Name.to_output T.infix_op_format Term_var n.term) qnames)) ^
+    flat (interspace (List.map (fun (QName n) -> Name.to_output T.infix_op_format Term_var n.term) qnames)) ^
     ws s2 ^ 
     kwd "."
   ) else emp) ^
 
 let isa_funcl_header_indrel_seplist clause_sl =
   let clauseL = Seplist.to_list clause_sl in
-  let (_, clauseL_filter) = List.fold_left (fun (ns, acc) (_, _, _, _, _, _, rname, _) ->
+  let (_, clauseL_filter) = List.fold_left (fun (ns, acc) (Rule(_,_, _, _, _, _, _, rname, _)) ->
       let n = Name.strip_lskip rname.term in 
       if NameSet.mem n ns then (ns, acc) else (NameSet.add n ns, rname :: acc)) (NameSet.empty, []) clauseL in
   let headerL = List.map (fun rname -> 
 
 (******* End Isabelle ********)
 
-let range = function
-  | GtEq(_,n1,s,n2) -> nexp n1 ^ ws s ^ kwd ">=" ^ nexp n2
-  | Eq(_,n1,s,n2) -> nexp n1 ^ ws s ^ kwd "=" ^ nexp n2
-
-let constraints = function
-  | None -> emp
-  | Some(Cs_list(l_c,op_s,l_r,s)) ->
-      flat (Seplist.to_sep_list
-              (fun (id,tv) ->
-                 Ident.to_output T.infix_op_format Type_var T.path_sep id ^
-                 tyvar tv)
-              (sep (kwd","))
-              l_c) ^
-      (match op_s with
-        | None -> emp
-        | Some s1 -> ws s1 ^ kwd ";") ^
-      flat (Seplist.to_sep_list range (sep (kwd",")) l_r) ^
-      ws s ^
-      kwd "=>"
-
-let constraint_prefix (Cp_forall(s1,tvs,s2,constrs)) =
-  ws s1 ^
-  T.forall ^
-  flat (List.map tyvar tvs) ^
-  ws s2 ^
-  kwd "." ^
-  constraints constrs
 
 let rec hol_strip_args_n type_names n ts =
   match type_names with
       ws s ^
       T.module_open ^
       Ident.to_output T.infix_op_format Module_name T.path_sep (resolve_ident_path m m.descr.mod_binding)
-  | Indreln(s,targets,clauses) ->
+  | Indreln(s,targets,names,clauses) ->
       if in_target targets then
         ws s ^
         T.reln_start ^
            targets_opt targets 
          else
            emp) ^
+        flat (Seplist.to_sep_list indreln_name (sep T.reln_sep) names) ^
         flat (Seplist.to_sep_list indreln_clause (sep T.reln_sep) clauses) ^
         T.reln_end
       else
   | Val_spec(s1,(n,l),s2,t) ->
       raise (Reporting_basic.err_todo false l "Isabelle: Top-level type constraints omited; should not occur at the moment")
 
-  | Indreln(s,targets,clauses) ->
+  (* TODO INDRELN THe names should be output *)
+  | Indreln(s,targets,names,clauses) ->
       if in_target targets then
         ws s ^
         T.reln_start ^

src/convert_relations.ml

+(* Converting a relation *)
+
+open Typed_ast
+open Types
+open Util
+open Typed_ast_syntax
+
+(* Notes on names :
+ Name.strip_lskip
+ Name.add_lskip
+
+type ('a,'b) annot = { term : 'a; locn : Ast.l; typ : t; rest : 'b }
+
+*)
+
+module Converter(C : Exp_context) = struct
+
+module C = Exps_in_context(C)
+open C
+
+module Nmap = Typed_ast.Nfmap
+module Nset = Nmap.S
+
+(* Split on infix (&&) : ((a && b) && (c && d)) && true -> [a;b;c;d] *)
+
+let is_true l = match l.term with
+  | L_true _ -> true
+  | _ -> false
+
+let r = Ulib.Text.of_latin1
+let mk_string_path ns n = Path.mk_path (List.map (fun s -> Name.from_rope (r s)) ns) (Name.from_rope (r n))
+let and_path = mk_string_path ["Pervasives"] "&&"
+
+let mk_option ty = 
+  { Types.t = Types.Tapp([ty], mk_string_path ["Pervasives"] "option") } 
+
+let remove_option ty = 
+  match ty.t with
+    | Types.Tapp([ty], _) -> ty
+    | _ -> failwith "???"
+
+let path_to_string_list p = 
+  let (mp,n) = Path.to_name_list p in
+  (List.map Name.to_string mp, Name.to_string n)
+
+let mk_const_from_path env l path inst = 
+  let (mp,n) = path_to_string_list path in
+  mk_const_exp env l mp n inst
+
+
+let names_get_constructor env mp n = 
+  let env' = lookup_env env mp in
+  let cname = Name.to_string n in
+  match Nfmap.apply env'.v_env n with
+    | Some(Constr d) -> d
+    | _ -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal(Ast.Unknown, "names_get_constructor env did not contain constructor!" ^ cname)))
+
+let get_constructor env mp n = 
+    names_get_constructor env (List.map (fun n -> (Name.from_rope (r n))) mp) (Name.from_rope (r n))
+
+let get_constr_id l env mp n tys =
+  { id_path = Id_none None;
+    id_locn = l;
+    descr = get_constructor env mp n;
+    instantiation = tys }
+
+let mk_constr_exp env mp n tys args = 
+  let l = Ast.Trans ("mk_constr_exp", None) in
+  let c = get_constr_id l env mp n tys in
+  List.fold_left (fun fn arg -> mk_app l fn arg None) (mk_constr l c None) args
+
+let mk_pconstr_pat env mp n tys args = 
+  let l = Ast.Trans ("mk_pconstr_pat", None) in
+  let c = get_constr_id l env mp n tys in
+  mk_pconstr l c args None
+
+module LemOptionMonad = struct
+
+
+let mk_none env ty = mk_constr_exp env ["Pervasives"] "None" [ty] [] 
+let mk_some env e = mk_constr_exp env ["Pervasives"] "Some" [exp_to_typ e] [e]
+let mk_pnone env ty = mk_pconstr_pat env ["Pervasives"] "None" [ty] []
+let mk_psome env p = mk_pconstr_pat env ["Pervasives"] "Some" [p.typ] [p]
+
+let mk_bind env call pat code = 
+  let l = Ast.Trans ("mk_bind", None) in
+  mk_case_exp false l call
+    [(mk_psome env pat, code);
+     (mk_pwild l None (exp_to_typ call), mk_none env (remove_option (exp_to_typ code)))]
+    (exp_to_typ code)
+
+let mk_cond env cond code = 
+  let l = Ast.Trans ("mk_cond", None) in
+  mk_if_exp l cond code (mk_none env (remove_option (exp_to_typ code)))
+
+
+end
+
+
+let is_and e = match C.exp_to_term e with
+  | Constant c -> Path.compare c.descr.const_binding and_path = 0
+  | _ -> false
+
+let rec split_and (e : exp) = match C.exp_to_term e with
+  | Infix(e1, op_and, e2) when is_and op_and ->
+    split_and e1 @ split_and e2
+  | Lit lit_true when is_true lit_true -> []
+  | Paren(_,e,_) -> split_and e
+  | Typed(_,e,_,_,_) -> split_and e
+  | _ -> [e]
+
+(* 
+  Group rules by output relation
+*)
+
+type ruledescr = {
+  rule_name : Name.t;
+  rule_vars : (Name.t * Types.t) list;
+  rule_conds : exp list;
+  rule_args : exp list
+} 
+
+type reldescr = {
+  rel_name : Name.t;
+  rel_type : typschm;
+  rel_argtypes : Types.t list;
+  rel_witness : Name.t option;
+  rel_check : Name.t option;
+  rel_indfns : (Name.t * (mode * bool)) list;
+  rel_rules : ruledescr list
+}
+
+type relsdescr = reldescr Nfmap.t
+
+
+let mk_list_type ty = 
+  { Types.t = Types.Tapp([ty], Path.listpath) }
+
+let map_option f = function
+  | Some(x) -> Some(f x)
+  | None -> None
+
+let to_in_out (typ : src_t) : input_or_output = 
+  match typ.term with
+    | Typ_app({id_path = p}, []) ->
+      begin match p with
+        | Id_some(i) -> 
+          begin match Name.to_string (Name.strip_lskip (Ident.get_name i)) with
+            | "input" -> I
+            | "out" -> O
+            | s -> raise (Invalid_argument ("to_in_out: "^s))
+          end
+        | _ -> raise (Invalid_argument "to_in_out")
+      end
+    | _ -> raise (Invalid_argument "to_in_out")
+
+
+(* This is all wrong *)
+let rec src_t_to_mode (typ : src_t) : mode * bool =
+  match typ.term with
+    | Typ_paren(_,t,_) -> src_t_to_mode t
+    | Typ_fn(x1,_,x2) -> 
+      let (mode,wit) = src_t_to_mode x2 in
+      (to_in_out x1::mode, wit)
+    | Typ_app({id_path = p },[]) ->
+      begin 
+        try ([to_in_out typ], false)
+        with Invalid_argument _ -> 
+          begin match p with
+            | Id_some(i) ->
+              let n = Name.to_string (Name.strip_lskip (Ident.get_name i)) in
+              ([], not (n = "unit" || n = "bool"))
+            | _ -> raise (Invalid_argument "src_t_to_mode")
+          end
+      end
+    | _ -> raise (Invalid_argument "src_t_to_mode")
+
+
+let rec decompose_rel_type typ = 
+  match typ.term with
+    | Typ_fn(u,_,v) -> u.typ::decompose_rel_type v
+    | _ -> [] (* The return value is assumed to be bool, we don't check it *)
+
+(* the src_t is frustrating ! *)
+let out_ty_from_mode env localenv reldescr (mode, wit) = 
+  let ret = map_filter (function
+    | (O,x) -> Some x
+    | _ -> None
+  ) (List.map2 (fun x y -> (x,y)) mode reldescr.rel_argtypes) in
+  let ret = if wit then 
+    let Some(x) = Nfmap.apply localenv.r_env reldescr.rel_name in
+    let Some(t,_) = x.ri_witness in
+    ret@[{t = Tapp([],t)}]
+    else ret 
+  in
+  mk_list_type {t=Ttup(ret)}
+ 
+let in_tys_from_mode env reldescr (mode, _wit) = 
+  map_filter (function
+    | (I,x) -> Some x
+    | _ -> None
+  ) (List.map2 (fun x y -> (x,y)) mode reldescr.rel_argtypes)
+
+let ty_from_mode env localenv reldescr mode = 
+  let args = in_tys_from_mode env reldescr mode in
+  let ret = out_ty_from_mode env localenv reldescr mode in
+  List.fold_right (fun a b -> {t=Tfn(a,b)}) args ret
+
+
+let get_rels (names : indrel_name lskips_seplist) 
+    (l: Typed_ast.rule lskips_seplist) : relsdescr =
+  let names = List.fold_left (fun s (RName(_,n,_,t,wit,chk,fn,_)) ->
+    let relname = Name.strip_lskip n in
+    let witness = map_option (fun (Witness(_,_,n,_)) -> Name.strip_lskip n) wit in 
+    let check = map_option (fun (_,n,_) -> Name.strip_lskip n) chk in
+    let (_constraints, typ) = t in
+    let argtypes = decompose_rel_type typ in
+    let fn = match fn with None -> [] | Some(x) -> x in
+    let indfns = List.map 
+      (fun (Fn(n,_,t,_)) -> (Name.strip_lskip n, src_t_to_mode t)) fn in
+    let descr = {
+      rel_name = relname;
+      rel_type = t;
+      rel_argtypes = argtypes; 
+      rel_witness = witness;
+      rel_check = check;
+      rel_indfns = indfns;
+      rel_rules = []
+    } in
+    Nfmap.insert s (relname, descr)
+  ) Nfmap.empty (Seplist.to_list names) in
+  List.fold_left (fun s (Rule(rulename,_,_,vars,_,cond,_,rel,args)) ->
+    let rulename = Name.strip_lskip rulename in
+    let relname = Name.strip_lskip rel.term in
+    let rulecond = match cond with
+      | Some x -> x
+      | None -> C.mk_lit Ast.Unknown ({term = L_true None; locn = Ast.Unknown; typ =  {t = Tapp([], Path.boolpath)}; rest = ()}) None in
+    let vars = List.map (function
+      | QName(n) -> n
+      | Name_typ(_,n,_,_,_) -> n
+    ) vars in
+    let ruledescr = {
+      rule_name = rulename;
+      rule_vars = List.map (fun v -> (Name.strip_lskip v.term, v.typ) ) vars;
+      rule_conds = split_and rulecond;
+      rule_args = args
+    } in
+    match Nfmap.apply s relname with
+      | None -> failwith "Relation without description (is this ok ?)" (* TODO *)
+      | Some rel -> Nfmap.insert s 
+        (relname, {rel with rel_rules = ruledescr::rel.rel_rules})
+  ) names (Seplist.to_list l)
+
+type ('a,'b) choice = Left of 'a | Right of 'b
+
+let map_partition f l = 
+  List.fold_right (fun x (ls,rs) ->
+    match f x with
+      | Left l -> (l::ls,rs)
+      | Right r -> (ls,r::rs)
+  ) l ([],[])
+
+
+(* Just a small model of the code we will generate later
+   We will need a partial "exp to pattern" function somewhere *)
+type code = 
+  | IF of exp * code 
+  | CALL of (Name.t * Types.t, Path.t) choice * exp list * pat list * code
+  | IFEQ of exp * exp * code 
+  | RETURN of exp list
+
+exception No_translation of exp option
+
+let no_translation e = raise (No_translation e)
+
+let make_namegen names = 
+  let names = ref names in
+  let fresh n = 
+    let n' = Name.fresh n (fun n -> not (Nset.mem n !names)) in
+    names := Nset.add n' !names;
+    n'
+  in
+  fresh
+
+(* Problems : 
+   - the user can't shadow relation names
+   - we probably rename relation names anyway
+*)
+let make_renamer quantified_orig rules = 
+  let scope = Nset.union quantified_orig rules in
+  let gen_name = make_namegen scope in
+  let used = ref Nset.empty in
+  let gen_eqused () = 
+    let seen = ref Nset.empty in 
+    let equalities = ref [] in
+    let check_rename v typ =
+      let n = Name.strip_lskip v in
+      if not (Nset.mem n quantified_orig)
+      then no_translation None
+      else 
+        begin 
+          let varname = 
+            if not (Nset.mem n !used)
+            then n
+            else 
+              let n' = gen_name (Name.to_rope n)  in
+              let v' =  Name.add_lskip n' in
+              equalities := (C.mk_var Ast.Unknown v typ,
+                             C.mk_var Ast.Unknown v' typ) :: !equalities;
+              n'
+          in
+          used := Nset.add varname !used;
+          seen := Nset.add varname !seen;
+          Name.add_lskip varname
+        end
+    in
+    let transform_exp e typ = 
+      let n = gen_name (Ulib.Text.of_latin1 "pat") in
+      let v = Name.add_lskip n in
+      used := Nset.add n !used;
+      seen := Nset.add n !seen;
+      equalities := (C.mk_var Ast.Unknown v typ, e) :: !equalities;
+      C.mk_pvar_annot Ast.Unknown v (C.t_to_src_t typ) (Some typ)
+    in
+    (check_rename, transform_exp, seen, equalities)
+  in
+  gen_eqused
+
+(* Try to convert an expression to a pattern
+
+    `check_rename' checks that the translated vars are forall-bound and not
+    relations, and renames them if necessary to make the pattern matching
+    linear 
+*)
+
+
+let split_app e = 
+  let rec split_app e args = match C.exp_to_term e with
+    | App(e1,e2) -> split_app e1 (e2::args)
+    | Paren(_,e,_) | Begin(_,e,_) | Typed(_,e,_,_,_) -> split_app e args
+    | Infix(e2, e1, e3) -> split_app e1 (e2::e3::args)
+    | _ -> (e,args)
+  in
+  split_app e []
+
+let id x = x
+
+let cons_path = mk_string_path ["Pervasives"] "::"
+let is_cons cons = Path.compare cons.descr.const_binding cons_path = 0
+
+let exp_to_pat e check_rename transform_exp  =
+  let rec exp_to_pat e = 
+    let loc = exp_to_locn e in
+    let typ = Some(exp_to_typ e) in
+    let ty = exp_to_typ e in
+    let (head, args) = split_app e in
+    match C.exp_to_term head, args with
+      | Constructor c, args -> mk_pconstr loc c (List.map exp_to_pat args) typ
+      | Constant cons, [e1;e2] when is_cons cons -> 
+        mk_pcons loc (exp_to_pat e1) None (exp_to_pat e2) typ 
+      | Var v, [] ->
+            mk_pvar_annot loc (check_rename v ty) 
+              (C.t_to_src_t ty) typ
+      | Record(s1, fields,s2), [] -> 
+        let pfields = Seplist.map (fun (field, skip, e, _loc) ->
+          (field, skip, exp_to_pat e)) fields in
+        mk_precord loc s1 pfields s2 typ 
+      | Vector(s1, es, s2), [] -> 
+        mk_pvector loc s1 (exps_to_pats es) s2 ty
+      | Tup(s1, es, s2), [] -> 
+        mk_ptup loc s1 (exps_to_pats es) s2 typ
+      | List(s1, es, s2), [] ->
+        mk_plist loc s1 (exps_to_pats es) s2 ty
+      | Lit l, [] -> mk_plit loc l typ
+      | Set(s1, es, s2), [] when Seplist.length es = 1 ->
+        (* XXX TODO FIXME XXX: cheat here *)
+        let se = Seplist.hd es in
+        let pat = exp_to_pat se in
+        Reporting.print_debug_exp "Cheated on set expression" [e];
+        transform_exp e ty
+      | _ -> Reporting.print_debug_exp "Untranslatable" [e]; transform_exp e ty
+  and exps_to_pats es = Seplist.map exp_to_pat es in
+  exp_to_pat e
+(* TODO : what is Nvar_e*)
+
+let find_some f l = try Some(List.find f l) with Not_found -> None
+
+let convert_output gen_rn exps mask = 
+  let (check_rename, transform_exp, bound, equalities) = gen_rn () in
+  let outargs = map_filter id (List.map2 (fun exp inarg ->
+    if inarg then None
+    else Some (exp_to_pat exp check_rename transform_exp)
+  ) exps mask) in
+  (outargs, !bound, !equalities)
+
+let report_no_translation rule notok eqconds sideconds =
+  let (%) f x = Ulib.Text.to_string (f x) in
+  Reporting.print_debug_exp "No translation for relation with args" rule.rule_args;
+  Reporting.print_debug_exp "Conditions are" rule.rule_conds;
+  no_translation None
+(*
+let transform_rule mode_env _ty mode (rule : ruledescr) = 
+  let vars = Nfmap.domain (Nfmap.from_list rule.rule_vars) in
+  let gen_rn = make_renamer vars (Nmap.domain mode_env) in
+  let (patterns, initknown, initeqs) = 
+    convert_output gen_rn rule.rule_args (List.map (fun x -> x = O) mode) in
+  (* TODO : we should substitute *)
+  let relknowns = 
+    Nfmap.fold (fun set rel (_ty,modes) ->
+      if List.exists (fun (_n,m,_t) -> List.for_all (fun k -> k = I) m) modes
+      then Nset.add rel set
+      else set) Nset.empty mode_env in
+  let returns = map_filter (function
+    | (I, _) -> None
+    | (O, r) -> Some(r)
+  ) (List.map2 (fun x y -> (x,y)) mode rule.rule_args) in
+  let rec build_code known indconds sideconds eqconds =
+    let exp_known e = Nfmap.fold (fun b v _ -> b && Nset.mem v known) 
+      true (C.exp_to_free e) in
+    let (selected_eqs,eqconds2) = 
+      List.partition (fun (e1,e2) -> exp_known e1 && exp_known e2) eqconds in
+    let (selected_side,sideconds2) = 
+      List.partition (fun e -> exp_known e) sideconds in
+    let add_eq eq x = List.fold_left (fun x (e1,e2) -> IFEQ(e1,e2,x)) x eq in
+    let add_side side x = List.fold_left (fun x e -> IF(e,x)) x side in 
+    let rec search notok = function
+      | [] ->
+        begin match eqconds2,sideconds2 with
+          | [], [] when notok = [] -> RETURN returns
+          | _ -> report_no_translation rule notok eqconds2 sideconds2
+        end
+      | (head,modes,args) as c::cs ->
+        let inargs = List.map exp_known args in
+        let mode_matches (_name,mode,_ty) = 
+          List.for_all (fun x -> x) 
+            (List.map2 (fun inp m -> inp || m = O) inargs mode) in
+        match List.filter mode_matches modes with
+          | [] -> search (c::notok) cs
+          | (name,mode,ty)::ms -> 
+            let (outputs, bound, equalities) = convert_output gen_rn args 
+              (List.map (fun m -> m = I) mode) in
+            let inputs = map_filter id (List.map2 (fun exp m ->
+              match m with
+                | I -> Some(exp)
+                | O -> None
+            ) args mode) in
+            CALL(name, ty, inputs, outputs,
+                 build_code (Nset.union bound known) (cs@notok) 
+                   sideconds2 (equalities@eqconds2))
+    in
+    add_eq selected_eqs (add_side selected_side (search [] indconds))
+  in
+  let (indconds, sideconds) = 
+    List.fold_left (fun (left, right) x -> 
+      let (e, args) = split_app x in
+      match Typed_ast_syntax.dest_var_exp e with
+        | Some(n) when not (Nset.mem n vars)-> begin
+          match Nfmap.apply mode_env n with
+            | Some(_ty,modes) -> ((n,modes,args)::left, right)
+            | _ -> (left, e::right)
+        end
+        | _ -> (left, e::right)) ([],[]) rule.rule_conds in
+  (patterns, build_code initknown indconds sideconds initeqs)
+*)  
+
+(*
+let debug_print_transformed trans = 
+  let module B = Backend.Make(struct
+    let avoid = (false, (fun _ -> true), Name.fresh)
+  end) in
+  let (%) f x = Ulib.Text.to_string (f x) in
+  let print_compiled (patterns, code) =
+    Format.eprintf "PATTERNS: ";
+    List.iter (fun pat -> 
+      Format.eprintf "[%s] " (B.ident_pat % pat)
+    ) patterns;
+    Format.eprintf "\n--CODE: \n";
+    let rec print_code = function 
+      | IF(e,c) -> 
+        Format.eprintf "IF [%s]\n" (B.ident_exp % e); 
+        print_code c
+      | IFEQ(e1,e2,c) -> 
+        Format.eprintf "IFEQ [%s] == [%s]\n" (B.ident_exp % e1) (B.ident_exp % e2);
+        print_code c
+      | CALL(n,ty,inputs, outputs,c) ->
+        Format.eprintf "CALL (%s : %s) " (Name.to_rope % n) (B.ident_typ % ty);
+        List.iter (fun i->Format.eprintf "[%s] "(B.ident_exp%i)) inputs;
+        Format.eprintf "==> ";
+        List.iter (fun o->Format.eprintf "[%s] "(B.ident_pat%o)) outputs; 
+        Format.eprintf "\n";
+        print_code c
+      | RETURN returns -> 
+        Format.eprintf "RETURN ";
+        List.iter (fun exp -> Format.eprintf "[%s] " (B.ident_exp % exp)) returns;
+        Format.eprintf "\n"
+    in
+    print_code code;
+    Format.eprintf "--END CODE\n\n";
+    Format.pp_print_flush Format.err_formatter ()
+  in
+  Nfmap.iter (fun rel (_ty, modes) ->
+    Format.eprintf "### RELATION : %s\n" (Name.to_rope % rel);
+    List.iter (fun (n, mode, _ty, rules) ->
+      Format.eprintf "# %s : " (Name.to_rope % n);
+      List.iter (function
+        | I -> Format.eprintf "I"
+        | O -> Format.eprintf "O"
+      ) mode;
+      Format.eprintf "\n\n";
+      List.iter print_compiled rules;
+      Format.eprintf "\n\n\n"
+    ) modes;
+    Format.eprintf "-------------------------------------\n"
+  ) trans
+*)
+
+let sep_no_skips l = Seplist.from_list_default None l
+
+(*
+module Compile_pure_code = struct
+(* TODO : not correct (must check excluded & renames) *)
+(* TODO : parametrize w/ a monad or something *)
+let rec compile_code env excluded renames = function
+  | RETURN(exps) -> mk_tup Ast.Unknown None (sep_no_skips exps) None None
+  | IF(cond, code) -> 
+    let subexp = compile_code env excluded renames code in 
+    let undef = mk_undefined_exp Ast.Unknown "Undef" (exp_to_typ subexp) in
+    mk_if_exp Ast.Unknown cond subexp undef
+  | IFEQ(e1,e2,code) ->
+    let subexp = compile_code env excluded renames code in
+    let undef = mk_undefined_exp Ast.Unknown "Undef" (exp_to_typ subexp) in
+    let cond = mk_eq_exp env e1 e2 in
+    mk_if_exp Ast.Unknown cond subexp undef
+  | CALL(n, ty, inp, outp, code) ->
+    let subexp = compile_code env excluded renames code in
+    let undef = mk_undefined_exp Ast.Unknown "Undef" (exp_to_typ subexp) in
+    let call = List.fold_left (fun func arg -> mk_app Ast.Unknown func arg None) 
+      (mk_var Ast.Unknown (Name.add_lskip n) ty) inp in
+    let pat = mk_ptup Ast.Unknown None (sep_no_skips outp) None None in
+    mk_case_exp false Ast.Unknown call
+      [(pat, subexp);
+       (mk_pwild Ast.Unknown None (exp_to_typ call),undef)] 
+      (exp_to_typ subexp)
+
+let compile_rule env (patterns, code) = 
+  let pattern = mk_ptup Ast.Unknown None (sep_no_skips patterns) None None in
+  let lemcode = compile_code env Nset.empty Nfmap.empty code in
+  (pattern, lemcode) 
+
+
+(* TODO : check overlap *)
+let compile_to_typed_ast env prog =
+  let funcs = Nfmap.fold (fun l _ (_ty,funcs) -> 
+    (List.map (fun (name, _, _, _) -> name) funcs)@l) [] prog in
+  let fun_names = List.fold_right Nset.add funcs Nset.empty in
+  let defs = Nfmap.map (fun _rel (ty,modes) ->
+    List.map (fun (n, mode, mty, rules) ->
+      let gen_name = make_namegen fun_names in
+      let vars = map_filter (function 
+        | (I, ty) -> Some(Name.add_lskip (gen_name (Ulib.Text.of_latin1 "input")),
+                          ty)
+        | (O, _) -> None
+      ) (List.combine mode ty) in
+      let tuple_of_vars = mk_tup Ast.Unknown None (sep_no_skips (List.map (fun (var,ty) -> mk_var Ast.Unknown var ty) vars)) None None in
+      let pats_of_vars = List.map (fun (var,ty) -> mk_pvar Ast.Unknown var ty) vars in
+      let cases = List.map (compile_rule env) rules in
+      let output_type = {t=Ttup(map_filter (function (O,ty) -> Some ty | _ -> None) (List.combine mode ty))} in
+      let case = mk_case_exp false Ast.Unknown tuple_of_vars cases output_type in
+      let annot = { term = Name.add_lskip n;
+                    locn = Ast.Unknown;
+                    typ = mty;
+                    rest = () } in
+      (annot, pats_of_vars, None, None, case)
+    ) modes 
+  ) prog in
+  let defs = sep_no_skips (Nfmap.fold (fun l _ c -> c@l) [] defs) in
+  ((Val_def(Rec_def(None,None,None,defs), Types.TNset.empty, []), None), 
+   Ast.Unknown)
+
+
+let ty_from_mode ty mode = 
+  let open Types in
+  let inputs = map_filter id (
+    List.map2 (fun ty mode -> if mode = I then Some(ty) else None) ty mode) in
+  let outputs = map_filter id (
+    List.map2 (fun ty mode -> if mode = O then Some(ty) else None) ty mode) in
+  let ret = {t=Ttup(outputs)} in
+  List.fold_left (fun ret arg -> {t=Tfn(arg,ret)}) (ret) 
+    (List.rev inputs)
+
+
+end
+
+module Compile_option_code = struct
+
+  open LemOptionMonad
+
+(* TODO : not correct (must check excluded & renames) *)
+(* TODO : parametrize w/ a monad or something *)
+let rec compile_code env excluded renames = function
+  | RETURN(exps) -> mk_some env (mk_tup Ast.Unknown None (sep_no_skips exps) None None)
+  | IF(cond, code) -> 
+    let subexp = compile_code env excluded renames code in 
+    mk_cond env cond subexp
+  | IFEQ(e1,e2,code) ->
+    let subexp = compile_code env excluded renames code in
+    let cond = mk_eq_exp env e1 e2 in
+    mk_cond env cond subexp
+  | CALL(n, ty, inp, outp, code) ->
+    let subexp = compile_code env excluded renames code in
+    let call = List.fold_left (fun func arg -> mk_app Ast.Unknown func arg None) 
+      (mk_var Ast.Unknown (Name.add_lskip n) ty) inp in
+    let pat = mk_ptup Ast.Unknown None (sep_no_skips outp) None None in
+    mk_bind env call pat subexp
+
+let compile_rule env (patterns, code) = 
+  let pattern = mk_ptup Ast.Unknown None (sep_no_skips patterns) None None in
+  let lemcode = compile_code env Nset.empty Nfmap.empty code in
+  (pattern, lemcode) 
+
+
+
+(* TODO : check overlap *)
+let compile_to_typed_ast env prog =
+  let funcs = Nfmap.fold (fun l _ (_ty,funcs) -> 
+    (List.map (fun (name, _, _, _) -> name) funcs)@l) [] prog in
+  let fun_names = List.fold_right Nset.add funcs Nset.empty in
+  let defs = Nfmap.map (fun _rel (ty,modes) ->
+    List.map (fun (n, mode, mty, rules) ->
+      let gen_name = make_namegen fun_names in
+      let vars = map_filter (function 
+        | (I, ty) -> Some(Name.add_lskip (gen_name (Ulib.Text.of_latin1 "input")),
+                          ty)
+        | (O, _) -> None
+      ) (List.combine mode ty) in
+      let tuple_of_vars = mk_tup Ast.Unknown None (sep_no_skips (List.map (fun (var,ty) -> mk_var Ast.Unknown var ty) vars)) None None in
+      let pats_of_vars = List.map (fun (var,ty) -> mk_pvar Ast.Unknown var ty) vars in
+      let cases = List.map (compile_rule env) rules in
+      let output_type = {t=Ttup(map_filter (function (O,ty) -> Some ty | _ -> None) (List.combine mode ty))} in
+      let lastcase = (mk_pwild Ast.Unknown None (exp_to_typ tuple_of_vars), 
+                      mk_none env output_type) in
+      let case = mk_case_exp false Ast.Unknown tuple_of_vars 
+        (cases @ [lastcase])  (mk_option output_type) in
+      let annot = { term = Name.add_lskip n;
+                    locn = Ast.Unknown;
+                    typ = mty;
+                    rest = () } in
+      (annot, pats_of_vars, None, None, case)
+    ) modes 
+  ) prog in
+  let defs = sep_no_skips (Nfmap.fold (fun l _ c -> c@l) [] defs) in
+  ((Val_def(Rec_def(None,None,None,defs), Types.TNset.empty, []), None), 
+   Ast.Unknown)
+
+
+let ty_from_mode ty mode = 
+  let open Types in
+  let inputs = map_filter id (
+    List.map2 (fun ty mode -> if mode = I then Some(ty) else None) ty mode) in
+  let outputs = map_filter id (
+    List.map2 (fun ty mode -> if mode = O then Some(ty) else None) ty mode) in
+  let ret = {t=Ttup(outputs)} in
+  List.fold_left (fun ret arg -> {t=Tfn(arg,ret)}) (mk_option ret) 
+    (List.rev inputs)
+
+end
+*)
+
+
+module Compile_list_code = struct
+
+(* XXX *)
+let remove_list ty = 
+  match ty.t with
+    | Types.Tapp([ty], _) -> ty
+    | _ -> failwith "???"
+
+let mk_list_map env fn lst = 
+  let l = Ast.Trans ("mk_list_map", None) in
+  match (exp_to_typ fn).t with
+    | Types.Tfn(a,b) ->
+      mk_app l (mk_app l (mk_const_exp env l ["List"] "map" [a;b]) fn None) lst None
+    | _ -> failwith "???"
+
+let mk_list_concat env lst = 
+  let t = remove_list (remove_list (exp_to_typ lst)) in
+  let l = Ast.Trans ("mk_list_concat", None) in
+  mk_app l (mk_const_exp env l ["List"] "concat" [t]) lst None
+
+let mk_bind env call pat code = 
+  let l = Ast.Trans ("mk_bind", None) in
+  let namegen = make_namegen (Nfmap.domain (exp_to_free code)) in
+  let var = Name.add_lskip (namegen (Ulib.Text.of_latin1 "x")) in
+  let inty = pat.typ in 
+  let fn = mk_fun l None [mk_pvar l var inty] None 
+    (mk_case_exp false l (mk_var l var inty) 
+    [(pat, code);
+     (mk_pwild l None inty, mk_list l None (sep_no_skips []) None (exp_to_typ code))
+    ] (exp_to_typ code)) None in
+  mk_list_concat env (mk_list_map env fn call)
+
+let mk_cond env cond code = 
+  let l = Ast.Trans ("mk_cond", None) in
+  mk_if_exp l cond code (mk_list l None (sep_no_skips []) None (exp_to_typ code))
+
+
+let rec compile_code env excluded renames code = 
+  let l = Ast.Trans ("compile_code", None) in
+  match code with
+  | RETURN(exps) -> 
+    let ret = mk_tup l None (sep_no_skips exps) None None in
+    mk_list l None (sep_no_skips [ret]) None (mk_list_type (exp_to_typ ret))
+  | IF(cond, code) -> 
+    let subexp = compile_code env excluded renames code in 
+    mk_cond env cond subexp
+  | IFEQ(e1,e2,code) ->
+    let subexp = compile_code env excluded renames code in
+    let cond = mk_eq_exp env e1 e2 in
+    mk_cond env cond subexp
+  | CALL(n, inp, outp, code) ->
+    let subexp = compile_code env excluded renames code in
+    let func = match n with 
+      | Left(n,ty) -> mk_var l (Name.add_lskip n) ty 
+      | Right(path) -> mk_const_from_path env l path []
+    in
+    let call = List.fold_left (fun func arg -> mk_app l func arg None) 
+      func inp in
+    let pat = mk_ptup l None (sep_no_skips outp) None None in
+    mk_bind env call pat subexp
+
+let compile_rule env (patterns, code) = 
+  let pattern = mk_ptup (Ast.Trans("compile_rule", None)) None (sep_no_skips patterns) None None in
+  let lemcode = compile_code env Nset.empty Nfmap.empty code in
+  (pattern, lemcode) 
+
+
+
+(* TODO : check overlap *)
+let compile_to_typed_ast env localenv prog =
+  let l = Ast.Trans ("compile_to_typed_ast", None) in
+  let funcs = Nfmap.fold (fun l _ (_,funcs) -> 
+    (List.map (fun (name, _, _, _) -> name) funcs)@l) [] prog in
+  let fun_names = List.fold_right Nset.add funcs Nset.empty in
+  let defs = Nfmap.map (fun _rel (reldescr, modes) ->
+    List.map (fun (n, mode, mty, rules) ->
+      let gen_name = make_namegen fun_names in
+      let vars = List.map 
+        (fun ty -> Name.add_lskip (gen_name (Ulib.Text.of_latin1 "input")), ty)
+        (in_tys_from_mode env reldescr mode) in
+      let tuple_of_vars = mk_tup l None (sep_no_skips (List.map (fun (var,ty) -> mk_var Ast.Unknown var ty) vars)) None None in
+      let pats_of_vars = List.map (fun (var,ty) -> mk_pvar l var ty) vars in
+      let cases = List.map (compile_rule env) rules in
+      let output_type = out_ty_from_mode env localenv reldescr mode in
+      (* Generate a list of binds and concat them ! *)
+      let bcases = List.map 
+        (fun (pat,code) -> 
+          mk_bind env 
+            (mk_list l None (sep_no_skips [tuple_of_vars]) None (mk_list_type (exp_to_typ tuple_of_vars))) 
+            pat code)
+        cases in
+      let body = mk_list_concat env (mk_list l None (sep_no_skips bcases)
+                                       None (mk_list_type output_type)) in
+      let annot = { term = Name.add_lskip n;
+                    locn = l;
+                    typ = mty;
+                    rest = () } in
+      (annot, pats_of_vars, None, None, body)
+    ) modes 
+  ) prog in
+  let defs = sep_no_skips (Nfmap.fold (fun l _ c -> c@l) [] defs) in
+  ((Val_def(Rec_def(None,None,None,defs), Types.TNset.empty, []), None), l)
+
+end
+
+open Typecheck_ctxt
+
+
+let gen_consname relname = Name.from_string (Name.to_string relname ^ "_witness")
+
+let mk_name_l n = (Name.add_lskip n , Ast.Unknown)
+
+let make_typedef tds =
+  let tds = Nfmap.fold (fun l _ td -> td::l) [] tds in
+  let make_cons (_crule, cname, cargs) = 
+    (mk_name_l cname, None, sep_no_skips (List.map snd cargs))
+  in
+  let make_def (tname,tconses) =
+    let texp = Te_variant(None, sep_no_skips (List.map make_cons tconses)) in
+    (mk_name_l tname, [], texp, None)
+  in
+  Type_def(None, sep_no_skips (List.map make_def tds))
+
+let register_types ctxt mod_path tds = 
+  Nfmap.fold (fun ctxt relname (tname, tconses) ->
+    (* Register a type constructor *)
+    let type_path = Path.mk_path mod_path tname in
+    let l = Ast.Unknown in
+    let () =
+      match Nfmap.apply ctxt.new_defs.p_env tname with
+        | None -> ()
+        | Some(p, _) ->
+          begin
+            match Pfmap.apply ctxt.all_tdefs p with
+              | None -> assert false
+              | Some(Tc_type _) ->
+                raise_error l "duplicate type constructor definition"
+                  Name.pp tname
+              | Some(Tc_class _) ->
+                raise_error l "type constructor already defined as a type class" 
+                  Name.pp tname
+          end
+    in
+    let ctxt = ctxt_add (fun x -> x.p_env) (fun x y -> { x with p_env = y })
+      ctxt (tname, (type_path,l)) in
+    let ctxt = add_d_to_ctxt ctxt type_path (Tc_type([],None,None)) in
+    (* Register the value constructors FIXME *)
+    let cnames = List.fold_left (fun s (_,cname,_) -> NameSet.add cname s) 
+      NameSet.empty tconses in
+    let mk_descr cname cargs =
+        {
+                constr_binding = Path.mk_path mod_path cname;
+                constr_tparams = [];
+                constr_args = List.map fst cargs;
+                constr_tconstr = type_path;
+                constr_names = cnames;
+                constr_l = Ast.Unknown
+        } 
+    in
+    let cdescrs = Nfmap.from_list 
+      (List.map (fun (crule, cname, cargs) -> (cname, mk_descr cname cargs)) tconses) in
+    let rule_to_constr = Nfmap.from_list 
+      (List.map (fun (crule, cname, cargs) -> (crule, mk_descr cname cargs)) tconses) in
+    let ctxt = ctxt_add (fun x -> x.r_env) (fun x y -> { x with r_env = y })
+      ctxt (relname, { ri_witness = Some(type_path, rule_to_constr); ri_check = None; ri_fns = [] }) in
+    List.fold_left (fun ctxt (crule, cname, cargs) ->
+      let () = 
+        match Nfmap.apply ctxt.new_defs.v_env cname with
+          | None -> ()
+          | Some(Constr _) ->
+            raise_error l "duplicate constructor definition"
+              Name.pp cname
+          | Some(Val(c)) ->
+            begin
+              match c.env_tag with
+                | K_method|K_instance ->
+                  raise_error l "constructor already defined as a class method name"
+                    Name.pp cname
+                | K_val | K_let | K_target _ ->
+                  raise_error l "constructor already defined as a top-level variable binding" 
+                    Name.pp cname
+            end
+      in
+      ctxt_add (fun x -> x.v_env) (fun x y -> { x with v_env = y }) 
+        ctxt (cname, Constr(mk_descr cname cargs))
+    ) ctxt tconses
+  ) ctxt tds 
+
+let rec path_lookup (e : env) (mp : Name.t list) : env option = 
+  match mp with
+    | [] -> Some(e)
+    | n::ns ->
+        match Nfmap.apply e.m_env n with
+          | None -> None
+          | Some(e) -> path_lookup e.mod_env ns
+
+(* TODO : || -> either, && -> *, forall -> (->), exists -> ... *)
+(* TODO : remove this get_typepath_from_rel nonsense *)
+let gen_witness_type_aux env get_typepath_from_rel names rules = 
+  let rels = get_rels names rules in
+  let reltypes = Nfmap.fold (fun reltypes relname reldescr ->
+    match get_typepath_from_rel relname reldescr with
+      | None -> reltypes
+      | Some(ty) -> Nfmap.insert reltypes (relname, ty)
+  ) Nfmap.empty rels in
+  (* We want to return a type here *)
+  let is_relation e = match exp_to_term e with
+    | Var v ->
+      begin match Nfmap.apply reltypes (Name.strip_lskip v) with
+        | None -> None
+        | Some tn -> Some tn
+      end
+    | Constant c -> 
+      let (mpath, n) = Path.to_name_list c.descr.const_binding in
+      begin match path_lookup env mpath with
+        | Some(env) -> 
+          begin match Nfmap.apply env.r_env n with
+            | None -> None
+            | Some { ri_witness = None } ->
+              raise_error Ast.Unknown "no witness for relation"
+                Path.pp c.descr.const_binding 
+            | Some { ri_witness = Some(tn,_) } -> 
+              let t = {t=Tapp([],tn)} in
+              Some(t, t_to_src_t t) 
+          end
+        | None -> failwith "Impossible"
+      end
+    | _ -> None
+  in
+  let tds = Nfmap.fold (fun tds relname reldescr ->
+    match reldescr.rel_witness with
+      | None -> tds
+      | Some(typename) ->
+        let constructors = List.map (fun rule  ->
+          let consname = gen_consname rule.rule_name in
+          let vars_ty = List.map (fun x -> (snd x,t_to_src_t (snd x))) rule.rule_vars in
+          let conds_ty = map_filter 
+            (fun cond -> is_relation (fst (split_app cond))) rule.rule_conds in
+          let argstypes = vars_ty @ conds_ty in
+          (rule.rule_name, consname, argstypes)
+        ) reldescr.rel_rules in
+        Nfmap.insert tds (relname, (typename, constructors))
+  ) Nfmap.empty rels in
+  tds
+
+let clean_src_app p = 
+  let t = {t=Tapp([],p)} in
+  let tn = snd (Path.to_name_list p) in
+  let ident = Ident.mk_ident [] (Name.add_lskip tn) Ast.Unknown in
+  let pid = {
+    id_path = Id_some ident;
+    id_locn = Ast.Unknown;
+    descr = p;
+    instantiation = []
+  } in
+  let loc = Ast.Trans("clean_src_app", None) in
+  (t, mk_tapp loc pid [] (Some t) (* t_to_src_t t *))
+
+let gen_witness_type_info mod_path ctxt names rules = 
+  let tds = gen_witness_type_aux ctxt.cur_env 
+    (fun relname reldescr -> 
+      match reldescr.rel_witness with
+        | None -> None
+        | Some(tn) ->
+          let p = Path.mk_path mod_path tn in
+          Some(clean_src_app p)
+    ) 
+    names rules in
+  let newctxt = register_types ctxt mod_path tds in
+  newctxt
+
+let gen_witness_type_def env mpath localenv names rules =
+  let tds = gen_witness_type_aux env 
+    (fun relname _ -> 
+      match Nfmap.apply localenv.r_env relname with
+        | Some({ri_witness = Some(tn,_)}) -> Some(clean_src_app tn)
+        | _ -> None
+    )
+    names rules in
+  if Nfmap.is_empty tds then []
+  else [(make_typedef tds, None),  Ast.Unknown]
+
+let ctxt_mod update ctxt = 
+  { ctxt with
+    cur_env = update ctxt.cur_env;
+    new_defs = update ctxt.new_defs
+  }
+
+let gen_witness_check_info mod_path ctxt names rules =
+  let rels = get_rels names rules in
+  let defs = Nfmap.fold (fun defs relname reldescr ->
+    match reldescr.rel_check with
+      | None -> defs
+      | Some(check_name) -> 
+        let rules = reldescr.rel_rules in
+        let ret = List.map exp_to_typ (List.hd rules).rule_args in
+        let check_path = Path.mk_path mod_path check_name in
+        let witness_type = 
+          match Nfmap.apply ctxt.cur_env.r_env relname with
+            | Some({ri_witness = Some(witness_type,_)}) -> 
+              {t = Tapp([],witness_type)}
+            | _ -> raise_error Ast.Unknown 
+              "no witness for relation while generating witness-checking function"
+              Path.pp check_path
+        in
+        let check_type = {t=Tfn(witness_type, mk_option {t=Ttup(ret)})} in
+        Nfmap.insert defs (relname, (check_name, check_path, check_type))
+  ) Nfmap.empty rels in
+  (* Register the functions *)
+  Nfmap.fold (fun ctxt relname (cname,cpath,ctype) ->
+    let const_descr = {
+      const_binding = cpath;
+      const_tparams = [];
+      const_class = [];
+      const_ranges = [];
+      const_type = ctype;
+      env_tag = K_let;
+      spec_l = Ast.Unknown;
+      substitutions = Targetmap.empty
+    } in
+    let ctxt = ctxt_add (fun x -> x.v_env) (fun x y -> {x with v_env = y})
+      ctxt (cname, Val(const_descr)) in
+    ctxt_mod (fun x -> {x with r_env = let Some r_info = Nfmap.apply x.r_env relname in Nfmap.insert x.r_env (relname, {r_info with ri_check = Some cpath})}) ctxt
+  ) ctxt defs
+
+let nset_of_list l = List.fold_left (fun set x -> Nset.add x set) Nset.empty l
+
+open LemOptionMonad
+
+let rel_lookup env path = 
+  let (mpath, n) = Path.to_name_list path in
+  match path_lookup env mpath with
+    | None -> None
+    | Some(env) -> Nfmap.apply env.r_env n
+
+let gen_witness_check_def env mpath localenv names rules = 
+  let rels = get_rels names rules in
+  let localdefs = Nfmap.fold (fun localdefs relname rules ->
+    match Nfmap.apply localenv.r_env relname with
+      | Some({ri_witness = Some(witness_info); ri_check = Some(check_path)}) 
+        when rules.rel_check <> None ->
+        let (_,def_name) = Path.to_name_list check_path in
+         Nfmap.insert localdefs (relname,(def_name, witness_info,check_path, rules))
+      | _ -> localdefs
+  ) Nfmap.empty rels in
+  let defs = Nfmap.map (fun relname (def_name, (witness_path, witness_constrs), check_path, reldescr) ->
+    let rules = reldescr.rel_rules in
+    let witness_ty = {t=Tapp([],witness_path)} in
+    let pats = List.map (fun rule ->
+      (* Bad indices from get_witness_type_info, sorry *)
+      let Some(constr) = Nfmap.apply witness_constrs rule.rule_name in
+      (* THIS IS WRONG *)
+     (* (* If a var and a localdef share a name, we need to rename the var *)
+      let defvars = nset_of_list (Nfmap.fold (fun acc _ (v,_,_) -> v::acc) [] localdefs) in
+      let (vars,conds,args) = do_what_i_mean in
+      let excludevars = List.map snd vars @
+        Nfmap.fold (fun acc _ (v,_,_) -> v::acc) [] localdefs in
+      let excludevars = List.fold_right Nset.add excludevars Nset.empty in *)
+      let gen_name = make_namegen Nset.empty in
+      (* Travailler sur les conds *)
+      let is_rel_or_aux e = 
+        let (head, args) = split_app e in
+        match exp_to_term head with
+          | Var v ->
+            (* TODO : factorisation *)
+            let n = Name.strip_lskip v in
+            begin match Nfmap.apply localenv.r_env n with
+              | None -> Right e
+              (* TODO : adjust ids for local things *)
+              | Some {ri_check = Some(check_path);
+                      ri_witness = Some(witness_path, witness_constrs)} ->
+                let check_exp = match Nfmap.apply localdefs n with
+                  | Some(def_name,_,_,_) -> 
+                    let witness_ty = {t=Tapp([],witness_path)} in
+                    let out_ty = mk_option {t=Ttup(List.map exp_to_typ args)} in
+                    mk_var Ast.Unknown (Name.add_lskip def_name) {t=Tfn(witness_ty, out_ty)}
+                  | None -> mk_const_from_path env Ast.Unknown check_path []
+                in
+                Left(args, witness_path, check_exp)
+              | Some _ ->
+                raise_error Ast.Unknown "no witness checking function for relation"
+                  Path.pp check_path
+            end
+          | Constant c ->
+            begin match rel_lookup env c.descr.const_binding with
+              | None -> Right e
+              | Some { ri_witness = Some(witness_path, _);
+                           ri_check = Some(check_path) } ->
+                    let check_exp = mk_const_from_path env Ast.Unknown check_path [] in
+                    Left (args, witness_path, check_exp)
+              | Some _ -> 
+                raise_error Ast.Unknown "no witness checking function for relation"
+                  Path.pp check_path
+            end
+          | _ -> Right e
+      in    
+      let (relconds,auxconds) = map_partition is_rel_or_aux rule.rule_conds in
+      let relconds = List.map (fun (args,witness_path,check_exp) ->
+        let witness_ty = {t=Tapp([],witness_path)} in
+        let witness_name = gen_name (Ulib.Text.of_latin1 "witness") in
+        (args, witness_ty, check_exp, witness_name)
+      ) relconds in
+      let pvars = List.map 
+        (fun (var,typ) -> mk_pvar Ast.Unknown (Name.add_lskip var) typ) rule.rule_vars in
+      let pconds = List.map
+        (fun (_,witness_ty,_,var) -> 
+          mk_pvar Ast.Unknown (Name.add_lskip var) witness_ty
+        ) relconds in
+      let constr_id = { id_path = Id_none None;
+                        id_locn = Ast.Unknown;
+                        descr = constr;
+                        instantiation = [] } in
+      let pattern = mk_pconstr Ast.Unknown constr_id (pvars @ pconds) None in
+      let ret = mk_some env 
+        (mk_tup Ast.Unknown None (sep_no_skips rule.rule_args) None None) in
+      let genconds_exps = List.map (fun (args,witness_ty,check_fun,witness) ->
+        let witness_var = mk_var Ast.Unknown (Name.add_lskip witness) witness_ty in
+        let rhs = mk_some env (mk_tup Ast.Unknown None (sep_no_skips args) None None) in
+        let lhs = mk_app Ast.Unknown check_fun witness_var None in
+        mk_eq_exp env rhs lhs
+      ) relconds in
+      let ifconds = auxconds @ genconds_exps in
+      let lit_true = mk_lit Ast.Unknown ({term=L_true(None); locn = Ast.Unknown;
+                                          typ={t=Tapp([],Path.boolpath)};
+                                          rest=()}) None in
+      let cond = List.fold_left (mk_and_exp env) lit_true ifconds in
+      let code = mk_if_exp Ast.Unknown cond ret (mk_none env (remove_option (exp_to_typ ret))) in
+      (pattern, code)
+    ) rules in
+    let x = Name.add_lskip (make_namegen Nset.empty (Ulib.Text.of_latin1 "x")) in
+    let xpat = mk_pvar Ast.Unknown x witness_ty in
+    let xvar = mk_var Ast.Unknown x witness_ty in
+    let return_ty = exp_to_typ (snd (List.hd pats))  in
+    let body = mk_case_exp false Ast.Unknown xvar pats return_ty in
+    let annot = { term = Name.add_lskip def_name;
+                  locn = Ast.Unknown;
+                  typ = {t=Tfn(witness_ty,return_ty)};
+                  rest = () } in
+    (annot, [xpat], None, None, body)
+  ) localdefs in
+  let defs = Nfmap.fold (fun l _ v -> v::l) [] defs in
+  let def = Rec_def(None,None,None,sep_no_skips defs) in
+  if defs = [] then []
+  else [((Val_def(def, Types.TNset.empty, []), None), Ast.Unknown)]
+
+(* Rec_def of lskips * sips * targtets_opt * funcl_aux lskips_seplist 
+and funcl_aux = name_lskips_annot * pat list * (lskips * src_t) option * lskips * exp
+*)
+
+let gen_fns_info mod_path (ctxt : defn_ctxt) names rules =
+  let rels = get_rels names rules in
+  Nfmap.fold (fun ctxt relname reldescr ->
+    List.fold_left (fun ctxt (name, (mode, wit)) ->
+      let ty = ty_from_mode ctxt.cur_env ctxt.cur_env reldescr (mode, wit) in
+      let path = Path.mk_path mod_path name in
+      let ctxt = ctxt_mod (fun x -> {x with r_env =
+          Nfmap.insert x.r_env 
+            (relname, 
+             let info = match Nfmap.apply x.r_env relname with
+              | Some y -> y
+              | None -> { ri_witness = None; ri_check = None; ri_fns = [] } in
+             {info with ri_fns = ((mode, wit), path)::info.ri_fns})}) ctxt in
+      let const_descr = {
+        const_binding = path;
+        const_tparams = [];
+        const_class = [];
+        const_ranges = [];
+        const_type = ty;
+        env_tag = K_let;
+        spec_l = Ast.Unknown;
+        substitutions = Targetmap.empty
+      } in
+      ctxt_add (fun x -> x.v_env) (fun x y -> {x with v_env = y})
+        ctxt (name, Val(const_descr))
+    ) ctxt reldescr.rel_indfns
+  ) ctxt rels
+
+let transform_rule env localenv localrels (mode, need_wit) rel (rule : ruledescr) = 
+  let vars = Nfmap.domain (Nfmap.from_list rule.rule_vars) in
+  let avoid = Nfmap.fold (fun avoid relname reldescr ->
+    List.fold_left (fun avoid (funname, _) -> Nset.add funname avoid)
+      (Nset.add relname avoid) reldescr.rel_indfns
+  ) Nset.empty localrels in
+  let gen_rn = make_renamer vars avoid in
+  let (patterns, initknown, initeqs) = 
+    convert_output gen_rn rule.rule_args (List.map (fun x -> x = O) mode) in
+  (* TODO : generate better names *)
+  let gen_witness_name = 
+    let gen = make_namegen Nset.empty in
+    fun () -> gen (Ulib.Text.of_latin1 "witness") in
+  let gen_witness_var relinfo =
+    match relinfo.ri_witness with
+      | None -> None
+      | Some(t,_) -> Some(gen_witness_name (), {t=Tapp([],t)})
+  in
+  let (indconds, sideconds) = 
+    map_partition (fun x ->
+      let (e,args) = split_app x in
+      match exp_to_term e with
+        | Var n ->
+          begin match Nfmap.apply localrels (Name.strip_lskip n) with
+            | Some(rel) ->
+              let modes = List.map (fun (name, mode) -> (mode, Left(name,ty_from_mode env localenv rel mode))) rel.rel_indfns in
+              let Some(relinfo) = Nfmap.apply localenv.r_env rel.rel_name in
+              Left(modes,args,gen_witness_var relinfo)
+            | None -> Right(x)
+          end
+        | Constant c ->
+          begin match rel_lookup env c.descr.const_binding with
+            | Some(relinfo) ->
+              Left(List.map (fun (mode,path) -> (mode, Right(path))) relinfo.ri_fns,args,gen_witness_var relinfo)
+            | None -> Right(x)
+          end
+        | _ -> Right(x)
+    ) rule.rule_conds
+  in
+  (* map_filter drops relations with no witnesses.
+     it's not a problem because if our relation has a witness, all these
+     relations must have one *)
+  let witness_var_order = map_filter (fun (_,_,var) -> var) indconds in
+  let returns = map_filter (function
+    | (I, _) -> None
+    | (O, r) -> Some(r)
+  ) (List.map2 (fun x y -> (x,y)) mode rule.rule_args) in
+  let returns = 
+    if not need_wit then returns
+    else
+      let Some(rel_info) = Nfmap.apply localenv.r_env rel.rel_name in
+      let Some(_, wit_constrs) = rel_info.ri_witness in
+      let Some(constr_descr) = Nfmap.apply wit_constrs rule.rule_name in
+      let args = rule.rule_vars @ witness_var_order in
+      let args = List.map 
+        (fun (name,ty) -> mk_var Ast.Unknown (Name.add_lskip name) ty) args in
+      let constr_id = {id_path = Id_none None; id_locn = Ast.Unknown;
+                       descr = constr_descr; instantiation = []} in
+      let constr = mk_constr Ast.Unknown constr_id None in
+      let wit = List.fold_left (fun u v -> mk_app Ast.Unknown u v None) constr args in
+      returns@[wit]
+  in
+  let rec build_code known indconds sideconds eqconds =
+    let exp_known e = Nfmap.fold (fun b v _ -> b && Nset.mem v known) 
+      true (C.exp_to_free e) in
+    let (selected_eqs,eqconds2) = 
+      List.partition (fun (e1,e2) -> exp_known e1 && exp_known e2) eqconds in
+    let (selected_side,sideconds2) = 
+      List.partition (fun e -> exp_known e) sideconds in
+    let add_eq eq x = List.fold_left (fun x (e1,e2) -> IFEQ(e1,e2,x)) x eq in
+    let add_side side x = List.fold_left (fun x e -> IF(e,x)) x side in 
+    let rec search notok = function
+      | [] ->
+        begin match eqconds2,sideconds2 with
+          | [], [] when notok = [] -> RETURN returns
+          | _ -> report_no_translation rule notok eqconds2 sideconds2
+        end
+      | (modes,args,wit_var) as c::cs ->
+        let inargs = List.map exp_known args in
+        let mode_matches ((fun_mode, fun_wit),_info) = 
+          List.for_all (fun x -> x)
+            (List.map2 (fun inp m -> inp || m = O) inargs fun_mode)
+            && (not need_wit || fun_wit) in
+        match List.filter mode_matches modes with
+          | [] -> search (c::notok) cs
+          | ((fun_mode, fun_wit), fun_info) ::ms -> 
+            (* Still some work to do to generate witnesses *)
+            let (outputs, bound, equalities) = convert_output gen_rn args 
+              (List.map (fun m -> m = I) mode) in
+            let outputs = 
+              if not fun_wit
+              then outputs
+              else
+                let Some(wit_name, wit_ty) = wit_var in
+                outputs@[mk_pvar Ast.Unknown (Name.add_lskip wit_name) wit_ty]
+            in
+            let inputs = map_filter id (List.map2 (fun exp m ->
+              match m with
+                | I -> Some(exp)
+                | O -> None
+            ) args mode) in
+            CALL(fun_info, inputs, outputs,
+                 build_code (Nset.union bound known) (cs@notok) 
+                   sideconds2 (equalities@eqconds2))
+    in
+    add_eq selected_eqs (add_side selected_side (search [] indconds))
+  in
+  (patterns, build_code initknown indconds sideconds initeqs)
+
+
+let transform_rules env localenv localrels (mode, wit) reldescr =
+  List.map (transform_rule env localenv localrels (mode,wit) reldescr) reldescr.rel_rules
+
+let gen_fns_def env mpath localenv names rules =
+  let rels = get_rels names rules in
+  let transformed_rules = Nfmap.map (fun relname reldescr ->
+    (reldescr, List.map (fun (name, mode) ->
+      (name, mode, ty_from_mode env localenv reldescr mode,transform_rules env localenv rels mode reldescr)
+    ) reldescr.rel_indfns)
+  ) rels in
+  let code = Compile_list_code.compile_to_typed_ast env localenv transformed_rules in
+  let emptydef = 
+    Nfmap.fold (fun b _ (_,l) -> b && [] = l) true transformed_rules in
+  if emptydef then []
+  else [code]
+
+let gen_witness_type_macro env mpath localenv def =
+  match def with
+    | (Indreln(x,y,names,rules),z), t ->
+      let remove_witness = 
+        function RName(a,b,c,d,_witness,f,g,h) ->
+          RName(a,b,c,d,None,f,g,h)
+      in
+      let def = (Indreln(x,y,Seplist.map remove_witness names, rules),z),t in
+      let tdefs = gen_witness_type_def env mpath localenv names rules in
+      if tdefs = []
+      then None
+      else Some(localenv, def::tdefs)
+    | _ -> None
+
+let gen_witness_check_macro env mpath localenv def_ =
+  match def_ with
+    | (Indreln(x,y,names,rules),z), t ->
+      let remove_check = 
+        function RName(a,b,c,d,e,_check,g,h) ->
+          (* TODO : preserve lskips *)
+          RName(a,b,c,d,e,None,g,h)
+      in
+      let def = (Indreln(x,y,Seplist.map remove_check names, rules),z),t in
+      let cdefs = gen_witness_check_def env mpath localenv names rules in
+      if cdefs = []
+      then None
+      else Some(localenv, def::cdefs)
+    | _ -> None
+
+
+let gen_fns_macro env mpath localenv def =
+  match def with
+    | (Indreln(x,y,names,rules),z), t ->
+      let remove_indfns = 
+        function RName(a,b,c,d,e,f,_indfns,h) ->
+          RName(a,b,c,d,e,f,None,h)
+      in
+      let def = (Indreln(x,y,Seplist.map remove_indfns names, rules),z),t in
+      let fdefs = gen_fns_def env mpath localenv names rules in
+      if fdefs = []
+      then None
+      else Some(localenv, def::fdefs)
+    | _ -> None
+
+end
+
+
+
+
+
+

src/coq_backend.ml

                 Output.flat [
                   ws skips; from_string "Require Import "; mod_name; from_string ".\n"
                 ]
-      | Indreln (skips, targets, cs) ->
+      | Indreln (skips, targets, names,cs) -> (*INDERL_TODO Only added the name declaration parameter here*)
           if in_target targets then
             let c = Seplist.to_list cs in
               clauses c
         let rec gather_names_aux buffer clauses =
           match clauses with
             | []    -> buffer
-            | (_, _, _, _, _, _, name_lskips_annot, _)::xs ->
+            | (Rule(_,_, _, _, _, _, _, name_lskips_annot, _))::xs ->
               let name = name_lskips_annot.term in
               let name = Name.strip_lskip name in
               if List.mem name buffer then
           gather_names_aux [] clause_list
       in