1 files changed, 251 insertions, 51 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b449..a566028d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x
 
 (* Insertion of constants and parameters in environment. *)
 
-let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
+let mk_pure_proof c = (c, Univ.ContextSet.empty), []
 
-let handle_side_effects env body side_eff =
-  let handle_sideff t se =
+let equal_eff e1 e2 =
+  let open Entries in
+  match e1, e2 with
+  | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
+        Names.Constant.equal c1 c2
+  | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
+        CList.for_all2eq
+          (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
+          cl1 cl2
+  | _ -> false
+
+let rec uniq_seff = function
+  | [] -> []
+  | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
+(* The list of side effects is in reverse order (most recent first).
+ * To keep the "topological" order between effects we have to uniq-ize from
+ * the tail *)
+let uniq_seff l = List.rev (uniq_seff (List.rev l))
+
+let inline_side_effects env body ctx side_eff =
+  let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
     let cbl = match se with
       | SEsubproof (c,cb,b) -> [c,cb,b]
       | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -65,8 +84,8 @@ let handle_side_effects env body side_eff =
     let rec sub_body c u b i x = match kind_of_term x with
       | Const (c',u') when eq_constant c c' -> 
 	Vars.subst_instance_constr u' b
-      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
-    let fix_body (c,cb,b) t =
+      | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
+    let fix_body (c,cb,b) (t,ctx) =
       match cb.const_body, b with
       | Def b, _ ->
           let b = Mod_subst.force_constr b in
@@ -74,37 +93,86 @@ let handle_side_effects env body side_eff =
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
               let t = sub c 1 (Vars.lift 1 t) in
-		mkLetIn (cname c, b, b_ty, t)
+	        mkLetIn (cname c, b, b_ty, t),
+		Univ.ContextSet.union ctx
+		  (Univ.ContextSet.of_context cb.const_universes)
 	    else 
 	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | OpaqueDef _, `Opaque (b,_) -> 
 	  let poly = cb.const_polymorphic in
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
               let t = sub c 1 (Vars.lift 1 t) in
-		mkApp (mkLambda (cname c, b_ty, t), [|b|]) 
+	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
+		Univ.ContextSet.union ctx
+		  (Univ.ContextSet.of_context cb.const_universes)
 	    else
 	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | _ -> assert false
     in
-      List.fold_right fix_body cbl t
+    let t, ctx = List.fold_right fix_body cbl (t,ctx) in
+    t, ctx, (mb,List.length cbl) :: sl
   in
   (* CAVEAT: we assure a proper order *)
-  Declareops.fold_side_effects handle_sideff body
-    (Declareops.uniquize_side_effects side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+
+(* Given the list of signatures of side effects, checks if they match.
+ * I.e. if they are ordered descendants of the current revstruct *)
+let check_signatures curmb sl =
+  let is_direct_ancestor (sl, curmb) (mb, how_many) =
+    match curmb with
+    | None -> None, None
+    | Some curmb ->
+        try
+          let mb = Ephemeron.get mb in
+          match sl with
+          | None -> sl, None
+          | Some n ->
+              if List.length mb >= how_many && CList.skipn how_many mb == curmb
+              then Some (n + how_many), Some mb
+              else None, None
+        with Ephemeron.InvalidKey -> None, None in
+  let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
+  sl
+
+let skip_trusted_seff sl b e =
+  let rec aux sl b e acc =
+    match sl, kind_of_term b with
+    | (None|Some 0), _ -> b, e, acc
+    | Some sl, LetIn (n,c,ty,bo) ->
+       aux (Some (sl-1)) bo
+         (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+    | Some sl, App(hd,arg) ->
+       begin match kind_of_term hd with
+       | Lambda (n,ty,bo) ->
+           aux (Some (sl-1)) bo
+             (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+       | _ -> assert false
+       end
+    | _ -> assert false
+    in
+  aux sl b e []
+
+let rec unzip ctx j =
+  match ctx with
+  | [] -> j
+  | `Let (n,c,ty) :: ctx ->
+      unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) }
+  | `Cut (n,ty,arg) :: ctx ->
+      unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
 let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
-let infer_declaration env kn dcl =
+	      
+let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context uctx env in
+      let env = push_context ~strict:(not poly) uctx env in
       let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,34 +183,41 @@ let infer_declaration env kn dcl =
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:true c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
-          let body = handle_side_effects env body side_eff in
-	  let env' = push_context_set ctx env in
-          let j = infer env' body in
+        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+          let body, uctx, signatures =
+            inline_side_effects env body uctx side_eff in
+          let valid_signatures = check_signatures trust signatures in
+	  let env' = push_context_set uctx env in
+          let j =
+            let body,env',ectx = skip_trusted_seff valid_signatures body env' in
+            let j = infer env' body in
+            unzip ectx j in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
 	    (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, ctx) in
+          j.uj_val, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
 
   | DefinitionEntry c ->
-      let env = push_context c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      assert(Univ.ContextSet.is_empty ctx);
-      let body = handle_side_effects env body side_eff in
+      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+      let body, ctx, _ = inline_side_effects env body
+        (Univ.ContextSet.union univsctx ctx) side_eff in
+      let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
-      let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
+      let usubst, univs =
+	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
       let j = infer env body in
       let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
@@ -176,14 +251,17 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+  let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
-      (List.map (fun (id, _,_) -> Id.to_string id)
-        (keep_hyps env (Id.Set.union s1 s2))) in
-  Aux_file.record_in_aux "context_used" v
+      (CList.map_filter (fun (id, _,_) ->
+          if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
 
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -198,6 +276,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
+  let sort evn l =
+    List.filter (fun (id,_,_) ->
+      List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+    (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map pi1 (named_context env) in
@@ -215,19 +297,21 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            !suggest_proof_using kn env vars ids_typ context_ids;
+            let expr =
+              !suggest_proof_using (Constant.to_string kn)
+                env vars ids_typ context_ids in
             if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars;
+              record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
-          record_aux env Id.Set.empty Id.Set.empty;
+          record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
-        declared,
+        sort env declared,
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
@@ -243,16 +327,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
   let tps = 
-    (* FIXME: incompleteness of the bytecode vm: we compile polymorphic 
-       constants like opaque definitions. *)
-    if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
-    else
-      let res = 
-	match proj with
-	| None -> compile_constant_body env def
-	| Some pb ->
-	   compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
-      in Option.map Cemitcodes.from_val res
+    let res =
+      let comp_univs = if poly then Some univs else None in
+      match proj with
+      | None -> compile_constant_body env comp_univs def
+      | Some pb ->
+	(* The compilation of primitive projections is a bit tricky, because
+           they refer to themselves (the body of p looks like fun c =>
+           Proj(p,c)). We break the cycle by building an ad-hoc compilation
+           environment. A cleaner solution would be that kernel projections are
+           simply Proj(i,c) with i an int and c a constr, but we would have to
+           get rid of the compatibility layer. *)
+	let cb =
+	  { const_hyps = hyps;
+	    const_body = def;
+	    const_type = typ;
+	    const_proj = proj;
+	    const_body_code = None;
+	    const_polymorphic = poly;
+	    const_universes = univs;
+	    const_inline_code = inline_code }
+	in
+	let env = add_constant kn cb env in
+	compile_constant_body env comp_univs def
+    in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
     const_body = def;
@@ -263,11 +361,95 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_universes = univs;
     const_inline_code = inline_code }
 
-
 (*s Global and local constant declaration. *)
 
-let translate_constant env kn ce =
-  build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant mb env kn ce =
+  build_constant_declaration kn env
+    (infer_declaration ~trust:mb env (Some kn) ce)
+
+let constant_entry_of_side_effect cb u =
+  let pt =
+    match cb.const_body, u with
+    | OpaqueDef _, `Opaque (b, c) -> b, c
+    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    | _ -> assert false in
+  DefinitionEntry {
+    const_entry_body = Future.from_val (pt, []);
+    const_entry_secctx = None;
+    const_entry_feedback = None;
+    const_entry_type =
+      (match cb.const_type with RegularArity t -> Some t | _ -> None);
+    const_entry_polymorphic = cb.const_polymorphic;
+    const_entry_universes = cb.const_universes;
+    const_entry_opaque = Declareops.is_opaque cb;
+    const_entry_inline_code = cb.const_inline_code }
+;;
+
+let turn_direct (kn,cb,u,r as orig) =
+  match cb.const_body, u with
+  | OpaqueDef _, `Opaque (b,c) ->
+      let pt = Future.from_val (b,c) in
+      kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
+   | _ -> orig
+;;
+
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects constant_entry * side_effect_role
+
+let export_side_effects mb env ce =
+  match ce with
+  | ParameterEntry _ | ProjectionEntry _ -> [], ce
+  | DefinitionEntry c ->
+      let { const_entry_body = body } = c in
+      let _, eff = Future.force body in
+      let ce = DefinitionEntry { c with
+        const_entry_body = Future.chain ~greedy:true ~pure:true body
+          (fun (b_ctx, _) -> b_ctx, []) } in
+      let not_exists (c,_,_,_) =
+        try ignore(Environ.lookup_constant c env); false
+        with Not_found -> true in 
+      let aux (acc,sl) { eff = se; from_env = mb } =
+        let cbl = match se with
+          | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
+          | SEscheme (cl,k) ->
+              List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
+        let cbl = List.filter not_exists cbl in
+        if cbl = [] then acc, sl
+        else cbl :: acc, (mb,List.length cbl) :: sl in
+      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+      let trusted = check_signatures mb signatures in
+      let push_seff env = function
+        | kn, cb, `Nothing, _ ->
+            Environ.add_constant kn cb env
+        | kn, cb, `Opaque(_, ctx), _ -> 
+            let env = Environ.add_constant kn cb env in
+            Environ.push_context_set
+              ~strict:(not cb.const_polymorphic) ctx env in
+      let rec translate_seff sl seff acc env =
+        match sl, seff with
+        | _, [] -> List.rev acc, ce
+        | (None | Some 0), cbs :: rest ->
+           let env, cbs =
+             List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+               let ce = constant_entry_of_side_effect ocb u in
+               let cb = translate_constant mb env kn ce in
+               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
+             (env,[]) cbs in
+           translate_seff sl rest (cbs @ acc) env
+        | Some sl, cbs :: rest ->
+           let cbs_len = List.length cbs in
+           let cbs = List.map turn_direct cbs in
+           let env = List.fold_left push_seff env cbs in
+           let ecbs = List.map (fun (kn,cb,u,r) ->
+             kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+           translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
+     in
+       translate_seff trusted seff [] env
+;;
 
 let translate_local_assum env t =
   let j = infer env t in
@@ -277,18 +459,36 @@ let translate_local_assum env t =
 let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant env r)
 
-let translate_local_def env id centry =
+let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration env None (DefinitionEntry centry) in
+    infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
+  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+    match def with
+    | Undef _ -> ()
+    | Def _ -> ()
+    | OpaqueDef lc ->
+       let context_ids = List.map pi1 (named_context env) in
+       let ids_typ = global_vars_set env typ in
+       let ids_def = global_vars_set env
+         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let expr =
+         !suggest_proof_using (Id.to_string id)
+           env ids_def ids_typ context_ids in
+       record_aux env ids_typ ids_def expr
+  end;
   def, typ, univs
 
 (* Insertion of inductive types. *)
 
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
-let handle_entry_side_effects env ce = { ce with
+let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
-      (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
+      let body, ctx',_ = inline_side_effects env body ctx side_eff in
+      (body, ctx'), []);
 }
+
+let inline_side_effects env body side_eff =
+  pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff)