From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 13:08:25 +0000 (+0000) Subject: Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc. X-Git-Tag: LucaOK~57 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=264523336352a5241b747b7e04b33630f6010aeb Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc. --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index e6194df96..d629a155e 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,9 +1,5 @@ proofEngine.cmo: proofEngine.cmi proofEngine.cmx: proofEngine.cmi -eta_fixing.cmo: eta_fixing.cmi -eta_fixing.cmx: eta_fixing.cmi -content2cic.cmo: content2cic.cmi -content2cic.cmx: content2cic.cmi logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi disambiguate.cmo: disambiguate.cmi @@ -24,9 +20,7 @@ invokeTactics.cmi: termEditor.cmi termViewer.cmi hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi hbugs.cmi: invokeTactics.cmi -gTopLevel.cmo: eta_fixing.cmi hbugs.cmi invokeTactics.cmi \ - logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi \ - texTermEditor.cmi -gTopLevel.cmx: eta_fixing.cmx hbugs.cmx invokeTactics.cmx \ - logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx \ - texTermEditor.cmx +gTopLevel.cmo: hbugs.cmi invokeTactics.cmi logicalOperations.cmi \ + proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi +gTopLevel.cmx: hbugs.cmx invokeTactics.cmx logicalOperations.cmx \ + proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml deleted file mode 100644 index e8a95fc89..000000000 --- a/helm/gTopLevel/content2cic.ml +++ /dev/null @@ -1,161 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(***************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 17/06/2003 *) -(* *) -(***************************************************************************) - -exception TO_DO;; - -let proof2cic term2cic p = - let rec proof2cic premise_env p = - let module C = Cic in - let module Con = Content in - let rec extend_premise_env current_env = - function - [] -> current_env - | p::atl -> - extend_premise_env - ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in - let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in - let body = conclude2cic new_premise_env p.Con.proof_conclude in - context2cic premise_env p.Con.proof_context body - - and context2cic premise_env context body = - List.fold_right (ce2cic premise_env) context body - - and ce2cic premise_env ce target = - let module C = Cic in - let module Con = Content in - match ce with - `Declaration d -> - (match d.Con.dec_name with - Some s -> - C.Lambda (C.Name s, term2cic d.Con.dec_type, target) - | None -> - C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target)) - | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> - C.Lambda (C.Name s, term2cic h.Con.dec_type, target) - | None -> - C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target)) - | `Proof p -> - (match p.Con.proof_name with - Some s -> - C.LetIn (C.Name s, proof2cic premise_env p, target) - | None -> - C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | `Definition d -> - (match d.Con.def_name with - Some s -> - C.LetIn (C.Name s, proof2cic premise_env p, target) - | None -> - C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | `Joint ho -> - raise TO_DO - - and conclude2cic premise_env conclude = - let module C = Cic in - let module Con = Content in - if conclude.Con.conclude_method = "TD_Conversion" then - (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2cic [] p (* empty! *) - | _ -> prerr_endline "1"; assert false) - else if conclude.Con.conclude_method = "BU_Conversion" then - (match conclude.Con.conclude_args with - [Con.Premise prem] -> - (try List.assoc prem.Con.premise_xref premise_env - with Not_found -> - prerr_endline ("Not_found: " ^ prem.Con.premise_xref); - raise Not_found) - | _ -> prerr_endline "2"; assert false) - else if conclude.Con.conclude_method = "Exact" then - (match conclude.Con.conclude_args with - [Con.Term t] -> term2cic t - | _ -> prerr_endline "3"; assert false) - else if conclude.Con.conclude_method = "Intros+LetTac" then - (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2cic [] p (* empty! *) - | _ -> prerr_endline "4"; assert false) - else if (conclude.Con.conclude_method = "ByInduction") then - (match (List.tl conclude.Con.conclude_args) with - Con.Term (C.AAppl - id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args -> - let subst = - List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in - let cargs = args2cic premise_env args in - let cparams_and_IP = List.map term2cic params_and_IP in - C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs) - | _ -> prerr_endline "5"; assert false) - else if (conclude.Con.conclude_method = "Rewrite") then - (match conclude.Con.conclude_args with - Con.Term (C.AConst (sid,uri,exp_named_subst))::args -> - let subst = - List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in - let cargs = args2cic premise_env args in - C.Appl (C.Const(uri,subst)::cargs) - | _ -> prerr_endline "6"; assert false) - else if (conclude.Con.conclude_method = "Apply") then - let cargs = (args2cic premise_env conclude.Con.conclude_args) in - C.Appl cargs - else (prerr_endline "7"; assert false) - - and args2cic premise_env l = - List.map (arg2cic premise_env) l - - and arg2cic premise_env = - let module C = Cic in - let module Con = Content in - function - Con.Aux n -> prerr_endline "8"; assert false - | Con.Premise prem -> - (match prem.Con.premise_n with - Some n -> - C.Rel n - | _ -> - (try List.assoc prem.Con.premise_xref premise_env - with Not_found -> - prerr_endline ("Not_found: " ^ prem.Con.premise_xref); - raise Not_found)) - | Con.Term t -> - term2cic t - | Con.ArgProof p -> - proof2cic [] p (* empty! *) - | Con.ArgMethod s -> raise TO_DO - -in proof2cic [] p -;; - - - - - - diff --git a/helm/gTopLevel/content2cic.mli b/helm/gTopLevel/content2cic.mli deleted file mode 100644 index 74d530182..000000000 --- a/helm/gTopLevel/content2cic.mli +++ /dev/null @@ -1,37 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 27/6/2003 *) -(* *) -(**************************************************************************) - -val proof2cic : - (Cic.annterm -> Cic.term) -> - Cic.annterm Content.proof -> Cic.term diff --git a/helm/gTopLevel/eta_fixing.ml b/helm/gTopLevel/eta_fixing.ml deleted file mode 100644 index c3b84b605..000000000 --- a/helm/gTopLevel/eta_fixing.ml +++ /dev/null @@ -1,191 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception ReferenceToVariable;; -exception RferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; - -let rec fix_lambdas_wrt_type ty te = - let module C = Cic in - let module S = CicSubstitution in -(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); - flush stderr ; *) - (* cast e altra porcheria ???? *) - match ty,te with - C.Prod (_,_,ty'), C.Lambda (n,s,te') -> - C.Lambda (n,s,fix_lambdas_wrt_type ty' te') - | C.Prod (_,s,ty'), C.Appl l -> - prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); - flush stderr ; - let l' = List.map (S.lift 1) l in - C.Lambda (C.Name "x",s, - fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1]))) - | C.Prod (_,s,ty'), _ -> - prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); - flush stderr ; - let te' = S.lift 1 te in - C.Lambda (C.Name "x",s, - fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1])) - | _, _ -> te -;; - -let fix_according_to_type ty hd tl = - let module C = Cic in - let module S = CicSubstitution in - let rec aux ty tl res = - (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); - flush stderr ; *) - match ty with - C.Rel _ - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit -> - (match tl with - [] -> C.Appl res - | _ -> - prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); - flush stderr ; - C.LetIn - (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) - | C.Cast (v,t) -> aux v tl res - | C.Prod (n,s,t) -> - (match tl with - [] -> - prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); - flush stderr ; - let res' = List.map (S.lift 1) res - in - C.Lambda - (C.Name "x", (* Andrea: to do: generate a fresh name *) - s, - aux t [] (res'@[C.Rel 1])) - | hd::tl' -> - let hd' = fix_lambdas_wrt_type s hd - in - aux (S.subst hd' t) tl' (res@[hd'])) - | C.Lambda _ -> assert false - | C.LetIn (n,s,t) -> aux (S.subst s t) tl res - | C.Appl _ - | C.Const _ - | C.MutInd _ - | C.MutConstruct _ - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> (* ???? *) - (match tl with - [] -> C.Appl res - | _ -> (* Andrea: to do: generate a fresh name *) - C.LetIn - (C.Name "H", - C.Appl res, - C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) - in - aux ty tl [hd] -;; - -let eta_fix metasenv t = - let rec eta_fix' t = -(* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); - flush stderr ; *) - let module C = Cic in - match t with - C.Rel n -> C.Rel n - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' t)) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (n,l) -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - let l' = - List.map2 - (fun ct t -> - match (ct, t) with - None, _ -> None - | _, Some t -> Some (eta_fix' t) - | Some _, None -> assert false (* due to typing rules *)) - canonical_context l - in - C.Meta (n,l') - | C.Sort s -> C.Sort s - | C.Implicit -> C.Implicit - | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t) - | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t) - | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t) - | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t) - | C.Appl l -> - let l' = List.map eta_fix' l - in - (match l' with - C.Const(uri,exp_named_subst)::l'' -> - let constant_type = - (match CicEnvironment.get_obj uri with - C.Constant (_,_,ty,_) -> ty - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - in - fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' - | _ -> C.Appl l' ) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' t)) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' t)) exp_named_subst - in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri, tyno, outty, term, patterns) -> - C.MutCase (uri, tyno, eta_fix' outty, - eta_fix' term, List.map eta_fix' patterns) - | C.Fix (funno, funs) -> - C.Fix (funno, - List.map - (fun (name, no, ty, bo) -> - (name, no, eta_fix' ty, eta_fix' bo)) funs) - | C.CoFix (funno, funs) -> - C.CoFix (funno, - List.map - (fun (name, ty, bo) -> - (name, eta_fix' ty, eta_fix' bo)) funs) - in - eta_fix' t -;; - diff --git a/helm/gTopLevel/eta_fixing.mli b/helm/gTopLevel/eta_fixing.mli deleted file mode 100644 index 6da260aab..000000000 --- a/helm/gTopLevel/eta_fixing.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val eta_fix : Cic.metasenv -> Cic.term -> Cic.term - - diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend index 1ec905424..d12896d47 100644 --- a/helm/ocaml/cic_omdoc/.depend +++ b/helm/ocaml/cic_omdoc/.depend @@ -1,4 +1,7 @@ contentPp.cmi: content.cmi +content2cic.cmi: content.cmi +eta_fixing.cmo: eta_fixing.cmi +eta_fixing.cmx: eta_fixing.cmi doubleTypeInference.cmo: doubleTypeInference.cmi doubleTypeInference.cmx: doubleTypeInference.cmi cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi @@ -7,3 +10,5 @@ content.cmo: content.cmi content.cmx: content.cmi contentPp.cmo: content.cmi contentPp.cmi contentPp.cmx: content.cmx contentPp.cmi +content2cic.cmo: content.cmi content2cic.cmi +content2cic.cmx: content.cmx content2cic.cmi diff --git a/helm/ocaml/cic_omdoc/Makefile b/helm/ocaml/cic_omdoc/Makefile index 0fbb566ae..e1e081ac6 100644 --- a/helm/ocaml/cic_omdoc/Makefile +++ b/helm/ocaml/cic_omdoc/Makefile @@ -2,8 +2,8 @@ PACKAGE = cic_omdoc REQUIRES = helm-cic_proof_checking PREDICATES = -INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli content.mli \ - contentPp.mli +INTERFACE_FILES = eta_fixing.mli doubleTypeInference.mli cic2acic.mli \ + content.mli contentPp.mli content2cic.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = \ diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml new file mode 100644 index 000000000..e8a95fc89 --- /dev/null +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -0,0 +1,161 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 17/06/2003 *) +(* *) +(***************************************************************************) + +exception TO_DO;; + +let proof2cic term2cic p = + let rec proof2cic premise_env p = + let module C = Cic in + let module Con = Content in + let rec extend_premise_env current_env = + function + [] -> current_env + | p::atl -> + extend_premise_env + ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in + let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in + let body = conclude2cic new_premise_env p.Con.proof_conclude in + context2cic premise_env p.Con.proof_context body + + and context2cic premise_env context body = + List.fold_right (ce2cic premise_env) context body + + and ce2cic premise_env ce target = + let module C = Cic in + let module Con = Content in + match ce with + `Declaration d -> + (match d.Con.dec_name with + Some s -> + C.Lambda (C.Name s, term2cic d.Con.dec_type, target) + | None -> + C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target)) + | `Hypothesis h -> + (match h.Con.dec_name with + Some s -> + C.Lambda (C.Name s, term2cic h.Con.dec_type, target) + | None -> + C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target)) + | `Proof p -> + (match p.Con.proof_name with + Some s -> + C.LetIn (C.Name s, proof2cic premise_env p, target) + | None -> + C.LetIn (C.Anonymous, proof2cic premise_env p, target)) + | `Definition d -> + (match d.Con.def_name with + Some s -> + C.LetIn (C.Name s, proof2cic premise_env p, target) + | None -> + C.LetIn (C.Anonymous, proof2cic premise_env p, target)) + | `Joint ho -> + raise TO_DO + + and conclude2cic premise_env conclude = + let module C = Cic in + let module Con = Content in + if conclude.Con.conclude_method = "TD_Conversion" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2cic [] p (* empty! *) + | _ -> prerr_endline "1"; assert false) + else if conclude.Con.conclude_method = "BU_Conversion" then + (match conclude.Con.conclude_args with + [Con.Premise prem] -> + (try List.assoc prem.Con.premise_xref premise_env + with Not_found -> + prerr_endline ("Not_found: " ^ prem.Con.premise_xref); + raise Not_found) + | _ -> prerr_endline "2"; assert false) + else if conclude.Con.conclude_method = "Exact" then + (match conclude.Con.conclude_args with + [Con.Term t] -> term2cic t + | _ -> prerr_endline "3"; assert false) + else if conclude.Con.conclude_method = "Intros+LetTac" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2cic [] p (* empty! *) + | _ -> prerr_endline "4"; assert false) + else if (conclude.Con.conclude_method = "ByInduction") then + (match (List.tl conclude.Con.conclude_args) with + Con.Term (C.AAppl + id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args -> + let subst = + List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in + let cargs = args2cic premise_env args in + let cparams_and_IP = List.map term2cic params_and_IP in + C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs) + | _ -> prerr_endline "5"; assert false) + else if (conclude.Con.conclude_method = "Rewrite") then + (match conclude.Con.conclude_args with + Con.Term (C.AConst (sid,uri,exp_named_subst))::args -> + let subst = + List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in + let cargs = args2cic premise_env args in + C.Appl (C.Const(uri,subst)::cargs) + | _ -> prerr_endline "6"; assert false) + else if (conclude.Con.conclude_method = "Apply") then + let cargs = (args2cic premise_env conclude.Con.conclude_args) in + C.Appl cargs + else (prerr_endline "7"; assert false) + + and args2cic premise_env l = + List.map (arg2cic premise_env) l + + and arg2cic premise_env = + let module C = Cic in + let module Con = Content in + function + Con.Aux n -> prerr_endline "8"; assert false + | Con.Premise prem -> + (match prem.Con.premise_n with + Some n -> + C.Rel n + | _ -> + (try List.assoc prem.Con.premise_xref premise_env + with Not_found -> + prerr_endline ("Not_found: " ^ prem.Con.premise_xref); + raise Not_found)) + | Con.Term t -> + term2cic t + | Con.ArgProof p -> + proof2cic [] p (* empty! *) + | Con.ArgMethod s -> raise TO_DO + +in proof2cic [] p +;; + + + + + + diff --git a/helm/ocaml/cic_omdoc/content2cic.mli b/helm/ocaml/cic_omdoc/content2cic.mli new file mode 100644 index 000000000..74d530182 --- /dev/null +++ b/helm/ocaml/cic_omdoc/content2cic.mli @@ -0,0 +1,37 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(**************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 27/6/2003 *) +(* *) +(**************************************************************************) + +val proof2cic : + (Cic.annterm -> Cic.term) -> + Cic.annterm Content.proof -> Cic.term diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml new file mode 100644 index 000000000..c3b84b605 --- /dev/null +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -0,0 +1,191 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception ReferenceToVariable;; +exception RferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; + +let rec fix_lambdas_wrt_type ty te = + let module C = Cic in + let module S = CicSubstitution in +(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + flush stderr ; *) + (* cast e altra porcheria ???? *) + match ty,te with + C.Prod (_,_,ty'), C.Lambda (n,s,te') -> + C.Lambda (n,s,fix_lambdas_wrt_type ty' te') + | C.Prod (_,s,ty'), C.Appl l -> + prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + flush stderr ; + let l' = List.map (S.lift 1) l in + C.Lambda (C.Name "x",s, + fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1]))) + | C.Prod (_,s,ty'), _ -> + prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + flush stderr ; + let te' = S.lift 1 te in + C.Lambda (C.Name "x",s, + fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1])) + | _, _ -> te +;; + +let fix_according_to_type ty hd tl = + let module C = Cic in + let module S = CicSubstitution in + let rec aux ty tl res = + (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); + flush stderr ; *) + match ty with + C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> + (match tl with + [] -> C.Appl res + | _ -> + prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); + flush stderr ; + C.LetIn + (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) + | C.Cast (v,t) -> aux v tl res + | C.Prod (n,s,t) -> + (match tl with + [] -> + prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); + flush stderr ; + let res' = List.map (S.lift 1) res + in + C.Lambda + (C.Name "x", (* Andrea: to do: generate a fresh name *) + s, + aux t [] (res'@[C.Rel 1])) + | hd::tl' -> + let hd' = fix_lambdas_wrt_type s hd + in + aux (S.subst hd' t) tl' (res@[hd'])) + | C.Lambda _ -> assert false + | C.LetIn (n,s,t) -> aux (S.subst s t) tl res + | C.Appl _ + | C.Const _ + | C.MutInd _ + | C.MutConstruct _ + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> (* ???? *) + (match tl with + [] -> C.Appl res + | _ -> (* Andrea: to do: generate a fresh name *) + C.LetIn + (C.Name "H", + C.Appl res, + C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) + in + aux ty tl [hd] +;; + +let eta_fix metasenv t = + let rec eta_fix' t = +(* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); + flush stderr ; *) + let module C = Cic in + match t with + C.Rel n -> C.Rel n + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (n,l) -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv + in + let l' = + List.map2 + (fun ct t -> + match (ct, t) with + None, _ -> None + | _, Some t -> Some (eta_fix' t) + | Some _, None -> assert false (* due to typing rules *)) + canonical_context l + in + C.Meta (n,l') + | C.Sort s -> C.Sort s + | C.Implicit -> C.Implicit + | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t) + | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t) + | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t) + | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t) + | C.Appl l -> + let l' = List.map eta_fix' l + in + (match l' with + C.Const(uri,exp_named_subst)::l'' -> + let constant_type = + (match CicEnvironment.get_obj uri with + C.Constant (_,_,ty,_) -> ty + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + in + fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' + | _ -> C.Appl l' ) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.MutInd (uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (eta_fix' t)) exp_named_subst + in + C.MutConstruct (uri, tyno, consno, exp_named_subst') + | C.MutCase (uri, tyno, outty, term, patterns) -> + C.MutCase (uri, tyno, eta_fix' outty, + eta_fix' term, List.map eta_fix' patterns) + | C.Fix (funno, funs) -> + C.Fix (funno, + List.map + (fun (name, no, ty, bo) -> + (name, no, eta_fix' ty, eta_fix' bo)) funs) + | C.CoFix (funno, funs) -> + C.CoFix (funno, + List.map + (fun (name, ty, bo) -> + (name, eta_fix' ty, eta_fix' bo)) funs) + in + eta_fix' t +;; + diff --git a/helm/ocaml/cic_omdoc/eta_fixing.mli b/helm/ocaml/cic_omdoc/eta_fixing.mli new file mode 100644 index 000000000..6da260aab --- /dev/null +++ b/helm/ocaml/cic_omdoc/eta_fixing.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val eta_fix : Cic.metasenv -> Cic.term -> Cic.term + +