Define canonical Idriç information and prepaint model

.github/workflows/idric-core.yml

@@ -22,7 +22,7 @@ jobs:
     env:
       IDRIS2_CG: chez
       SCHEME: scheme
-      IDRIC_REF: 61970be77769f607cca8650bf424c0f0b22ddee7
+      IDRIC_REF: d2463ec8a3a0dd4ac167029927452f3e83805dc3
     steps:
       - uses: actions/checkout@v4
 
@@ -34,7 +34,7 @@ jobs:
         uses: actions/cache/restore@v4
         with:
           path: /tmp/idric
-          key: idric-${{ runner.os }}-61970be77769f607cca8650bf424c0f0b22ddee7
+          key: idric-${{ runner.os }}-d2463ec8a3a0dd4ac167029927452f3e83805dc3
 
       - name: Build and install Idric compiler through Grease
         if: steps.idric-cache.outputs.cache-hit != 'true'
@@ -45,18 +45,35 @@ jobs:
         uses: actions/cache/save@v4
         with:
           path: /tmp/idric
-          key: idric-${{ runner.os }}-61970be77769f607cca8650bf424c0f0b22ddee7
+          key: idric-${{ runner.os }}-d2463ec8a3a0dd4ac167029927452f3e83805dc3
 
       - name: Exercise HTML-first information renderer
         run: sh bin/ci_browser_foundation.grease exercise-information
 
+      - name: Exercise canonical information model
+        run: |
+          cd src
+          /tmp/idric/bin/idris2 CanonicalInformationSmoke.idric -o ib-canonical-information 2>&1 | tee /tmp/idric-canonical-information-compile.txt
+          test -x ./build/exec/ib-canonical-information
+          ! grep -q '^Error:' /tmp/idric-canonical-information-compile.txt
+          ./build/exec/ib-canonical-information | tee /tmp/ib-canonical-information.txt
+          grep -Fx 'canonical-information=constructed' /tmp/ib-canonical-information.txt
+          grep -Fx 'canonical-blocks=6' /tmp/ib-canonical-information.txt
+          grep -Fx 'canonical-row-cells=2' /tmp/ib-canonical-information.txt
+          grep -Fx 'empty-image-refused=True' /tmp/ib-canonical-information.txt
+          grep -Fx 'seventh-heading-refused=True' /tmp/ib-canonical-information.txt
+          grep -Fx 'revision-zero=0' /tmp/ib-canonical-information.txt
+          grep -Fx 'nonincreasing-revision-refused=True' /tmp/ib-canonical-information.txt
+          grep -Fx 'version1=serialized' /tmp/ib-canonical-information.txt
+
       - name: Exercise browser-owned Idric core
         run: sh bin/ci_browser_foundation.grease exercise-core
 
       - name: Exercise developer workbench
         run: sh bin/ci_browser_foundation.grease exercise-workbench
 
   scientific-media:
+    needs: idric-core
     runs-on: ubuntu-latest
     env:
       PDF_HARVESTER_REF: 77d85dc6f7e89d109cb9e06f42706bc34f00e4a3
@@ -72,7 +89,7 @@ jobs:
         uses: actions/cache/restore@v4
         with:
           path: /tmp/idric
-          key: idric-${{ runner.os }}-61970be77769f607cca8650bf424c0f0b22ddee7
+          key: idric-${{ runner.os }}-d2463ec8a3a0dd4ac167029927452f3e83805dc3
 
       - name: Verify PDF harvester pin
         run: sh bin/ci_browser_foundation.grease verify-pdf-harvester

bin/ci_browser_foundation.grease

@@ -18,8 +18,14 @@ build_idric() {
   git -C /tmp/Idric fetch --depth 1 origin "$idric_ref"
   git -C /tmp/Idric checkout --detach -q FETCH_HEAD
   test "$(git -C /tmp/Idric rev-parse HEAD)" = "$idric_ref"
-  SCHEME=chezscheme make -C /tmp/Idric bootstrap PREFIX="$idric_prefix"
-  SCHEME=chezscheme make -C /tmp/Idric install PREFIX="$idric_prefix"
+
+  idric_build_root=/tmp/Idric
+  if [ -f /tmp/Idric/_/Makefile ]; then
+    idric_build_root=/tmp/Idric/_
+  fi
+
+  SCHEME=chezscheme make -C "$idric_build_root" bootstrap PREFIX="$idric_prefix"
+  SCHEME=chezscheme make -C "$idric_build_root" install PREFIX="$idric_prefix"
 }
 
 verify_pdf_harvester() {

src/CanonicalInformationSmoke.idric

@@ -0,0 +1,76 @@
+module CanonicalInformationSmoke
+
+import IB.Information.Model
+import IB.Prepaint.Model
+import IB.Prepaint.Version1
+
+%default total
+
+fixture_strand : Maybe Strand
+fixture_strand = do
+  source_reference <- nonempty_text "fixture:strand-1"
+  requested <- requested_address "https://example.test/requested"
+  resolved <- resolved_address "https://example.test/resolved"
+  image <- fetched_image "asset:figure-1"
+  let source = Source source_reference HtmlRepresentation CompleteRepresentation
+  pure
+    (MakeStrand
+      source
+      requested
+      resolved
+      (Just "Example")
+      [ InformationHeading Heading2 "Section"
+      , InformationText "Visible paragraph"
+      , InformationLink "Next" (LinkReference "/next")
+      , InformationTableRow (TableCells "first" ["second"])
+      , InformationForm "Search" (FormReference "/search")
+      , InformationImage image "diagram" "Figure 1" (Just (LinkReference "/figure/1"))
+      ])
+
+empty_image_refused : Bool
+empty_image_refused =
+  case fetched_image "" of
+    Nothing ⇒ True
+    Just _ ⇒ False
+
+seventh_heading_refused : Bool
+seventh_heading_refused =
+  case heading_level 7 of
+    Nothing ⇒ True
+    Just _ ⇒ False
+
+nonincreasing_revision_refused : Strand → Bool
+nonincreasing_revision_refused strand =
+  let first = revision_from_strand (Revision 1) PartialRevision strand in
+  let second = revision_from_strand (Revision 1) CompleteRevision strand in
+  case serialize_version1 [first, second] of
+    Nothing ⇒ True
+    Just _ ⇒ False
+
+version1_result : Maybe String → String
+version1_result Nothing = "version1=serialization-failed"
+version1_result (Just version1_text) =
+  "version1=serialized\n" ++
+  "version1-bytes=" ++ show (length (unpack version1_text))
+
+strand_report : Strand → String
+strand_report strand =
+  let partial = revision_from_strand (Revision 0) PartialRevision strand in
+  let complete = revision_from_strand (Revision 1) CompleteRevision strand in
+  unlines
+    [ "canonical-information=constructed"
+    , "canonical-blocks=" ++ show (length strand.blocks)
+    , "canonical-row-cells=" ++ show (length (table_row_cells (TableCells "first" ["second"])))
+    , "empty-image-refused=" ++ show empty_image_refused
+    , "seventh-heading-refused=" ++ show seventh_heading_refused
+    , "revision-zero=" ++ show (revision_sequence_value partial.sequence)
+    , "nonincreasing-revision-refused=" ++ show (nonincreasing_revision_refused strand)
+    , version1_result (serialize_version1 [partial, complete])
+    ]
+
+fixture_report : Maybe Strand → String
+fixture_report Nothing = "canonical-information=construction-failed"
+fixture_report (Just strand) = strand_report strand
+
+main : IO ()
+main = putStrLn (fixture_report fixture_strand)

src/IB/Information/Model.idric

@@ -0,0 +1,137 @@
+module IB.Information.Model
+
+%default total
+
+public export
+data NonemptyText = TextBeginning Char (List Char)
+
+public export
+nonempty_text : String → Maybe NonemptyText
+nonempty_text value =
+  case unpack value of
+    [] => Nothing
+    first :: rest => Just (TextBeginning first rest)
+
+public export
+nonempty_text_value : NonemptyText → String
+nonempty_text_value (TextBeginning first rest) = pack (first :: rest)
+
+public export
+data RepresentationOrigin
+  = HtmlRepresentation
+  | PdfRepresentation
+  | PlainTextRepresentation
+  | DerivedRepresentation
+  | OtherRepresentation
+
+public export
+data RepresentationCompleteness
+  = PartialRepresentation
+  | CompleteRepresentation
+
+public export
+record SourceRepresentation where
+  constructor Source
+  reference : NonemptyText
+  origin : RepresentationOrigin
+  completeness : RepresentationCompleteness
+
+public export
+data RequestedAddressText = RequestedAddress NonemptyText
+
+public export
+data ResolvedAddressText = ResolvedAddress NonemptyText
+
+public export
+data LinkReferenceText = LinkReference String
+
+public export
+data FormReferenceText = FormReference String
+
+public export
+data FetchedImageReference = FetchedImage NonemptyText
+
+public export
+requested_address : String → Maybe RequestedAddressText
+requested_address value = map RequestedAddress (nonempty_text value)
+
+public export
+resolved_address : String → Maybe ResolvedAddressText
+resolved_address value = map ResolvedAddress (nonempty_text value)
+
+public export
+fetched_image : String → Maybe FetchedImageReference
+fetched_image value = map FetchedImage (nonempty_text value)
+
+public export
+requested_address_value : RequestedAddressText → String
+requested_address_value (RequestedAddress value) = nonempty_text_value value
+
+public export
+resolved_address_value : ResolvedAddressText → String
+resolved_address_value (ResolvedAddress value) = nonempty_text_value value
+
+public export
+link_reference_value : LinkReferenceText → String
+link_reference_value (LinkReference value) = value
+
+public export
+form_reference_value : FormReferenceText → String
+form_reference_value (FormReference value) = value
+
+public export
+fetched_image_value : FetchedImageReference → String
+fetched_image_value (FetchedImage value) = nonempty_text_value value
+
+public export
+data HeadingLevel
+  = Heading1
+  | Heading2
+  | Heading3
+  | Heading4
+  | Heading5
+  | Heading6
+
+public export
+heading_level_number : HeadingLevel → Nat
+heading_level_number Heading1 = 1
+heading_level_number Heading2 = 2
+heading_level_number Heading3 = 3
+heading_level_number Heading4 = 4
+heading_level_number Heading5 = 5
+heading_level_number Heading6 = 6
+
+public export
+heading_level : Nat → Maybe HeadingLevel
+heading_level 1 = Just Heading1
+heading_level 2 = Just Heading2
+heading_level 3 = Just Heading3
+heading_level 4 = Just Heading4
+heading_level 5 = Just Heading5
+heading_level 6 = Just Heading6
+heading_level _ = Nothing
+
+public export
+data NonemptyTableRow = TableCells String (List String)
+
+public export
+table_row_cells : NonemptyTableRow → List String
+table_row_cells (TableCells first rest) = first :: rest
+
+public export
+data InformationBlock
+  = InformationHeading HeadingLevel String
+  | InformationText String
+  | InformationLink String LinkReferenceText
+  | InformationTableRow NonemptyTableRow
+  | InformationForm String FormReferenceText
+  | InformationImage FetchedImageReference String String (Maybe LinkReferenceText)
+
+public export
+record Strand where
+  constructor MakeStrand
+  source : SourceRepresentation
+  requested : RequestedAddressText
+  resolved : ResolvedAddressText
+  title : Maybe String
+  blocks : List InformationBlock

src/IB/Prepaint/Model.idric

@@ -0,0 +1,40 @@
+module IB.Prepaint.Model
+
+import IB.Information.Model
+
+%default total
+
+public export
+data RevisionSequence = Revision Nat
+
+public export
+revision_sequence_value : RevisionSequence → Nat
+revision_sequence_value (Revision value) = value
+
+public export
+data RevisionState
+  = PartialRevision
+  | CompleteRevision
+
+public export
+record PrepaintRevision where
+  constructor Prepaint
+  sequence : RevisionSequence
+  state : RevisionState
+  source : SourceRepresentation
+  requested : RequestedAddressText
+  resolved : ResolvedAddressText
+  title : Maybe String
+  blocks : List InformationBlock
+
+public export
+revision_from_strand : RevisionSequence → RevisionState → Strand → PrepaintRevision
+revision_from_strand sequence state strand =
+  Prepaint
+    sequence
+    state
+    strand.source
+    strand.requested
+    strand.resolved
+    strand.title
+    strand.blocks