From: Claudio Sacerdoti Coen Date: Wed, 22 Nov 2000 19:46:31 +0000 (+0000) Subject: Many cleanings in the repository X-Git-Tag: nogzip~147 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=857b7321250fd66596523596c8ef104f8978fe05;p=helm.git Many cleanings in the repository --- diff --git a/helm/interface/ISTRUZIONI b/helm/interface/ISTRUZIONI deleted file mode 100644 index fe6c09efc..000000000 --- a/helm/interface/ISTRUZIONI +++ /dev/null @@ -1,22 +0,0 @@ -============================== -ISTRUZIONI PER CHI USA LA TCSH -============================== - -Lanciare: - - source PER_FARLO_ANDARE_TCSH - -Poi far partire altri due xterm. -Nel primo lanciare: - - make start-xaland3 - -Nel secondo lanciare: - - make start-http-getter - -Se non funziona significa che ce ne e' gia' uno attivo. - -Infini lanciare, dall'ultima shell, - - ./mmlinterface.opt.saved diff --git a/helm/interface/NON_VA b/helm/interface/NON_VA deleted file mode 100644 index 375447103..000000000 --- a/helm/interface/NON_VA +++ /dev/null @@ -1,29 +0,0 @@ - - *********************************************************************** - - A T T E N Z I O N E ! ! ! - - Quando si usa fix_params.opt, scrivere - - find /really_very_local/helm/PARSER/examples - - invece di examples - - *********************************************************************** - - PROBLEMA NON FIXATO CON fix_params - - LA SOLUZIONE E' - - - -Correggere: - - examples/coq/SETS/Powerset_facts/Sets_as_an_algebra/setcover_intro.con.xml - -aggiungendo paramMode="POSSIBLE" - -Un esempio che altrimenti non funziona e': - -examples/coq/SETS/Powerset_Classical_facts/Sets_as_an_algebra/Add_covers.con.xml - diff --git a/helm/interface/PER_FARLO_ANDARE b/helm/interface/PER_FARLO_ANDARE deleted file mode 100644 index 20fb52a86..000000000 --- a/helm/interface/PER_FARLO_ANDARE +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=.:/really_very_local/helm/proveluca/mml-browser/ -export no_proxy=cs.unibo.it diff --git a/helm/interface/PER_FARLO_ANDARE_TCSH b/helm/interface/PER_FARLO_ANDARE_TCSH deleted file mode 100644 index b527fabea..000000000 --- a/helm/interface/PER_FARLO_ANDARE_TCSH +++ /dev/null @@ -1,4 +0,0 @@ -setenv PATH "/home/projects/java/jdk1.2.2/bin:$PATH" -setenv CLASSPATH "/really_very_local/helm/java/xalan_1_1/xalan.jar:/really_very_local/helm/java/xalan_1_1/xerces.jar:." -setenv CLASSPATH "/really_very_local/helm/java/saxon-5.3.2/saxon.jar:$CLASSPATH" -setenv LD_LIBRARY_PATH ".:/really_very_local/helm/proveluca/mml-browser/" diff --git a/helm/interface/PER_FARLO_ANDARE_TCSH_D01 b/helm/interface/PER_FARLO_ANDARE_TCSH_D01 deleted file mode 100644 index 208f00a0e..000000000 --- a/helm/interface/PER_FARLO_ANDARE_TCSH_D01 +++ /dev/null @@ -1,4 +0,0 @@ -setenv PATH "/home/projects/java/jdk1.2.2/bin:$PATH" -setenv CLASSPATH "/really_very_local/helm/java/xalan_1_2_D01/xalan.jar:/really_very_local/helm/java/xalan_1_2_D01/xerces.jar:." -setenv CLASSPATH "/really_very_local/helm/java/saxon-5.3.2/saxon.jar:$CLASSPATH" -setenv LD_LIBRARY_PATH ".:/really_very_local/helm/proveluca/mml-browser/" diff --git a/helm/interface/cicXPath.prima_degli_identificatori.ml b/helm/interface/cicXPath.prima_degli_identificatori.ml deleted file mode 100644 index 8a69d1a24..000000000 --- a/helm/interface/cicXPath.prima_degli_identificatori.ml +++ /dev/null @@ -1,102 +0,0 @@ -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 11/04/2000 *) -(* *) -(* *) -(******************************************************************************) - -(* functions to parse an XPath to retrieve the annotation *) - -exception WrongXPath of string;; - -let rec get_annotation_of_inductiveFun f xpath = - let module C = Cic in - match (xpath,f) with - 1::tl,(_,_,ty,_) -> get_annotation_of_term ty tl - | 2::tl,(_,_,_,te) -> get_annotation_of_term te tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) - -and get_annotation_of_coinductiveFun f xpath = - let module C = Cic in - match (xpath,f) with - 1::tl,(_,ty,_) -> get_annotation_of_term ty tl - | 2::tl,(_,_,te) -> get_annotation_of_term te tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) - -and get_annotation_of_inductiveType ty xpath = - let module C = Cic in - match (xpath,ty) with - 1::tl,(_,_,arity,_) -> get_annotation_of_term arity tl - | n::tl,(_,_,_,cons) when n <= List.length cons + 1 -> - let (_,ty,_) = List.nth cons (n-2) in - get_annotation_of_term ty tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) - -and get_annotation_of_term term xpath = - let module C = Cic in - match (xpath,term) with - [],C.ARel (_,ann,_,_) -> ann - | [],C.AVar (_,ann,_) -> ann - | [],C.AMeta (_,ann,_) -> ann - | [],C.ASort (_,ann,_) -> ann - | [],C.AImplicit (_,ann) -> ann - | [],C.ACast (_,ann,_,_) -> ann - | 1::tl,C.ACast (_,_,te,_) -> get_annotation_of_term te tl - | 2::tl,C.ACast (_,_,_,ty) -> get_annotation_of_term ty tl - | [],C.AProd (_,ann,_,_,_) -> ann - | 1::tl,C.AProd (_,_,_,so,_) -> get_annotation_of_term so tl - | 2::tl,C.AProd (_,_,_,_,ta) -> get_annotation_of_term ta tl - | [],C.ALambda (_,ann,_,_,_) -> ann - | 1::tl,C.ALambda (_,_,_,so,_) -> get_annotation_of_term so tl - | 2::tl,C.ALambda (_,_,_,_,ta) -> get_annotation_of_term ta tl - | [],C.AAppl (_,ann,_) -> ann - | n::tl,C.AAppl (_,_,l) when n <= List.length l -> - get_annotation_of_term (List.nth l (n-1)) tl - | [],C.AConst (_,ann,_,_) -> ann - | [],C.AAbst (_,ann,_) -> ann - | [],C.AMutInd (_,ann,_,_,_) -> ann - | [],C.AMutConstruct (_,ann,_,_,_,_) -> ann - | [],C.AMutCase (_,ann,_,_,_,_,_,_) -> ann - | 1::tl,C.AMutCase (_,_,_,_,_,outt,_,_) -> get_annotation_of_term outt tl - | 2::tl,C.AMutCase (_,_,_,_,_,_,te,_) -> get_annotation_of_term te tl - | n::tl,C.AMutCase (_,_,_,_,_,_,_,pl) when n <= List.length pl -> - get_annotation_of_term (List.nth pl (n-1)) tl - | [],C.AFix (_,ann,_,_) -> ann - | n::tl,C.AFix (_,_,_,fl) when n <= List.length fl -> - get_annotation_of_inductiveFun (List.nth fl (n-1)) tl - | [],C.ACoFix (_,ann,_,_) -> ann - | n::tl,C.ACoFix (_,_,_,fl) when n <= List.length fl -> - get_annotation_of_coinductiveFun (List.nth fl (n-1)) tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) -;; - -let get_annotation (annobj,_) xpath = - let module C = Cic in - match (xpath,annobj) with - [],C.ADefinition (_,ann,_,_,_,_) -> ann - | 1::tl,C.ADefinition (_,_,_,bo,_,_) -> get_annotation_of_term bo tl - | 2::tl,C.ADefinition (_,_,_,_,ty,_) -> get_annotation_of_term ty tl - | [],C.AAxiom (_,ann,_,_,_) -> ann - | 1::tl,C.AAxiom (_,_,_,ty,_) -> get_annotation_of_term ty tl - | [],C.AVariable (_,ann,_,_) -> ann - | 1::tl,C.AVariable (_,_,_,ty) -> get_annotation_of_term ty tl - | [],C.ACurrentProof (_,ann,_,_,_,_) -> ann - | n::tl,C.ACurrentProof (_,ann,_,conjs,_,_) when n <= List.length conjs -> - get_annotation_of_term (snd (List.nth conjs (n-1))) tl - | n::tl,C.ACurrentProof (_,ann,_,conjs,bo,_) when n = List.length conjs + 1 -> - get_annotation_of_term bo tl - | n::tl,C.ACurrentProof (_,ann,_,conjs,_,ty) when n = List.length conjs + 2 -> - get_annotation_of_term ty tl - | [],C.AInductiveDefinition (_,ann,_,_,_) -> ann - | n::tl,C.AInductiveDefinition (_,_,tys,_,_) when n <= List.length tys -> - get_annotation_of_inductiveType (List.nth tys (n-1)) tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) -;; diff --git a/helm/interface/gmon.out b/helm/interface/gmon.out deleted file mode 100644 index c48b8406f..000000000 Binary files a/helm/interface/gmon.out and /dev/null differ diff --git a/helm/interface/latinize.pl b/helm/interface/latinize.pl deleted file mode 100755 index 7fa678736..000000000 --- a/helm/interface/latinize.pl +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/perl - -while() -{ - s/→/->/g; - s/⇒/=>/g; - s/λ/\\/g; - s/Π/||/g; - print; -} diff --git a/helm/interface/mml.dtd b/helm/interface/mml.dtd deleted file mode 100644 index 10ce5cb5d..000000000 --- a/helm/interface/mml.dtd +++ /dev/null @@ -1,55 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/interface/mml.ml b/helm/interface/mml.ml deleted file mode 100644 index 88c281350..000000000 --- a/helm/interface/mml.ml +++ /dev/null @@ -1,11 +0,0 @@ -type expr = - Null - | Mi of string - | Mo of string - | Mn of string - | Mtext of string - | Mrow of expr list - | Mfenced of string * string * string * expr list (* open, close, separators *) -type fragment = - Math of expr list -;; diff --git a/helm/interface/mmlinterface.opt.saved b/helm/interface/mmlinterface.opt.saved deleted file mode 100755 index cb5708ade..000000000 Binary files a/helm/interface/mmlinterface.opt.saved and /dev/null differ