From 6e61c5884aa89838a04659f90dc8d210e3703502 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 21:36:49 +0000 Subject: [PATCH] Quick hack: matita natural numbers are now accepted by the parser/disambiguator. If nat/nat.ma is not compiled yet, I do not know what happens. --- .../software/components/cic/libraryObjects.ml | 13 +++ .../components/cic/libraryObjects.mli | 1 + .../cic_disambiguation/number_notation.ml | 3 + .../matita/library/assembly/assembly.ma | 101 +++++++++++------- 4 files changed, 80 insertions(+), 38 deletions(-) diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml index 579c21eed..e2f5fd363 100644 --- a/helm/software/components/cic/libraryObjects.ml +++ b/helm/software/components/cic/libraryObjects.ml @@ -194,3 +194,16 @@ let false_URI () = try Some (List.hd !false_URIs_ref) with Failure "hd" -> None let absurd_URI () = try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None + +let nat_URI = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" + +let zero = Cic.MutConstruct (nat_URI,0,1,[]) +let succ = Cic.MutConstruct (nat_URI,0,2,[]) + +let build_nat n = + if n < 0 then assert false; + let rec aux = function + | 0 -> zero + | n -> Cic.Appl [ succ; (aux (n - 1)) ] + in + aux n diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli index f0d8e4631..8aacd8da3 100644 --- a/helm/software/components/cic/libraryObjects.mli +++ b/helm/software/components/cic/libraryObjects.mli @@ -64,3 +64,4 @@ val false_URI : unit -> UriManager.uri option val true_URI : unit -> UriManager.uri option val absurd_URI : unit -> UriManager.uri option +val build_nat : int -> Cic.term diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml index 2b3ce2d60..781deb90e 100644 --- a/helm/software/components/cic_disambiguation/number_notation.ml +++ b/helm/software/components/cic_disambiguation/number_notation.ml @@ -28,6 +28,9 @@ let _ = DisambiguateChoices.add_num_choice ("natural number", + (fun _ num _ -> LibraryObjects.build_nat (int_of_string num))); + DisambiguateChoices.add_num_choice + ("Coq natural number", (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); DisambiguateChoices.add_num_choice ("real number", diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma index 783262008..bf928dfe3 100644 --- a/helm/software/matita/library/assembly/assembly.ma +++ b/helm/software/matita/library/assembly/assembly.ma @@ -18,7 +18,7 @@ include "nat/times.ma". include "nat/compare.ma". include "list/list.ma". -alias id "OO" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". +(*alias id "OO" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "SS" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". let rec matita_nat_of_coq_nat n ≝ @@ -28,7 +28,7 @@ let rec matita_nat_of_coq_nat n ≝ ]. coercion cic:/matita/assembly/matita_nat_of_coq_nat.con. alias num (instance 0) = "natural number". - +*) definition byte ≝ nat. definition addr ≝ nat. @@ -41,15 +41,16 @@ inductive opcode: Type ≝ | LDAd: opcode (* 3, 182 *) | STAd: opcode. (* 3, 183 *) -let rec cycles_of_opcode op ≝ +alias num (instance 0) = "natural number". +let rec cycles_of_opcode op : nat ≝ match op with - [ ADDd ⇒ matita_nat_of_coq_nat 3 - | BEQ ⇒ matita_nat_of_coq_nat 3 - | BRA ⇒ matita_nat_of_coq_nat 3 - | DECd ⇒ matita_nat_of_coq_nat 5 - | LDAi ⇒ matita_nat_of_coq_nat 2 - | LDAd ⇒ matita_nat_of_coq_nat 3 - | STAd ⇒ matita_nat_of_coq_nat 3 + [ ADDd ⇒ 3 + | BEQ ⇒ 3 + | BRA ⇒ 3 + | DECd ⇒ 5 + | LDAi ⇒ 2 + | LDAd ⇒ 3 + | STAd ⇒ 3 ]. inductive cartesian_product (A,B: Type) : Type ≝ @@ -72,7 +73,7 @@ definition opcode_of_byte ≝ | cons c tl ⇒ match c with [ couple op n ⇒ - match eqb (matita_nat_of_coq_nat n) b with + match eqb n b with [ true ⇒ op | false ⇒ aux tl ]]] @@ -97,12 +98,12 @@ definition byte_of_opcode : opcode → byte ≝ λop. let rec aux l ≝ match l with - [ nil ⇒ matita_nat_of_coq_nat 0 + [ nil ⇒ 0 | cons c tl ⇒ match c with [ couple op' n ⇒ match opcodeeqb op op' with - [ true ⇒ matita_nat_of_coq_nat n + [ true ⇒ n | false ⇒ aux tl ]]] in @@ -114,26 +115,18 @@ for @{ 'byte_of_opcode $a }. interpretation "byte_of_opcode" 'byte_of_opcode a = (cic:/matita/assembly/byte_of_opcode.con a). -definition byte_of_coq_nat : nat → byte ≝ matita_nat_of_coq_nat. - -notation "hvbox(@ break a)" - non associative with precedence 80 -for @{ 'matita_nat_of_coq_nat $a }. -interpretation "matita_nat_of_coq_nat" 'matita_nat_of_coq_nat a = - (cic:/matita/assembly/byte_of_coq_nat.con a). - definition mult_source : list byte ≝ - [#LDAi; @0; - #STAd; @18; (* 18 = locazione $12 *) - #LDAd; @17; (* 17 = locazione $11 *) - #BEQ; @14; - #LDAd; @18; - #DECd; @17; - #ADDd; @16; (* 16 = locazione $10 *) - #STAd; @18; - #LDAd; @17; - #BRA; @246; (* 246 = -10 *) - #LDAd; @18]. + [#LDAi; 0; + #STAd; 32; (* 18 = locazione $12 *) + #LDAd; 31; (* 17 = locazione $11 *) + #BEQ; 12; + #LDAd; 18; + #DECd; 31; + #ADDd; 30; (* 16 = locazione $10 *) + #STAd; 32; + #LDAd; 31; + #BRA; 246; (* 242 = -14 *) + #LDAd; 32]. definition mult_source' : list byte. @@ -148,9 +141,14 @@ record status : Type ≝ { }. definition mult_status : status ≝ - mk_status @0 @0 @0 false false (λa:addr. nth ? mult_source @0 a) 0. + mk_status 0 0 0 false false (λa:addr. nth ? mult_source 0 a) 0. + +definition update ≝ + λf: addr → byte.λa.λv.λx. + match eqb x a with + [ true ⇒ v + | false ⇒ f x ]. -alias id "update" = "cic:/Marseille/GC/card/card/update.con". definition tick ≝ λs:status. (* fetch *) @@ -194,9 +192,14 @@ definition tick ≝ let mem' ≝ update (mem s) op1 x in mk_status (acc s) (2 + pc s) (spc s) (eqb O x) (cf s) mem' 0 (* check zb!!! *) - | LDAi ⇒ s - | LDAd ⇒ s - | STAd ⇒ s + | LDAi ⇒ + mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0 + | LDAd ⇒ + let x ≝ pred (mem s op1) in + mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0 + | STAd ⇒ + mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s) + (update (mem s) op1 (acc s)) 0 ] ]. @@ -209,9 +212,30 @@ let rec execute s n on n ≝ lemma foo: ∀s,n. execute s (S n) = execute (tick s) n. intros; reflexivity. qed. +(* +lemma goo: pc (execute mult_status 4) = O. + reduce; + CSC. + -lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status. simplify; + whd in ⊢ (? ? (? (? (? %))) ?); + do 2 (simplify in match (matita_nat_of_coq_nat ?)); + simplify in match (matita_nat_of_coq_nat ?); + whd in ⊢ (? ? (? (? (? (? ? ? ? ? ? ? %)))) ?); + whd in ⊢ (? ? (? (? (? %))) ?); + + + + + + + + + + + + change with (tick (tick (tick mult_status)) = mult_status); change with (tick (tick mult_status) = mult_status); change with (tick mult_status = mult_status); @@ -287,4 +311,5 @@ match % in opcode return ? with |STAd\rArr ?] ?); simplify; reflexivity. +*) *) \ No newline at end of file -- 2.39.2