Intégration du Termast et du Retyping de HH, et modifications connexes

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

6 files changed, 19 insertions, 83 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 533d1f3c1..dc398cc36 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -227,77 +227,10 @@ let coe_value i =
   let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
   v,b
 
-(* pretty-print functions *)
-
-open Printer
-
-let string_of_strength = function 
-  | NeverDischarge -> "(global)"
-  | DischargeAt sp -> "(disch@"^(string_of_path sp)
-
-let print_coercion_value v = prterm v.cOE_VALUE.uj_val
-
-let print_index_coercion c = 
-  let _,v = coercion_info_from_index c in
-  print_coercion_value v
-
-let print_class i =
-  let cl,x = class_info_from_index i in
-  [< 'sTR x.cL_STR >]
-  
-let print_path ((i,j),p) = 
-  [< 'sTR"["; 
-     prlist_with_sep (fun () -> [< 'sTR"; " >])
-       (fun c ->  print_index_coercion c) p;
-     'sTR"] : "; print_class i; 'sTR" >-> ";
-     print_class j >]
-
-let print_graph () = 
-  [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >]
-
-let print_classes () = 
-  [< prlist_with_sep pr_spc
-       (fun (_,(cl,x)) -> 
-          [< 'sTR x.cL_STR  (*; 'sTR(string_of_strength x.cL_STRE) *) >]) 
-       (!cLASSES) >]
-
-let print_coercions () = 
-  [< prlist_with_sep pr_spc
-       (fun (_,(_,v)) -> [< print_coercion_value v >]) (!cOERCIONS) >]
-  
-let cl_of_id id = 
-  match string_of_id id with
-    | "FUNCLASS" -> CL_FUN
-    | "SORTCLASS" -> CL_SORT
-    | _ -> let v = Declare.global_reference CCI id in
-	   let cl,_ = constructor_at_head v in 
-	   cl
-
-let index_cl_of_id id =
-  try 
-    let cl = cl_of_id id in
-    let i,_=class_info cl in 
-    i
-  with _ -> 
-    errorlabstrm "index_cl_of_id"
-      [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
-
-let print_path_between ids idt = 
-  let i = (index_cl_of_id ids) in
-  let j = (index_cl_of_id idt) in
-  let p = 
-    try 
-      lookup_path_between (i,j) 
-    with _ -> 
-      errorlabstrm "index_cl_of_id"
-        [< 'sTR"No path between ";'sTR(string_of_id ids); 
-	   'sTR" and ";'sTR(string_of_id ids) >]
-  in
-  print_path ((i,j),p)
-
+(* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
  
-let message_ambig l =
+let message_ambig l = 
   [< 'sTR"Ambiguous paths : ";
      prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >]
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8c2f84887..709b26b85 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -43,7 +43,9 @@ type inheritance_path = int list
 
 val cte_of_constr : constr -> cte_typ
 val class_info : cl_typ -> (int * cl_info_typ)
+val class_info_from_index : int -> cl_typ * cl_info_typ
 val coercion_info : coe_typ -> (int * coe_info_typ)
+val coercion_info_from_index : int -> coe_typ * coe_info_typ
 val constructor_at_head : constr -> cl_typ * int
 val class_of : env -> 'c evar_map -> constr -> constr * int
 val class_args_of : constr -> constr list
@@ -55,10 +57,6 @@ val lookup_path_between : (int * int) -> inheritance_path
 val lookup_path_to_fun_from : int -> inheritance_path
 val lookup_path_to_sort_from : int -> inheritance_path
 val coe_value : int -> (unsafe_judgment * bool)
-val print_graph : unit -> (int * string) Pp.ppcmd_token Stream.t
-val print_classes : unit -> (int * string) Pp.ppcmd_token Stream.t
-val print_coercions : unit -> (int * string) Pp.ppcmd_token Stream.t
-val print_path_between : identifier -> identifier -> (int * string) ppcmd_token Stream.t
 val arity_sort : constr -> int
 val fully_applied : identifier -> int -> int -> unit
 val stre_of_cl : cl_typ -> strength
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 500e6bfe7..96e97a040 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -328,7 +328,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	check_cofix env !isevars cofix;
 	make_judge cofix lara.(i))
 
-| RSort (loc,RProp c) -> make_judge_of_prop_contents c
+| RSort (loc,RProp c) -> judge_of_prop_contents c
 
 | RSort (loc,RType) -> 
     { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort }
@@ -424,7 +424,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
        uj_kind = snd (splay_prod env !isevars evalPt)}
 
 | RCases (loc,prinfo,po,tml,eqns) ->
-    Multcase.compile_multcase
+    Cases.compile_multcase
       ((fun vtyc env -> pretype vtyc env isevars),isevars)
       vtcon env (po,tml,eqns)
 
@@ -473,6 +473,11 @@ let j_apply f env sigma j =
        variables du sigma original. il faudrait que la fonction de typage
        retourne aussi le nouveau sigma...
 *)
+let ise_resolve_casted sigma env typ c =
+  let isevars = ref sigma in
+  let j = unsafe_fmachine (mk_tycon typ) false isevars [] env c in
+  (j_apply (fun _ -> process_evars true) env !isevars j).uj_val
+
 let ise_resolve fail_evar sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine mt_tycon false isevars metamap env c in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 995779783..c22653dab 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -49,6 +49,9 @@ val ise_resolve_type : bool -> unit evar_map -> (int * constr) list ->
  * if we must coerce to a type *)
 val ise_resolve1 : bool -> unit evar_map -> env -> rawconstr -> constr
 
+val ise_resolve_casted : unit evar_map -> env -> 
+  constr -> rawconstr -> constr
+
 (* progmach.ml tries to type ill-typed terms: does not perform the conversion
  * test in application.
  *)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 03d0d6e47..29fdf560c 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -11,12 +11,9 @@ open Type_errors
 
 type loc = int * int
 
-type inductive_key = section_path * int
-type constructor_key = inductive_key * int
-
 type pattern =  (* locs here refers to the ident's location, not whole pat *)
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_key * identifier list) * pattern list
+  | PatCstr of loc * (constructor_path * identifier list) * pattern list
   | PatAs of loc * identifier * pattern
 
 type binder_kind = BProd | BLambda
@@ -25,8 +22,8 @@ type rawsort = RProp of Term.contents | RType
 
 type reference =
   | RConst of section_path * identifier list
-  | RInd of inductive_key * identifier list
-  | RConstruct of constructor_key * identifier list
+  | RInd of inductive_path * identifier list
+  | RConstruct of constructor_path * identifier list
   | RAbst of section_path
   | RVar of identifier
   | REVar of int * identifier list
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 44af99e19..af922be37 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -73,10 +73,10 @@ let rec execute mf env sigma cstr =
 	make_judge cofix larv.(i)
 	  
     | IsSort (Prop c) -> 
-	make_judge_of_prop_contents c
+	judge_of_prop_contents c
 
     | IsSort (Type u) ->
-	let (j,_) = make_judge_of_type u in j
+	let (j,_) = judge_of_type u in j
 	  
     | IsAppL (f,args) ->
 	let j = execute mf env sigma f in