trying f

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

5 files changed, 173 insertions, 133 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 160764799..dd2316644 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -54,101 +54,88 @@ let observe s =
   if do_observe () 
   then Pp.msgnl s 
 
-(* 
-   Transform an inductive induction principle into 
-   a functional one
-*)  
-let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
+type rel_to_fun_info = { thefun:constr; theargs: int array }
+
+let array_lasts a n =
+  let res = ref [] in
+  for i = Array.length a - n - 1 to Array.length a - 1 do 
+    res := a.(i) :: !res
+  done;
+  List.rev !res
+
+(** [compute_new_princ_type_from_rel rel_to_fun sorts princ_type]
+    transforms the inductive induction principle [princ_type] from a
+    graph relation into a functional one. The array [rel_to_fun]
+    contains the functions corresponding to each (mutual), that is:
+    the ith function corresponds to the ith mutul relation. [sorts]
+    contains the sort asked for each mutual principle. *)  
+let compute_new_princ_type_from_rel (rel_to_fun: (rel_to_fun_info list) Link.t)
+    sorts princ_type =
   let princ_type_info = compute_elim_sig princ_type in 
   let env = Global.env () in 
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context)  : Sign.rel_context = 
+  let rec change_predicates_names (avoid:identifier list) 
+      (predicates:Sign.rel_context)  : Sign.rel_context = 
     match predicates with 
     | [] -> []
     |(Name x,v,t)::predicates -> 
        let id =  Nameops.next_ident_away x avoid in 
        Hashtbl.add tbl id x;
        (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
-    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
-  in
+    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder " in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info = 
     { princ_type_info with
-	predicates = change_predicates_names avoid princ_type_info.predicates
-    }
-  in 
-(*   observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
-(*   observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
+	predicates = change_predicates_names avoid princ_type_info.predicates} in 
+  (* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
+  (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
   let change_predicate_sort i (x,_,t) = 
     let new_sort = sorts.(i) in
     let args,_ = decompose_prod t in 
     let real_args = 
-      if princ_type_info.indarg_in_concl 
-      then List.tl args 
-      else args
-    in
-    Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) 
-  in
+      if princ_type_info.indarg_in_concl then List.tl args else args in
+    Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) in
   let new_predicates = 
-    list_map_i
-      change_predicate_sort 
-      0
-      princ_type_info.predicates
-  in
-  let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
+    list_map_i change_predicate_sort 0 princ_type_info.predicates in
+  let env_with_params_and_predicates = 
+    List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn = 
     fst (match princ_type_info.indref with
 	   | Some (Libnames.IndRef ind) -> ind 
-	   | _ -> error "Not a valid predicate"
-	)
-  in
+	   | _ -> error "Not a valid predicate") in
   let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
   let is_pte = 
     let set = List.fold_right Idset.add ptes_vars Idset.empty in 
     fun t -> 
       match kind_of_term t with 
 	| Var id -> Idset.mem id set 
-	| _ -> false 
-  in
+	| _ -> false in
   let pre_princ = 
     it_mkProd_or_LetIn 
       ~init:
       (it_mkProd_or_LetIn 
-	 ~init:(Option.fold_right
-			   mkProd_or_LetIn
-			   princ_type_info.indarg
-			   princ_type_info.concl
-			)
-	 princ_type_info.args
-      )
-      princ_type_info.branches
-  in
+	~init:(Option.fold_right mkProd_or_LetIn princ_type_info.indarg 
+	  princ_type_info.concl)
+	princ_type_info.args)
+      princ_type_info.branches in
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match kind_of_term c with
-      | Ind((u,_)) -> u = rel_as_kn
-      | Construct((u,_),_) -> u = rel_as_kn
-      | _ -> false
-  in
+      | Ind((u,_)) | Construct((u,_),_) -> u = rel_as_kn
+      | _ -> false in
   let get_fun_num c =
     match kind_of_term c with
-      | Ind(_,num) -> num
-      | Construct((_,num),_) -> num
-      | _ -> assert false
-  in
+      | Ind(_,num) | Construct((_,num),_) -> num
+      | _ -> assert false in
   let dummy_var = mkVar (id_of_string "________") in
   let mk_replacement c i args =
-    let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in 
-(*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
-    res
-  in
+    let res = mkApp((Link.find i rel_to_fun).thefun,Array.map pop (array_get_start args)) in 
+    (* observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
+    res in
   let rec has_dummy_var t  =
-    fold_constr
-      (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
-      false
-      t
-  in
+    fold_constr (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
+      false t in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
       match kind_of_term pre_princ with
@@ -156,17 +143,19 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    begin
 	      try match Environ.lookup_rel n env with
 		| _,_,t when is_dom t -> raise Toberemoved
-		| _ -> pre_princ,[] with Not_found -> assert false
+		| _ -> pre_princ,[] 
+	      with Not_found -> assert false
 	    end
-	| Prod(x,t,b) ->
-	    compute_new_princ_type_for_binder remove mkProd env x t b
+	| Prod(x,t,b) -> compute_new_princ_type_for_binder remove mkProd env x t b
 	| Lambda(x,t,b) ->
 	    compute_new_princ_type_for_binder  remove mkLambda env x t b
 	| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
 	| App(f,args) when is_dom f ->
-	    let var_to_be_removed = destRel (array_last args) in
+	    (* let var_to_be_removed = destRel (array_last args) in *)
+	    let vars_to_be_removed = 
+	      List.map destRel (array_lasts args) in
 	    let num = get_fun_num f in
-	    raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args))
+	    raise (Toberemoved_with_rel (vars_to_be_removed,mk_replacement pre_princ num args))
 	| App(f,args) ->
 	    let args = 
 	      if is_pte f && remove 
@@ -201,26 +190,23 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : name = get_name (ids_of_context env) x in
 	let new_env = Environ.push_rel (x,None,t) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	 then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
-	 else
-	   (
-	     bind_fun(new_x,new_t,new_b),
-	     list_union_eq
-	       eq_constr
-	       binders_to_remove_from_t
-	       (List.map pop binders_to_remove_from_b)
-	   )
-
-       with
-	 | Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	else (
+	  bind_fun(new_x,new_t,new_b),
+	  list_union_eq eq_constr binders_to_remove_from_t
+	    (List.map pop binders_to_remove_from_b))
+      with
+	| Toberemoved ->
+	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = 
+	      compute_new_princ_type remove env (substnl [c] n b)  in
+	    new_b, 
+	    list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -232,44 +218,39 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
 	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
-	else
-	  (
-	    mkLetIn(new_x,new_v,new_t,new_b),
-	    list_union_eq
-	      eq_constr
-	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
-	      (List.map pop binders_to_remove_from_b)
-	  )
-	
+	else (
+	  mkLetIn(new_x,new_v,new_t,new_b),
+	  list_union_eq eq_constr
+	    (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+	    (List.map pop binders_to_remove_from_b))
       with
 	| Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
+	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = 
+	      compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = 
+	      compute_new_princ_type remove env (substnl [c] n b)  in
+	    new_b,
+	    list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
-    let new_e,to_remove_from_e = compute_new_princ_type remove env e
-    in
-    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
-  in
-(*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
+    let new_e,to_remove_from_e = compute_new_princ_type remove env e in
+    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc in
+  (* observe (str "Computing new principe from " 
+              ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
   let pre_res,_ = 
-    compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ 
-  in 
+    compute_new_princ_type princ_type_info.indarg_in_concl 
+      env_with_params_and_predicates pre_princ in 
   let pre_res = 
-    replace_vars 
-      (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
-      (lift (List.length ptes_vars) pre_res)
-  in
-  it_mkProd_or_LetIn  	 
+    replace_vars (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+      (lift (List.length ptes_vars) pre_res) in
+  it_mkProd_or_LetIn
     ~init:(it_mkProd_or_LetIn 
-	     ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) 
-			      new_predicates)
-	  )
+      ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) 
+	new_predicates))
     princ_type_info.params
     
   
@@ -316,16 +297,22 @@ let defined () =
 
 
 
+let build_rel_to_fun_info funs =
+  let rel2funinfoAUX = ref Link.empty in
+  let _ = 
+    Array.iteri 
+      (fun i x -> rel2funinfoAUX := Link.add i {thefun=mkConst x; theargs=[||]} !rel2funinfoAUX)
+      funs in
+  !rel2funinfoAUX
+  
+
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in 
   (*   let time1 = System.get_time ()  in *)
+  let rel2funinfo = build_rel_to_fun_info funs in
   let new_principle_type =
-    compute_new_princ_type_from_rel
-      (Array.map mkConst funs)
-      sorts
-      old_princ_type
-  in
+    compute_new_princ_type_from_rel rel2funinfo sorts old_princ_type in
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
   (*    observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
@@ -333,11 +320,9 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     next_global_ident_away true (id_of_string "___________princ_________") []
   in
   begin
-    Command.start_proof
-      new_princ_name
+    Command.start_proof new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-      new_principle_type
-      (hook new_principle_type)
+      new_principle_type (hook new_principle_type)
     ;
     (*       let _tim1 = System.get_time ()  in *)
     Pfedit.by  (proof_tac (Array.map mkConst funs) mutr_nparams);
@@ -576,10 +561,9 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     [const]
   else
     let other_fun_princ_types = 
-      let funs = Array.map mkConst this_block_funs in 
       let sorts = Array.of_list sorts in 
-      List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
-    in
+      List.map (compute_new_princ_type_from_rel (build_rel_to_fun_info this_block_funs) sorts)
+	other_princ_types in
     let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in 
     let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in 
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
index cf28c6e6c..6fa4fa70c 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/contrib/funind/functional_principles_types.mli
@@ -21,8 +21,11 @@ val generate_functional_principle :
   (constr array -> int -> Tacmach.tactic) -> 
   unit
 
-val compute_new_princ_type_from_rel : constr array -> sorts array -> 
-  types -> types
+(* TODO: hide [rel_to_fun_info] and [compute_new_princ_type_from_rel]. *)
+type rel_to_fun_info = { thefun:constr; theargs: int array }
+
+val compute_new_princ_type_from_rel : (rel_to_fun_info list) Indfun_common.Link.t
+  -> sorts array -> types -> types
 
 
 exception No_graph_found
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 78e2c4408..c02a483a1 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -3,6 +3,9 @@ open Pp
 
 open Libnames
 
+(* This map is used to deal with debruijn linked indices. *)
+module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
+
 let mk_prefix pre id = id_of_string (pre^(string_of_id id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -506,3 +509,20 @@ let do_observe () =
     
 exception Building_graph of exn 
 exception Defining_principle of exn
+
+
+(* type 'a ctactic = 'a -> Proof_type.goal Evd.sigma -> (('a * Proof_type.goal) list Evd.sigma * Proof_type.validation) *)
+open Proof_type
+open Evd
+let ctclThen (tac1:tactic) (tac2:tactic): tactic =
+  (fun g -> 
+    let _gls,_valid = tac1 g in
+    Tacticals.tclTHEN tac1 tac2 g
+  )
+(* 
+   let lres = List.map (fun g -> tac2 {it=g;sigma=sig_sig gls}) (sig_it gls) in
+   let lgls,lvalid = List.split lres in
+   let newvalid = 
+     (fun lpftree -> List.map2 (fun x y -> x y) lvalid lpftree) in
+   lgls,newvalid
+*)
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 7da1d6f0b..dd7078f4c 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -1,6 +1,9 @@
 open Names
 open Pp
 
+(* This map is used to deal with debruijn linked indices. *)
+module Link : Map.S with type key = int
+
 (* 
    The mk_?_id function build different name w.r.t. a function 
    Each of their use is justified in the code 
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index adec67e36..94bb3779d 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -21,6 +21,7 @@ open Declarations
 open Environ
 open Rawterm
 open Rawtermops
+open Functional_principles_types
 
 (** {1 Utilities}  *)
 
@@ -79,7 +80,7 @@ let next_ident_fresh (id:identifier) =
 
 (** {2 Debugging} *)
 (* comment this line to see debug msgs *)
-let msg x = () ;; let pr_lconstr c = str ""
+(* let msg x = () ;; let pr_lconstr c = str "" *)
 (* uncomment this to see debugging *)
 let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c)
 let prconstrnl c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
@@ -195,6 +196,16 @@ struct
   let fold i j = if i<j then foldup i j else folddown i j
 end
 
+(** Inductive lookup *)
+let lookup_induct_princ id: Names.constant*constr =
+  let ind_kn =
+    fst (locate_with_msg
+      (Libnames.pr_reference (Libnames.Ident (dummy_loc , id)) ++ str ": Not an inductive type!")
+      locate_ind (Libnames.Ident (dummy_loc , id))) in  
+  (* TODO: replace 0 by the mutual number *)
+  let princ = destConst (Indrec.lookup_eliminator (ind_kn,0) (InProp)) in 
+  let princ_type = Typeops.type_of_constant (Global.env()) princ in
+  princ,princ_type
 
 (** {1 Parameters shifting and linking information} *)
 
@@ -235,8 +246,6 @@ let linkmonad f lnkvar =
 
 let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar
 
-(* This map is used to deal with debruijn linked indices. *)
-module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
 
 let pr_links l = 
   Printf.printf "links:\n";
@@ -897,16 +906,12 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let _ = 
     List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in
   let _ = prstr "\nend rawlist\n" in
-(* FIX: retransformer en constr ici
-   let shift_prm = 
-    { shift_prm with
-      recprms1=prms1;
-      recprms1=prms1;    
-    } in *)
+  (* FIX: retransformer en constr ici
+     let shift_prm = { shift_prm with recprms1=prms1; recprms1=prms1; } in *)
   let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
-  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
-
+  let _ = Command.build_mutual [(indexpr,None)] true (* means: not coinductive *) in
+  ()
 
 (* Find infos on identifier id. *)
 let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
@@ -918,6 +923,7 @@ let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
     with Not_found ->
       errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
 
+
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
     [ind1] and [ind2]. identifiers occuring in both arrays [args1] and
@@ -946,7 +952,31 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
   (* setting functional results *)
   let _ = lnk1.(Array.length lnk1 - 1) <- Funres in 
   let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
-  merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id
+  let res = merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id in  
+  let princ,princ_type= lookup_induct_princ id in
+  prconstr princ_type;  
+  let argnums1 = Array.mapi (fun i _ -> i) args1 in
+  let cpt = ref 0 in
+  let argnums2 = Array.mapi 
+    (fun i x -> 
+      match x with
+        | Unlinked -> !cpt + Array.length argnums1
+        | Linked j -> j 
+        | Funres -> assert false) 
+    lnk2 in
+  let rel2funinfo = 
+    Link.add 0 { thefun = mkConst finfo2.function_constant; theargs = argnums1}
+      (Link.add 0 { thefun = mkConst finfo1.function_constant; theargs = argnums2}
+        Link.empty) in
+  let _type_scheme = 
+    Functional_principles_types.compute_new_princ_type_from_rel 
+      rel2funinfo
+      [|Termops.new_sort_in_family InProp|] (* FIXME: la sort doit être réglable *)
+      princ_type
+  in
+  prstr "AFTER COMPUTATION OF MERGED TYPE SCHEME\n";
+  (* prconstr type_scheme; *)
+  res