]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_refiner/nCicCoercion.ml
freescale porting, work in progress
[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
13
14 let debug s = prerr_endline (Lazy.force s);;
15 let debug _ = ();;
16
17 module COT : Set.OrderedType with type t = NCic.term * int * int = 
18   struct
19         type t = NCic.term * int * int
20         let compare = Pervasives.compare
21   end
22
23 module CoercionSet = Set.Make(COT)
24
25 module DB = 
26   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
27
28 type db = DB.t * DB.t
29
30 let empty_db = DB.empty,DB.empty
31
32 class status =
33  object
34   val db = empty_db
35   method coerc_db = db
36   method set_coerc_db v = {< db = v >}
37   method set_coercion_status
38    : 'status. < coerc_db : db; .. > as 'status -> 'self
39    = fun o -> {< db = o#coerc_db >}
40  end
41
42 let index_coercion status c src tgt arity arg =
43   let db_src,db_tgt = status#coerc_db in
44   let data = (c,arity,arg) in
45
46   debug (lazy ("INDEX:" ^ 
47     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
48     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
49     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ 
50     string_of_int arg ^ " " ^ string_of_int arity));
51
52   let db_src = DB.index db_src src data in
53   let db_tgt = DB.index db_tgt tgt data in
54   status#set_coerc_db (db_src, db_tgt)
55 ;;
56
57 let index_old_db odb (status : #status) =
58   List.fold_left 
59     (fun status (_,tgt,clist) -> 
60        List.fold_left 
61          (fun status (uri,_,arg) ->
62            try
63             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
64             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
65             let src, tgt = 
66               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
67               let scty, metasenv,_ = 
68                 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
69               in
70               match scty with
71               | NCic.Prod (_, src, tgt) -> 
72                  let tgt =
73                    NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
74                  in
75 (*
76             debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s" 
77               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
78               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
79               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
80 *)
81                 src, tgt
82               | t -> 
83                   debug (lazy (
84                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
85                   assert false
86             in
87             index_coercion status c src tgt arity arg
88            with 
89            | NCicEnvironment.BadDependency _ 
90            | NCicTypeChecker.TypeCheckerFailure _ -> status)
91          status clist)
92     status (CoercDb.to_list odb)
93 ;;
94
95 let look_for_coercion status metasenv subst context infty expty =
96  let db_src,db_tgt = status#coerc_db in
97   match infty, expty with
98   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
99     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
100   | _ ->
101
102     debug (lazy ("LOOK FOR COERCIONS: " ^ 
103       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
104       NCicPp.ppterm ~metasenv ~subst ~context expty));
105
106     let set_src = DB.retrieve_unifiables db_src infty in
107     let set_tgt = DB.retrieve_unifiables db_tgt expty in
108     let candidates = CoercionSet.inter set_src set_tgt in
109
110     debug (lazy ("CANDIDATES: " ^ 
111       String.concat "," (List.map (fun (t,_,_) ->
112         NCicPp.ppterm ~metasenv ~subst ~context t) 
113       (CoercionSet.elements candidates))));
114
115     List.map
116       (fun (t,arity,arg) ->
117           let ty =
118             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
119             with NCicTypeChecker.TypeCheckerFailure s ->
120              prerr_endline ("illtyped coercion: "^Lazy.force s);
121              prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
122              assert false
123           in
124           let ty, metasenv, args = 
125            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
126           in
127
128           debug (lazy (
129             NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
130             NCicPp.ppterm ~metasenv ~subst ~context
131             (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
132               string_of_int (List.length args) ^ " == " ^ string_of_int arg)); 
133              
134           metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
135       (CoercionSet.elements candidates)
136 ;;
137
138 (* CSC: very inefficient implementation!
139    Enrico, can we use a discrimination tree here? *)
140 let match_coercion status ~metasenv ~subst ~context t =
141  let db =
142   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
143  in
144     (HExtlib.list_findopt
145       (fun (p,arity,cpos) _ ->
146         try
147          let t =
148           match p,t with
149              NCic.Appl lp, NCic.Appl lt ->
150               (match fst (HExtlib.split_nth (List.length lp) lt) with
151                   [t] -> t
152                 | l -> NCic.Appl l)
153            | _,NCic.Appl (he::_) -> he
154            | _,_ -> t
155          in
156          let b = NCicReduction.alpha_eq metasenv subst context p t in
157          if not b then None else
158          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
159          let pis = 
160            let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
161            aux ty
162          in
163          Some (p,pis - arity - cpos - 1,cpos)
164         with
165          Failure _ -> None (* raised by split_nth *)
166       ) db)
167 ;;