From: Claudio Sacerdoti Coen Date: Fri, 23 Sep 2005 12:45:32 +0000 (+0000) Subject: The disambiguation now returns the aliases diff. It used to return the X-Git-Tag: LAST_BEFORE_NEW~46 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2751c5d09df1148706c65de38a9a4946687d4589;p=helm.git The disambiguation now returns the aliases diff. It used to return the new aliases and a slow diff operation was performed later on. --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b66e12d5e..e9ce2e81c 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -638,7 +638,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term -> - (environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term* CicUniv.universe_graph) list * (* disambiguated term *) @@ -651,7 +651,7 @@ sig universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> - (environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * CicUniv.universe_graph) list * (* disambiguated obj *) @@ -790,12 +790,12 @@ in refine_profiler.CicUtil.profile foo () | Invalid_choice -> Ko, ugraph in (* (4) build all possible interpretations *) - let rec aux aliases todo_dom base_univ = + let rec aux aliases diff todo_dom base_univ = match todo_dom with | [] -> (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ aliases, metasenv, thing, new_univ ] + [ aliases, diff, metasenv, thing, new_univ ] | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" @@ -806,16 +806,17 @@ in refine_profiler.CicUtil.profile foo () | codomain_item :: tl -> debug_print (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ; let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in (match test_env new_env remaining_dom univ with | Ok (thing, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, metasenv, thing, new_univ ] - | _ -> aux new_env remaining_dom new_univ )@ + | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] + | _ -> aux new_env new_diff remaining_dom new_univ )@ filter univ tl | Uncertain,new_univ -> (match remaining_dom with | [] -> [] - | _ -> aux new_env remaining_dom new_univ )@ + | _ -> aux new_env new_diff remaining_dom new_univ )@ filter univ tl | Ko,_ -> filter univ tl) in @@ -824,16 +825,16 @@ in refine_profiler.CicUtil.profile foo () let base_univ = initial_ugraph in try let res = - match aux aliases todo_dom base_univ with + match aux aliases [] todo_dom base_univ with | [] -> raise NoWellTypedInterpretation - | [ e,me,t,u ] -> + | [_,diff,metasenv,t,ugraph] -> debug_print (lazy "SINGLE INTERPRETATION"); - [ e,me,t,u ], false + [diff,metasenv,t,ugraph], false | l -> debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map - (fun (env, _, _, _) -> + (fun (env, _, _, _, _) -> List.map (fun domain_item -> let description = @@ -844,19 +845,10 @@ in refine_profiler.CicUtil.profile foo () l in let choosed = C.interactive_interpretation_choice choices in - (List.map (List.nth l) choosed), true + (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed), + true in -(* - (if benchmark then - let res_size = List.length res in - debug_print (lazy (sprintf - ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^ - "BENCHMARK: estimated %.2f") - !actual_refinements !max_refinements !domain_size res_size - !choices_avg - (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)))); -*) - res + res with CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 87e09daef..1c6d4bbe7 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -46,7 +46,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> DisambiguateTypes.term -> - (DisambiguateTypes.environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term * CicUniv.universe_graph) list * (* disambiguated term *) @@ -60,7 +60,7 @@ sig universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> - (DisambiguateTypes.environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * CicUniv.universe_graph) list * (* disambiguated obj *) @@ -83,7 +83,7 @@ sig ?initial_ugraph:CicUniv.universe_graph -> ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*) string -> - (DisambiguateTypes.environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term * CicUniv.universe_graph) list (* disambiguated term *)