Better fixpoint translation.

src/abstraction.ml4

@@ -14,6 +14,8 @@
 (**************************************************************************)
 
 
+(*i camlp4deps: "src/parametricity.cmo" "src/declare_translation.cmo" i*)
+
 DECLARE PLUGIN "parametricity"
 open Parametricity
 open Declare_translation
@@ -36,14 +38,23 @@ END
 VERNAC COMMAND EXTEND DebugAbstraction CLASSIFIED AS SIDEFF
 | [ "DebugParametricity" constr(c)] -> 
   [
-    print_translation_command default_arity c 
+    print_translation_command false default_arity c 
+  ]
+END
+
+VERNAC COMMAND EXTEND DebugAbstractionWithRetyping CLASSIFIED AS SIDEFF
+| [ "DebugParametricity" constr(c) "with" "retyping"] -> 
+  [
+    print_translation_command true default_arity c 
   ]
 END
 
+
+
 VERNAC COMMAND EXTEND DebugAbstractionWithArity CLASSIFIED AS SIDEFF
 | [ "DebugTranslation" constr(c) "arity" integer(arity)] -> 
   [
-    print_translation_command arity c
+    print_translation_command false arity c
   ]
 END 
 
@@ -110,6 +121,36 @@ VERNAC COMMAND EXTEND TranslateModule CLASSIFIED AS SIDEFF
   ]
 END
 
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+| [ "Parametricity" "Test" ] -> 
+  [
+    Names.(Constr.(
+    let program_mode_before = Flags.is_program_mode () in 
+    Obligations.set_program_mode !Parametricity.program_mode;
+    let env = Global.env () in 
+    let evdr = ref Evd.empty in  
+    let id_X = Name (id_of_string "X") in 
+    let id_x = Name (id_of_string "x") in 
+    let id_f = Name (id_of_string "f") in 
+    let sort_X = Evarutil.e_new_Type env evdr in 
+    let id_type = mkProd (id_x, mkRel 1, mkRel 2) in 
+    let id_fun = mkLambda(id_x, mkRel 1, mkRel 1) in  
+    let pred = mkLambda (id_f, id_type, Parametricity.CoqConstants.eq evdr
+            [| Vars.lift 1 id_type; mkRel 1; mkRel 1 |]) in 
+    let term = 
+      mkLambda (id_X, sort_X, Parametricity.CoqConstants.transport evdr [| id_type; id_fun; pred |])
+    in 
+    let term = Typing.solve_evars env evdr term in 
+    let name = id_of_string "marc" in 
+    let ctx = Evd.evar_universe_context !evdr in
+    let typ = Retyping.get_type_of env !evdr term in 
+    let obls, _, term, typ = Obligations.eterm_obligations env name !evdr 0 term typ in 
+    let kind = Decl_kinds.Global, true, Decl_kinds.Definition in
+    ignore (Obligations.add_definition name ~kind ~term:term typ ctx obls);
+    Obligations.set_program_mode program_mode_before))
+  ]
+END
+
 VERNAC COMMAND EXTEND TranslateModuleWithArity CLASSIFIED AS SIDEFF
 | [ "Parametricity" "Module" global(qid) "arity" integer(arity) ] ->
   [

src/declare_translation.ml

@@ -6,43 +6,59 @@ open Libnames
 
 let default_continuation = ignore
 
-let print_translation_command arity c =  
+let add_coercions env evdr term = 
+  (*
+    let glob = Detyping.detype true [] env !evdr term in 
+    Pretyping.understand_tcc_evars env evdr glob
+  *)
+  term
+
+let print_translation_command retype arity c =  
   let (evd, env) = Lemmas.get_current_context () in 
   let (evd, c) = Constrintern.interp_open_constr env evd c in
   let evdr = ref evd in 
   try
     let c_R = translate arity evdr env c in 
+    let c_R = if retype then add_coercions env evdr c_R else c_R in
     Pp.(msg_notice (Printer.pr_lconstr_env env !evdr c_R))
   with e -> 
     Pp.(msg_notice (str (Printexc.to_string e)))
 
 
-
 (** Adds the definition name := ⟦a⟧ : ⟦b⟧ a a. *)
 let declare_abstraction ?(opaque = false) ?(continuation = default_continuation) ?kind order evdr env a name =
+  let program_mode_before = Flags.is_program_mode () in 
+  Obligations.set_program_mode !Parametricity.program_mode;
   debug_string [`Abstraction] "### Begin declaration !";
   debug_evar_map [`Abstraction] "starting evarmap:" !evdr;
-  let refresh = false in 
-  let evd, b = Typing.e_type_of ~refresh env !evdr a in
-  evdr := evd;
-  Obligations.check_evars env evd;
-
+  let b = Retyping.get_type_of env !evdr a in
+  debug_string [`Time] "starting translation of term";
   debug [`Abstraction] "translate term :" env !evdr a;
   let a_R = translate order evdr env a  in
+  let a_R = add_coercions env evdr a_R in
+  let a_R = Typing.solve_evars env evdr a_R in
   debug [`Abstraction] "translate type :" env !evdr b;
+  debug_string [`Time] "starting translation of type";
   let b_R = relation order evdr env b in 
+  debug_string [`Time] "done translating";
   let sub = range (fun k -> prime order k a) order in 
   let b_R = substl sub b_R in
+  debug_string [`Time] "detyping ...";
+  let b_R = add_coercions env evdr b_R in
+  debug_string [`Time] "typing ...";
+  let b_R = Typing.solve_evars env evdr b_R in
+  debug_string [`Time] "retyping ...";
+  let b_R' = Retyping.get_type_of env !evdr a_R in 
+  debug_string [`Time] "unifying ...";
+  evdr := Unification.w_unify env !evdr Reduction.CUMUL b_R' b_R; 
+  debug_evar_map [`Abstraction] "after type checking (before simplification):" !evdr; 
+  let nf, _ = Evarutil.e_nf_evars_and_universes evdr in 
+  let a_R, b_R = nf a_R, nf b_R in 
   debug [`Abstraction] "translation of term, a_R = " env !evdr a_R;
-  debug [`Abstraction] "translate of type, b_R = " env !evdr b_R;
-  debug_evar_map [`Abstraction] "type checking b_R in" !evdr;
-  let evd, _ = Typing.e_type_of ~refresh env !evdr b_R in
-  debug_evar_map [`Abstraction] "type checking  a_R in " evd;
-  let evd, b_R' = Typing.e_type_of ~refresh env evd a_R in
+  let evd = !evdr in
+  debug_evar_map [`Abstraction] "after type checking :" evd; 
   debug [`Abstraction] "infered type is b_R' = " env evd b_R';
-  debug_string [`Abstraction] "checking cumulativity";
-  let evd = Unification.w_unify env evd Reduction.CUMUL b_R' b_R in 
-  debug_evar_map [`Abstraction] "after type checking :" evd;
+  debug_string [`Abstraction] "Cooking obligation ...";
   let obls, _, a_R, b_R = Obligations.eterm_obligations env name evd 0 a_R b_R in 
   let ctx = Evd.evar_universe_context evd in
   let hook = 
@@ -59,7 +75,8 @@ let declare_abstraction ?(opaque = false) ?(continuation = default_continuation)
   debug_string [`Abstraction] "add_definition:";
   debug [`Abstraction] "a_R:\t" env evd a_R;
   debug [`Abstraction] "b_R:\t" env evd b_R;
-  ignore (Obligations.add_definition ~opaque name ~hook ?kind ~tactic:(snd (Relations.get_parametricity_tactic ())) ~term:a_R b_R ctx obls)
+  ignore (Obligations.add_definition ~opaque name ~hook ?kind ~tactic:(snd (Relations.get_parametricity_tactic ())) ~term:a_R b_R ctx obls);
+  Obligations.set_program_mode program_mode_before
 
 let translate_command arity c names =  
   let (evd, env) = Lemmas.get_current_context () in