← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to plugins/funind/rawterm_to_relation.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/funind/rawterm_to_relation.ml
716
716
        *)
717
717
        let case_resl =
718
718
            List.fold_right
719
 
            (fun (case_arg,_) ctxt_argsl ->
720
 
               let arg_res = build_entry_lc env funname avoid case_arg  in
721
 
               combine_results combine_args arg_res ctxt_argsl
722
 
            )
723
 
            el
 
719
              (fun (case_arg,_) ctxt_argsl ->
 
720
                let arg_res = build_entry_lc env funname avoid case_arg  in
 
721
                combine_results combine_args arg_res ctxt_argsl
 
722
              )
 
723
              el
724
724
              (mk_result [] [] avoid)
725
725
        in
726
726
        let types =
876
876
  with Invalid_argument _ -> false
877
877
 
878
878
 
 
879
 
 
880
let same_raw_term rt1 rt2 = 
 
881
  match rt1,rt2 with 
 
882
    | RRef(_,r1), RRef (_,r2) -> r1=r2
 
883
    | RHole _, RHole _ -> true
 
884
    | _ -> false
 
885
let decompose_raw_eq lhs rhs = 
 
886
  let rec decompose_raw_eq lhs rhs acc = 
 
887
    observe (str "decomposing eq for " ++ pr_rawconstr lhs ++ str " " ++ pr_rawconstr rhs);
 
888
    let (rhd,lrhs) = raw_decompose_app rhs in 
 
889
    let (lhd,llhs) = raw_decompose_app lhs in 
 
890
    observe (str "lhd := " ++ pr_rawconstr lhd);
 
891
    observe (str "rhd := " ++ pr_rawconstr rhd);
 
892
    observe (str "llhs := " ++ int (List.length llhs));
 
893
    observe (str "lrhs := " ++ int (List.length lrhs));
 
894
    let sllhs = List.length llhs in 
 
895
    let slrhs = List.length lrhs in 
 
896
    if same_raw_term lhd rhd && sllhs = slrhs 
 
897
    then
 
898
      (* let _ = assert false in  *)
 
899
      List.fold_right2 decompose_raw_eq llhs lrhs acc
 
900
    else (lhs,rhs)::acc
 
901
  in
 
902
  decompose_raw_eq lhs rhs []
 
903
     
 
904
 
879
905
exception Continue
880
906
(*
881
907
   The second phase which reconstruct the real type of the constructor.
1032
1058
                     mkRProd(n,t,new_b),id_to_exclude
1033
1059
                     else new_b, Idset.add id id_to_exclude
1034
1060
                  *)
 
1061
            | RApp(loc1,RRef(loc2,eq_as_ref),[ty;rt1;rt2])
 
1062
                when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
 
1063
                  ->
 
1064
              begin
 
1065
                try 
 
1066
                  let l = decompose_raw_eq rt1 rt2 in 
 
1067
                  if List.length l > 1 
 
1068
                  then 
 
1069
                    let new_rt =
 
1070
                      List.fold_left 
 
1071
                        (fun acc (lhs,rhs) -> 
 
1072
                          mkRProd(Anonymous,
 
1073
                                  mkRApp(mkRRef(eq_as_ref),[mkRHole ();lhs;rhs]),acc)
 
1074
                        )
 
1075
                        b
 
1076
                        l
 
1077
                    in
 
1078
                    rebuild_cons env nb_args relname args crossed_types depth new_rt
 
1079
                  else raise Continue
 
1080
              with Continue -> 
 
1081
                observe (str "computing new type for prod : " ++ pr_rawconstr rt);
 
1082
                let t' = Pretyping.Default.understand Evd.empty env t in
 
1083
                let new_env = Environ.push_rel (n,None,t') env in
 
1084
                let new_b,id_to_exclude =
 
1085
                  rebuild_cons new_env
 
1086
                    nb_args relname
 
1087
                    args new_crossed_types
 
1088
                    (depth + 1) b
 
1089
                in
 
1090
                match n with
 
1091
                  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
 
1092
                      new_b,Idset.remove id
 
1093
                        (Idset.filter not_free_in_t id_to_exclude)
 
1094
                  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 
1095
              end
1035
1096
            | _ ->
1036
1097
                observe (str "computing new type for prod : " ++ pr_rawconstr rt);
1037
1098
                let t' = Pretyping.Default.understand Evd.empty env t in
1122
1183
 
1123
1184
(* debuging wrapper *)
1124
1185
let rebuild_cons env nb_args relname args crossed_types rt =
1125
 
(*   observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++  *)
1126
 
(*               str "nb_args := " ++ str (string_of_int nb_args)); *)
 
1186
  observe  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++
 
1187
                 str "nb_args := " ++ str (string_of_int nb_args));
1127
1188
  let res =
1128
1189
    rebuild_cons env nb_args relname args crossed_types 0 rt
1129
1190
  in
1130
 
(*   observe (str " leads to "++ pr_rawconstr (fst res)); *)
 
1191
  observe (str " leads to "++ pr_rawconstr (fst res));
1131
1192
  res
1132
1193
 
1133
1194
 
1266
1327
      (function result (* (args',concl') *) ->
1267
1328
         let rt = compose_raw_context result.context result.value in
1268
1329
         let nb_args = List.length funsargs.(i) in
1269
 
         (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
 
1330
          (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
1270
1331
         fst (
1271
1332
           rebuild_cons env_with_graphs nb_args relnames.(i)
1272
1333
             []