1. Peter_Sewell
  2. lem

Commits

Thomas Tuerk  committed b520f3e Merge with conflicts

Merge remote-tracking branch 'origin/master' into library-format

some manual merging was needed, this resulted into adding documentation, renaming and
reordering things. Especially the represention of inductive relations in typed_ast got
modified. Done by Thomas Williams and Thomas Tuerk

Conflicts:
src/ast.ml
src/backend.ml
src/coq_backend.ml
src/def_trans.ml
src/ident.ml
src/initial_env.ml
src/macro_expander.ml
src/rename_top_level.ml
src/target_binding.ml
src/target_syntax.ml
src/target_trans.ml
src/typecheck.ml
src/typed_ast.ml
src/typed_ast.mli
src/typed_ast_syntax.ml

  • Participants
  • Parent commits 8c8169e, 1428b75
  • Branches master

Comments (0)

Files changed (23)

File language/lem.ott

View file
  • Ignore whitespace
   | 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

File language/lem.pdf

  • Ignore whitespace
Binary file modified.

File src/ast.ml

View file
  • Ignore whitespace
 
 
 type
-a = terminal * text
-
-
-type
 n = terminal * text
 
 
-type 
-id =  (* Long identifers *)
-   Id of ((x_l * terminal)) list * x_l * l
-
-
-type 
-a_l =  (* Location-annotated type variables *)
-   A_l of a * l
+type
+a = terminal * text
 
 
 type 
 
 
 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 
+id =  (* Long identifers *)
+   Id of ((x_l * terminal)) list * x_l * 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 
 lit_aux =  (* Literal constants *)
    L_true of terminal
  | L_false of terminal
 
 
 type 
-n_l =  (* Location-annotated numeric variables *)
-   N_l of n * l
-
-
-type 
-lit = 
-   Lit_l of lit_aux * l (* Location-annotated literal constants *)
+nexp_constraint =  (* Location-annotated Nexp range *)
+   Range_l of nexp_constraint_aux * l
 
 
 type 
-nexp_constraint_aux =  (* Whether a vector is bounded or fixed size *)
-   Fixed of nexp * terminal * nexp
- | Bounded of nexp * terminal * nexp
+c =  (* Typeclass constraints *)
+   C of id * tnvar
 
 
 type 
-tnvar =  (* Union of type variables and Nexp type variables, with locations *)
-   Avl of a_l
- | Nvl of n_l
+lit = 
+   Lit_l of lit_aux * l (* Location-annotated literal constants *)
 
 
 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 *)
+
+
+type 
 pat_aux =  (* Patterns *)
    P_wild of terminal (* Wildcards *)
  | P_as of terminal * pat * terminal * x_l * terminal (* Named patterns *)
 
 
 type 
-nexp_constraint =  (* Location-annotated Nexp range *)
-   Range_l of nexp_constraint_aux * l
-
-
-type 
-c =  (* Typeclass constraints *)
-   C of id * tnvar
-
-
-type 
 t =  (* Internal types *)
    T_var of a
  | T_fn of t * terminal * t
 
 
 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 
 target =  (* Backend target names *)
    Target_hol of terminal
  | Target_isa of terminal
 
 
 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 *)
+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 
+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 
-x_l_opt =  (* Optional name for inductively defined relation clauses *)
-   X_l_none
- | X_l_some of x_l * terminal
+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 
 
 
 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 *)
+rule_aux =  (* Inductively defined relation clauses *)
+   Rule of x_l * terminal * terminal * (name_t) list * terminal * exp * terminal * x_l * (exp) list
 
 
 type 
-rule_aux =  (* Inductively defined relation clauses *)
-   Rule of x_l_opt * terminal * (x_l) list * terminal * exp * terminal * x_l * (exp) list
+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 
 
 
 type 
-typschm =  (* Type schemes *)
-   Ts of c_pre * typ
-
-
-type 
 nec =  (* Numeric expression constraints *)
    Lessthan of ne * terminal * nec
  | Eq of ne * terminal * nec
 
 
 type 
+indreln_name =  (* Location-annotated name for inductively defined relations *)
+   Name_l of indreln_name_aux * l
+
+
+type 
 td =  (* Type definitions *)
    Td of x_l * tnvar list * name_opt * terminal * texp
  | Td_opaque of x_l * tnvar list * name_opt (* Definitions of opaque types *)
 
 
 type 
-defs =  (* Definition sequences *)
-   Defs of ((def * terminal * bool)) list
-
-and def_aux =  (* Top-level definitions *)
+def_aux =  (* Top-level definitions *)
    Type_def of terminal * (td * terminal) list (* Type definitions *)
  | Val_def of val_def (* Value definitions *)
  | Lemma of lemma_decl (* Lemmata *)
  | 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 *)
 and def =  (* Location-annotated definitions *)
    Def_l of def_aux * l
 
+and defs =  (* Definition sequences *)
+   Defs of ((def * terminal * bool)) list
+
+
+type 
+name_ts =  (* Names with optional types for inductively defined relation clauses *)
+   NameTs of (name_t) list
+
 
 type 
 semC =  (* Typeclass constraint lists *)

File src/backend.ml

View file
  • Ignore whitespace
   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, c, 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 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,name_ref,s2,(constraint_pre,t),witness,checks,functions,s3)) =
+  ws s1 ^
+  T.reln_name_start ^ 
+  (Name.to_output Term_method (B.const_ref_to_name name name_ref)) ^ 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, rname_ref, es),_) =
   (if T.reln_clause_show_name then (
-    (match name_opt with None -> emp | Some name ->
-      Name.to_output_quoted Term_method name ^
+    ((if T.reln_clause_quote_name then Name.to_output_quoted else Name.to_output) 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 Term_var n.term) qnames)) ^
+    flat (interspace (List.map (fun (QName n) -> Name.to_output Term_var n.term) qnames)) ^
     ws s2 ^ 
     kwd "."
   ) else emp) ^
   (match e_opt with None -> ws s3 | Some e -> 
      exp (if T.reln_clause_add_paren then Typed_ast_syntax.mk_opt_paren_exp e else e) ^ 
      ws s3 ^ kwd "==>") ^
-  Name.to_output Term_var rname.term ^
+  Name.to_output Term_var (B.const_ref_to_name rname.term rname_ref) ^
   flat (interspace (List.map exp es)) ^
   T.reln_clause_end
 
 
 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, c, _) ->
+  let (_, clauseL_filter) = List.fold_left (fun (ns, acc) (Rule(_,_, _, _, _, _, _, rname, c, _),_) ->
       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 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
     | [] -> false
       ws s ^
       T.module_open ^
       Ident.to_output Module_name T.path_sep (B.module_id_to_ident m)
-  | 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),n_ref,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 ^

File src/convert_relations.ml

View file
  • Ignore whitespace
+(* Converting a relation *)
+
+open Typed_ast
+open Types
+open Util
+open Typed_ast_syntax
+
+module Converter(C : Exp_context) = struct
+
+module C = Exps_in_context(C)
+open C
+
+module Nmap = Typed_ast.Nfmap
+module Nset = Nmap.S
+
+let loc_trans s l = Ast.Trans(s, Some(l))
+
+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
+
+(* Splits on infix (&&) : ((a && b) && (c && d)) && true -> [a;b;c;d] *)
+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;
+  rule_loc : Ast.l;
+} 
+
+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 * output_type)) list;
+  rel_rules : ruledescr list;
+  rel_loc : Ast.l;
+}
+
+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
+            | "output" -> O
+            | s -> raise (Invalid_argument ("to_in_out: "^s))
+          end
+        | _ -> raise (Invalid_argument "to_in_out")
+      end
+    | _ -> raise (Invalid_argument "to_in_out")
+
+let default_out_mode = Out_pure
+
+let rec src_t_to_mode (typ : src_t) : mode * bool * output_type =
+  match typ.term with
+    | Typ_paren(_,t,_) -> src_t_to_mode t
+    | Typ_fn(x1,_,x2) -> 
+      let (mode, wit, out) = src_t_to_mode x2 in
+      (to_in_out x1::mode, wit, out)
+    | Typ_app({id_path = p },args) ->
+      begin 
+        try ([to_in_out typ], false, default_out_mode)
+        with Invalid_argument _ -> 
+          begin match p with
+            | Id_some(i) ->
+              let n = Name.to_string (Name.strip_lskip (Ident.get_name i)) in
+              begin match n with 
+                | "unit" | "bool" -> ([], false, default_out_mode)
+                | "list" -> ([], args <> [], Out_list)
+                | "option" -> ([], args <> [], Out_option)
+                | "unique" -> ([], args <> [], Out_unique)
+                | _ -> ([], true, default_out_mode)
+              end
+            | _ -> 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 *)
+
+let get_rels (l : Ast.l) (names : indrel_name lskips_seplist) 
+    (rules: 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 = [];
+      rel_loc = l; 
+    } in
+    Nfmap.insert s (relname, descr)
+  ) Nfmap.empty (Seplist.to_list names) in
+  List.fold_left (fun s (Rule(rulename,_,_,vars,_,cond,_,rel,args),l) ->
+    let rulename = Name.strip_lskip rulename in
+    let relname = Name.strip_lskip rel.term in
+    let l' = loc_trans "get_rels" l in
+    let rulecond = match cond with
+      | Some x -> x
+      | None -> C.mk_lit l'
+        {term = L_true None; 
+         locn = l'; 
+         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;
+      rule_loc = l;
+    } in
+    match Nfmap.apply s relname with
+      | None -> failwith "Relation without description"
+      | Some rel -> Nfmap.insert s 
+        (relname, {rel with rel_rules = ruledescr::rel.rel_rules})
+  ) names (Seplist.to_list rules)
+
+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 l v typ =
+      let l = loc_trans "make_renamer" l in
+      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 l v typ,
+                             C.mk_var l v' typ) :: !equalities;
+              n'
+          in
+          used := Nset.add varname !used;
+          seen := Nset.add varname !seen;
+          Name.add_lskip varname
+        end
+    in
+    let transform_exp l e typ = 
+      let l = loc_trans "make_renamer" l in
+      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 l v typ, e) :: !equalities;
+      C.mk_pvar_annot l 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 = loc_trans "exp_to_pat" (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 loc 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 loc e ty
+      | _ -> Reporting.print_debug_exp "Untranslatable" [e]; transform_exp loc e ty
+  and exps_to_pats es = Seplist.map exp_to_pat es in
+  exp_to_pat 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 =
+  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 sep_no_skips l = Seplist.from_list_default None l
+
+let newline = Some([Ast.Nl])
+let space = Some([Ast.Ws(Ulib.Text.of_latin1 " ")])
+
+let sep_newline l = Seplist.from_list_default newline l
+
+let mk_pvar_ty l n t =
+  mk_ptyp l space (mk_pvar l n t) None (t_to_src_t t) None None
+
+module type COMPILATION_CONTEXT = sig
+  (* lem signature : type a -> type m a) *)
+  val mk_type : Types.t -> Types.t
+  val remove_type : Types.t -> Types.t
+
+  (* lem signature : type a -> exp m a *)
+  val mk_failure : Typed_ast.env -> Ast.l -> Types.t -> Typed_ast.exp
+
+  (* exp a -> exp m a *)
+  val mk_return : Typed_ast.env -> Ast.l -> Typed_ast.exp -> Typed_ast.exp
+
+  (* exp m a -> pat a -> exp m b -> exp m b *)
+  val mk_bind : Typed_ast.env -> Ast.l -> Typed_ast.exp -> Typed_ast.pat -> Typed_ast.exp -> Typed_ast.exp
+
+  (* exp bool -> exp m a -> exp m a *)
+  val mk_cond : Typed_ast.env -> Ast.l -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
+
+  (* type b -> exp a -> (exp a * exp m b) list -> m b *)
+  val mk_choice : Typed_ast.env -> Ast.l -> Types.t -> Typed_ast.exp ->
+    (Typed_ast.pat * Typed_ast.exp) list -> Typed_ast.exp
+end
+
+module Context_list : COMPILATION_CONTEXT = struct
+
+  let mk_type ty = 
+    { Types.t = Types.Tapp([ty], Path.listpath) }
+
+  let remove_type ty = 
+    match ty.t with
+      | Types.Tapp([ty], _) -> ty
+      | _ -> failwith "???"
+
+  let remove_list = remove_type
+
+  let mk_list_map env l fn lst = 
+    let l = loc_trans "mk_list_map" l 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 l lst = 
+    let t = remove_list (remove_list (exp_to_typ lst)) in
+    let l = loc_trans "mk_list_concat" l in
+    mk_app l (mk_const_exp env l ["List"] "concat" [t]) lst None
+
+  let mk_return env l e =
+    mk_list (loc_trans "mk_return" l) None (sep_no_skips [e]) None (mk_type (exp_to_typ e))
+
+  let mk_failure env l t = 
+    mk_list (loc_trans "mk_failure" l) None (sep_no_skips []) None (mk_type t)
+      
+  let mk_bind env l call pat code = 
+    let l = loc_trans "mk_bind" l 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 l (mk_list_map env l fn call)
+      
+  let mk_cond env l cond code = 
+    let l = loc_trans "mk_cond" l in
+    mk_if_exp l cond code (mk_list l None (sep_no_skips []) None (exp_to_typ code))
+
+  let mk_let env l pat v code = 
+    let l = loc_trans "mk_let" l in
+    mk_case_exp false l v
+      [(pat, code);
+       (mk_pwild l None pat.typ, mk_list l None (sep_no_skips []) None (exp_to_typ code))
+      ] (exp_to_typ code)
+
+  let mk_choice env l ty input pats = 
+    let l = loc_trans "mk_choice" l in
+    mk_list_concat env l
+      (mk_list l None (sep_newline (List.map (fun (pat, code) -> mk_let env l pat input code) pats)) None (mk_list_type (mk_list_type ty)))
+
+end
+
+module Context_pure : COMPILATION_CONTEXT = struct
+  let mk_type x = x
+  let remove_type x = x
+
+  let mk_return _ l e = e
+  let mk_failure _ l t = mk_undefined_exp (loc_trans "mk_undefined" l)
+    "Undef" t
+
+  let mk_bind _ l e pat code =
+    let l = loc_trans "mk_bind" l in
+    mk_case_exp false l e [(pat, code)] (exp_to_typ code)
+
+  let mk_cond env l cond code =
+    let l = loc_trans "mk_cond" l in
+    mk_if_exp l cond code (mk_failure env l (remove_type (exp_to_typ code)))
+
+  let mk_choice env l t v pats = 
+    let l = loc_trans "mk_choice" l in
+    (* Check pattern non-overlap & completeness or emit a warning *)
+    let props = Patterns.check_pat_list env (List.map fst pats) in
+    (match props with
+      | None -> failwith "Pattern matching compilation failed"
+      | Some(props) ->
+        if not props.Patterns.is_exhaustive
+        then Reporting.report_warning 
+          (Reporting.Warn_general(true, l, "non-exhaustive patterns in inductive relation"));
+        if props.Patterns.overlapping_pats <> []
+        then Reporting.report_warning
+          (Reporting.Warn_general(true, l, "overlapping patterns in inductive relation")));
+    mk_case_exp false l v pats (mk_type t)
+end
+
+(* TODO : merge with LemOptionMonad ? *)
+module Context_option_pre = struct
+
+  let mk_type ty = 
+    { Types.t = Types.Tapp([ty], mk_string_path ["Pervasives"] "option") } 
+
+  let remove_type ty = 
+    match ty.t with
+      | Types.Tapp([ty], _) -> ty
+      | _ -> failwith "???"
+
+  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_return env l e = mk_some env e
+
+  let mk_failure env l ty = mk_none env ty
+
+  let mk_bind env l call pat code = 
+    let l = loc_trans "mk_bind" l 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 l cond code = 
+    let l = loc_trans "mk_cond" l in
+    mk_if_exp l cond code (mk_none env (remove_option (exp_to_typ code)))
+
+end
+
+module Context_option : COMPILATION_CONTEXT = struct
+  include Context_option_pre
+
+  let mk_choice _ = failwith "Not implemented"
+end
+
+module Context_unique : COMPILATION_CONTEXT = struct
+  include Context_option_pre
+
+  let mk_choice _ = failwith "Not implemented"
+end
+
+let select_module = function
+  | Out_list -> (module Context_list : COMPILATION_CONTEXT)
+  | Out_pure -> (module Context_pure : COMPILATION_CONTEXT)
+  | Out_unique -> (module Context_unique : COMPILATION_CONTEXT)
+  | Out_option -> (module Context_option : COMPILATION_CONTEXT)
+
+let out_ty_from_mode env localenv reldescr (mode, wit, _out) = 
+  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
+  {t=Ttup(ret)}
+        
+let in_tys_from_mode env reldescr (mode, _wit, _out) = 
+  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 ((_,_,out) as mode) = 
+  let args = in_tys_from_mode env reldescr mode in
+  let ret = out_ty_from_mode env localenv reldescr mode in
+  let module M = (val select_module out : COMPILATION_CONTEXT) in
+  List.fold_right (fun a b -> {t=Tfn(a,b)}) args (M.mk_type ret)
+
+module Compile(M : COMPILATION_CONTEXT) = struct
+  
+  (* FIXME : renaming *)
+  let rec compile_code env loc code = 
+    let l = loc_trans "compile_code" loc in
+    match code with
+      | RETURN(exps) -> 
+        let ret = mk_tup l None (sep_no_skips exps) None None in
+        M.mk_return env l ret
+      | IF(cond, code) -> 
+        let subexp = compile_code env loc code in 
+        M.mk_cond env l cond subexp
+      | IFEQ(e1,e2,code) ->
+        let subexp = compile_code env loc code in
+        let cond = mk_eq_exp env e1 e2 in
+        M.mk_cond env l cond subexp
+      | CALL(n, inp, outp, code) ->
+        let subexp = compile_code env loc 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
+        M.mk_bind env l call pat subexp
+          
+  let compile_rule env (loc, patterns, code) = 
+    let pattern = mk_ptup (loc_trans "compile_rule" loc) None (sep_no_skips patterns) None None in
+    let lemcode = compile_code env loc code in
+    (pattern, lemcode) 
+
+  let compile_function env localenv fun_names reldescr (n,mode,mty,rules) : funcl_aux =
+    let l = loc_trans "compile_function" reldescr.rel_loc in 
+    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 l var ty) vars)) None None in
+    let pats_of_vars = List.map (fun (var,ty) -> mk_pvar_ty 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 body = M.mk_choice env l output_type tuple_of_vars cases in
+    let annot = { term = Name.add_lskip n;
+                  locn = l;
+                  typ = mty;
+                  rest = () } in
+    (annot, pats_of_vars, Some(space, t_to_src_t (M.mk_type output_type)), space, body)
+end
+
+let compile_function env localenv fun_names reldescr 
+    ((_,(_,_,out_mode),_,_) as m) = 
+  let module M = (* (val select_module out_mode) *) Context_list in
+  let module C = Compile(M) in
+  C.compile_function env localenv fun_names reldescr m
+
+
+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 (compile_function env localenv fun_names reldescr) modes 
+  ) prog in
+  let defs = sep_newline (Nfmap.fold (fun l _ c -> c@l) [] defs) in
+  ((Val_def(Rec_def(newline,None,None,defs), Types.TNset.empty, []), None), l)
+
+module Compile_list = Compile(Context_list)
+module Compile_pure = Compile(Context_pure)
+module Compile_unique = Compile(Context_unique)
+module Compile_option = Compile(Context_option)
+
+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(newline, sep_no_skips (List.map make_def tds))
+
+let register_types rel_loc 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 = loc_trans "register_types" rel_loc 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
+    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 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 l get_typepath_from_rel names rules = 
+  let rels = get_rels l 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 l "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 -> 
+          (Format.eprintf "MODULE LOOKUP FAILURE\n"; None)
+      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
+
+(* TODO : remove this once the backend is fixed *)
+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))
+
+
+let initial_env : Typed_ast.env =
+  { m_env = Nfmap.empty;
+    v_env = Nfmap.empty;
+    f_env = Nfmap.empty;
+    r_env = Nfmap.empty;
+    p_env = Nfmap.from_list 
+              [(Name.from_rope (r"bool"), (Path.boolpath, Ast.Unknown));
+               (Name.from_rope (r"bit"), (Path.bitpath, Ast.Unknown));
+               (Name.from_rope (r"vector"), (Path.vectorpath, Ast.Unknown));
+               (Name.from_rope (r"set"), (Path.setpath, Ast.Unknown));
+               (Name.from_rope (r"list"), (Path.listpath, Ast.Unknown));
+               (Name.from_rope (r"string"), (Path.stringpath, Ast.Unknown));
+               (Name.from_rope (r"unit"), (Path.unitpath, Ast.Unknown));
+               (Name.from_rope (r"num"), (Path.numpath, Ast.Unknown))] }
+
+let path_from_name_list_rev (u::v) = Path.mk_path (List.rev v) u
+
+let path_to_list p = let (u,v) = Path.to_name_list p in 
+                     u@[v]
+
+let unfocus_env env mod_path = 
+  let rec insert_mod env m where = function
+    | [] -> m
+    | p::ps ->
+      let e = match Nfmap.apply env.m_env p with
+        | None -> { mod_binding = path_from_name_list_rev (p::where);
+                    mod_env = initial_env }
+        | Some(e) -> e
+      in
+      let e = { e with mod_env = insert_mod e.mod_env m (p::where) ps } in
+      {env with m_env = Nfmap.insert env.m_env (p, e) }
+  in
+  let e = initial_env in 
+  let e = insert_mod e env [] mod_path in
+  Nfmap.fold (fun env _ m -> insert_mod env m.mod_env [] (path_to_list m.mod_binding)) e env.m_env 
+
+let gen_witness_type_info l mod_path ctxt names rules = 
+  (* Ugly hack *)
+  let unfocused_env = unfocus_env ctxt.cur_env mod_path in
+  let tds = gen_witness_type_aux unfocused_env l 
+    (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 l ctxt mod_path tds in
+  newctxt
+
+let gen_witness_type_def env l mpath localenv names rules =
+  let l = loc_trans "gen_witness_type_def" l in
+  let tds = gen_witness_type_aux env l
+    (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),  l]
+
+let ctxt_mod update ctxt = 
+  { ctxt with
+    cur_env = update ctxt.cur_env;
+    new_defs = update ctxt.new_defs
+  }
+
+let gen_witness_check_info l mod_path ctxt names rules =
+  let rels = get_rels l 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 l
+              "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 = loc_trans "gen_witness_check_info" l;
+      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 l mpath localenv names rules = 
+  let rels = get_rels l names rules in
+  let mkloc = loc_trans "gen_witness_check_def" in
+  let l = mkloc l 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
+      let l = mkloc rule.rule_loc 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 (mkloc (exp_to_locn head)) (Name.add_lskip def_name) {t=Tfn(witness_ty, out_ty)}
+                  | None -> mk_const_from_path env (mkloc (exp_to_locn head)) check_path []
+                in
+                Left(args, witness_path, check_exp)
+              | Some _ ->
+                raise_error (exp_to_locn e) "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 (mkloc (exp_to_locn head)) check_path [] in
+                    Left (args, witness_path, check_exp)
+              | Some _ -> 
+                raise_error (exp_to_locn e) "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 l (Name.add_lskip var) typ) rule.rule_vars in
+      let pconds = List.map
+        (fun (_,witness_ty,_,var) -> 
+          mk_pvar l (Name.add_lskip var) witness_ty
+        ) relconds in
+      let constr_id = { id_path = Id_none None;
+                        id_locn = l;
+                        descr = constr;
+                        instantiation = [] } in
+      let pattern = mk_pconstr l constr_id (pvars @ pconds) None in
+      let ret = mk_some env 
+        (mk_tup l 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 l (Name.add_lskip witness) witness_ty in
+        let rhs = mk_some env (mk_tup l None (sep_no_skips args) None None) in
+        let lhs = mk_app l 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 l ({term=L_true(None); locn = l;
+                                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 l 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_ty l x witness_ty in
+    let xvar = mk_var l x witness_ty in
+    let return_ty = exp_to_typ (snd (List.hd pats))  in
+    let body = mk_case_exp false l xvar pats return_ty in
+    let annot = { term = Name.add_lskip def_name;
+                  locn = l;
+                  typ = {t=Tfn(witness_ty,return_ty)};
+                  rest = () } in
+    (annot, [xpat], Some(space, t_to_src_t return_ty), space, body)
+  ) localdefs in
+  let defs = Nfmap.fold (fun l _ v -> v::l) [] defs in
+  let def = Rec_def(newline,None,None,sep_newline defs) in
+  if defs = [] then []
+  else [((Val_def(def, Types.TNset.empty, []), None), l)]
+
+open Compile_list
+
+let gen_fns_info l mod_path (ctxt : defn_ctxt) names rules =
+  let rels = get_rels l names rules in
+  let l = loc_trans "gen_fns_info" l in
+  Nfmap.fold (fun ctxt relname reldescr ->
+    List.fold_left (fun ctxt (name, mode) ->
+      let ty = ty_from_mode ctxt.cur_env ctxt.cur_env reldescr mode 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, 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 = l;
+        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, out_mode) rel (rule : ruledescr) = 
+  let l = loc_trans "transform_rule" rule.rule_loc in
+  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
+  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 l (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 l constr_id None in
+      let wit = List.fold_left (fun u v -> mk_app l 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, fun_out_mode),_info) = 
+          List.for_all (fun x -> x)
+            (List.map2 (fun inp m -> inp || m = O) inargs fun_mode)
+            && (not need_wit || fun_wit) 
+            && (fun_out_mode = out_mode)
+        in
+        match List.filter mode_matches modes with
+          | [] -> search (c::notok) cs
+          | ((fun_mode, fun_wit, _out_mode), 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 l (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
+  (l, patterns, build_code initknown indconds sideconds initeqs)
+
+
+let transform_rules env localenv localrels mode reldescr =
+  List.map (transform_rule env localenv localrels mode reldescr) reldescr.rel_rules
+
+let gen_fns_def env l mpath localenv names rules =
+  let rels = get_rels l 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_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), l ->
+      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),l in
+      let tdefs = gen_witness_type_def env l 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), l ->
+      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),l in
+      let cdefs = gen_witness_check_def env l 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), l ->
+      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),l in
+      let fdefs = gen_fns_def env l mpath localenv names rules in
+      if fdefs = []
+      then None
+      else Some(localenv, def::fdefs)
+    | _ -> None
+
+end

File src/coq_backend.ml

View file
  • Ignore whitespace
               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
       in
       let gathered = gather_names clause_list in
       (* TODO: use refs instead of names *)
-      let compare_clauses_by_name name (_, _, _, _, _, _, name', _, _) =
+      let compare_clauses_by_name name (Rule(_,_, _, _, _, _, _, name', _, _),_) =
         let name' = name'.term in
         let name' = Name.strip_lskip name' in
           Pervasives.compare name name' = 0
           let index_types =
             match bodies with
               | [] -> [from_string "Prop"]
-              | (_, _, _, _, _, _, _, _, exp_list)::xs ->
+              | (Rule(_,_, _, _, _, _, _, _, _, exp_list),_)::xs ->
                   List.map (fun t ->
                     Output.flat [
                       from_string "("; field_typ @@ C.t_to_src_t (Typed_ast.exp_to_typ t); from_string ")"
                   ) exp_list
           in
           let bodies =
-            Util.list_mapi (fun counter -> fun (name_lskips_t_opt, skips, name_lskips_annot_list, skips', exp_opt, skips'', name_lskips_annot, c, exp_list) ->
+            Util.list_mapi (fun counter -> fun (Rule(name_lskips_t, skips0, skips, name_lskips_annot_list, skips', exp_opt, skips'', name_lskips_annot, c, exp_list),_) ->
               let constructor_name =
-                match name_lskips_t_opt with
+              (* Note, now that names are not optional, this code is likely unneccessary, and an extra skip is added*)
+(*                match name_lskips_t_opt with
                   | None ->
                     let fresh = string_of_int counter in
                     let name = Name.to_string name in
                       Output.flat [
                         from_string name; from_string "_"; from_string fresh
                       ]
-                  | Some name -> from_string (Name.to_string (Name.strip_lskip name))
+                  | Some name ->*) from_string (Name.to_string (Name.strip_lskip name_lskips_t))
               in
               let antecedent =
                 match exp_opt with
                         from_string "Prop_of_bool ("; exp e; from_string ")"
                       ]
               in
+              (* Indrel TODO This does not match variables with type annotations *)
               let bound_variables =
-                concat_str " " @@ List.map (fun n ->
+                concat_str " " @@ List.map (fun (QName n) ->
                   from_string (Name.to_string (Name.strip_lskip n.term))
                 ) name_lskips_annot_list
               in

File src/def_trans.ml

View file
  • Ignore whitespace
 let remove_indrelns_true_lhs _ env ((d,s),l,lenv) =
   let l_unk = Ast.Trans ("remove_indrelns_true_lhs", Some l) in
   match d with
-    | Indreln (s', targ, sl) ->
-        let remove_true (name_opt, s1, qnames, s2, e_opt, s3, rname, c, es) =
+    | Indreln (s', targ, names, sl) ->
+        let remove_true (Rule (name_opt,s0, s1, qnames, s2, e_opt, s3, rname, c, es),l) =
             (match e_opt with None -> None | Some e -> (if Typed_ast_syntax.is_tf_exp true e then 
-                Some (name_opt, s1, qnames, s2, None, s3, rname, c, es) else None))
+                Some (Rule(name_opt, s0,s1, qnames, s2, None, s3, rname, c, es),l) else None))
         in
         (match Seplist.map_changed remove_true sl with
              None -> None
            | Some sl' -> 
-             let def = (((Indreln (s', targ, sl'), s), l_unk, lenv):def) in 
+             let def = (((Indreln (s', targ, names, sl'), s), l_unk,lenv):def) in 
              Some(env, [def]))
     | _ -> None
 
               const_type = dict_type;
               env_tag = K_let;
               spec_l = l;
+              relation_info = None;
               target_rep = Targetmap.empty;
             }
           in
 
 let get_name def l = match def with
 
-  | Indreln(_,_,clauses) -> (match Seplist.to_list clauses with 
+  (*TODO : Check the name section, no just within the clauses*)
+  | Indreln(_,_,_,clauses) -> (match Seplist.to_list clauses with 
     | [] ->  
         raise (Reporting_basic.err_todo false l "Error while pruning target definitions: empty Indreln clauses in get_name [debug]")
         
-    | ((_,_,_,_,_,_,name,_,_)::cs) -> Name.strip_lskip name.term     
+    | ((Rule(_,_,_,_,_,_,_,name,_,_),_)::cs) -> Name.strip_lskip name.term
     )
   
   | Val_def(Fun_def(_,_,_,clauses),ntvs,_) -> (match Seplist.to_list clauses with
       match def with
         | (Val_def(Let_def(_,topt,_),_,_) |
           Val_def(Fun_def(_,_,topt,_),_,_) |