mach -> typing; machops -> typeops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@27 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 600 insertions, 0 deletions

diff --git a/kernel/typing.ml b/kernel/typing.ml
new file mode 100644
index 0000000000..2311fb9992
--- /dev/null
+++ b/kernel/typing.ml
@@ -0,0 +1,600 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Univ
+open Generic
+open Term
+open Reduction
+open Sign
+open Environ
+open Type_errors
+open Machops
+
+(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
+
+let tjudge_of_cast env = function
+  | DOP2 (Cast, b, t) ->
+      (match whd_betadeltaiota env t with
+	 | DOP0 (Sort s) -> {body=b; typ=s}
+	 | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]"
+	 | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]")
+  | _ -> anomaly "Not casted (tjudge_of_cast)"
+	
+let tjudge_of_judge env j =
+  { body = j.uj_val;
+    typ = match whd_betadeltaiota env j.uj_type with
+      (* Nécessaire pour ZFC *)
+      | DOP0 (Sort s) -> s
+      | DOP0 Implicit -> anomaly "Tiens, un implicit"
+      | _ -> anomaly "Not a type (tjudge_ofjudge)" }
+
+let vect_lift = Array.mapi lift
+let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+
+(*s The machine flags. 
+   [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$)
+   like [Acc_rec.fw].
+   [nocheck] indicates if we can skip some verifications to accelerate
+   the type inference. *)
+
+type 'a mach_flags = {
+  fix : bool;
+  nocheck : bool }
+
+(* The typing machine without information. *)
+
+let rec execute mf env cstr =
+  let u0 = universes env in
+  match kind_of_term cstr with
+    | IsMeta n ->
+       	let metaty =
+          try lookup_meta n env
+          with Not_found -> error "A variable remains non instanciated" 
+	in
+        (match kind_of_term metaty with
+           | IsCast (typ,kind) -> 
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind}, u0)
+           | _ ->
+	       let (jty,u1) = execute mf env metaty in
+	       let k = hnf_constr env jty.uj_type in
+	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1))
+	
+    | IsRel n -> 
+	(relative env n, u0)
+
+    | IsVar id -> 
+	(make_judge cstr (snd (lookup_var id env)), u0)
+	  
+    | IsAbst _ ->
+        if evaluable_abst env cstr then 
+	  execute mf env (abst_value env cstr)
+        else 
+	  error "Cannot typecheck an unevaluable abstraction"
+	      
+    | IsConst _ ->
+        (make_judge cstr (type_of_constant_or_existential env cstr), u0)
+	  
+    | IsMutInd _ ->
+	(make_judge cstr (type_of_inductive env cstr), u0)
+	  
+    | IsMutConstruct _ -> 
+	let (typ,kind) = destCast (type_of_constructor env cstr) in
+        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , u0)
+	  
+    | IsMutCase (_,p,c,lf) ->
+        let (cj,u1) = execute mf env c in
+	let env1 = set_universes u1 env in
+        let (pj,u2) = execute mf env1 p in
+	let env2 = set_universes u2 env1 in
+        let (lfj,u3) = execute_array mf env2 lf in
+	let env3 = set_universes u3 env2 in
+        (type_of_case env3 pj cj lfj, u3)
+  
+    | IsFix (vn,i,lar,lfi,vdef) ->
+        if (not mf.fix) && array_exists (fun n -> n < 0) vn then
+          error "General Fixpoints not allowed";
+        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let fix = mkFix vn i larv lfi vdefv in
+        check_fix env fix;
+	(make_judge fix larv.(i), u1)
+	  
+    | IsCoFix (i,lar,lfi,vdef) ->
+        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let cofix = mkCoFix i larv lfi vdefv in
+        check_cofix env cofix;
+	(make_judge cofix larv.(i), u1)
+	  
+    | IsSort (Prop c) -> 
+	(type_of_prop_or_set c, u0)
+
+    | IsSort (Type u) ->
+	type_of_type u u0
+	  
+    | IsAppL a ->
+	let la = Array.length a in
+	if la = 0 then error_cant_execute CCI env cstr;
+	let hd = a.(0)
+	and tl = Array.to_list (Array.sub a 1 (la - 1)) in
+	let (j,u1) = execute mf env hd in
+	let env1 = set_universes u1 env in
+        let (jl,u2) = execute_list mf env1 tl in
+	let env2 = set_universes u2 env1 in
+	apply_rel_list env2 mf.nocheck jl j
+	    
+    | IsLambda (name,c1,c2) -> 
+        let (j,u1) = execute mf env c1 in
+        let var = assumption_of_judgement env j in
+	let env1 = push_rel (name,var) (set_universes u1 env) in
+        let (j',u2) = execute mf env1 c2 in 
+	let env2 = set_universes u2 env1 in
+        abs_rel env2 name var j'
+	  
+    | IsProd (name,c1,c2) ->
+        let (j,u1) = execute mf env c1 in
+        let var = assumption_of_judgement env j in
+	let env1 = push_rel (name,var) (set_universes u1 env) in
+        let (j',u2) = execute mf env1 c2 in
+	let env2 = set_universes u2 env1 in
+        gen_rel env2 name var j'
+	  
+    | IsCast (c,t) ->
+        let (cj,u1) = execute mf env c in
+	let env1 = set_universes u1 env in
+        let (tj,u2) = execute mf env1 t in
+	let env2 = set_universes u2 env1 in
+        (cast_rel env2 cj tj, u2)
+	  
+      | _ -> error_cant_execute CCI env cstr
+	  
+and execute_fix mf env lar lfi vdef =
+  let (larj,u1) = execute_array mf env lar in
+  let env1 = set_universes u1 env in
+  let lara = Array.map (assumption_of_judgement env1) larj in
+  let nlara = 
+    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
+  let env2 = 
+    List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in
+  let (vdefj,u2) = execute_array mf env2 vdef in
+  let env3 = set_universes u2 env2 in
+  let vdefv = Array.map j_val_only vdefj in
+  let u3 = type_fixpoint env3 lfi lara vdefj in
+  (lara,vdefv,u3)
+
+and execute_array mf env v =
+  let (jl,u1) = execute_list mf env (Array.to_list v) in
+  (Array.of_list jl, u1)
+
+and execute_list mf env = function
+  | [] -> ([], universes env)
+  | c::r -> 
+      let (j,u') = execute mf env c in 
+      let (jr,u'') = execute_list mf (set_universes u' env) r in
+      (j::jr, u'')
+
+
+(* The typed type of a judgment. *)
+
+let execute_type mf env constr = 
+  let (j,_) = execute mf env constr in
+  typed_type_of_judgment env j
+
+
+(* Exported machines.  First safe machines, with no general fixpoint
+   allowed (the flag [fix] is not set) and all verifications done (the
+   flag [nocheck] is not set). *)
+
+let safe_machine env constr = 
+  let mf = { fix = false; nocheck = false } in
+  execute mf env constr
+
+let safe_machine_type env constr = 
+  let mf = { fix = false; nocheck = false } in
+  execute_type mf env constr
+
+(* Machines with general fixpoint. *)
+
+let fix_machine env constr = 
+  let mf = { fix = true; nocheck = false } in
+  execute mf env constr
+
+let fix_machine_type env constr = 
+  let mf = { fix = true; nocheck = false } in
+  execute_type mf env constr
+
+(* Fast machines without any verification. *)
+
+let unsafe_machine env constr = 
+  let mf = { fix = true; nocheck = true } in
+  execute mf env constr
+
+let unsafe_machine_type env constr = 
+  let mf = { fix = true; nocheck = true } in
+  execute_type mf env constr
+
+
+(* ``Type of'' machines. *)
+
+let type_of env c = 
+  let (j,_) = safe_machine env c in nf_betaiota env j.uj_type
+
+let type_of_type env c = 
+  let tt = safe_machine_type env c in DOP0 (Sort tt.typ)
+
+let unsafe_type_of env c = 
+  let (j,_) = unsafe_machine env c in nf_betaiota env j.uj_type
+
+let unsafe_type_of_type env c = 
+  let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
+
+
+(*s Machines with information. *)
+
+type information = Logic | Inf of unsafe_judgment
+
+(*i
+let implicit_judgment = {body=mkImplicit;typ=implicit_sort}
+
+let add_inf_rel (na,inf) env =
+  match inf with
+      Logic -> add_rel (na,implicit_judgment) env
+    | Inf j -> add_rel (na,tjudge_of_judge j) env
+
+
+let fw_mutind sigma fenv k =
+  let (sp,x,args) = destMutInd k in
+  let mis = mind_specif_of_mind k in
+    match mis_singl mis with 
+	Some a -> Some (a,true)
+      | None ->
+	  if is_info_cast_type sigma (mis_arity mis) then
+	    let infK =
+              global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x)))
+	    in Some (infK,false)
+	  else None
+
+let inf_of_mind sigma fenv mind = 
+  try
+    match fw_mutind sigma fenv mind with
+        Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK)
+      | None -> Logic
+  with
+      Not_found | Failure _ -> 
+	anomaly "cannot convert an inductive to an finductive"
+
+let inf_mconstructor (sigma,metamap) fenv k = 
+  let (sp,x,i,cl) = destMutConstruct k in
+  let mind = mkMutInd sp x cl in 
+    (match fw_mutind sigma fenv mind with
+         None -> Logic
+       | Some(infi,singl) ->
+	   (match mind_lamexp mind with
+	      | Some clamexp ->
+		  if singl
+		  then Inf(cast_fmachine (sigma,[]) fenv clamexp)
+		  else
+		    let (infsp, infx, infcl) = destMutInd infi in
+		    let infmconstructor = mkMutConstruct infsp infx i infcl in
+		    let infval = subst1 infmconstructor clamexp in
+		      Inf (cast_fmachine (sigma,fst metamap) fenv infval)
+	      | _ -> assert false))
+
+
+exception DefinedExtraction
+
+(* when c is an evaluable constant with an extraction which 
+   contains an implicit, gives the value of the c constant
+   otherwise raise DefinedExtraction
+*)
+
+let value_implicit_const sigma c cinf = 
+  match c with DOPN(Const(_),_) -> 
+    if evaluable_const sigma c then 
+      let cv = const_value sigma cinf in 
+	if is_implicit cv (* or contains_implicit sigma cv *)
+	then const_value sigma c 
+	else raise DefinedExtraction
+    else raise DefinedExtraction
+    | _ -> raise DefinedExtraction
+
+let unsafe_infmachine (sigma,metamap) env fenv c = 
+  let rec infexec env fenv cstr = match cstr with
+       DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic
+    |  DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic
+    |  DOP2(Cast,c,_) -> infexec env fenv c
+    |  DOP0(Meta n) ->
+         (match List.assoc n (snd metamap) with
+             Logic -> Logic
+           | Inf j -> Inf{uj_val=DOP0(Meta n);
+                          uj_type=j.uj_val;
+                          uj_kind = hnf_constr sigma j.uj_type})
+
+    | Rel n ->
+        inf_rel fenv
+          (contents_of_type sigma (snd (lookup_rel n env))) n
+
+    | VAR str ->
+        inf_var fenv
+          (contents_of_type sigma (snd(lookup_glob str env))) str
+
+    | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr
+
+    | DOPN(Abst _,_) ->
+        if evaluable_abst cstr then infexec env fenv (abst_value cstr)
+        else error "cannot extract from an unevaluable abstraction"
+
+    | DOP0(Sort s) -> inf_sort s
+
+    | DOPN(AppL,tl) ->
+        let c1 =  (hd_vect tl)
+        and cl = tl_vect tl in
+          let funinf = infexec env fenv c1 in
+            (match funinf with Logic -> Logic
+	      | Inf(j) -> let cinf = j.uj_val in
+             (* try to expand constants corresponding 
+		    to non extractable terms *)
+	      (try if is_extraction_expanded() then 
+		 let valcte = value_implicit_const sigma c1 cinf 
+		 in infexec env fenv (whd_betaiota (appvect(valcte,cl))) 
+	       else raise DefinedExtraction
+               with DefinedExtraction -> 
+		 let argsinf = Array.map (infexec env fenv) cl
+		 in it_vect inf_apply funinf argsinf))
+
+    | DOP2(Lambda,c1,DLAM(name,c2)) ->
+        let varinf = infexec env fenv c1 in
+        let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
+                        (add_inf_rel (name,varinf) fenv) c2
+        in inf_abs_rel name bodyinf varinf
+
+    | DOP2(Prod,c1,DLAM(name,c2)) ->
+        let c1inf = infexec env fenv c1 in
+        let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
+                      (add_inf_rel (name,c1inf) fenv) c2
+        in inf_gen_rel name c2inf c1inf
+
+    | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr
+
+    | DOPN(MutConstruct _,_) ->
+        inf_mconstructor (sigma,metamap) fenv cstr
+
+    | DOPN(Fix(vn,i),cl) ->
+        let lar = Array.sub cl 0 ((Array.length cl) - 1) in
+        let inflar = Array.map (infexec env fenv) lar in
+        let infAi = inflar.(i) in 
+          (match infAi with 
+              Logic   -> Logic 
+            | Inf aij ->
+                let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in
+                let (new_env,new_fenv) =
+                  it_vect2
+                    (fun (ne,nfe) fk ak -> 
+                       (add_rel (fk,tjudge_of_cast sigma ak) ne,
+                        let infAk = infexec ne nfe ak
+                        in (add_inf_rel (fk,infAk) nfe)))
+                    (env,fenv)
+                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
+(* a special function to localize the recursive index in the extracted term *)
+                let rec exec_def ne nfe n def = 
+                  (match hnf_constr sigma def with 
+                      DOP2(Lambda,c1,DLAM(name,c2)) ->
+                        let varinf = infexec ne nfe c1 in
+                        let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) 
+                        and nfe' = add_inf_rel (name,varinf) nfe in
+                          if n = 0 then
+                            let infc2 = infexec ne' nfe' c2 
+                            in let infdef = inf_abs_rel name infc2 varinf
+                               and index =
+                                 if varinf = Logic then -1
+                        (* the recursive call was on a non-informative term *) 
+                                 else 0 in (infdef,index)
+                          else
+                            let bodyinf,countl = 
+                              exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) 
+                                (add_inf_rel (name,varinf) nfe) (n-1) c2 in
+                            let (infabs,abs) =
+                              inf_abs_rel_count name bodyinf varinf
+                            in (infabs,
+                                if abs = ERASE then countl
+                                else if countl<0 then countl-1
+                                else countl+1)
+                    | _ -> anomaly "exec_def : should be a lambda") in
+                let infdefs_ind =
+                  map2_vect (exec_def new_env new_fenv) vn ldefs
+                in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind)
+
+    | DOPN(CoFix i,cl) ->
+        let lar    = Array.sub cl 0 ((Array.length cl) - 1) in 
+        let inflar = Array.map (infexec env fenv) lar in
+        let infAi  = inflar.(i) in
+          (match infAi with 
+              Logic   -> Logic 
+            | Inf aij -> 
+                let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in 
+                let (new_env,new_fenv) = 
+                  it_vect2 (fun (ne,nfe) fk ak -> 
+                              (add_rel (fk,tjudge_of_cast sigma ak) ne, 
+                               let infAk = infexec ne nfe ak
+                               in (add_inf_rel (fk,infAk) nfe)))
+                    (env,fenv) 
+                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
+                                   
+                let infdefs = Array.map (infexec new_env new_fenv) ldefs 
+                in  inf_cofix sigma i aij.uj_type lfi inflar infdefs)
+
+    | DOPN(MutCase _,_) ->
+        let (ci,p,c,lf) = destCase cstr in
+        let pinf = infexec env fenv p in 
+          (match pinf with
+              Logic  -> Logic 
+            | Inf pj -> 
+		if is_extraction_expanded() then 
+		  let (d,l) = whd_betadeltaiota_stack sigma c [] in 
+                 (match d with (DOPN(MutConstruct(_,_),_)) ->
+		    let cstr' = 
+		      DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf)
+		    in infexec env fenv (whd_betaiota cstr')
+		    | _ -> 
+                  let cinf = infexec env fenv c
+                  and lfinf = Array.map (infexec env fenv) lf
+                  in inf_mutcase fenv sigma pj ci cinf lfinf
+		 )
+               else let cinf = infexec env fenv c
+                  and lfinf = Array.map (infexec env fenv) lf
+                  in inf_mutcase fenv sigma pj ci cinf lfinf)
+	 
+    | _ -> error "Cannot extract information"
+  in infexec env fenv c
+
+
+let core_infmachine meta env fenv c =
+  try unsafe_infmachine meta env fenv c
+  with (UserError _ | Failure _) -> Logic
+
+(* WITH INFORMATION *)
+(* does not check anymore that extracted terms are well-formed *)
+let judgement_infmachine meta env fenv c ct = 
+  try
+    match unsafe_infmachine meta env fenv c with
+        Inf infj ->
+          let inftyp =
+            try unsafe_infmachine meta env fenv ct
+            with (UserError _ | Failure _) ->
+              (warning "Failed to extract in type"; Logic)
+          in (match inftyp with
+                  Inf infjt ->
+                    Inf{uj_val=infj.uj_val;
+                        uj_type=infjt.uj_val;
+                        uj_kind=infj.uj_kind}
+                | Logic -> Inf infj)
+      | Logic -> Logic
+  with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic)
+
+let infmachine_type nocheck (sigma,metamap) env fenv constr =
+  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
+  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
+  let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in
+  let inf = 
+    if is_info_type sigma t then (* Case the term is informative *)
+      let uniarc = get_uniarc () in
+      let infjt =
+        judgement_infmachine
+          (sigma,(constr_metamap,inf_metamap)) env fenv 
+	  t.body 
+	  (DOP0 (Sort t.typ)) in
+      let _ = set_uniarc uniarc in
+        infjt
+    else Logic
+
+  in hash_jpair_type
+       ({body = strip_all_casts t.body; typ = t.typ},
+        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
+                            uj_type = nf_beta j.uj_type;
+                            uj_kind = j.uj_kind }) inf))
+
+let infmachine nocheck (sigma,metamap) env fenv constr =
+  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
+  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
+  let j = core_fmachine nocheck (sigma,constr_metamap) env constr in
+  let inf = 
+    if is_info_judge sigma j then (* Case the term is informative *)
+      let uniarc = get_uniarc () in
+      let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in
+      let infjt =
+        judgement_infmachine
+          (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in
+      let _ = set_uniarc uniarc in
+        infjt
+    else Logic
+
+  in hash_jpair
+       ({uj_val = strip_all_casts j.uj_val;
+         uj_type = strip_all_casts j.uj_type;
+         uj_kind = j.uj_kind},
+        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
+                            uj_type = nf_beta j.uj_type;
+                            uj_kind = j.uj_kind }) inf))
+
+
+let jsign_of_sign sigma sign =
+  sign_it
+    (fun id a (sign,fsign) ->
+      let sign' = add_sign (id,a) sign in
+      let fsign' =
+        match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body
+ 	with
+          (_,Logic) -> fsign
+        | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign
+      in (sign',fsign'))
+    sign (([],[]),([],[]))
+
+
+let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign)
+
+let infexemeta_type sigma metamap (env,fenv) c =
+  infmachine_type true (sigma,metamap) env fenv c
+
+let infexecute_rec_type sigma (env,fenv) c =
+  infmachine_type false (sigma,[]) env fenv c
+
+let infexecute_type sigma (sign,fsign) c =
+  infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c
+
+let infexemeta sigma metamap (env,fenv) c =
+  infmachine true (sigma,metamap) env fenv c
+
+let infexecute_rec sigma (env,fenv) c =
+  infmachine false (sigma,[]) env fenv c
+
+let infexecute sigma (sign,fsign) c =
+  infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c
+
+(* A adapter pour les nouveaux env
+let fvar_type sigma (sign,fsign) v = 
+  let na = destVar v in
+  let varty = (snd(lookup_sign na sign))
+  in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with
+      Inf ft -> ft.uj_val
+    | Logic -> invalid_arg "Fvar with a non-informative type (1)!"
+
+*)
+
+(* MACHINE WITH UNIVERSES *)
+(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab,
+   recuperer le graphe local, et restaurer l'acien graphe global *)
+
+let whd_instuni = function
+    DOP0(Sort(Type(u))) ->
+      let u = (if u = dummy_univ then new_univ() else u)
+      in DOP0(Sort(Type(u)))
+  | c -> c
+
+(* Instantiate universes: replace all dummy_univ by fresh universes.
+   This is already done by the machine.
+   Indtypes instantiates the universes itself, because in the case of
+   large constructor, additionnal constraints must be considered. *)
+let instantiate_universes c = strong whd_instuni c
+
+
+(* sp est le nom de la constante pour laquelle il faut que c soit bien type.
+   Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles
+   independamment.
+   Au lieu de sp, Lib.cwd() serait peut-etre suffisant.
+   Cela eviterai de donner un section-path quand on veut typer. *)
+let fexecute_type_with_univ sigma sign sp c =
+  with_universes (fexecute_type sigma sign) (sp,initial_universes,c) 
+
+
+let fexecute_with_univ sigma sign sp c =
+  with_universes (fexecute sigma sign) (sp,initial_universes,c) 
+
+
+let infexecute_type_with_univ sigma psign sp c =
+  with_universes (infexecute_type sigma psign) (sp,initial_universes,c) 
+
+
+let infexecute_with_univ sigma psign sp c =
+  with_universes (infexecute sigma psign) (sp,initial_universes,c) 
+i*)