From: lordi Date: Thu, 13 Jun 2002 17:18:40 +0000 (+0000) Subject: let in implemented X-Git-Tag: V_0_3_0_debian_8~43 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97050ceab872afb33c5ff862f3f96743437e4346;p=helm.git let in implemented --- diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 71ddf6b00..e93fc1a14 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -5,6 +5,7 @@ intersect.cmi: mathql_semantics.cmo union.cmi: mathql_semantics.cmo pattern.cmi: mathql_semantics.cmo use.cmi: mathql_semantics.cmo +letin.cmi: mathql_semantics.cmo dbconn.cmo: dbconn.cmi dbconn.cmx: dbconn.cmi eval.cmo: eval.cmi @@ -27,6 +28,8 @@ pattern.cmo: dbconn.cmi eval.cmi mathql_semantics.cmo utility.cmi pattern.cmi pattern.cmx: dbconn.cmx eval.cmx mathql_semantics.cmx utility.cmx pattern.cmi use.cmo: dbconn.cmi mathql_semantics.cmo utility.cmi use.cmi use.cmx: dbconn.cmx mathql_semantics.cmx utility.cmx use.cmi +letin.cmo: func.cmi utility.cmi letin.cmi +letin.cmx: func.cmx utility.cmx letin.cmi mqint.cmo: dbconn.cmi diff.cmi eval.cmi intersect.cmi mathql_semantics.cmo \ pattern.cmi select.cmi sortedby.cmi union.cmi use.cmi utility.cmi \ mqint.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index f57141358..290258d17 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -4,7 +4,7 @@ PREDICATES = INTERFACE_FILES = dbconn.mli eval.mli utility.mli func.mli diff.mli \ sortedby.mli select.mli intersect.mli union.mli \ - pattern.mli use.mli mqint.mli + pattern.mli use.mli letin.mli mqint.mli IMPLEMENTATION_FILES = mathql_semantics.ml \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/mathql_interpreter/func.ml b/helm/ocaml/mathql_interpreter/func.ml index 314ad2b01..857a4c698 100644 --- a/helm/ocaml/mathql_interpreter/func.ml +++ b/helm/ocaml/mathql_interpreter/func.ml @@ -33,6 +33,9 @@ open MathQL;; (* * implementazione della funzione NAME + * + * esempio: + * name "cic:/Algebra/CC_Props/CC_CauchySeq.ind#xpointer(1/1/1)" = CC_CauchySeq *) let func_name value = try ( diff --git a/helm/ocaml/mathql_interpreter/letin.ml b/helm/ocaml/mathql_interpreter/letin.ml new file mode 100644 index 000000000..3cf1fb617 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/letin.ml @@ -0,0 +1,61 @@ +(* 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://www.cs.unibo.it/helm/. + *) + +(* + * implementazione dei comandi LETIN e REF + *) + +open MathQL;; + +let letin_pool = ref None;; + +let see_pool () = + match !letin_pool with + None -> print_endline "None" + | Some c -> List.iter (fun elem -> print_endline (fst elem)) c +;; + +let letin_ex rvar alist = + let _ = + match !letin_pool with + Some pool -> letin_pool := Some ((rvar,alist)::(List.remove_assoc rvar pool)) + | None -> letin_pool := Some ([(rvar,alist)]) + in +(* let _ = see_pool () in*) + [] +;; + +let letref_ex rvar = + match !letin_pool with + None -> [] + | Some pool -> + ( + try + List.assoc rvar pool + with + Not_found -> let _ = print_endline "nun ce sta" in [] + ) +;; + diff --git a/helm/ocaml/mathql_interpreter/letin.mli b/helm/ocaml/mathql_interpreter/letin.mli new file mode 100644 index 000000000..805633583 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/letin.mli @@ -0,0 +1,27 @@ +(* 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://www.cs.unibo.it/helm/. + *) + +val letin_ex : MathQL.mqrvar -> Mathql_semantics.result -> Mathql_semantics.result +val letref_ex : MathQL.mqrvar -> Mathql_semantics.result diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index bb89c1d19..f0ec5cbfd 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -37,6 +37,7 @@ open Diff;; open Sortedby;; open Use;; open Select;; +open Letin;; let fi_to_string fi = match fi with @@ -84,6 +85,10 @@ let rec execute_ex env = | MQIntersect (l1, l2) -> intersect_ex (execute_ex env l1) (execute_ex env l2) | MQLRVar rvar -> [List.assoc rvar env] + | MQLetIn (rvar, alist) -> + letin_ex rvar (execute_ex env alist) + | MQLetRef rvar -> + letref_ex rvar ;; (* Let's initialize the execute in Select, creating a cyclical recursion *) diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml index 7c7d7f2a7..772f6964e 100644 --- a/helm/ocaml/mathql_interpreter/select.ml +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -20,7 +20,7 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://www.cs.unibo.it/helm/. *) (* diff --git a/helm/ocaml/mathql_interpreter/utility.mli b/helm/ocaml/mathql_interpreter/utility.mli index 763893247..9e9e8290d 100644 --- a/helm/ocaml/mathql_interpreter/utility.mli +++ b/helm/ocaml/mathql_interpreter/utility.mli @@ -20,7 +20,7 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://www.cs.unibo.it/helm/. *) val pgresult_to_string_list : < get_list : string list list; .. > -> string list