diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 26 | ||||
| -rw-r--r-- | contrib/funind/merge.ml | 30 |
2 files changed, 30 insertions, 26 deletions
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 26a1066c0..afc78fec0 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -443,25 +443,13 @@ VERNAC COMMAND EXTEND Showindinfo END VERNAC COMMAND EXTEND MergeFunind - [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] -> + [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" + "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> [ - let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in - let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in - let id1,args1 = - try - let hd,args = destApp c1 in - if Term.isInd hd then hd , args - else raise (Util.error "Ill-formed (fst) argument") - with Invalid_argument _ - -> Util.error ("Bad argument form for merging schemes") in - let id2,args2 = - try - let hd,args = destApp c2 in - if isInd hd then hd , args - else raise (Util.error "Ill-formed (snd) argument") - with Invalid_argument _ - -> Util.error ("Bad argument form for merging schemes") in - (* TOFO: enlever le ignore et declarer l'inductif *) - ignore(Merge.merge c1 c2 args1 args2 id) + let _ = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Util.dummy_loc,id1))) in + let _ = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Util.dummy_loc,id2)))in + Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id ] END diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index 5ec600a47..376e6e5f5 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -10,6 +10,7 @@ (*i $Id: i*) +open Indfun_common open Util open Topconstr open Vernacexpr @@ -78,7 +79,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") @@ -797,11 +798,26 @@ let merge_inductive (ind1: inductive) (ind2: inductive) Command.build_mutual [(indexpr,None)] true (* means: not coinductive *) +let kn_of_id id = + let f_ref = Libnames.Ident (dummy_loc,id) in + locate_with_msg (Libnames.pr_reference f_ref ++ str ": Not found!") + locate_constant + f_ref -let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) id = - let env = Global.env() in - let ind1,_cstrlist1 = Inductiveops.find_inductive env Evd.empty cstr1 in - let ind2,_cstrlist2 = Inductiveops.find_inductive env Evd.empty cstr2 in + + +let merge (id1:identifier) (id2:identifier) (args1:identifier array) + (args2:identifier array) id = + let kn1 = kn_of_id id1 in + let kn2 = kn_of_id id2 in + let finfo1 = + try find_Function_infos kn1 + with Not_found -> errorlabstrm "indfun" (Nameops.pr_id id1 ++ str " unknown") in + let finfo2 = + try find_Function_infos kn2 + with Not_found -> errorlabstrm "indfun" (Nameops.pr_id id2 ++ str " unknown") in + let ind1 = finfo1.graph_ind in + let ind2 = finfo2.graph_ind in let lnk1 = (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *) Array.mapi (fun i c -> Unlinked) args1 in let _ = lnk1.(Array.length lnk1 - 1) <- Funres in (* last arg is functional result *) @@ -814,8 +830,8 @@ let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array | None -> Unlinked) args2 in let _ = lnk2.(Array.length lnk2 - 1) <- Funres in (* last arg is functional result *) - let resa = merge_inductive ind1 ind2 lnk1 lnk2 id in - resa + let _ = merge_inductive ind1 ind2 lnk1 lnk2 id in + () |