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
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
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 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
-;;
-
-
-
-
-
-
+++ /dev/null
-(* 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 <asperti@cs.unibo.it> *)
-(* 27/6/2003 *)
-(* *)
-(**************************************************************************)
-
-val proof2cic :
- (Cic.annterm -> Cic.term) ->
- Cic.annterm Content.proof -> Cic.term
+++ /dev/null
-(* 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
-;;
-
+++ /dev/null
-(* 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
-
-
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
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
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 = \
--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 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
+;;
+
+
+
+
+
+
--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 27/6/2003 *)
+(* *)
+(**************************************************************************)
+
+val proof2cic :
+ (Cic.annterm -> Cic.term) ->
+ Cic.annterm Content.proof -> Cic.term
--- /dev/null
+(* 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
+;;
+
--- /dev/null
+(* 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
+
+
projects / helm.git / commitdiff